English
For a representation ρ of a group on a k-module V, the invariant submodules form a sublattice of Submodules(V) given by the infimum over all g of the invariant submodules for ρ(g). In other words, a submodule P is invariant under ρ iff it is invariant under every ρ(g).
Русский
Для представления ρ группы над модулем V над полем k множество инвариантных подпольных образует подпредложение подпонят Submodule(V), равное пересечению инвариантных подмодулей End(ρ(g)) по всем g ∈ G; то есть p инвариантно относительно ρ(g) для каждого g.
LaTeX
$$$\\operatorname{invtSubmodule}(\\rho) = \\bigwedge_{g \\in G} \\operatorname{Module.End}.\\invtSubmodule(\\rho(g)).$$$
Lean4
/-- Given a representation `ρ` of a group, `ρ.invtSubmodule` is the sublattice of all
`ρ`-invariant submodules. -/
def invtSubmodule : Sublattice (Submodule k V) :=
⨅ g, Module.End.invtSubmodule (ρ g)
