Distributive actions on the quotient by a stable additive subgroup

Let a monoid G act distributively on an additive group M, and let N be a G-stable additive subgroup: g • x ∈ N for every g : G and x ∈ N. Then G acts distributively on N by restriction. When M is commutative, the action also descends to the quotient M ⧸ N, with g • ↑x = ↑(g • x). Mathlib provides these actions for submodules (Submodule.Quotient.distribMulAction) but not for a bare G-stable additive subgroup, where the stability is a hypothesis rather than an instance, so the actions are definitions rather than instances.

The file also records that stability passes to N ⊔ zmultiples x when the class of x is fixed by G modulo N, which is what lets a G-stable subgroup be enlarged one element at a time, and that the additive subgroup generated by the G-orbits of a family is G-stable and generated, for the restricted action, by the orbits of the same family read inside it.

Main declarations

• AddSubgroup.restrictDistribMulAction: the action of G on a G-stable N by restriction.
• AddSubgroup.restrictDistribMulAction_coe_smul: its defining equation ↑(g • x) = g • ↑x.
• AddSubgroup.smul_mem_closure_orbits: the additive subgroup generated by the G-orbits of a family v is G-stable.
• AddSubgroup.mem_closure_orbits_orbitsGenerator: that subgroup is generated, for the restricted action, by the orbits of the members AddSubgroup.orbitsGenerator v i of v read in it.
• AddSubgroup.quotientDistribMulAction: the action of G on M ⧸ N for a G-stable N.
• AddSubgroup.quotientDistribMulAction_smul_mk: its defining equation g • ↑x = ↑(g • x).
• AddSubgroup.subquotientDistribMulAction: the induced action on K ⧸ N.addSubgroupOf K for two stable subgroups N and K, the quotient action for the restricted action on K.
• TauCeti.smul_mem_sup_zmultiples: if N is G-stable and g • x - x ∈ N for every g, then N ⊔ zmultiples x is G-stable.
• TauCeti.subquotient_smul_eq_self_of_eq_sup_zmultiples: adjoining a generator fixed modulo N gives a quotient on which the induced action is trivial.

@[reducible, inline]

abbrev AddSubgroup.restrictDistribMulAction {G : Type u_1} [Monoid G] {M : Type u_2} [AddGroup M] [DistribMulAction G M] (N : AddSubgroup M) (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) : DistribMulAction G ↥N

The action of G on a G-stable additive subgroup N of M, by restriction. It is a definition rather than an instance because it depends on the stability hypothesis. See note [reducible non-instances].

Equations

• N.restrictDistribMulAction hN = Function.Injective.distribMulAction N.subtype ⋯ ⋯

@[simp]

theorem AddSubgroup.restrictDistribMulAction_coe_smul {G : Type u_1} [Monoid G] {M : Type u_2} [AddGroup M] [DistribMulAction G M] (N : AddSubgroup M) (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) (g : G) (x : ↥N) : ↑(g • x) = g • ↑x

The defining equation of AddSubgroup.restrictDistribMulAction: the inclusion of N in M is equivariant.

theorem AddSubgroup.restrictDistribMulAction_inclusion_smul {G : Type u_1} [Monoid G] {M : Type u_2} [AddGroup M] [DistribMulAction G M] {N K : AddSubgroup M} (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) (hK : ∀ (g : G), ∀ x ∈ K, g • x ∈ K) (h : N ≤ K) (g : G) (x : ↥N) : (inclusion h) (g • x) = g • (inclusion h) x

The inclusion of one G-stable additive subgroup in another is equivariant for the restricted actions.

theorem AddSubgroup.smul_mem_closure_orbits {G : Type u_1} [Monoid G] {M : Type u_2} [AddGroup M] [DistribMulAction G M] {ι : Type u_3} (v : ι → M) (g : G) (b : M) (hb : b ∈ closure (Set.range fun (x : G × ι) => x.1 • v x.2)) : g • b ∈ closure (Set.range fun (x : G × ι) => x.1 • v x.2)

The additive subgroup generated by the G-orbits of a family v is G-stable. The element is explicit so that the partial application to v has the shape of a stability hypothesis.

def AddSubgroup.orbitsGenerator {G : Type u_1} [Monoid G] {M : Type u_2} [AddGroup M] [DistribMulAction G M] {ι : Type u_3} (v : ι → M) (i : ι) : ↥(closure (Set.range fun (x : G × ι) => x.1 • v x.2))

