Lower ramification groups of a local field extension

For a finite Galois extension L/K of nonarchimedean local fields, the canonical lower ramification group consists of automorphisms acting trivially on the integer ring modulo the (i + 1)-st power of its maximal ideal. The integer index is total: at i ≤ -1 the group is the full Galois group.

This is the local field specialization of TauCeti.IsLocalRing.ramificationGroup. Besides the integer-indexed filtration, the file provides the real indexing G_u = G_{⌈u⌉} on which the Herbrand function is built, the largest jump of the filtration, and its compatibility with the subgroup Gal(L/K') ≤ Gal(L/K) of a tower L/K'/K.

Main definitions

• TauCeti.LocalFieldsRamification.lowerRamificationGroup K L i: the i-th lower-numbering ramification group of L/K.
• TauCeti.LocalFieldsRamification.lowerRamificationGroupReal K L u: the same filtration indexed by u : ℝ through the ceiling.
• TauCeti.LocalFieldsRamification.LowerJump K L u: a strict break of the lower filtration.
• TauCeti.LocalFieldsRamification.largestLowerJump K L: for a nontrivial Galois group, the largest index t with G_t ≠ 1; it is -1 by convention when the Galois group is trivial.

Main results

• TauCeti.LocalFieldsRamification.mem_lowerRamificationGroup_iff: the defining congruence σ • x ≡ x mod 𝔪 ^ (i + 1) on 𝒪[L], and TauCeti.LocalFieldsRamification.mem_lowerRamificationGroup_iff_le_lowerIndex: its reading i + 1 ≤ i(σ) on Serre's lower index TauCeti.IsLocalRing.lowerIndex.
• TauCeti.LocalFieldsRamification.lowerRamificationGroup_eq_top_of_le_neg_one, TauCeti.LocalFieldsRamification.lowerRamificationGroup_zero and TauCeti.LocalFieldsRamification.lowerRamificationGroup_antitone: the filtration is ⊤ below 0, starts with the inertia group of the maximal ideal, and decreases.
• TauCeti.LocalFieldsRamification.lowerRamificationGroup_natCast: at a nonnegative index it is Ideal.ramificationGroup of the maximal ideal of 𝒪[L].
• TauCeti.LocalFieldsRamification.lowerRamificationGroup_zero_eq_map_inertiaSubgroup: G_0 is Mathlib's ValuationSubring.inertiaSubgroup of the valuation subring of L.
• TauCeti.LocalFieldsRamification.natCard_lowerRamificationGroup_zero: #G_0 = e(L/K).
• TauCeti.LocalFieldsRamification.lowerRamificationGroup_zero_eq_top_iff: G_0 is the whole Galois group exactly when L/K is totally ramified.
• TauCeti.LocalFieldsRamification.instNormalLowerRamificationGroup: each G_i is normal.
• TauCeti.LocalFieldsRamification.exists_forall_lowerRamificationGroup_eq_bot and TauCeti.LocalFieldsRamification.lowerRamificationGroup_eq_bot_iff: G_i = 1 for large i, precisely for i past the largest jump when the Galois group is nontrivial.
• TauCeti.LocalFieldsRamification.lowerRamificationGroupReal_eq_of_sub_one_lt_of_le: the real indexing is constant on each interval (i - 1, i].
• TauCeti.LocalFieldsRamification.mem_lowerRamificationGroupReal_iff_of_lowerIndex_eq: when i(σ) = n is finite, σ ∈ G_u ↔ u ≤ n - 1.
• TauCeti.LocalFieldsRamification.lowerRamificationGroupReal_eq_bot_iff: for a nontrivial Galois group, G_u = 1 exactly for real u past the largest jump.
• TauCeti.LocalFieldsRamification.lowerJump_eq_intCast: every lower break has an integer index.
• TauCeti.LocalFieldsRamification.lowerJump_intCast_iff: an integer is a lower break exactly when the adjacent lower groups differ.
• TauCeti.LocalFieldsRamification.map_restrictScalarsHom_lowerRamificationGroup: for a tower L/K'/K, the filtration of H = Gal(L/K') is H ∩ G_i.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §1.

@[reducible, inline]

abbrev TauCeti.LocalFieldsRamification.RamificationIndexDomain : Set ℝ

The interval [-1, ∞), the domain of the Herbrand function and of its inverse. The lower ramification groups are indexed by real numbers u ≥ -1, and G_u is the whole automorphism group for u ≤ -1.

Equations

• TauCeti.LocalFieldsRamification.RamificationIndexDomain = Set.Ici (-1)

