The ramification filtration of a group acting on a local ring

Let G act by ring automorphisms on a local ring S. The ramification groups of the action are the decreasing family of subgroups

ramificationGroup G S i = {σ | ∀ x : S, σ • x - x ∈ 𝔪 ^ (i + 1)},

indexed by i : ℤ with the convention that 𝔪 ^ 0 = ⊤, so that the family is total and equals ⊤ below 0. This is Serre's lower-numbering filtration G_i, written here for the pair (G, S) rather than for an extension of local fields: nothing in the definition, and nothing in the results below, uses a valuation on a fraction field. The filtration of a finite Galois extension of nonarchimedean local fields is the case G = L ≃ₐ[K] L, S = 𝒪[L].

Mathlib's Ideal.inertia already names {σ | ∀ x, σ • x - x ∈ I} for an ideal I; the content here is the family it forms as I runs through the powers of the maximal ideal, together with the integer indexing that Herbrand theory uses.

Main definitions

• TauCeti.IsLocalRing.ramificationGroup G S i: the i-th ramification group, for i : ℤ.
• TauCeti.IsLocalRing.ramificationGroupReal G S u: the same family reindexed by a real number through ⌈·⌉, the convention under which the step function is constant on (i - 1, i].
• TauCeti.IsLocalRing.RamificationGroupGraded G S i: the successive quotient G_i / G_{i+1}.
• TauCeti.IsLocalRing.lowerIndex S σ: over a discrete valuation ring, Serre's lower index i_G(σ) = min_x v (σ x - x) in ℕ∞.

Main results

• TauCeti.IsLocalRing.ramificationGroup_natCast: at a nonnegative index G_i is Ideal.ramificationGroup of the maximal ideal.
• TauCeti.IsLocalRing.ramificationGroup_eq_top_of_le_neg_one and TauCeti.IsLocalRing.ramificationGroup_antitone: the filtration starts at ⊤ and decreases.
• TauCeti.IsLocalRing.ramificationGroup_zero_eq_inertia: G_0 is the inertia subgroup of the maximal ideal, TauCeti.IsLocalRing.ramificationGroup_zero_eq_ker_toRingAut identifies it with the kernel of the action on the residue field, and TauCeti.IsLocalRing.residue_smul_eq_of_mem_ramificationGroup_zero is its pointwise form, while TauCeti.IsLocalRing.ramificationGroup_zero_eq_inertiaSubgroup reads that off as Mathlib's ValuationSubring.inertiaSubgroup for a valuation subring of a field.
• TauCeti.IsLocalRing.instNormalRamificationGroup: each G_i is normal in G.
• TauCeti.IsLocalRing.ramificationGroupGradedSubgroupHom: subgroup inclusion induces an injective homomorphism H_i / H_{i+1} → G_i / G_{i+1} on successive quotients.
• TauCeti.IsLocalRing.ramificationGroupGradedConj: conjugation by an element of the ambient group induces an automorphism of each successive quotient.
• TauCeti.IsLocalRing.iInf_ramificationGroup_eq_ker and TauCeti.IsLocalRing.exists_forall_ramificationGroup_eq_ker: over a Noetherian local ring the filtration cuts out the kernel of the action, and reaches it at a finite index once G_0 is finite; TauCeti.IsLocalRing.iInf_ramificationGroup_eq_bot and TauCeti.IsLocalRing.exists_forall_ramificationGroup_eq_bot are the faithful case.
• TauCeti.IsLocalRing.mem_ramificationGroup_iff_of_adjoin_eq_top: when S is generated over a base ring R whose elements G fixes by a set s, membership in G_i is decided on s alone; TauCeti.IsLocalRing.mem_ramificationGroup_iff_of_adjoin_singleton_eq_top is the monogenic case, where a single generator decides it.
• TauCeti.IsLocalRing.mem_ramificationGroup_iff_le_addVal: over a discrete valuation ring the defining condition is the valuation inequality v (σ x - x) ≥ i + 1; TauCeti.IsLocalRing.mem_ramificationGroup_iff_le_lowerIndex reads it as i + 1 ≤ i_G(σ).
• TauCeti.IsLocalRing.lowerIndex_eq_top_iff: for a faithful action only the identity has lower index ⊤, and TauCeti.IsLocalRing.lowerIndex_eq_addVal_of_adjoin_singleton_eq_top computes the lower index at a single generator.
• TauCeti.IsLocalRing.mem_ramificationGroup_natCast_iff_le_addVal_of_adjoin_singleton_eq_top tests membership in G_n at a single generator.
• TauCeti.IsLocalRing.sum_addVal_smul_sub_eq_finsum_card_ramificationGroup_sub_one: Hilbert's counting identity ∑_{σ ≠ 1} v (σ ξ - ξ) = ∑_{i ≥ 0} (#G_i - 1) for a generator ξ of a discrete valuation ring under a faithful action of a finite group.
• TauCeti.IsLocalRing.sum_min_lowerIndex_natCast: the truncated count ∑_{σ ∈ G} min (i_G(σ), m) = ∑_{k < m} #G_k for a finite group G.
• TauCeti.IsLocalRing.mem_ramificationGroup_iff_of_lowerIndex_eq and TauCeti.IsLocalRing.mem_ramificationGroupReal_iff_of_lowerIndex_eq: when i_G(σ) = n is finite, σ ∈ G_i ↔ i + 1 ≤ n and σ ∈ G_u ↔ u ≤ n - 1.

References

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

def TauCeti.IsLocalRing.ramificationGroup (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (i : ℤ) : Subgroup G

The i-th ramification group, in the lower numbering, of a group G acting by ring automorphisms on a local ring S: the subgroup of elements acting trivially on S ⧸ 𝔪 ^ (i + 1). The index is an integer, and 𝔪 ^ (i + 1) is read as 𝔪 ^ (i + 1).toNat, so that the family is total and constantly ⊤ for i ≤ -1.

Equations

• TauCeti.IsLocalRing.ramificationGroup G S i = Ideal.inertia G (IsLocalRing.maximalIdeal S ^ (i + 1).toNat)

theorem TauCeti.IsLocalRing.ramificationGroup_def (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (i : ℤ) : ramificationGroup G S i = Ideal.inertia G (IsLocalRing.maximalIdeal S ^ (i + 1).toNat)

The ramification groups are the inertia subgroups of the powers of the maximal ideal.

@[simp]

theorem TauCeti.IsLocalRing.mem_ramificationGroup_iff {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsLocalRing S] [MulSemiringAction G S] {i : ℤ} {σ : G} : σ ∈ ramificationGroup G S i ↔ ∀ (x : S), σ • x - x ∈ IsLocalRing.maximalIdeal S ^ (i + 1).toNat

The defining membership criterion of the ramification groups.

theorem TauCeti.IsLocalRing.mem_ramificationGroup_natCast_iff {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsLocalRing S] [MulSemiringAction G S] {n : ℕ} {σ : G} : σ ∈ ramificationGroup G S ↑n ↔ ∀ (x : S), σ • x - x ∈ IsLocalRing.maximalIdeal S ^ (n + 1)

At a nonnegative index the truncation disappears from the membership criterion.

@[simp]

theorem TauCeti.IsLocalRing.ramificationGroup_natCast {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (n : ℕ) : ramificationGroup G S ↑n = Ideal.ramificationGroup G (IsLocalRing.maximalIdeal S) n

At a nonnegative index, the ramification group of the local ring is the ramification group Ideal.ramificationGroup of its maximal ideal.

theorem TauCeti.IsLocalRing.mem_ramificationGroup_zero_iff {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsLocalRing S] [MulSemiringAction G S] {σ : G} : σ ∈ ramificationGroup G S 0 ↔ ∀ (x : S), σ • x - x ∈ IsLocalRing.maximalIdeal S

At the index 0 the defining condition is congruence modulo the maximal ideal itself.

theorem TauCeti.IsLocalRing.mem_ramificationGroup_iff_quotient_mk_smul_eq {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsLocalRing S] [MulSemiringAction G S] {i : ℤ} {σ : G} : σ ∈ ramificationGroup G S i ↔ ∀ (x : S), (Ideal.Quotient.mk (IsLocalRing.maximalIdeal S ^ (i + 1).toNat)) (σ • x) = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal S ^ (i + 1).toNat)) x

Membership in G_i says that σ acts trivially on S ⧸ 𝔪 ^ (i + 1).

theorem TauCeti.IsLocalRing.ramificationGroup_eq_top_of_le_neg_one (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] {i : ℤ} (hi : i ≤ -1) : ramificationGroup G S i = ⊤

Below the index 0 the filtration is the whole group.

theorem TauCeti.IsLocalRing.ramificationGroup_zero_eq_inertia (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] : ramificationGroup G S 0 = Ideal.inertia G (IsLocalRing.maximalIdeal S)

The zeroth ramification group is the inertia subgroup of the maximal ideal.

@[reducible, inline]

abbrev TauCeti.IsLocalRing.RamificationGroupGraded (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (i : ℤ) : Type u_1

The successive quotient G_i / G_{i+1} of the ramification filtration.

Equations

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

theorem TauCeti.IsLocalRing.ramificationGroup_antitone (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] : Antitone (ramificationGroup G S)

The ramification filtration is decreasing.

theorem TauCeti.IsLocalRing.mem_ramificationGroup_iff_of_adjoin_eq_top {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsLocalRing S] [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S] [SMulCommClass G R S] {s : Set S} (hs : Algebra.adjoin R s = ⊤) {i : ℤ} {σ : G} : σ ∈ ramificationGroup G S i ↔ ∀ x ∈ s, σ • x - x ∈ IsLocalRing.maximalIdeal S ^ (i + 1).toNat

Serre's criterion for the ramification filtration: when S is generated over R by a set s and G acts by R-algebra automorphisms, membership in G_i is decided on s alone. This is TauCeti.Ideal.mem_inertia_iff_of_adjoin_eq_top at a power of the maximal ideal.

theorem TauCeti.IsLocalRing.mem_ramificationGroup_iff_of_adjoin_singleton_eq_top {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsLocalRing S] [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S] [SMulCommClass G R S] {ξ : S} (hξ : R[ξ] = ⊤) {i : ℤ} {σ : G} : σ ∈ ramificationGroup G S i ↔ σ • ξ - ξ ∈ IsLocalRing.maximalIdeal S ^ (i + 1).toNat

The monogenic case of Serre's criterion: when S is generated over R by a single element ξ, membership in G_i is decided at ξ alone. This is what makes the filtration computable, and it applies to the integer ring of a finite separable extension of local fields through local monogenicity.

instance TauCeti.IsLocalRing.instNormalRamificationGroup (G : Type u_3) [Group G] (S : Type u_4) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (i : ℤ) : (ramificationGroup G S i).Normal

Every ramification group is normal, because the action fixes the powers of the maximal ideal.

theorem TauCeti.IsLocalRing.ramificationGroup_zero_eq_ker_toRingAut (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] : ramificationGroup G S 0 = (MulSemiringAction.toRingAut G (IsLocalRing.ResidueField S)).ker

The zeroth ramification group is the inertia group: the kernel of the induced action on the residue field.

theorem TauCeti.IsLocalRing.residue_smul_eq_of_mem_ramificationGroup_zero (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] {g : G} (hg : g ∈ ramificationGroup G S 0) (x : S) : (IsLocalRing.residue S) (g • x) = (IsLocalRing.residue S) x

An element of the zeroth ramification group acts trivially on every residue class.

theorem TauCeti.IsLocalRing.ramificationGroup_zero_eq_inertiaSubgroup (K : Type u_3) {L : Type u_4} [Field K] [Field L] [Algebra K L] (A : ValuationSubring L) : ramificationGroup (↥(ValuationSubring.decompositionSubgroup K A)) (↥A) 0 = ValuationSubring.inertiaSubgroup K A

For a valuation subring of a field, the zeroth ramification group of the decomposition subgroup is Mathlib's ValuationSubring.inertiaSubgroup, which is defined as that same kernel.

theorem TauCeti.IsLocalRing.iInf_ramificationGroup_eq_ker (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] [IsNoetherianRing S] : ⨅ (i : ℤ), ramificationGroup G S i = (MulSemiringAction.toRingAut G S).ker

Over a Noetherian local ring the ramification filtration cuts out the kernel of the action: an element moving no point of S into every power of the maximal ideal is one that moves no point at all.

theorem TauCeti.IsLocalRing.iInf_ramificationGroup_eq_bot (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] [IsNoetherianRing S] [FaithfulSMul G S] : ⨅ (i : ℤ), ramificationGroup G S i = ⊥

A faithful action on a Noetherian local ring is separated by its ramification filtration.

theorem TauCeti.IsLocalRing.exists_forall_ramificationGroup_eq_ker (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] [IsNoetherianRing S] [Finite ↥(ramificationGroup G S 0)] : ∃ (N : ℤ), ∀ (i : ℤ), N ≤ i → ramificationGroup G S i = (MulSemiringAction.toRingAut G S).ker

Once the zeroth ramification group is finite, the filtration over a Noetherian local ring reaches the kernel of the action at a finite index.

theorem TauCeti.IsLocalRing.exists_forall_ramificationGroup_eq_bot (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] [IsNoetherianRing S] [FaithfulSMul G S] [Finite ↥(ramificationGroup G S 0)] : ∃ (N : ℤ), ∀ (i : ℤ), N ≤ i → ramificationGroup G S i = ⊥

For a faithful action whose zeroth ramification group is finite, the ramification groups over a Noetherian local ring vanish from some index on.

theorem TauCeti.IsLocalRing.mem_ramificationGroup_iff_le_addVal {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] {i : ℤ} {σ : G} : σ ∈ ramificationGroup G S i ↔ ∀ (x : S), ↑(i + 1).toNat ≤ (IsDiscreteValuationRing.addVal S) (σ • x - x)

Over a discrete valuation ring the ramification groups are cut out by the valuation inequality v (σ x - x) ≥ i + 1, which is Serre's definition.

noncomputable def TauCeti.IsLocalRing.lowerIndex {G : Type u_1} [Group G] (S : Type u_2) [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] (σ : G) : ℕ∞

Serre's lower index i_G(σ) of an element σ acting on a discrete valuation ring S: the least valuation v (σ x - x) over all x : S, with value ⊤ when σ acts trivially. Its superlevel sets are the ramification groups: σ ∈ G_i ↔ i + 1 ≤ i_G(σ).

Equations

• TauCeti.IsLocalRing.lowerIndex S σ = ⨅ (x : S), (IsDiscreteValuationRing.addVal S) (σ • x - x)

theorem TauCeti.IsLocalRing.lowerIndex_def {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] (σ : G) : lowerIndex S σ = ⨅ (x : S), (IsDiscreteValuationRing.addVal S) (σ • x - x)

The lower index is the infimum of the valuations of all displacements.

theorem TauCeti.IsLocalRing.le_lowerIndex_iff {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] {n : ℕ∞} {σ : G} : n ≤ lowerIndex S σ ↔ ∀ (x : S), n ≤ (IsDiscreteValuationRing.addVal S) (σ • x - x)

A lower bound for the lower index is a lower bound for every v (σ x - x).

theorem TauCeti.IsLocalRing.lowerIndex_le_addVal {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] (σ : G) (x : S) : lowerIndex S σ ≤ (IsDiscreteValuationRing.addVal S) (σ • x - x)

The lower index is at most the valuation v (σ x - x) at any x.

theorem TauCeti.IsLocalRing.mem_ramificationGroup_iff_le_lowerIndex {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] {i : ℤ} {σ : G} : σ ∈ ramificationGroup G S i ↔ ↑(i + 1).toNat ≤ lowerIndex S σ

The ramification groups are the superlevel sets of the lower index: σ ∈ G_i exactly when i + 1 ≤ i_G(σ).

theorem TauCeti.IsLocalRing.natCast_le_lowerIndex_iff_mem_ramificationGroup {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] {n : ℕ} {σ : G} : ↑n ≤ lowerIndex S σ ↔ σ ∈ ramificationGroup G S (↑n - 1)

A natural number bounds the lower index exactly when the automorphism belongs to the corresponding ramification group.

theorem TauCeti.IsLocalRing.mem_ramificationGroup_iff_of_lowerIndex_eq {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] {i : ℤ} {σ : G} {n : ℕ} (hn : lowerIndex S σ = ↑n) : σ ∈ ramificationGroup G S i ↔ i + 1 ≤ ↑n

When the lower index of σ is the natural number n, σ ∈ G_i exactly when i + 1 ≤ n.

@[simp]

theorem TauCeti.IsLocalRing.lowerIndex_inv {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] (σ : G) : lowerIndex S σ⁻¹ = lowerIndex S σ

The lower index is unchanged by inversion.

@[simp]

theorem TauCeti.IsLocalRing.lowerIndex_conj {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] (σ τ : G) : lowerIndex S (σ * τ * σ⁻¹) = lowerIndex S τ

The lower index is constant on conjugacy classes.

theorem TauCeti.IsLocalRing.min_le_lowerIndex_mul {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] (σ τ : G) : min (lowerIndex S σ) (lowerIndex S τ) ≤ lowerIndex S (σ * τ)

The lower index of a product is at least the minimum of the two lower indices.

@[simp]

theorem TauCeti.IsLocalRing.lowerIndex_one {G : Type u_1} [Group G] (S : Type u_2) [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] : lowerIndex S 1 = ⊤

The identity has lower index ⊤.

@[simp]

theorem TauCeti.IsLocalRing.lowerIndex_eq_top_iff {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] [FaithfulSMul G S] {σ : G} : lowerIndex S σ = ⊤ ↔ σ = 1

For a faithful action, only the identity has lower index ⊤.

theorem TauCeti.IsLocalRing.lowerIndex_eq_addVal_of_adjoin_singleton_eq_top {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S] [SMulCommClass G R S] {ξ : S} (hξ : R[ξ] = ⊤) (σ : G) : lowerIndex S σ = (IsDiscreteValuationRing.addVal S) (σ • ξ - ξ)

When S is generated over a base ring R fixed by G by a single element ξ, the lower index is read at ξ alone: i_G(σ) = v (σ ξ - ξ). This recovers Serre's monogenic computation formula.

theorem TauCeti.IsLocalRing.mem_ramificationGroup_natCast_iff_le_addVal_of_adjoin_singleton_eq_top {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S] [SMulCommClass G R S] {ξ : S} (hξ : R[ξ] = ⊤) {n : ℕ} {σ : G} : σ ∈ ramificationGroup G S ↑n ↔ ↑(n + 1) ≤ (IsDiscreteValuationRing.addVal S) (σ • ξ - ξ)

When the discrete valuation ring S is generated over a base R fixed by G by a single element ξ, membership in G_n for n : ℕ is the single inequality v (σ • ξ - ξ) ≥ n + 1.

theorem TauCeti.IsLocalRing.sum_addVal_smul_sub_eq_finsum_card_ramificationGroup_sub_one {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S] [SMulCommClass G R S] [Fintype G] [DecidableEq G] [FaithfulSMul G S] {ξ : S} (hξ : R[ξ] = ⊤) : ∑ σ ∈ Finset.univ.erase 1, (IsDiscreteValuationRing.addVal S) (σ • ξ - ξ) = ↑(∑ᶠ (i : ℕ), (Nat.card ↥(ramificationGroup G S ↑i) - 1))

Hilbert's counting identity. Let a finite group G act faithfully on a discrete valuation ring S generated over a base R fixed by G by a single element ξ. Then the sum over the nontrivial σ ∈ G of the valuations v (σ • ξ - ξ) is ∑_{i ≥ 0} (#G_i - 1), where G_i is the i-th ramification group: each σ ≠ 1 lies in exactly v (σ • ξ - ξ) of the groups G_0, G_1, …, and the sum is finite because the filtration is eventually trivial.

theorem TauCeti.IsLocalRing.sum_min_lowerIndex_natCast {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] [Fintype G] (m : ℕ) : ∑ σ : G, min (lowerIndex S σ) ↑m = ∑ k ∈ Finset.range m, ↑(Nat.card ↥(ramificationGroup G S ↑k))

Counting the filtration by truncated lower indices. For a finite group G, ∑_{σ ∈ G} min (i_G(σ), m) = ∑_{k < m} #G_k: each σ lies in exactly min (i_G(σ), m) of the groups G_0, …, G_{m-1}.

@[simp]

theorem TauCeti.IsLocalRing.subgroupOf_ramificationGroup (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (H : Subgroup G) (i : ℤ) : (ramificationGroup G S i).subgroupOf H = ramificationGroup (↥H) S i

The ramification filtration of a subgroup is the trace on it of the ramification filtration of the ambient group.

def TauCeti.IsLocalRing.ramificationGroupSubgroupHom (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (H : Subgroup G) (i : ℤ) : ↥(ramificationGroup (↥H) S i) →* ↥(ramificationGroup G S i)

Inclusion of the i-th ramification group for a subgroup H ≤ G into the i-th ramification group for G.

Equations

• TauCeti.IsLocalRing.ramificationGroupSubgroupHom G S H i = { toFun := fun (σ : ↥(TauCeti.IsLocalRing.ramificationGroup (↥H) S i)) => ⟨↑↑σ, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.IsLocalRing.coe_ramificationGroupSubgroupHom (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (H : Subgroup G) (i : ℤ) (σ : ↥(ramificationGroup (↥H) S i)) : ↑((ramificationGroupSubgroupHom G S H i) σ) = ↑↑σ

The inclusion of a subgroup ramification group agrees with the ambient inclusion.

def TauCeti.IsLocalRing.ramificationGroupGradedSubgroupHom (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (H : Subgroup G) (i : ℤ) : RamificationGroupGraded (↥H) S i →* RamificationGroupGraded G S i

Inclusion H → G induces a homomorphism H_i/H_{i+1} → G_i/G_{i+1} on every successive ramification quotient.

Equations

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

@[simp]

theorem TauCeti.IsLocalRing.ramificationGroupGradedSubgroupHom_mk (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (H : Subgroup G) (i : ℤ) (σ : ↥(ramificationGroup (↥H) S i)) : (ramificationGroupGradedSubgroupHom G S H i) ↑σ = ↑((ramificationGroupSubgroupHom G S H i) σ)

The map on ramification quotients induced by subgroup inclusion sends the class of an element to the class of the same element in the ambient group.

theorem TauCeti.IsLocalRing.ramificationGroupGradedSubgroupHom_injective (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (H : Subgroup G) (i : ℤ) : Function.Injective ⇑(ramificationGroupGradedSubgroupHom G S H i)

The map H_i/H_{i+1} → G_i/G_{i+1} induced by subgroup inclusion is injective.

Conjugation on the graded pieces

noncomputable def TauCeti.IsLocalRing.ramificationGroupGradedConj (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (g : G) (i : ℤ) : RamificationGroupGraded G S i ≃* RamificationGroupGraded G S i

Conjugation by an element of the ambient group induces an automorphism on every successive quotient G_i/G_{i+1} of the ramification filtration.

Equations

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

@[simp]

theorem TauCeti.IsLocalRing.ramificationGroupGradedConj_mk (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (g : G) (i : ℤ) (x : ↥(ramificationGroup G S i)) : (ramificationGroupGradedConj G S g i) ↑x = ↑((MulAut.conjNormal g) x)

On a class represented by x ∈ G_i, the induced conjugation is represented by g * x * g⁻¹.

@[simp]

theorem TauCeti.IsLocalRing.ramificationGroupGradedConj_one (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (i : ℤ) (x : RamificationGroupGraded G S i) : (ramificationGroupGradedConj G S 1 i) x = x

Conjugation by the identity acts trivially on each ramification quotient.

@[simp]

theorem TauCeti.IsLocalRing.ramificationGroupGradedConj_mul (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (g h : G) (i : ℤ) (x : RamificationGroupGraded G S i) : (ramificationGroupGradedConj G S (g * h) i) x = (ramificationGroupGradedConj G S g i) ((ramificationGroupGradedConj G S h i) x)

Conjugation by a product is the composite of the corresponding conjugation automorphisms.

noncomputable def TauCeti.IsLocalRing.ramificationGroupReal (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (u : ℝ) : Subgroup G

The ramification filtration reindexed by a real number, through the ceiling. This is the indexing convention of Herbrand theory: the resulting step function is constant on (i - 1, i].

Equations

• TauCeti.IsLocalRing.ramificationGroupReal G S u = TauCeti.IsLocalRing.ramificationGroup G S ⌈u⌉

theorem TauCeti.IsLocalRing.ramificationGroupReal_def (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (u : ℝ) : ramificationGroupReal G S u = ramificationGroup G S ⌈u⌉

The real-indexed filtration at u is the integer-indexed one at ⌈u⌉.

@[simp]

theorem TauCeti.IsLocalRing.mem_ramificationGroupReal_iff {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsLocalRing S] [MulSemiringAction G S] {u : ℝ} {σ : G} : σ ∈ ramificationGroupReal G S u ↔ ∀ (x : S), σ • x - x ∈ IsLocalRing.maximalIdeal S ^ (⌈u⌉ + 1).toNat

The defining membership criterion of the real-indexed ramification groups.

instance TauCeti.IsLocalRing.instNormalRamificationGroupReal (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (u : ℝ) : (ramificationGroupReal G S u).Normal

Every real-indexed ramification group is normal in G.

theorem TauCeti.IsLocalRing.ramificationGroupReal_antitone (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] : Antitone (ramificationGroupReal G S)

The real-indexed ramification filtration is decreasing.

@[simp]

theorem TauCeti.IsLocalRing.subgroupOf_ramificationGroupReal (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (H : Subgroup G) (u : ℝ) : (ramificationGroupReal G S u).subgroupOf H = ramificationGroupReal (↥H) S u

The real-indexed filtration of a subgroup is the trace on it of the real-indexed filtration of the ambient group.

@[simp]

theorem TauCeti.IsLocalRing.ramificationGroupReal_intCast (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] (i : ℤ) : ramificationGroupReal G S ↑i = ramificationGroup G S i

At an integer argument the real-indexed filtration agrees with the integer-indexed one.

theorem TauCeti.IsLocalRing.ramificationGroupReal_eq_of_sub_one_lt_of_le (G : Type u_1) [Group G] (S : Type u_2) [CommRing S] [IsLocalRing S] [MulSemiringAction G S] {i : ℤ} {u : ℝ} (hleft : ↑i - 1 < u) (hright : u ≤ ↑i) : ramificationGroupReal G S u = ramificationGroup G S i

The real indexing is constant on the interval (i - 1, i].

theorem TauCeti.IsLocalRing.mem_ramificationGroupReal_iff_of_lowerIndex_eq {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [MulSemiringAction G S] {u : ℝ} {σ : G} {n : ℕ} (hn : lowerIndex S σ = ↑n) : σ ∈ ramificationGroupReal G S u ↔ u ≤ ↑n - 1

When the lower index of σ is the natural number n, σ ∈ G_u for a real u exactly when u ≤ n - 1.