Testing the inertia subgroup of an ideal on algebra generators

Let G act by ring automorphisms on a commutative ring S, and let I be an ideal of S. Mathlib's Ideal.inertia G I collects the σ with σ x - x ∈ I for every x. That condition is multiplicative and additive in x up to I, so the elements it holds for form a subalgebra over any base ring R whose elements G fixes: it is enough to test it on a generating set of S over R.

This is the ring-theoretic content of Serre's Lemme 1 in Corps Locaux, Chapter IV, §1, where it is used for I a power of the maximal ideal of a discrete valuation ring and s a single generator.

Main results

• TauCeti.Ideal.mem_inertia_iff_of_adjoin_eq_top: membership in Ideal.inertia G I is decided on a generating set.
• TauCeti.smul_sub_dvd_smul_sub_of_adjoin_singleton_eq_top: for a single generator ξ, every σ • x - x is a multiple of σ • ξ - ξ.

References

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

theorem TauCeti.Ideal.mem_inertia_iff_of_adjoin_eq_top {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S] [SMulCommClass G R S] {I : Ideal S} {s : Set S} (hs : Algebra.adjoin R s = ⊤) {σ : G} : σ ∈ Ideal.inertia G I ↔ ∀ x ∈ s, σ • x - x ∈ I

Serre's criterion. When S is generated over R by a set s and G acts by R-algebra automorphisms, membership in the inertia subgroup of an ideal I is decided on s alone: the elements moved into I form an R-subalgebra.

theorem TauCeti.Ideal.mem_inertia_iff_of_adjoin_singleton_eq_top {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S] [SMulCommClass G R S] {I : Ideal S} {ξ : S} (hξ : R[ξ] = ⊤) {σ : G} : σ ∈ Ideal.inertia G I ↔ σ • ξ - ξ ∈ I

The monogenic case of Serre's criterion: when S is generated over R by a single element ξ, membership in the inertia subgroup of I is decided at ξ alone.

theorem TauCeti.smul_sub_dvd_smul_sub_of_adjoin_singleton_eq_top {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S] [SMulCommClass G R S] {ξ : S} (hξ : R[ξ] = ⊤) (σ : G) (x : S) : σ • ξ - ξ ∣ σ • x - x

When S is generated over R by a single element ξ and G acts by R-algebra automorphisms, every displacement σ • x - x is a multiple of σ • ξ - ξ. This is the monogenic case of Serre's criterion, applied to the principal ideal generated by σ • ξ - ξ.