# Algebraic operations on `SeparationQuotient` #

In this file we construct a section of the quotient map `E → SeparationQuotient E` as a continuous linear map `SeparationQuotient E →L[K] E`.

source
theorem SeparationQuotient.exists_out_continuousLinearMap (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul K E] :
∃ (f : SeparationQuotient E →L[K] E), (mkCLM K E).comp f = ContinuousLinearMap.id K (SeparationQuotient E)

There exists a continuous `K`-linear map from `SeparationQuotient E` to `E` such that `mk (outCLM x) = x` for all `x`.

Note that continuity of this map comes for free, because `mk` is a topology inducing map.

source
noncomputable def SeparationQuotient.outCLM (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul K E] :
SeparationQuotient E →L[K] E

A continuous `K`-linear map from `SeparationQuotient E` to `E` such that `mk (outCLM x) = x` for all `x`.

Equations

- SeparationQuotient.outCLM K E = ⋯.choose

Instances For

source
@[simp]
theorem SeparationQuotient.mkCLM_comp_outCLM (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul K E] :
(mkCLM K E).comp (outCLM K E) = ContinuousLinearMap.id K (SeparationQuotient E)
source
@[simp]
theorem SeparationQuotient.mk_outCLM (K : Type u_1) {E : Type u_2} [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul K E] (x : SeparationQuotient E) :
mk ((outCLM K E) x) = x
source
@[simp]
theorem SeparationQuotient.mk_comp_outCLM (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul K E] :
mk ∘ ⇑(outCLM K E) = id
source
theorem SeparationQuotient.postcomp_mkCLM_surjective {K : Type u_1} (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul K E] {L : Type u_3} [Semiring L] (σ : L →+* K) (F : Type u_4) [AddCommMonoid F] [Module L F] [TopologicalSpace F] :
Function.Surjective (mkCLM K E).comp
source
theorem SeparationQuotient.isEmbedding_outCLM (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul K E] :
Topology.IsEmbedding ⇑(outCLM K E)

The `SeparationQuotient.outCLM K E` map is a topological embedding.

source
theorem SeparationQuotient.outCLM_injective (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul K E] :
Function.Injective ⇑(outCLM K E)
source
theorem SeparationQuotient.outCLM_isUniformInducing (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul K E] :
IsUniformInducing ⇑(outCLM K E)
source
theorem SeparationQuotient.outCLM_isUniformEmbedding (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul K E] :
IsUniformEmbedding ⇑(outCLM K E)
source
theorem SeparationQuotient.outCLM_uniformContinuous (K : Type u_1) (E : Type u_2) [DivisionRing K] [AddCommGroup E] [Module K E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul K E] :
UniformContinuous ⇑(outCLM K E)