Theorems · Definition · functional analysis

ContinuousLinearEquiv.submoduleMap

{R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_3} →
      {M₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid M₂] →
                  [inst_5 : TopologicalSpace M₂] →
                    {module_M : Module R M} →
                      {module_M₂ : Module R₂ M₂} →
                        {σ₁₂ : R →+* R₂} →
                          {σ₂₁ : R₂ →+* R} →
                            {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                              {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                                (e : M ≃SL[σ₁₂] M₂) → (p : Submodule R M) → ↥p ≃SL[σ₁₂] ↥(Submodule.map (↑↑e) p)

A continuous linear equivalence of two modules restricts to a continuous linear equivalence from any submodule p of the domain onto the image of that submodule. This is the continuous linear version of LinearEquiv.submoduleMap. This is ContinuousLinearEquiv.ofSubmodule' but with map on the right instead of comap on the left.

Defined in

Mathlib.Topology.Algebra.Module.Equiv

Cited by

2 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringSemiringAddCommMonoidTopologicalSpaceAddCommMonoidTopologicalSpace