Documentation

LeanPool.Monlib4.LinearAlgebra.InvariantSubmodule

Invariant submodules #

This file defines and proves 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: U ≤ U.comap T.

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 ↔ 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.MapsTo 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 q : Submodule R E} (hpq : IsCompl p q) (x : E) :
    ↑((p.projectionOnto 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 V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) (h : U.InvariantUnder T) (x : ↥U) :
    ↑((U.projectionOnto 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 V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) (h : ∀ (x : ↥U), ↑((U.projectionOnto 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 V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) :
    U.InvariantUnder T ↔ ∀ (x : ↥U), ↑((U.projectionOnto V hUV) (T ↑x)) = T ↑x

    U is invariant under T iff pᵤ ∘ₗ T = T on U.

    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 q : Submodule R E} (hpq : IsCompl p q) (x : E) :
    ↑((q.projectionOnto p ⋯) x) = x - ↑((p.projectionOnto q hpq) x)
    source
    theorem Submodule.linear_proj_add_linearProjOfIsCompl_eq_self {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.projectionOnto q hpq) x) + ↑((q.projectionOnto p ⋯) x) = x
    source
    theorem Submodule.linearProjOfIsCompl_idempotent {E : Type u_2} {R : Type u_1} [Ring R] [AddCommGroup E] [Module R E] {p q : Submodule R E} (hpq : IsCompl p q) :
    p.subtype ∘ₗ p.projectionOnto q hpq * p.subtype ∘ₗ p.projectionOnto q hpq = p.subtype ∘ₗ p.projectionOnto q hpq
    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 V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) :
    V.InvariantUnder T ↔ ∀ (x : E), ↑((U.projectionOnto V hUV) (T ↑((U.projectionOnto V hUV) x))) = ↑((U.projectionOnto V hUV) (T x))

    V is invariant under T iff pᵤ ∘ₗ (T ∘ₗ pᵤ) = pᵤ ∘ₗ T.

    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 V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) :
    U.InvariantUnder T ∧ V.InvariantUnder T ↔ Commute (U.subtype ∘ₗ U.projectionOnto V hUV) T

    Both U and V are invariant under T iff T commutes with pᵤ.

    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 ≤ map (↑T) U

    U is invariant under T.symm iff 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 V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) [Invertible T] :
    Commute (U.subtype ∘ₗ U.projectionOnto V hUV) T ↔ ⅟T ∘ₗ (U.subtype ∘ₗ U.projectionOnto V hUV) ∘ₗ T = U.subtype ∘ₗ U.projectionOnto 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 V : Submodule R E) (hUV : IsCompl U V) (T : E →ₗ[R] E) [Invertible T] :
    ⅟T ∘ₗ (U.subtype ∘ₗ U.projectionOnto V hUV) ∘ₗ T = U.subtype ∘ₗ U.projectionOnto 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 B : StarSubalgebra ℂ (M →ₗ[ℂ] M)) :
    (A.carrier ×ˢ B.carrier).centralizer = A.carrier.centralizer ×ˢ B.carrier.centralizer