theorem Nat.cast_mem_ramificationIndexDomain (n : ℕ) : ↑n ∈ TauCeti.LocalFieldsRamification.RamificationIndexDomain

A natural number lies in the domain [-1, ∞) of the Herbrand function.

noncomputable def TauCeti.LocalFieldsRamification.lowerRamificationGroup (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (i : ℤ) : Subgroup Gal(L/K)

The lower-numbering ramification group of a finite extension of local fields.

Equations

• TauCeti.LocalFieldsRamification.lowerRamificationGroup K L i = TauCeti.IsLocalRing.ramificationGroup Gal(L/K) (↥(ValuativeRel.valuation L).integer) i

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_def (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (i : ℤ) : lowerRamificationGroup K L i = IsLocalRing.ramificationGroup Gal(L/K) (↥(ValuativeRel.valuation L).integer) i

The local-field filtration is the ramification filtration of its integer ring.

@[simp]

theorem TauCeti.LocalFieldsRamification.mem_lowerRamificationGroup_iff {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {i : ℤ} {σ : Gal(L/K)} : σ ∈ lowerRamificationGroup K L i ↔ ∀ (x : ↥(ValuativeRel.valuation L).integer), σ • x - x ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer ^ (i + 1).toNat

The defining membership criterion of the lower ramification groups.

theorem TauCeti.LocalFieldsRamification.mem_lowerRamificationGroup_iff_le_lowerIndex (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {i : ℤ} {σ : Gal(L/K)} : σ ∈ lowerRamificationGroup K L i ↔ ↑(i + 1).toNat ≤ IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) σ

The lower ramification groups are the superlevel sets of Serre's lower index i(σ) = min_{x ∈ 𝒪[L]} v_L(σ x - x): σ ∈ G_i exactly when i + 1 ≤ i(σ).

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_eq_top_of_le_neg_one (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {i : ℤ} (hi : i ≤ -1) : lowerRamificationGroup K L i = ⊤

Below the index 0 the lower filtration is the whole Galois group.

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_zero (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : lowerRamificationGroup K L 0 = Ideal.inertia Gal(L/K) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer)

The zeroth lower ramification group is the inertia group of the maximal ideal of 𝒪[L].

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_antitone (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : Antitone (lowerRamificationGroup K L)

The lower ramification filtration is decreasing.

@[simp]

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_natCast (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (i : ℕ) : lowerRamificationGroup K L ↑i = Ideal.ramificationGroup Gal(L/K) (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation L).integer) i

At nonnegative indices, the canonical lower group is the maximal-ideal ramification group.

instance TauCeti.LocalFieldsRamification.instNormalLowerRamificationGroup (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (i : ℤ) : (lowerRamificationGroup K L i).Normal

Every lower ramification group is normal in the Galois group.

theorem TauCeti.LocalFieldsRamification.natCard_lowerRamificationGroup_zero (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] : Nat.card ↥(lowerRamificationGroup K L 0) = ramificationIndex K L

The inertia group has order the ramification index: #G_0 = e(L/K).

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_zero_eq_top_iff (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] : lowerRamificationGroup K L 0 = ⊤ ↔ IsTotallyRamified K L

The inertia group is the whole Galois group exactly in the totally ramified case: G_0 = Gal(L/K) if and only if e(L/K) = [L : K].

Comparison with Mathlib's inertia subgroup of a valuation subring

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_zero_eq_map_inertiaSubgroup (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : lowerRamificationGroup K L 0 = Subgroup.map (ValuationSubring.decompositionSubgroup K (ValuativeRel.valuation L).valuationSubring).subtype (ValuationSubring.inertiaSubgroup K (ValuativeRel.valuation L).valuationSubring)

The zeroth lower ramification group is Mathlib's ValuationSubring.inertiaSubgroup of the valuation subring of L, viewed inside the decomposition subgroup, which is everything by TauCeti.decompositionSubgroup_valuationSubring_eq_top.

Eventual triviality and the largest jump

theorem TauCeti.LocalFieldsRamification.iInf_lowerRamificationGroup_eq_bot (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : ⨅ (i : ℤ), lowerRamificationGroup K L i = ⊥

The lower ramification filtration separates the automorphisms of L/K.

theorem TauCeti.LocalFieldsRamification.exists_forall_lowerRamificationGroup_eq_bot (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : ∃ (N : ℤ), ∀ (i : ℤ), N ≤ i → lowerRamificationGroup K L i = ⊥

The lower ramification groups are trivial from some index on.

noncomputable def TauCeti.LocalFieldsRamification.largestLowerJump (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : ℤ

The largest jump t of the lower ramification filtration. For a nontrivial Galois group it is the largest index with G_t ≠ 1, so that G_t ≠ 1 and G_{t + 1} = 1 (lowerRamificationGroup_largestLowerJump_ne_bot and lowerRamificationGroup_eq_bot_iff); it is at least -1 because G_{-1} is the whole Galois group. When L ≃ₐ[K] L is trivial every G_i is trivial and there is no jump; the value is then -1 by convention.

Equations

• TauCeti.LocalFieldsRamification.largestLowerJump K L = ↑(sInf {n : ℕ | TauCeti.LocalFieldsRamification.lowerRamificationGroup K L ↑n = ⊥}) - 1

theorem TauCeti.LocalFieldsRamification.neg_one_le_largestLowerJump (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : -1 ≤ largestLowerJump K L

The largest lower jump is at least -1.

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_eq_bot_of_largestLowerJump_lt {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {i : ℤ} (hi : largestLowerJump K L < i) : lowerRamificationGroup K L i = ⊥

The lower ramification groups past the largest jump are trivial.

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_largestLowerJump_ne_bot (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [Nontrivial Gal(L/K)] : lowerRamificationGroup K L (largestLowerJump K L) ≠ ⊥

For a nontrivial automorphism group, the lower ramification group at the largest jump is nontrivial.

@[simp]

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_eq_bot_iff {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [Nontrivial Gal(L/K)] {i : ℤ} : lowerRamificationGroup K L i = ⊥ ↔ largestLowerJump K L < i

For a nontrivial automorphism group, G_i is trivial exactly past the largest lower jump.

Real indexing

noncomputable def TauCeti.LocalFieldsRamification.lowerRamificationGroupReal (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (u : ℝ) : Subgroup Gal(L/K)

The lower ramification filtration indexed by a real number through the ceiling, as needed by the Herbrand function: G_u = G_{⌈u⌉}, a step function constant on each interval (i - 1, i].

Equations

• TauCeti.LocalFieldsRamification.lowerRamificationGroupReal K L u = TauCeti.IsLocalRing.ramificationGroupReal Gal(L/K) (↥(ValuativeRel.valuation L).integer) u

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroupReal_def (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (u : ℝ) : lowerRamificationGroupReal K L u = lowerRamificationGroup K L ⌈u⌉

The real-indexed lower ramification group at u is the integer-indexed one at ⌈u⌉.

@[simp]

theorem TauCeti.LocalFieldsRamification.mem_lowerRamificationGroupReal_iff {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {u : ℝ} {σ : Gal(L/K)} : σ ∈ lowerRamificationGroupReal K L u ↔ σ ∈ lowerRamificationGroup K L ⌈u⌉

Membership in the real-indexed lower ramification groups.

@[simp]

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroupReal_intCast (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (i : ℤ) : lowerRamificationGroupReal K L ↑i = lowerRamificationGroup K L i

At an integer the real indexing agrees with the integer indexing.

theorem TauCeti.LocalFieldsRamification.mem_lowerRamificationGroupReal_iff_of_lowerIndex_eq {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {u : ℝ} {σ : Gal(L/K)} {n : ℕ} (hn : IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) σ = ↑n) : σ ∈ lowerRamificationGroupReal K L u ↔ u ≤ ↑n - 1

When Serre's lower index of σ is the natural number n, σ ∈ G_u exactly when u ≤ n - 1.

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroupReal_eq_of_sub_one_lt_of_le (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {i : ℤ} {u : ℝ} (hleft : ↑i - 1 < u) (hright : u ≤ ↑i) : lowerRamificationGroupReal K L u = lowerRamificationGroup K L i

The real-indexed lower filtration is constant on each interval (i - 1, i].

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroupReal_antitone (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] : Antitone (lowerRamificationGroupReal K L)

The real-indexed lower filtration is decreasing.

Breaks of the lower filtration

def TauCeti.LocalFieldsRamification.LowerJump (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (u : ↑RamificationIndexDomain) : Prop

A lower break: the ramification group at u is strictly larger than the group at every later index. Since lower numbering uses ceilings, its breaks occur at integers.

Equations

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

theorem TauCeti.LocalFieldsRamification.lowerJump_iff (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (u : ↑RamificationIndexDomain) : LowerJump K L u ↔ ∀ (v : ↑RamificationIndexDomain), u < v → lowerRamificationGroupReal K L ↑v < lowerRamificationGroupReal K L ↑u

A lower break is a strict drop of the lower ramification group at every later index.

theorem TauCeti.LocalFieldsRamification.lowerJump_eq_intCast (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {u : ↑RamificationIndexDomain} (h : LowerJump K L u) : ∃ (i : ℤ) (hi : -1 ≤ ↑i), u = ⟨↑i, hi⟩

Every lower break occurs at an integer index.

@[simp]

theorem TauCeti.LocalFieldsRamification.lowerJump_intCast_iff (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {i : ℤ} (hi : -1 ≤ ↑i) : LowerJump K L ⟨↑i, hi⟩ ↔ lowerRamificationGroup K L (i + 1) < lowerRamificationGroup K L i

At an integer i ≥ -1, a lower break is exactly a strict decrease from G_i to G_{i+1}.

@[simp]

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroupReal_eq_bot_iff {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [Nontrivial Gal(L/K)] {u : ℝ} : lowerRamificationGroupReal K L u = ⊥ ↔ ↑(largestLowerJump K L) < u

For a nontrivial automorphism group, G_u is trivial exactly for real u past the largest lower jump.

instance TauCeti.LocalFieldsRamification.instNormalLowerRamificationGroupReal (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (u : ℝ) : (lowerRamificationGroupReal K L u).Normal

Every real-indexed lower ramification group is normal in the Galois group.

Compatibility with subgroups

For a tower L/K'/K, the group Gal(L/K') is the subgroup H of Gal(L/K) fixing K', embedded by AlgEquiv.restrictScalarsHom. Its lower filtration is the trace of that of L/K: H_i = H ∩ G_i.

@[simp]

theorem TauCeti.LocalFieldsRamification.lowerIndex_restrictScalars {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] {K' : Type u_3} [Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K'] [Algebra K K'] [Algebra K' L] [IsScalarTower K K' L] [ValuativeExtension K' L] [Module.Finite K' L] (σ : Gal(L/K')) : IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) (AlgEquiv.restrictScalars K σ) = IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) σ

Restricting scalars leaves Serre's lower index unchanged.

theorem TauCeti.LocalFieldsRamification.comap_restrictScalarsHom_lowerRamificationGroup (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (K' : Type u_3) [Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K'] [Algebra K K'] [Algebra K' L] [IsScalarTower K K' L] [ValuativeExtension K' L] [Module.Finite K' L] (i : ℤ) : Subgroup.comap (AlgEquiv.restrictScalarsHom K) (lowerRamificationGroup K L i) = lowerRamificationGroup K' L i

An automorphism of L/K' lies in the i-th lower ramification group of L/K' exactly when it lies in that of L/K after restricting scalars.

theorem TauCeti.LocalFieldsRamification.map_restrictScalarsHom_lowerRamificationGroup (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (K' : Type u_3) [Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K'] [Algebra K K'] [Algebra K' L] [IsScalarTower K K' L] [ValuativeExtension K' L] [Module.Finite K' L] (i : ℤ) : Subgroup.map (AlgEquiv.restrictScalarsHom K) (lowerRamificationGroup K' L i) = (AlgEquiv.restrictScalarsHom K).range ⊓ lowerRamificationGroup K L i

Compatibility with subgroups: the image of the lower filtration of L/K' in Gal(L/K) is the trace H ∩ G_i of the lower filtration of L/K on the image H of Gal(L/K').

theorem TauCeti.LocalFieldsRamification.comap_restrictScalarsHom_lowerRamificationGroupReal (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (K' : Type u_3) [Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K'] [Algebra K K'] [Algebra K' L] [IsScalarTower K K' L] [ValuativeExtension K' L] [Module.Finite K' L] (u : ℝ) : Subgroup.comap (AlgEquiv.restrictScalarsHom K) (lowerRamificationGroupReal K L u) = lowerRamificationGroupReal K' L u

The real-indexed form of comap_restrictScalarsHom_lowerRamificationGroup.

theorem TauCeti.LocalFieldsRamification.map_restrictScalarsHom_lowerRamificationGroupReal (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (K' : Type u_3) [Field K'] [ValuativeRel K'] [TopologicalSpace K'] [IsNonarchimedeanLocalField K'] [Algebra K K'] [Algebra K' L] [IsScalarTower K K' L] [ValuativeExtension K' L] [Module.Finite K' L] (u : ℝ) : Subgroup.map (AlgEquiv.restrictScalarsHom K) (lowerRamificationGroupReal K' L u) = (AlgEquiv.restrictScalarsHom K).range ⊓ lowerRamificationGroupReal K L u

The real-indexed form of map_restrictScalarsHom_lowerRamificationGroup.