Ramification index for a place (AbsoluteValue)

(To be written)

References:

• [J. W. S. Cassels, A. Frohlich, editors, Algebraic Number Theory][cassels1967algebraic]

TODO: go mathlib

theorem IntermediateField.restrictRestrictAlgEquivMapHom_injective_of_tower_top (F : Type u_1) (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] : Function.Injective ⇑(restrictRestrictAlgEquivMapHom F L K L)

TODO: go mathlib

@[simp]

theorem AlgEquiv.algebraMap_restrictNormalHom_apply {F : Type u_1} [Field F] {K₁ : Type u_2} [Field K₁] [Algebra F K₁] (E : Type u_3) [Field E] [Algebra F E] [Algebra E K₁] [IsScalarTower F E K₁] [Normal F E] (φ : Gal(K₁/F)) (x : E) : (algebraMap E K₁) (((restrictNormalHom E) φ) x) = φ ((algebraMap E K₁) x)

TODO: go mathlib

@[simp]

theorem IntermediateField.alrebraMap_restrictRestrictAlgEquivMapHom_apply (F : Type u_1) (K : Type u_2) (L : Type u_3) (E : Type u_4) [Field F] [Field K] [Field L] [Field E] [Algebra F K] [Algebra F L] [Algebra F E] [Algebra K E] [Algebra L E] [IsScalarTower F K E] [IsScalarTower F L E] [Normal F K] (φ : Gal(E/L)) (x : K) : (algebraMap K E) (((restrictRestrictAlgEquivMapHom F K L E) φ) x) = φ ((algebraMap K E) x)

TODO: go mathlib

theorem IntermediateField.restrictRestrictAlgEquivMapHom_comp_restrictRestrictAlgEquivMapHom (F : Type u_1) (K : Type u_2) (F' : Type u_3) (K' : Type u_4) (F'' : Type u_5) (K'' : Type u_6) [Field F] [Field K] [Field F'] [Field K'] [Field F''] [Field K''] [Algebra F K] [Algebra F' K'] [Algebra F'' K''] [Algebra F F'] [Algebra F' F''] [Algebra F F''] [Algebra F K'] [Algebra F' K''] [Algebra F K''] [Algebra K K'] [Algebra K' K''] [Algebra K K''] [IsScalarTower F K K'] [IsScalarTower F' K' K''] [IsScalarTower F F' K'] [IsScalarTower F K K''] [IsScalarTower F F'' K''] [IsScalarTower F' F'' K''] [IsScalarTower K K' K''] [Normal F K] [Normal F' K'] : (restrictRestrictAlgEquivMapHom F K F' K').comp (restrictRestrictAlgEquivMapHom F' K' F'' K'') = restrictRestrictAlgEquivMapHom F K F'' K''

TODO: go mathlib

Ramification index of a place for an extension

noncomputable def AbsoluteValue.ramificationIdxOfIsScalarTower (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue L ℝ) : ℕ

If L / K / F is an extension tower with L / F Galois, v is a place of L, then the ramification index of v for K / F is defined to be the index of Iᵥ(L/K) in Iᵥ(L/F) (0 means infinite). Later we will show that this depends only on the place of K below v (AbsoluteValue.ramificationIdxOfIsScalarTower_eq_of_comp_eq), and is independent of the choice of L (AbsoluteValue.ramificationIdx_spec).

Equations

• One or more equations did not get rendered due to their size.

theorem AbsoluteValue.ramificationIdxOfIsScalarTower_eq_range_relIndex (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue L ℝ) : ramificationIdxOfIsScalarTower F K v = (IntermediateField.restrictRestrictAlgEquivMapHom F L K L).range.relIndex (inertiaSubgroup F v)

The ramification index of v for K / F is equal to [Iᵥ(L/F) ⊓ Gal(L/K) : Iᵥ(L/F)], since Iᵥ(L/K) = Iᵥ(L/F) ⊓ Gal(L/K).

theorem AbsoluteValue.ramificationIdxOfIsScalarTower_comp_algEquiv_eq (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] {L' : Type u_4} [Field L'] [Algebra F L'] [Algebra K L'] [IsScalarTower F K L'] [Normal F L'] (v : AbsoluteValue L ℝ) (σ : L' ≃ₐ[K] L) : ramificationIdxOfIsScalarTower F K (v.comp ⋯) = ramificationIdxOfIsScalarTower F K v

A place of L and its restriction to L' by an isomorphism L' ≃ₐ[K] L have the same ramification index for K / F.

theorem AbsoluteValue.ramificationIdxOfIsScalarTower_comp_ringEquiv_eq {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] {F' : Type u_4} {K' : Type u_5} [Field F'] [Field K'] [Algebra F' K'] {L' : Type u_6} [Field L'] [Algebra F' L'] [Algebra K' L'] [IsScalarTower F' K' L'] [Normal F' L'] (v : AbsoluteValue L ℝ) (e : F' ≃+* F) (f : K' ≃+* K) (g : L' ≃+* L) (hcomp0 : (algebraMap F K).comp ↑e = (↑f).comp (algebraMap F' K')) (hcomp : (algebraMap K L).comp ↑f = (↑g).comp (algebraMap K' L')) : ramificationIdxOfIsScalarTower F' K' (v.comp ⋯) = ramificationIdxOfIsScalarTower F K v

A generalization of AbsoluteValue.ramificationIdxOfIsScalarTower_comp_algEquiv_eq.

theorem AbsoluteValue.ramificationIdxOfIsScalarTower_eq_of_comp_eq (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] {v w : AbsoluteValue L ℝ} (h : v.comp ⋯ = w.comp ⋯) : ramificationIdxOfIsScalarTower F K v = ramificationIdxOfIsScalarTower F K w

Any two places of L which are the same when restricted to K have the same ramification index for K / F (since they are conjugate).

theorem Subgroup.relIndex_map_map_of_ker_inf_le {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (H K : Subgroup G) (hle : H ≤ K) (hf : f.ker ⊓ K ≤ H) : (map f H).relIndex (map f K) = H.relIndex K

TODO: go mathlib

theorem AddSubgroup.relIndex_map_map_of_ker_inf_le {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {f : G →+ G'} (H K : AddSubgroup G) (hle : H ≤ K) (hf : f.ker ⊓ K ≤ H) : (map f H).relIndex (map f K) = H.relIndex K

theorem AlgEquiv.restrictNormalHom_ker_eq_range {F : Type u_1} [Field F] {K₁ : Type u_2} [Field K₁] [Algebra F K₁] (E : Type u_3) [Field E] [Algebra F E] [Algebra E K₁] [IsScalarTower F E K₁] [Normal F E] [Normal F K₁] : (restrictNormalHom E).ker = (IntermediateField.restrictRestrictAlgEquivMapHom F K₁ E K₁).range

TODO: go mathlib

theorem AbsoluteValue.ramificationIdxOfIsScalarTower_eq_of_liesOver (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] {M : Type u_4} [Field M] [Algebra F M] [Algebra K M] [Algebra L M] [IsScalarTower F K M] [IsScalarTower F L M] [IsScalarTower K L M] [Normal F M] (v : AbsoluteValue L ℝ) (w : AbsoluteValue M ℝ) [w.LiesOver v] : ramificationIdxOfIsScalarTower F K v = ramificationIdxOfIsScalarTower F K w

If M / L / K / F is an extension tower, M / F and L / F are Galois, v is a place of L, w is a place of M above v, then v and w have the same ramification index for K / F.

theorem AbsoluteValue.ramificationIdxOfIsScalarTower_mul_ramificationIdxOfIsScalarTower (F : Type u_1) (K : Type u_2) (M : Type u_3) [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] [Algebra K M] [IsScalarTower F K M] {L : Type u_4} [Field L] [Algebra F L] [Algebra K L] [Algebra M L] [IsScalarTower F M L] [IsScalarTower K M L] [IsScalarTower F K L] [Normal F L] [Normal K L] (v : AbsoluteValue L ℝ) : ramificationIdxOfIsScalarTower F K v * ramificationIdxOfIsScalarTower K M v = ramificationIdxOfIsScalarTower F M v

noncomputable def AbsoluteValue.ramificationIdx (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] (v : AbsoluteValue K ℝ) : ℕ

If K / F is an algebraic extension, v is a place of K, then the ramification index of v for K / F is defined to be the ramification index of w for K / F, where w is any extension of v to the algebraic closure of K.

Equations

• AbsoluteValue.ramificationIdx F v = AbsoluteValue.ramificationIdxOfIsScalarTower F K ⋯.choose

theorem AbsoluteValue.ramificationIdx_spec (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ) [w.LiesOver v] : ramificationIdx F v = ramificationIdxOfIsScalarTower F K w

The ramification index is well-defined.

theorem AbsoluteValue.ramificationIdx_comp_algEquiv_eq (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] {K' : Type u_3} [Field K'] [Algebra F K'] [Algebra.IsAlgebraic F K'] (v : AbsoluteValue K ℝ) (f : K' ≃ₐ[F] K) : ramificationIdx F (v.comp ⋯) = ramificationIdx F v

A place of K and its restriction to K' by an isomorphism K' ≃ₐ[F] A have the same ramification index over F.

theorem AbsoluteValue.ramificationIdx_comp_ringEquiv_eq {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] {F' : Type u_3} {K' : Type u_4} [Field F'] [Field K'] [Algebra F' K'] [Algebra.IsAlgebraic F' K'] (v : AbsoluteValue K ℝ) {f : F' →+* F} {g : K' ≃+* K} (hsurj : Function.Surjective ⇑f) (hcomp : (algebraMap F K).comp f = (↑g).comp (algebraMap F' K')) : ramificationIdx F' (v.comp ⋯) = ramificationIdx F v

A generalization of AbsoluteValue.ramificationIdx_comp_algEquiv_eq.

theorem AbsoluteValue.ramificationIdx_eq_of_comp_eq (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [Normal F K] {v w : AbsoluteValue K ℝ} (h : v.comp ⋯ = w.comp ⋯) : ramificationIdx F v = ramificationIdx F w

If K / F is normal, then any two places of K which are the same when restricted to F have the same ramification index over F (since they are conjugate).

theorem AbsoluteValue.ramificationIdx_mul_ramificationIdx (F : Type u_1) (K : Type u_2) {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] [Algebra K M] [IsScalarTower F K M] [Algebra.IsAlgebraic F M] (v : AbsoluteValue M ℝ) (w : AbsoluteValue K ℝ) [v.LiesOver w] : ramificationIdx F w * ramificationIdx K v = ramificationIdx F v

Assertion that a place is unramified for an extension

def AbsoluteValue.IsUnramifiedOfIsScalarTower (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue L ℝ) : Prop

If L / K / F is an extension tower with L / F Galois, v is a place of L, then v is called unramified for K / F, if Iᵥ(L/F) ≤ Gal(L/K), or equivalently Iᵥ(L/K) = Iᵥ(L/F) (AbsoluteValue.isUnramifiedOfIsScalarTower_iff_map_inertiaSubgroup_eq). Later we will show that this depends only on the place of K below v, and is independent of the choice of L (AbsoluteValue.isUnramified_spec).

Equations

• AbsoluteValue.IsUnramifiedOfIsScalarTower F K v = (AbsoluteValue.inertiaSubgroup F v ≤ (IntermediateField.restrictRestrictAlgEquivMapHom F L K L).range)

theorem AbsoluteValue.isUnramifiedOfIsScalarTower_iff_map_inertiaSubgroup_eq (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue L ℝ) : IsUnramifiedOfIsScalarTower F K v ↔ Subgroup.map (IntermediateField.restrictRestrictAlgEquivMapHom F L K L) (inertiaSubgroup K v) = inertiaSubgroup F v

theorem AbsoluteValue.isUnramifiedOfIsScalarTower_iff_ramificationIdxOfIsScalarTower_eq_one (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue L ℝ) : IsUnramifiedOfIsScalarTower F K v ↔ ramificationIdxOfIsScalarTower F K v = 1

def AbsoluteValue.IsUnramified (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] (v : AbsoluteValue K ℝ) : Prop

If K / F is an algebraic extension, v is a place of K, then v is called unramified for K / F, if w is unramified for K / F, where w is any extension of v to the algebraic closure of K.

Equations

• AbsoluteValue.IsUnramified F v = AbsoluteValue.IsUnramifiedOfIsScalarTower F K ⋯.choose

theorem AbsoluteValue.isUnramified_iff_ramificationIdx_eq_one (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] (v : AbsoluteValue K ℝ) : IsUnramified F v ↔ ramificationIdx F v = 1

theorem AbsoluteValue.isUnramified_spec (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] {L : Type u_3} [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F L] (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ) [w.LiesOver v] : IsUnramified F v ↔ IsUnramifiedOfIsScalarTower F K w

theorem AbsoluteValue.isUnramified_comp_algEquiv_iff (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] {K' : Type u_3} [Field K'] [Algebra F K'] [Algebra.IsAlgebraic F K'] (v : AbsoluteValue K ℝ) (f : K' ≃ₐ[F] K) : IsUnramified F (v.comp ⋯) ↔ IsUnramified F v

theorem AbsoluteValue.isUnramified_comp_ringEquiv_iff {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] {F' : Type u_3} {K' : Type u_4} [Field F'] [Field K'] [Algebra F' K'] [Algebra.IsAlgebraic F' K'] (v : AbsoluteValue K ℝ) {f : F' →+* F} {g : K' ≃+* K} (hsurj : Function.Surjective ⇑f) (hcomp : (algebraMap F K).comp f = (↑g).comp (algebraMap F' K')) : IsUnramified F' (v.comp ⋯) ↔ IsUnramified F v

theorem AbsoluteValue.isUnramified_iff_of_comp_eq (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [Normal F K] {v w : AbsoluteValue K ℝ} (h : v.comp ⋯ = w.comp ⋯) : IsUnramified F v ↔ IsUnramified F w

theorem AbsoluteValue.IsUnramified.tower_top {F : Type u_1} (K : Type u_2) {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] [Algebra K M] [IsScalarTower F K M] [Algebra.IsAlgebraic F M] {v : AbsoluteValue M ℝ} (H : IsUnramified F v) : IsUnramified K v

theorem AbsoluteValue.IsUnramified.tower_bot {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] [Algebra K M] [IsScalarTower F K M] [Algebra.IsAlgebraic F M] {v : AbsoluteValue M ℝ} (H : IsUnramified F v) (w : AbsoluteValue K ℝ) [v.LiesOver w] : IsUnramified F w

theorem AbsoluteValue.IsUnramified.trans {F : Type u_1} {K : Type u_2} {M : Type u_3} [Field F] [Field K] [Field M] [Algebra F K] [Algebra F M] [Algebra K M] [IsScalarTower F K M] [Algebra.IsAlgebraic F K] [Algebra.IsAlgebraic K M] {v : AbsoluteValue M ℝ} {w : AbsoluteValue K ℝ} (H1 : IsUnramified F w) (H2 : IsUnramified K v) [v.LiesOver w] : IsUnramified F v

def AbsoluteValue.IsUnramifiedIn {F : Type u_1} (K : Type u_2) (L : Type u_3) [Field F] [Field K] [Field L] [Algebra F L] [Algebra K L] [Algebra.IsAlgebraic K L] (v : AbsoluteValue F ℝ) : Prop

If L / K is an algebraic extension, L / F is a field extension, v is a place of F, then v is called unramified for L / K, if all place w of L above v is unramified for L / K.

Equations

• AbsoluteValue.IsUnramifiedIn K L v = ∀ (w : AbsoluteValue L ℝ), w.LiesOver v → AbsoluteValue.IsUnramified K w

@[simp]

theorem AbsoluteValue.isUnramifiedIn_self_iff (F : Type u_1) {K : Type u_2} [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] (v : AbsoluteValue K ℝ) : IsUnramifiedIn F K v ↔ IsUnramified F v

theorem AbsoluteValue.IsUnramifiedIn.tower_top {F : Type u_1} {K : Type u_2} (L : Type u_3) {M : Type u_4} [Field F] [Field K] [Field L] [Field M] [Algebra F L] [Algebra F M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [Algebra.IsAlgebraic K M] {v : AbsoluteValue F ℝ} (H : IsUnramifiedIn K M v) : IsUnramifiedIn L M v

theorem AbsoluteValue.IsUnramifiedIn.tower_bot {F : Type u_1} {K : Type u_2} (L : Type u_3) {M : Type u_4} [Field F] [Field K] [Field L] [Field M] [Algebra F L] [Algebra F M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsScalarTower F L M] [Algebra.IsAlgebraic K M] {v : AbsoluteValue F ℝ} (H : IsUnramifiedIn K M v) : IsUnramifiedIn K L v

theorem AbsoluteValue.IsUnramifiedIn.trans {F : Type u_1} {K : Type u_2} {L : Type u_3} {M : Type u_4} [Field F] [Field K] [Field L] [Field M] [Algebra F L] [Algebra F M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsScalarTower F L M] [Algebra.IsAlgebraic K L] [Algebra.IsAlgebraic L M] {v : AbsoluteValue F ℝ} (H1 : IsUnramifiedIn K L v) (H2 : IsUnramifiedIn L M v) : IsUnramifiedIn K M v

theorem AbsoluteValue.isUnramifiedIn_comp_ringEquiv_iff {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F L] [Algebra K L] [Algebra.IsAlgebraic K L] {F' : Type u_4} {K' : Type u_5} {L' : Type u_6} [Field F'] [Field K'] [Field L'] [Algebra F' L'] [Algebra K' L'] [Algebra.IsAlgebraic K' L'] (v : AbsoluteValue F ℝ) {e : F' ≃+* F} {f : K' ≃+* K} {g : L' ≃+* L} (hcomp0 : (algebraMap F L).comp ↑e = (↑g).comp (algebraMap F' L')) (hcomp : (algebraMap K L).comp ↑f = (↑g).comp (algebraMap K' L')) : IsUnramifiedIn K' L' (v.comp ⋯) ↔ IsUnramifiedIn K L v

theorem AbsoluteValue.isUnramifiedIn_iff_of_algEquiv {F : Type u_1} {K : Type u_2} {L : Type u_3} {L' : Type u_4} [Field F] [Field K] [Field L] [Field L'] [Algebra F K] [Algebra F L] [Algebra K L] [Algebra F L'] [Algebra K L'] [IsScalarTower F K L] [IsScalarTower F K L'] [Algebra.IsAlgebraic K L] [Algebra.IsAlgebraic K L'] (v : AbsoluteValue F ℝ) (f : L ≃ₐ[K] L') : IsUnramifiedIn K L v ↔ IsUnramifiedIn K L' v