Invariant submodules of a group representation

def Representation.invtSubmodule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Sublattice (Submodule k V)

Given a representation ρ of a group, ρ.invtSubmodule is the sublattice of all ρ-invariant submodules.

Equations

• ρ.invtSubmodule = ⨅ (g : G), Module.End.invtSubmodule (ρ g)

theorem Representation.mem_invtSubmodule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) {p : Submodule k V} : p ∈ ρ.invtSubmodule ↔ ∀ (g : G), p ∈ Module.End.invtSubmodule (ρ g)

@[simp]

theorem Representation.invtSubmodule.top_mem {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ⊤ ∈ ρ.invtSubmodule

@[simp]

theorem Representation.invtSubmodule.bot_mem {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ⊥ ∈ ρ.invtSubmodule

instance Representation.invtSubmodule.instBoundedOrderSubtypeSubmoduleMemSublattice {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : BoundedOrder ↥ρ.invtSubmodule

Equations

• Representation.invtSubmodule.instBoundedOrderSubtypeSubmoduleMemSublattice ρ = BoundedOrder.mk

@[simp]

theorem Representation.invtSubmodule.coe_top {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ↑⊤ = ⊤

@[simp]

theorem Representation.invtSubmodule.coe_bot {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ↑⊥ = ⊥

theorem Representation.invtSubmodule.nontrivial_iff {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Nontrivial ↥ρ.invtSubmodule ↔ Nontrivial V

instance Representation.invtSubmodule.instNontrivialSubtypeSubmoduleMemSublattice {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) [Nontrivial V] : Nontrivial ↥ρ.invtSubmodule

theorem Representation.asAlgebraHom_mem_of_forall_mem {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (p : Submodule k V) (hp : ∀ (g : G), ∀ v ∈ p, (ρ g) v ∈ p) (v : V) (hv : v ∈ p) (x : MonoidAlgebra k G) : (ρ.asAlgebraHom x) v ∈ p

def Representation.mapSubmodule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ↥ρ.invtSubmodule ≃o Submodule (MonoidAlgebra k G) ρ.asModule

The natural order isomorphism between the two ways to represent invariant submodules.

Equations

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