This repository contains a formalization of Ramification group theory using the Lean 4 theorem prover. Our work builds upon the Mathlib library and Filippo A. E. Nuccio and María Inés de Frutos-Fernández's relevant developments in local class field theory. Our formalization primarily follows Serre's treatise [Local Fields](Local Fields (Jean-Pierre Serre) (Z-Library).pdf) as the foundational reference. Currently, we have completed Chaper 4, section 1 and 3. Below is a concise overview of the file structure to facilitate navigation:

Our work is contained in the RamificationGroup folder. The principal results are organized across the following three directories:

LowerNumbering

The result about lowernumbering ramification group.

Basic.lean

Main Definition

1. lowerRamificationGroup The lowernumbering ramification group.
2. AlgEquiv.lowerIndex The lower index function.
3. AlgEquiv.truncatedLowerIndex The lower index function with an explicit upper bound.

Main Theorem

1. lowerIndex_eq_top_iff_eq_refl
2. mem_lowerRamificationGroup_iff_of_generator the relationship of an element in lowernumbering ramification group and the value of lower index function.
3. le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup

Prop3.lean

Main theorem

1. prop3 Prop3 in 《Local fields》 Chap4, sec1.

HerbrandFunction

The result about Herbrand functions.

Basic.lean

Main Definition

1. phi The function phi.

Main Theorem

1. phi_strictMono The function phi is strictmono.

Bijective.lean

Main Theorem

1. phi_Bijective_aux The function phi is bijective.

Psi.lean

Main Definition

1. psi The function psi.
2. psi_bij The function psi is bijective.
3. phi_psi_eq_self and psi_phi_eq_self.

SumInf.lean

Main Theorem

1. phi_eq_sum_inf_aux Lemma3 in Chap4, Sec3.

UpperNumbering

Basic.lean

Main Definition

1. upperRamificationGroup_aux The uppernumbering ramification group of finite extension.
2. HerbrandFunction.FuncJ and HerbrandFunction.truncatedJ The j function mentioned in Lemma4 Chap4 sec3.

Main result

1. phi_truncatedJ_sub_one Lemma4 Chap4 sec3.
2. herbrand The herbrand theorem.

PhiComp.lean

Main Theorem

1. psi_comp_of_isValExtension the function phi is transitive.

phiReal.lean

Main Definition

1. phiReal The real version of function phi.

Upper.lean

Main Definition

1. upperRamificationGroup The infinite extension version of uppernumbering ramification group.