The ramification groups of an ideal

Let a group G act by ring automorphisms on a commutative ring B, and let Q be an ideal of B. The ramification groups of Q are the inertia subgroups of the powers of Q:

Q.ramificationGroup G i = {σ | ∀ x : B, σ • x - x ∈ Q ^ (i + 1)}, for i : ℕ.

For a Galois extension of number fields L/K, with G = Gal(L/K) acting on 𝓞 L and Q a nonzero prime of 𝓞 L, these are Hilbert's ramification groups G_i of Q, the global form of the lower-numbering filtration of Serre's Corps Locaux. They are indexed by ℕ, so that G_0 is the inertia group of Q; the decomposition group, the stabilizer of Q, contains every G_i but is not itself a member of the family.

Main definitions

• Ideal.ramificationGroup G Q i: the i-th ramification group of Q.

Main results

• Ideal.mem_ramificationGroup_iff: the defining congruence σ • x ≡ x mod Q ^ (i + 1).
• Ideal.ramificationGroup_zero: G_0 is the inertia group Q.inertia G.
• Ideal.ramificationGroup_antitone and Ideal.ramificationGroup_le_stabilizer: the groups decrease and lie in the decomposition group.
• Ideal.ramificationGroup_smul: moving Q by g conjugates its ramification groups by g, and Ideal.instNormalRamificationGroupStabilizer makes each G_i normal in the decomposition group.
• Ideal.iInf_ramificationGroup_eq_ker and Ideal.exists_forall_ramificationGroup_eq_bot: for a proper ideal Q of a Noetherian domain the filtration cuts out the kernel of the action, and a faithful action with finite inertia group has G_i = 1 for all large i.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §1.
• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter I, §9.

def Ideal.ramificationGroup (G : Type u_1) [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] (Q : Ideal B) (i : ℕ) : Subgroup G

The i-th ramification group of an ideal Q for a group G acting on the ring: the elements of G acting trivially on B ⧸ Q ^ (i + 1), that is, the inertia subgroup of Q ^ (i + 1).

Equations

• Ideal.ramificationGroup G Q i = Ideal.inertia G (Q ^ (i + 1))

theorem Ideal.ramificationGroup_def {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] (Q : Ideal B) (i : ℕ) : ramificationGroup G Q i = inertia G (Q ^ (i + 1))

The ramification groups are the inertia subgroups of the powers of Q.

@[simp]

theorem Ideal.mem_ramificationGroup_iff {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] {Q : Ideal B} {i : ℕ} {σ : G} : σ ∈ ramificationGroup G Q i ↔ ∀ (x : B), σ • x - x ∈ Q ^ (i + 1)

The defining membership criterion of the ramification groups.

@[simp]

theorem Ideal.ramificationGroup_subgroupOf {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] (Q : Ideal B) (i : ℕ) (H : Subgroup G) : (ramificationGroup G Q i).subgroupOf H = ramificationGroup (↥H) Q i

Restricting a ramification group to a subgroup H gives the ramification group for the action of H.

@[simp]

theorem Ideal.ramificationGroup_zero {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] (Q : Ideal B) : ramificationGroup G Q 0 = inertia G Q

The zeroth ramification group is the inertia group.

theorem Ideal.ramificationGroup_antitone (G : Type u_1) [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] (Q : Ideal B) : Antitone (ramificationGroup G Q)

The ramification groups decrease.

theorem Ideal.ramificationGroup_le_inertia {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] (Q : Ideal B) (i : ℕ) : ramificationGroup G Q i ≤ inertia G Q

Every ramification group lies in the inertia group.

theorem Ideal.ramificationGroup_le_stabilizer {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] (Q : Ideal B) (i : ℕ) : ramificationGroup G Q i ≤ MulAction.stabilizer G Q

Every ramification group lies in the decomposition group, the stabilizer of Q.

theorem Ideal.ramificationGroup_smul {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] (g : G) (Q : Ideal B) (i : ℕ) : ramificationGroup G (g • Q) i = Subgroup.map (↑(MulAut.conj g)) (ramificationGroup G Q i)

Moving the ideal by g conjugates its ramification groups by g.

instance Ideal.instNormalRamificationGroupStabilizer {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] (Q : Ideal B) (i : ℕ) : (ramificationGroup (↥(MulAction.stabilizer G Q)) Q i).Normal

Each ramification group is normal in the decomposition group.

theorem Ideal.iInf_ramificationGroup_eq_ker {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] [IsNoetherianRing B] [IsDomain B] {Q : Ideal B} (hQ : Q ≠ ⊤) : ⨅ (i : ℕ), ramificationGroup G Q i = (MulSemiringAction.toRingAut G B).ker

Over a Noetherian domain, the ramification groups of a proper ideal intersect in the kernel of the action: an element acting trivially modulo every power of Q acts trivially, by the Krull intersection theorem.

theorem Ideal.iInf_ramificationGroup_eq_bot {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] [IsNoetherianRing B] [IsDomain B] [FaithfulSMul G B] {Q : Ideal B} (hQ : Q ≠ ⊤) : ⨅ (i : ℕ), ramificationGroup G Q i = ⊥

For a faithful action on a Noetherian domain, the ramification groups of a proper ideal intersect in the trivial group.

theorem Ideal.exists_forall_ramificationGroup_eq_ker {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] [IsNoetherianRing B] [IsDomain B] {Q : Ideal B} (hQ : Q ≠ ⊤) [Finite ↥(inertia G Q)] : ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → ramificationGroup G Q i = (MulSemiringAction.toRingAut G B).ker

Once the inertia group is finite, the ramification groups of a proper ideal of a Noetherian domain reach the kernel of the action at a finite index.

theorem Ideal.exists_forall_ramificationGroup_eq_bot {G : Type u_1} [Group G] {B : Type u_2} [CommRing B] [MulSemiringAction G B] [IsNoetherianRing B] [IsDomain B] [FaithfulSMul G B] {Q : Ideal B} (hQ : Q ≠ ⊤) [Finite ↥(inertia G Q)] : ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → ramificationGroup G Q i = ⊥

For a faithful action on a Noetherian domain with finite inertia group, the ramification groups of a proper ideal are trivial from some index on.