Invariant submodules #
In this file, we define and prove some basic results on invariant submodules.
def
submodule.invariant_under
{E : Type u_1}
{R : Type u_2}
[ring R]
[add_comm_group E]
[module R E]
(U : submodule R E)
(T : E →ₗ[R] E) :
Prop
U is T invariant (ver 1): U ≤ U.comap
Equations
- U.invariant_under T = (U ≤ submodule.comap T U)
@[simp]
theorem
submodule.invariant_under_iff_map
{E : Type u_1}
{R : Type u_2}
[ring R]
[add_comm_group E]
[module R E]
(U : submodule R E)
(T : E →ₗ[R] E) :
U.invariant_under T ↔ submodule.map T U ≤ U
U is T invariant if and only if U.map T ≤ U
theorem
submodule.invariant_under_iff_maps_to
{E : Type u_1}
{R : Type u_2}
[ring R]
[add_comm_group E]
[module R E]
(U : submodule R E)
(T : E →ₗ[R] E) :
set.maps_to ⇑T ↑U ↑U ↔ U.invariant_under T
U is T invariant if and only if set.maps_to T U U
theorem
submodule.linear_proj_of_is_compl_eq_self_iff
{E : Type u_1}
{R : Type u_2}
[ring R]
[add_comm_group E]
[module R E]
{p q : submodule R E}
(hpq : is_compl p q)
(x : E) :
projection to p along q of x equals x if and only if x ∈ p
theorem
submodule.invariant_under_iff_linear_proj_comp_self_eq
{E : Type u_1}
{R : Type u_2}
[ring R]
[add_comm_group E]
[module R E]
(U V : submodule R E)
(hUV : is_compl U V)
(T : E →ₗ[R] E) :
U is invariant under T if and only if pᵤ ∘ₗ T = T,
where pᵤ denotes the linear projection to U along V
theorem
submodule.linear_proj_of_is_compl_eq_self_sub_linear_proj
{E : Type u_1}
{R : Type u_2}
[ring R]
[add_comm_group E]
[module R E]
{p q : submodule R E}
(hpq : is_compl p q)
(x : E) :
↑(⇑(q.linear_proj_of_is_compl p _) x) = x - ↑(⇑(p.linear_proj_of_is_compl 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]
[add_comm_group E]
[module R E]
(U V : submodule R E)
(hUV : is_compl U V)
(T : E →ₗ[R] E) :
V.invariant_under T ↔ ∀ (x : E), ↑(⇑(U.linear_proj_of_is_compl V hUV) (⇑T ↑(⇑(U.linear_proj_of_is_compl V hUV) x))) = ↑(⇑(U.linear_proj_of_is_compl 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.is_compl_invariant_under_iff_linear_proj_and_self_commute
{E : Type u_1}
{R : Type u_2}
[ring R]
[add_comm_group E]
[module R E]
(U V : submodule R E)
(hUV : is_compl U V)
(T : E →ₗ[R] E) :
U.invariant_under T ∧ V.invariant_under T ↔ commute (U.subtype.comp (U.linear_proj_of_is_compl 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.invariant_under_symm_iff_le_map
{E : Type u_1}
{R : Type u_2}
[ring R]
[add_comm_group E]
[module R E]
(U : submodule R E)
(T : E ≃ₗ[R] E) :
U.invariant_under ↑(T.symm) ↔ U ≤ submodule.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]
[add_comm_group E]
[module R E]
(U V : submodule R E)
(hUV : is_compl U V)
(T : E →ₗ[R] E)
[invertible T] :
commute (U.subtype.comp (U.linear_proj_of_is_compl V hUV)) T ↔ (⅟ T).comp ((U.subtype.comp (U.linear_proj_of_is_compl V hUV)).comp T) = U.subtype.comp (U.linear_proj_of_is_compl V hUV)
theorem
submodule.invariant_under_inv_iff_U_subset_image
{E : Type u_1}
{R : Type u_2}
[ring R]
[add_comm_group E]
[module R E]
(U : submodule R E)
(T : E →ₗ[R] E)
[invertible T] :
theorem
submodule.inv_linear_proj_comp_map_eq_linear_proj_iff_images_eq
{E : Type u_1}
{R : Type u_2}
[ring R]
[add_comm_group E]
[module R E]
(U V : submodule R E)
(hUV : is_compl U V)
(T : E →ₗ[R] E)
[invertible T] :
theorem
star_algebra.centralizer_prod
{M : Type u_1}
[add_comm_group M]
[module ℂ M]
[star_ring (M →ₗ[ℂ] M)]
[star_module ℂ (M →ₗ[ℂ] M)]
(A B : star_subalgebra ℂ (M →ₗ[ℂ] M)) :
(A.carrier ×ˢ B.carrier).centralizer = A.carrier.centralizer ×ˢ B.carrier.centralizer