Submodules invariant under a monoid action

Let a monoid Γ act on an R-module M by R-linear maps, that is by a DistribMulAction Γ M commuting with the scalars. A submodule V is Γ-invariant when γ • x ∈ V for every γ : Γ and x ∈ V. This file provides two constructions around that condition.

• The invariant core V.invariantCore Γ = ⨅ γ, V.comap (γ • ·) of a submodule V: the set of x with γ • x ∈ V for every γ. It is the largest Γ-invariant submodule contained in V, in the same way as Subgroup.normalCore is the largest normal subgroup contained in a subgroup, and it is monotone in V.
• The induced action on the quotient by a Γ-invariant submodule V: each γ descends to an R-linear endomorphism of M ⧸ V, and together they form a monoid homomorphism Submodule.quotientToModuleEnd hV : Γ →* Module.End R (M ⧸ V), the quotient analogue of DistribMulAction.toModuleEnd. Its kernel consists of the γ with γ • x - x ∈ V for all x, it grows with V, and the action is compatible with the factor maps M ⧸ V → M ⧸ V'.

For a compact monoid acting continuously on a topological module the invariant cores of the open submodules are open. If the module is linearly topologized, the invariant open submodules therefore form a basis of neighbourhoods of zero; that is where the invariant core is used.

Main definitions

• Submodule.invariantCore: the largest Γ-invariant submodule contained in a given one.
• Submodule.quotientToModuleEnd: the action of Γ on the quotient by an invariant submodule.

Main results

• Submodule.mem_invariantCore, Submodule.invariantCore_le, Submodule.smul_mem_invariantCore, Submodule.le_invariantCore_iff, Submodule.invariantCore_mono, Submodule.invariantCore_eq_self_iff: the characteristic properties of the invariant core.
• Submodule.quotientToModuleEnd_mk, Submodule.mem_mker_quotientToModuleEnd, Submodule.mker_quotientToModuleEnd_mono, Submodule.factor_quotientToModuleEnd: the induced action on classes, its kernel, and its compatibility with the factor maps.

def Submodule.invariantCore (Γ : Type u_1) {R : Type u_2} {M : Type u_3} [Monoid Γ] [Semiring R] [AddCommMonoid M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] (V : Submodule R M) : Submodule R M

The invariant core of a submodule V under the action of a monoid Γ: the elements x with γ • x ∈ V for every γ : Γ. It is the largest Γ-invariant submodule contained in V (Submodule.invariantCore_le, Submodule.smul_mem_invariantCore, Submodule.le_invariantCore_iff).

Equations

• Submodule.invariantCore Γ V = ⨅ (γ : Γ), Submodule.comap (DistribSMul.toLinearMap R M γ) V

@[simp]

theorem Submodule.mem_invariantCore {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid Γ] [Semiring R] [AddCommMonoid M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} {x : M} : x ∈ invariantCore Γ V ↔ ∀ (γ : Γ), γ • x ∈ V

An element belongs to the invariant core exactly when its entire orbit lies in V.

theorem Submodule.invariantCore_le (Γ : Type u_1) {R : Type u_2} {M : Type u_3} [Monoid Γ] [Semiring R] [AddCommMonoid M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] (V : Submodule R M) : invariantCore Γ V ≤ V

The invariant core is contained in the original submodule.

theorem Submodule.smul_mem_invariantCore {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid Γ] [Semiring R] [AddCommMonoid M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} (γ : Γ) {x : M} (hx : x ∈ invariantCore Γ V) : γ • x ∈ invariantCore Γ V

The invariant core is preserved by the action of Γ.

theorem Submodule.le_invariantCore_iff {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid Γ] [Semiring R] [AddCommMonoid M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V W : Submodule R M} : W ≤ invariantCore Γ V ↔ ∀ (γ : Γ), ∀ x ∈ W, γ • x ∈ V

A submodule lies in the invariant core of V exactly when every translate lies in V.

theorem Submodule.invariantCore_mono {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid Γ] [Semiring R] [AddCommMonoid M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] : Monotone (invariantCore Γ)

Taking invariant cores preserves inclusions of submodules.

theorem Submodule.invariantCore_eq_self_iff {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid Γ] [Semiring R] [AddCommMonoid M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} : invariantCore Γ V = V ↔ ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V

A submodule equals its invariant core exactly when it is preserved by the action.

def Submodule.quotientToModuleEnd {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid Γ] [Ring R] [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) : Γ →* Module.End R (M ⧸ V)

The action of Γ on the quotient M ⧸ V by a Γ-invariant submodule V, as a monoid homomorphism into the R-linear endomorphisms of the quotient: γ sends the class of x to the class of γ • x (Submodule.quotientToModuleEnd_mk). This is the quotient analogue of DistribMulAction.toModuleEnd.

Equations

• Submodule.quotientToModuleEnd hV = { toFun := fun (γ : Γ) => V.mapQ V (DistribSMul.toLinearMap R M γ) ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Submodule.quotientToModuleEnd_mk {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid Γ] [Ring R] [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (γ : Γ) (x : M) : ((quotientToModuleEnd hV) γ) (Quotient.mk x) = Quotient.mk (γ • x)

The induced action sends the class of x to the class of γ • x.

theorem Submodule.mem_mker_quotientToModuleEnd {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid Γ] [Ring R] [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) {γ : Γ} : γ ∈ MonoidHom.mker (quotientToModuleEnd hV) ↔ ∀ (x : M), γ • x - x ∈ V

An element acts trivially on the quotient exactly when it moves every x by an element of V. The kernel is a submonoid, so no inverses in Γ are needed.

theorem Submodule.mker_quotientToModuleEnd_mono {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid Γ] [Ring R] [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V V' : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (hV' : ∀ (γ : Γ), ∀ x ∈ V', γ • x ∈ V') (h : V ≤ V') : MonoidHom.mker (quotientToModuleEnd hV) ≤ MonoidHom.mker (quotientToModuleEnd hV')

The kernel of the induced action grows with the submodule.

theorem Submodule.factor_quotientToModuleEnd {Γ : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid Γ] [Ring R] [AddCommGroup M] [Module R M] [DistribMulAction Γ M] [SMulCommClass Γ R M] {V V' : Submodule R M} (hV : ∀ (γ : Γ), ∀ x ∈ V, γ • x ∈ V) (hV' : ∀ (γ : Γ), ∀ x ∈ V', γ • x ∈ V') (h : V ≤ V') (γ : Γ) (y : M ⧸ V) : (factor h) (((quotientToModuleEnd hV) γ) y) = ((quotientToModuleEnd hV') γ) ((factor h) y)

The induced actions on M ⧸ V and M ⧸ V', for invariant V ≤ V', are compatible with the factor map M ⧸ V → M ⧸ V'.