Documentation

Mathlib.Topology.Algebra.SeparationQuotient.Section

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
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)