Inertia subgroup for a place (AbsoluteValue)

(To be written)

References:

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

Inertia subgroup for a place

theorem AbsoluteValue.map_neg' {R : Type u_4} {S : Type u_5} [Semiring S] [LinearOrder S] [MulPosMono S] [Ring R] (abv : AbsoluteValue R S) (a : R) : abv (-a) = abv a

Another version of AbsoluteValue.map_neg with slightly different assumptions.

TODO: go mathlib

def AbsoluteValue.inertiaSubgroup (F : Type u_1) {K : Type u_2} {S : Type u_3} [CommSemiring F] [Ring K] [Algebra F K] [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue K S) : Subgroup (K ≃ₐ[F] K)

The inertia subgroup Iᵥ(K/F) in Gal(K/F) for a finite place v of K consists of all σ in the decomposition subgroup Dᵥ(K/F) such that for all x with v x ≤ 1, v (σ x - x) < 1. For infinite places Iᵥ(K/F) is just defined to be the decomposition subgroup Dᵥ(K/F).

Equations

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

theorem AbsoluteValue.mem_inertiaSubgroup_iff {F : Type u_1} {K : Type u_2} {S : Type u_3} [CommSemiring F] [Ring K] [Algebra F K] [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue K S) (σ : K ≃ₐ[F] K) : σ ∈ inertiaSubgroup F v ↔ σ ∈ decompositionSubgroup F v ∧ (¬IsNonarchimedean ⇑v ∨ ∀ (x : K), v x ≤ 1 → v (σ x - x) < 1)

theorem AbsoluteValue.mem_inertiaSubgroup_iff_of_isNonarchimedean {F : Type u_1} {K : Type u_2} {S : Type u_3} [CommSemiring F] [Ring K] [Algebra F K] [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue K S) (h : IsNonarchimedean ⇑v) (σ : K ≃ₐ[F] K) : σ ∈ inertiaSubgroup F v ↔ σ ∈ decompositionSubgroup F v ∧ ∀ (x : K), v x ≤ 1 → v (σ x - x) < 1

theorem AbsoluteValue.mem_inertiaSubgroup_iff_of_not_isNonarchimedean {F : Type u_1} {K : Type u_2} {S : Type u_3} [CommSemiring F] [Ring K] [Algebra F K] [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue K S) (h : ¬IsNonarchimedean ⇑v) (σ : K ≃ₐ[F] K) : σ ∈ inertiaSubgroup F v ↔ σ ∈ decompositionSubgroup F v

theorem AbsoluteValue.inertiaSubgroup_eq_bot_of_not_isNontrivial (F : Type u_4) {K : Type u_5} [Field F] [Field K] [Algebra F K] (v : AbsoluteValue K ℝ) (h : ¬v.IsNontrivial) : inertiaSubgroup F v = ⊥

theorem AbsoluteValue.inertiaSubgroup_le_decompositionSubgroup (F : Type u_1) {K : Type u_2} {S : Type u_3} [CommSemiring F] [Ring K] [Algebra F K] [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue K S) : inertiaSubgroup F v ≤ decompositionSubgroup F v

theorem AbsoluteValue.inertiaSubgroup_eq_decompositionSubgroup_of_not_isNonarchimedean (F : Type u_1) {K : Type u_2} {S : Type u_3} [CommSemiring F] [Ring K] [Algebra F K] [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue K S) (h : ¬IsNonarchimedean ⇑v) : inertiaSubgroup F v = decompositionSubgroup F v

theorem AbsoluteValue.apply_eq_of_mem_inertiaSubgroup {F : Type u_1} {K : Type u_2} {S : Type u_3} [CommSemiring F] [Ring K] [Algebra F K] [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue K S) {σ : K ≃ₐ[F] K} (h : σ ∈ inertiaSubgroup F v) (x : K) : v (σ x) = v x

theorem AbsoluteValue.apply_sub_lt_one_of_mem_inertiaSubgroup_of_isNonarchimedean {F : Type u_1} {K : Type u_2} {S : Type u_3} [CommSemiring F] [Ring K] [Algebra F K] [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue K S) {σ : K ≃ₐ[F] K} (h : σ ∈ inertiaSubgroup F v) (h2 : IsNonarchimedean ⇑v) {x : K} (hx : v x ≤ 1) : v (σ x - x) < 1

theorem AbsoluteValue.inertiaSubgroup_eq_of_isNonarchimedean (F : Type u_4) {K : Type u_5} [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] (v : AbsoluteValue K ℝ) (h : IsNonarchimedean ⇑v) : inertiaSubgroup F v = Subgroup.map (ValuationSubring.decompositionSubgroup F (v.toValuation h).valuationSubring).subtype (ValuationSubring.inertiaSubgroup F (v.toValuation h).valuationSubring)

Our definition is the same as ValuationSubring.inertiaSubgroup for finite places.

theorem AbsoluteValue.inertiaSubgroup_comp_algEquiv_eq_comap {F : Type u_1} {K : Type u_2} {S : Type u_3} [CommSemiring F] [Ring K] [Algebra F K] [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue K S) {K' : Type u_4} [Ring K'] [Algebra F K'] (f : K' ≃ₐ[F] K) : inertiaSubgroup F (v.comp ⋯) = Subgroup.comap (↑f.autCongr) (inertiaSubgroup F v)

theorem AbsoluteValue.inertiaSubgroup_comp_ringEquiv_eq_comap {S : Type u_3} [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] {F : Type u_4} {E : Type u_5} [CommSemiring F] [Ring E] [Algebra F E] {M : Type u_6} {N : Type u_7} [CommSemiring M] [Ring N] [Algebra M N] {f : F →+* M} {g : E ≃+* N} (v : AbsoluteValue N S) (hsurj : Function.Surjective ⇑f) (hcomp : (algebraMap M N).comp f = (↑g).comp (algebraMap F E)) : inertiaSubgroup F (v.comp ⋯) = Subgroup.comap (↑(AlgEquiv.autCongrOfSurjective hsurj hcomp)) (inertiaSubgroup M v)

theorem AbsoluteValue.inertiaSubgroup_comp_algEquiv_eq_smul {F : Type u_1} {K : Type u_2} {S : Type u_3} [CommSemiring F] [Ring K] [Algebra F K] [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue K S) (f : K ≃ₐ[F] K) : inertiaSubgroup F (v.comp ⋯) = (MulAut.conj f)⁻¹ • inertiaSubgroup F v

theorem AbsoluteValue.inertiaSubgroup_eq_comap (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] {S : Type u_4} [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue L S) : inertiaSubgroup K v = Subgroup.comap (IntermediateField.restrictRestrictAlgEquivMapHom F L K L) (inertiaSubgroup F v)

If L / K / F is an extension tower with L / F Galois, v is a place of L, then Iᵥ(L/K) = Iᵥ(L/F) ⊓ Gal(L/K).

theorem AbsoluteValue.map_inertiaSubgroup_le (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] {S : Type u_4} [Semiring S] [Nontrivial S] [LinearOrder S] [ZeroLEOneClass S] [MulPosMono S] (v : AbsoluteValue L S) : Subgroup.map (IntermediateField.restrictRestrictAlgEquivMapHom F L K L) (inertiaSubgroup K v) ≤ inertiaSubgroup F v

If L / K / F is an extension tower with L / F Galois, v is a place of L, then Iᵥ(L/K) ≤ Iᵥ(L/F).

theorem AbsoluteValue.map_inertiaSubgroup_eq_of_liesOver (F : Type u_1) {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Algebra F K] [Field L] [Algebra F L] [Algebra K L] [IsScalarTower F K L] [Normal F K] [Normal F L] (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ) [w.LiesOver v] : Subgroup.map (AlgEquiv.restrictNormalHom K) (inertiaSubgroup F w) = inertiaSubgroup F v

If L / K / F is an extension tower, L / F and K / F are Galois, v and w are places of K and L, respectively, such that w lies over v, then the image of I_w(L/F) in Gal(K/F) is equal to Iᵥ(K/F).