Theorems · Definition · functional analysis

ContinuousLinearEquiv.ofSubmodules

{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) →
                                    (q : Submodule R₂ M₂) → Submodule.map (↑↑e) p = q → ↥p ≃SL[σ₁₂] ↥q

A continuous linear equivalence which maps a submodule of one module onto another, restricts to a continuous linear equivalence of the two submodules. This is LinearEquiv.ofSubmodules as a continuous linear equivalence.

Defined in

Mathlib.Topology.Algebra.Module.Equiv

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringSemiringAddCommMonoidTopologicalSpaceAddCommMonoidTopologicalSpace