Documentation

Monlib.LinearAlgebra.InvariantSubmodule

Invariant submodules #

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

source
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
Instances For
    source
    @[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 ↔ Submodule.map T U ≤ U

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

    source
    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

    source
    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

    source
    theorem Submodule.linearProjOfIsCompl_eq_self_iff {E : Type u_2} {R : Type u_1} [Ring R] [AddCommGroup E] [Module R E] {p : Submodule R E} {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

    source
    theorem Submodule.InvariantUnder.linear_proj_comp_self_eq {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (U : Submodule R E) (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
    source
    theorem Submodule.invariantUnderOfLinearProjCompSelfEq {E : Type u_1} {R : Type u_2} [Ring R] [AddCommGroup E] [Module R E] (U : Submodule R E) (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
    source
    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 : Submodule R E) (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

    source
    theorem Submodule.linearProjOfIsCompl_eq_self_sub_linear_proj {E : Type u_2} {R : Type u_1} [Ring R] [AddCommGroup E] [Module R E] {p : Submodule R E} {q : Submodule R E} (hpq : IsCompl p q) (x : E) :
    ↑((q.linearProjOfIsCompl p ⋯) x) = x - ↑((p.linearProjOfIsCompl q hpq) x)
    source
    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 : Submodule R E) (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

    source
    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 : Submodule R E) (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

    source
    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 ≤ Submodule.map T U

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

    source
    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 : Submodule R E) (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
    source
    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
    source
    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 : Submodule R E) (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
    source
    theorem StarAlgebra.centralizer_prod {M : Type u_1} [AddCommGroup M] [Module ℂ M] [StarRing (M →ₗ[ℂ] M)] [StarModule ℂ (M →ₗ[ℂ] M)] (A : StarSubalgebra ℂ (M →ₗ[ℂ] M)) (B : StarSubalgebra ℂ (M →ₗ[ℂ] M)) :
    (A.carrier ×ˢ B.carrier).centralizer = A.carrier.centralizer ×ˢ B.carrier.centralizer