Continuous linear maps and quotient topological modules

In this file, we collect various continuous linear maps associated to quotient spaces.

Main definitions

• Submodule.mkQL S is the quotient map M →L[R] M ⧸ S. In other words, it is Submodule.mkQ S bundled as a ContinuousLinearMap.
• Submodule.liftQL S f h is the map M ⧸ S →SL[σ] N given by f : M →SL[σ] N and a proof h : S ≤ f.ker that f vanishes on S. In other words, it is Submodule.liftQ S f h bundled as a ContinuousLinearMap.

TODO

• Define Submodule.mapQL, the continuous linear bundling of Submodule.mapQ.

def Submodule.mkQL {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] (S : Submodule R M) : M →L[R] M ⧸ S

Submodule.mkQ as a ContinuousLinearMap.

Equations

• S.mkQL = { toLinearMap := S.mkQ, cont := ⋯ }

@[simp]

theorem Submodule.toLinearMap_mkQL {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] (S : Submodule R M) : ↑S.mkQL = S.mkQ

@[simp]

theorem Submodule.coe_mkQL {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] (S : Submodule R M) : ⇑S.mkQL = ⇑S.mkQ

theorem Submodule.mkQL_apply {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] (S : Submodule R M) (x : M) : S.mkQL x = S.mkQ x

theorem Submodule.isQuotientMap_mkQL {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] (S : Submodule R M) : Topology.IsQuotientMap ⇑S.mkQL

theorem Submodule.isOpenQuotientMap_mkQL {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] (S : Submodule R M) [ContinuousAdd M] : IsOpenQuotientMap ⇑S.mkQL

def Submodule.liftQL {R : Type u_1} {R₂ : Type u_2} [Ring R] [Ring R₂] {σ : R →+* R₂} {M : Type u_3} {M₂ : Type u_4} [TopologicalSpace M] [AddCommGroup M] [Module R M] [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] (S : Submodule R M) (f : M →SL[σ] M₂) (h : S ≤ (↑f).ker) : M ⧸ S →SL[σ] M₂

Submodule.liftQ as a ContinuousLinearMap.

Equations

• S.liftQL f h = { toLinearMap := S.liftQ (↑f) h, cont := ⋯ }

@[simp]

theorem Submodule.toLinearMap_liftQL {R : Type u_1} {R₂ : Type u_2} [Ring R] [Ring R₂] {σ : R →+* R₂} {M : Type u_3} {M₂ : Type u_4} [TopologicalSpace M] [AddCommGroup M] [Module R M] [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] (S : Submodule R M) (f : M →SL[σ] M₂) (h : S ≤ (↑f).ker) : ↑(S.liftQL f h) = S.liftQ (↑f) h

@[simp]

theorem Submodule.coe_liftQL {R : Type u_1} {R₂ : Type u_2} [Ring R] [Ring R₂] {σ : R →+* R₂} {M : Type u_3} {M₂ : Type u_4} [TopologicalSpace M] [AddCommGroup M] [Module R M] [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] (S : Submodule R M) (f : M →SL[σ] M₂) (h : S ≤ (↑f).ker) : ⇑(S.liftQL f h) = ⇑(S.liftQ (↑f) h)

theorem Submodule.liftQL_apply {R : Type u_1} {R₂ : Type u_2} [Ring R] [Ring R₂] {σ : R →+* R₂} {M : Type u_3} {M₂ : Type u_4} [TopologicalSpace M] [AddCommGroup M] [Module R M] [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] (S : Submodule R M) (f : M →SL[σ] M₂) (h : S ≤ (↑f).ker) (x : M ⧸ S) : (S.liftQL f h) x = (S.liftQ (↑f) h) x