The members v i of a family, read in the additive subgroup generated by their G-orbits; see AddSubgroup.coe_orbitsGenerator for its value.

Equations

• AddSubgroup.orbitsGenerator v i = ⟨v i, ⋯⟩

@[simp]

theorem AddSubgroup.coe_orbitsGenerator {G : Type u_1} [Monoid G] {M : Type u_2} [AddGroup M] [DistribMulAction G M] {ι : Type u_3} (v : ι → M) (i : ι) : ↑(orbitsGenerator v i) = v i

theorem AddSubgroup.mem_closure_orbits_orbitsGenerator {G : Type u_1} [Monoid G] {M : Type u_2} [AddGroup M] [DistribMulAction G M] {ι : Type u_3} (v : ι → M) (b : ↥(closure (Set.range fun (x : G × ι) => x.1 • v x.2))) : b ∈ closure (Set.range fun (x : G × ι) => x.1 • orbitsGenerator v x.2)

The additive subgroup K generated by the G-orbits of a family v is generated, as a G-module with the restricted action, by the orbits of the same family read in K.

@[reducible, inline]

abbrev AddSubgroup.quotientDistribMulAction {G : Type u_1} [Monoid G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] (N : AddSubgroup M) (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) : DistribMulAction G (M ⧸ N)

The action of G on the quotient of M by a G-stable additive subgroup N, with g • ↑x = ↑(g • x). It is a definition rather than an instance because it depends on the stability hypothesis. See note [reducible non-instances].

Equations

• N.quotientDistribMulAction hN = Function.Surjective.distribMulAction (QuotientAddGroup.mk' N) ⋯ ⋯

@[simp]

theorem AddSubgroup.quotientDistribMulAction_smul_mk {G : Type u_1} [Monoid G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] (N : AddSubgroup M) (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) (g : G) (x : M) : g • ↑x = ↑(g • x)

The defining equation of AddSubgroup.quotientDistribMulAction on the class of an element.

@[reducible, inline]

abbrev AddSubgroup.subquotientDistribMulAction {G : Type u_1} [Monoid G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] (N K : AddSubgroup M) (hN : ∀ (g : G), ∀ x ∈ N, g • x ∈ N) (hK : ∀ (g : G), ∀ x ∈ K, g • x ∈ K) : DistribMulAction G (↥K ⧸ N.addSubgroupOf K)

The induced action on K ⧸ N.addSubgroupOf K for two G-stable additive subgroups: the quotient action AddSubgroup.quotientDistribMulAction for the restricted action AddSubgroup.restrictDistribMulAction on K. The equation AddSubgroup.quotientDistribMulAction_smul_mk, applied to that restricted action, computes its value on quotient classes. See note [reducible non-instances].

Equations

• N.subquotientDistribMulAction K hN hK = (N.addSubgroupOf K).quotientDistribMulAction ⋯

theorem TauCeti.smul_mem_sup_zmultiples {G : Type u_1} [Monoid G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] {N : AddSubgroup M} (hN : ∀ (g : G), ∀ y ∈ N, g • y ∈ N) {x : M} (hx : ∀ (g : G), g • x - x ∈ N) (g : G) (y : M) (hy : y ∈ N ⊔ AddSubgroup.zmultiples x) : g • y ∈ N ⊔ AddSubgroup.zmultiples x

If N is G-stable and g • x - x ∈ N for every g, then N ⊔ zmultiples x is G-stable. The element is explicit so that the partial application to hN and hx has the shape of a stability hypothesis.

theorem TauCeti.subquotient_smul_eq_self_of_eq_sup_zmultiples {G : Type u_1} [Monoid G] {M : Type u_2} [AddCommGroup M] [DistribMulAction G M] {N K : AddSubgroup M} (hN : ∀ (g : G), ∀ y ∈ N, g • y ∈ N) {x : M} (hgen : K = N ⊔ AddSubgroup.zmultiples x) (hx : ∀ (g : G), g • x - x ∈ N) (g : G) (y : ↥K ⧸ N.addSubgroupOf K) : g • y = y

If K is obtained from N by adjoining an element fixed modulo N, then the induced action on K ⧸ N.addSubgroupOf K is trivial. The stability of K is automatic, by TauCeti.smul_mem_sup_zmultiples, so the induced action is stated for that proof of it; any other proof gives the same action by proof irrelevance. No finiteness or torsion assumption is needed.