Invariant submodules

In this file, we define and prove some basic results on invariant submodules.

def Submodule.InvariantUnder {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (U : Submodule R E) (T : E →ₗ[R] E) : Prop

U is T invariant (ver 1): U ≤ U.comap

Equations

• U.InvariantUnder T = (U ≤ Submodule.comap T U)

@[simp]

theorem Submodule.invariantUnder_iff_map {E : Type u_2} {R : Type u_1} [Ring R] [AddCommGroup E] [Module R E] (U : Submodule R E) (T : E →ₗ[R] E) : U.InvariantUnder T ↔ map T U ≤ U

U is T invariant if and only if U.map T ≤ U

theorem Submodule.invariantUnder_iff_mapsTo {E : Type u_2} {R : Type u_1} [Ring R] [AddCommGroup E] [Module R E] (U : Submodule R E) (T : E →ₗ[R] E) : Set.MapsTo ⇑T ↑U ↑U ↔ U.InvariantUnder T

U is T invariant if and only if set.maps_to T U U

theorem Submodule.invariantUnder_iff {E : Type u_2} {R : Type u_1} [Ring R] [AddCommGroup E] [Module R E] (U : Submodule R E) (T : E →ₗ[R] E) : U.InvariantUnder T ↔ ⇑T '' ↑U ⊆ ↑U

U is T invariant is equivalent to saying T(U) ⊆ U

theorem Submodule.linearProjOfIsCompl_eq_self_iff {E : Type u_2} {R : Type u_1} [Ring R] [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) : ↑((p.linearProjOfIsCompl q hpq) x) = x ↔ x ∈ p

projection to p along q of x equals x if and only if x ∈ p

theorem Submodule.InvariantUnder.linear_proj_comp_self_eq {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (U V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) (h : U.InvariantUnder T) (x : ↥U) : ↑((U.linearProjOfIsCompl V hUV) (T ↑x)) = T ↑x

theorem Submodule.invariantUnderOfLinearProjCompSelfEq {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (U V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) (h : ∀ (x : ↥U), ↑((U.linearProjOfIsCompl V hUV) (T ↑x)) = T ↑x) : U.InvariantUnder T

theorem Submodule.invariantUnder_iff_linear_proj_comp_self_eq {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (U V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) : U.InvariantUnder T ↔ ∀ (x : ↥U), ↑((U.linearProjOfIsCompl V hUV) (T ↑x)) = T ↑x

U is invariant under T if and only if pᵤ ∘ₗ T = T, where pᵤ denotes the linear projection to U along V

theorem Submodule.linearProjOfIsCompl_eq_self_sub_linear_proj {E : Type u_2} {R : Type u_1} [Ring R] [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) (x : E) : ↑((q.linearProjOfIsCompl p ⋯) x) = x - ↑((p.linearProjOfIsCompl q hpq) x)

theorem Submodule.invariant_under'_iff_linear_proj_comp_self_comp_linear_proj_eq {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (U V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) : V.InvariantUnder T ↔ ∀ (x : E), ↑((U.linearProjOfIsCompl V hUV) (T ↑((U.linearProjOfIsCompl V hUV) x))) = ↑((U.linearProjOfIsCompl V hUV) (T x))

V is invariant under T if and only if pᵤ ∘ₗ (T ∘ₗ pᵤ) = pᵤ ∘ₗ T, where pᵤ denotes the linear projection to U along V

theorem Submodule.isCompl_invariantUnder_iff_linear_proj_and_self_commute {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (U V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) : U.InvariantUnder T ∧ V.InvariantUnder T ↔ Commute (U.subtype ∘ₗ U.linearProjOfIsCompl V hUV) T

both U and V are invariant under T if and only if T commutes with pᵤ, where pᵤ denotes the linear projection to U along V

theorem Submodule.invariantUnder_symm_iff_le_map {E : Type u_2} {R : Type u_1} [Ring R] [AddCommGroup E] [Module R E] (U : Submodule R E) (T : E ≃ₗ[R] E) : U.InvariantUnder ↑T.symm ↔ U ≤ map T U

U is invariant under T.symm if and only if U ⊆ T(U)

theorem Submodule.commutes_with_linear_proj_iff_linear_proj_eq {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (U V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) [Invertible T] : Commute (U.subtype ∘ₗ U.linearProjOfIsCompl V hUV) T ↔ ⅟T ∘ₗ (U.subtype ∘ₗ U.linearProjOfIsCompl V hUV) ∘ₗ T = U.subtype ∘ₗ U.linearProjOfIsCompl V hUV

theorem Submodule.invariantUnder_inv_iff_U_subset_image {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (U : Submodule R E) (T : E →ₗ[R] E) [Invertible T] : U.InvariantUnder ⅟T ↔ ↑U ⊆ ⇑T '' ↑U

theorem Submodule.inv_linear_proj_comp_map_eq_linear_proj_iff_images_eq {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (U V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) [Invertible T] : ⅟T ∘ₗ (U.subtype ∘ₗ U.linearProjOfIsCompl V hUV) ∘ₗ T = U.subtype ∘ₗ U.linearProjOfIsCompl V hUV ↔ ⇑T '' ↑U = ↑U ∧ ⇑T '' ↑V = ↑V

theorem StarAlgebra.centralizer_prod {M : Type u_1} [AddCommGroup M] [Module ℂ M] [StarRing (M →ₗ[ℂ] M)] [StarModule ℂ (M →ₗ[ℂ] M)] (A B : StarSubalgebra ℂ (M →ₗ[ℂ] M)) : (A.carrier ×ˢ B.carrier).centralizer = A.carrier.centralizer ×ˢ B.carrier.centralizer