Transport of complemented submodules #
Topological complementedness is preserved by continuous semilinear equivalences, allowing continuous projections to be transported between different presentations of a module.
theorem
Submodule.ClosedComplemented.map
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Ring R]
[Ring S]
[AddCommGroup M]
[AddCommGroup N]
[TopologicalSpace M]
[TopologicalSpace N]
[Module R M]
[Module S N]
{σ : R →+* S}
{τ : S →+* R}
[RingHomInvPair σ τ]
[RingHomInvPair τ σ]
{p : Submodule R M}
(hp : p.ClosedComplemented)
(e : M ≃SL[σ] N)
:
(Submodule.map (↑↑e) p).ClosedComplemented
A continuous semilinear equivalence carries a complemented submodule to a complemented submodule.
@[simp]
theorem
ContinuousLinearEquiv.closedComplemented_map_iff
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Ring R]
[Ring S]
[AddCommGroup M]
[AddCommGroup N]
[TopologicalSpace M]
[TopologicalSpace N]
[Module R M]
[Module S N]
{σ : R →+* S}
{τ : S →+* R}
[RingHomInvPair σ τ]
[RingHomInvPair τ σ]
(e : M ≃SL[σ] N)
(p : Submodule R M)
:
Complementedness is invariant under a continuous semilinear equivalence.