Invariant submodules of a generating set of endomorphisms

A submodule invariant under each endomorphism of a set s is invariant under every element of the subalgebra of Module.End R M that s generates. Over a field a nonzero vector is carried to any other vector by some endomorphism, so when s generates all of Module.End K M the only submodules invariant under s are ⊥ and ⊤.

This is how irreducibility of a representation is read off from the statement that its operators generate the full endomorphism algebra.

Likewise, a common eigenvector of the endomorphisms in s is an eigenvector of every element of the subalgebra they generate.

Main results

• TauCeti.mem_invtSubmodule_of_mem_adjoin: invariance passes to the generated subalgebra.
• TauCeti.exists_smul_eq_of_mem_adjoin: a common eigenvector of s is an eigenvector of every element of the generated subalgebra.
• TauCeti.eq_bot_or_eq_top_of_adjoin_eq_top: over a field, a submodule invariant under a generating set of the endomorphism algebra is ⊥ or ⊤.

theorem TauCeti.mem_invtSubmodule_of_mem_adjoin {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {s : Set (Module.End R M)} {p : Submodule R M} (hp : ∀ f ∈ s, p ∈ f.invtSubmodule) {g : Module.End R M} (hg : g ∈ Algebra.adjoin R s) : p ∈ g.invtSubmodule

A submodule invariant under each endomorphism of a set s is invariant under every element of the subalgebra generated by s.

theorem TauCeti.exists_smul_eq_of_mem_adjoin {R : Type u_1} {K : Type u_2} {V : Type u_3} [CommSemiring R] [CommSemiring K] [Algebra R K] [AddCommMonoid V] [Module K V] [Module R V] [IsScalarTower R K V] {s : Set (Module.End K V)} {v : V} (hs : ∀ T ∈ s, ∃ (c : K), T v = c • v) {T : Module.End K V} (hT : T ∈ Algebra.adjoin R s) : ∃ (c : K), T v = c • v

A vector that is an eigenvector of each endomorphism of a set s is an eigenvector of every element of the R-subalgebra generated by s.

theorem TauCeti.eq_bot_or_eq_top_of_adjoin_eq_top {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] {s : Set (Module.End K M)} (hs : Algebra.adjoin K s = ⊤) {p : Submodule K M} (hp : ∀ f ∈ s, p ∈ f.invtSubmodule) : p = ⊥ ∨ p = ⊤

A submodule invariant under a generating set of the endomorphism algebra is trivial. Over a field, if s generates Module.End K M as an algebra, then the only submodules invariant under every element of s are ⊥ and ⊤.