Continuous linear equivalences involving submodules

Main Definitions

• ofEq: LinearEquiv.ofEq as a continuous linear equivalence.
• submoduleMap: LinearEquiv.submoduleMap as a continuous linear equivalence.
• ofSubmodules: LinearEquiv.ofSubmodules as a continuous linear equivalence.
• ofSubmodule': ofSubmodule but with comap on the left instead of map on the right.
• Submodule.topContEquiv: Submodule.topEquiv as a continuous linear equivalence.

def ContinuousLinearEquiv.ofEq {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] (p q : Submodule R M) (h : p = q) : ↥p ≃L[R] ↥q

Continuous linear equivalence between two equal submodules: this is LinearEquiv.ofEq as a continuous linear equivalence

Equations

• ContinuousLinearEquiv.ofEq p q h = { toLinearEquiv := LinearEquiv.ofEq p q h, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousLinearEquiv.submoduleMap {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {R₂ : Type u_3} {M₂ : Type u_4} [Semiring R₂] [AddCommMonoid M₂] [TopologicalSpace 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.

Equations

• e.submoduleMap p = { toLinearEquiv := (↑e).submoduleMap p, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.submoduleMap_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {R₂ : Type u_3} {M₂ : Type u_4} [Semiring R₂] [AddCommMonoid M₂] [TopologicalSpace M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃SL[σ₁₂] M₂) (p : Submodule R M) (x : ↥p) : ↑((e.submoduleMap p) x) = e ↑x

@[simp]

theorem ContinuousLinearEquiv.submoduleMap_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {R₂ : Type u_3} {M₂ : Type u_4} [Semiring R₂] [AddCommMonoid M₂] [TopologicalSpace M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃SL[σ₁₂] M₂) (p : Submodule R M) (x : ↥(Submodule.map (↑↑e) p)) : ↑((e.submoduleMap p).symm x) = e.symm ↑x

def ContinuousLinearEquiv.ofSubmodules {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {R₂ : Type u_3} {M₂ : Type u_4} [Semiring R₂] [AddCommMonoid M₂] [TopologicalSpace M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃SL[σ₁₂] M₂) (p : Submodule R M) (q : Submodule R₂ M₂) (h : 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.

Equations

• e.ofSubmodules p q h = (e.submoduleMap p).trans (ContinuousLinearEquiv.ofEq (Submodule.map (↑↑e) p) q h)

@[simp]

theorem ContinuousLinearEquiv.ofSubmodules_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {R₂ : Type u_3} {M₂ : Type u_4} [Semiring R₂] [AddCommMonoid M₂] [TopologicalSpace M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃SL[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂} (h : Submodule.map (↑↑e) p = q) (x : ↥p) : ↑((e.ofSubmodules p q h) x) = e ↑x

@[simp]

theorem ContinuousLinearEquiv.ofSubmodules_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {R₂ : Type u_3} {M₂ : Type u_4} [Semiring R₂] [AddCommMonoid M₂] [TopologicalSpace M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃SL[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂} (h : Submodule.map (↑↑e) p = q) (x : ↥q) : ↑((e.ofSubmodules p q h).symm x) = e.symm ↑x

def ContinuousLinearEquiv.ofSubmodule' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {R₂ : Type u_3} {M₂ : Type u_4} [Semiring R₂] [AddCommMonoid M₂] [TopologicalSpace M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M ≃SL[σ₁₂] M₂) (U : Submodule R₂ M₂) : ↥(Submodule.comap (↑↑f) U) ≃SL[σ₁₂] ↥U

A continuous linear equivalence of two modules restricts to a continuous linear equivalence from the preimage of any submodule to that submodule. This is ContinuousLinearEquiv.ofSubmodule but with comap on the left instead of map on the right.

Equations

• f.ofSubmodule' U = (f.symm.ofSubmodules U (Submodule.comap (↑(↑f).symm.symm) U) ⋯).symm

theorem ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {R₂ : Type u_3} {M₂ : Type u_4} [Semiring R₂] [AddCommMonoid M₂] [TopologicalSpace M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M ≃SL[σ₁₂] M₂) (U : Submodule R₂ M₂) : ↑(f.ofSubmodule' U) = (↑f ∘SL (Submodule.comap (↑↑f) U).subtypeL).codRestrict U ⋯

@[simp]

theorem ContinuousLinearEquiv.ofSubmodule'_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {R₂ : Type u_3} {M₂ : Type u_4} [Semiring R₂] [AddCommMonoid M₂] [TopologicalSpace M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M ≃SL[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : ↥(Submodule.comap (↑↑f) U)) : ↑((f.ofSubmodule' U) x) = f ↑x

@[simp]

theorem ContinuousLinearEquiv.ofSubmodule'_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] {R₂ : Type u_3} {M₂ : Type u_4} [Semiring R₂] [AddCommMonoid M₂] [TopologicalSpace M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M ≃SL[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : ↥U) : ↑((f.ofSubmodule' U).symm x) = f.symm ↑x

@[reducible, inline]

abbrev Submodule.topContEquiv {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] : ↥⊤ ≃L[R] M

The top submodule is continuous linearly equivalent to the module. This is the continuous version of Submodule.topEquiv.

Equations

• Submodule.topContEquiv = { toLinearEquiv := Submodule.topEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }