Mathlib.Topology.Algebra.SeparationQuotient.Section

SeparationQuotient.exists_out_continuousLinearMap theorem

: ∃ f : SeparationQuotient E →L[K] E, mkCLM K E ∘L f = .id K (SeparationQuotient E)

Full source

/-- 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.
-/
theorem exists_out_continuousLinearMap :
    ∃ f : SeparationQuotient E →L[K] E, mkCLM K E ∘L f = .id K (SeparationQuotient E) := by
  rcases (mkCLM K E).toLinearMap.exists_rightInverse_of_surjective
    (LinearMap.range_eq_top.mpr surjective_mk) with ⟨f, hf⟩
  replace hf : mkmk ∘ f = id := congr_arg DFunLike.coe hf
  exact ⟨⟨f, isInducing_mk.continuous_iff.2 (by continuity)⟩, DFunLike.ext' hf⟩

Existence of Continuous Linear Section for Separation Quotient

Informal description

There exists a continuous $K$-linear map $f \colon \operatorname{SeparationQuotient} E \to E$ such that the composition of the quotient map $\operatorname{mkCLM}_K E$ with $f$ is the identity map on $\operatorname{SeparationQuotient} E$, i.e., $\operatorname{mkCLM}_K E \circ f = \operatorname{id}_K (\operatorname{SeparationQuotient} E)$.

SeparationQuotient.outCLM definition

: SeparationQuotient E →L[K] E

Full source

/-- A continuous `K`-linear map from `SeparationQuotient E` to `E`
such that `mk (outCLM x) = x` for all `x`. -/
noncomputable def outCLM : SeparationQuotientSeparationQuotient E →L[K] E :=
  (exists_out_continuousLinearMap K E).choose

Continuous linear section of the separation quotient

Informal description

A continuous $K$-linear map from the separation quotient of $E$ to $E$ such that composing it with the quotient map gives the identity map on the separation quotient. In other words, for any $x$ in the separation quotient, applying the quotient map to the output of this function at $x$ returns $x$ itself.

SeparationQuotient.mkCLM_comp_outCLM theorem

: mkCLM K E ∘L outCLM K E = .id K (SeparationQuotient E)

Full source

@[simp]
theorem mkCLM_comp_outCLM : mkCLMmkCLM K E ∘L outCLM K E = .id K (SeparationQuotient E) :=
  (exists_out_continuousLinearMap K E).choose_spec

Composition of Quotient Map and Section Yields Identity on Separation Quotient

Informal description

The composition of the continuous linear quotient map $\operatorname{mkCLM}_K E$ with the continuous linear section $\operatorname{outCLM}_K E$ equals the identity map on the separation quotient of $E$, i.e., $\operatorname{mkCLM}_K E \circ \operatorname{outCLM}_K E = \operatorname{id}_{\operatorname{SeparationQuotient} E}$.

SeparationQuotient.mk_outCLM theorem

(x : SeparationQuotient E) : mk (outCLM K E x) = x

Full source

@[simp]
theorem mk_outCLM (x : SeparationQuotient E) : mk (outCLM K E x) = x :=
  DFunLike.congr_fun (mkCLM_comp_outCLM K E) x

Section Property of the Separation Quotient: $\operatorname{mk} \circ \operatorname{outCLM}_K E = \operatorname{id}$

Informal description

For any element $x$ in the separation quotient of a topological vector space $E$ over a field $K$, the projection map $\operatorname{mk}$ applied to the continuous linear section $\operatorname{outCLM}_K E$ evaluated at $x$ equals $x$ itself, i.e., $\operatorname{mk}(\operatorname{outCLM}_K E(x)) = x$.

SeparationQuotient.mk_comp_outCLM theorem

: mk ∘ outCLM K E = id

Full source

@[simp]
theorem mk_comp_outCLM : mkmk ∘ outCLM K E = id := funext (mk_outCLM K)

Identity Property of Separation Quotient Section: $\operatorname{mk} \circ \operatorname{outCLM}_K E = \operatorname{id}$

Informal description

The composition of the quotient map $\operatorname{mk} \colon E \to \operatorname{SeparationQuotient} E$ with the continuous linear section $\operatorname{outCLM}_K E \colon \operatorname{SeparationQuotient} E \to E$ equals the identity map on the separation quotient, i.e., $\operatorname{mk} \circ \operatorname{outCLM}_K E = \operatorname{id}$.

SeparationQuotient.postcomp_mkCLM_surjective theorem

 {L : Type*} [Semiring L] (σ : L →+* K) (F : Type*) [AddCommMonoid F] [Module L F] [TopologicalSpace F] :
  Function.Surjective ((mkCLM K E).comp : (F →SL[σ] E) → (F →SL[σ] SeparationQuotient E))

Full source

theorem postcomp_mkCLM_surjective {L : Type*} [Semiring L] (σ : L →+* K)
    (F : Type*) [AddCommMonoid F] [Module L F] [TopologicalSpace F] :
    Function.Surjective ((mkCLM K E).comp : (F →SL[σ] E) → (F →SL[σ] SeparationQuotient E)) := by
  intro f
  use (outCLM K E).comp f
  rw [← ContinuousLinearMap.comp_assoc, mkCLM_comp_outCLM, ContinuousLinearMap.id_comp]

Surjectivity of Postcomposition with Separation Quotient Map

Informal description

Let $L$ be a semiring, $\sigma : L \to K$ a ring homomorphism, and $F$ a topological module over $L$. Then the postcomposition map $(f \mapsto \operatorname{mkCLM}_K E \circ f)$ from continuous $\sigma$-linear maps $F \to E$ to continuous $\sigma$-linear maps $F \to \operatorname{SeparationQuotient} E$ is surjective.

SeparationQuotient.isEmbedding_outCLM theorem

: IsEmbedding (outCLM K E)

Full source

/-- The `SeparationQuotient.outCLM K E` map is a topological embedding. -/
theorem isEmbedding_outCLM : IsEmbedding (outCLM K E) :=
  Function.LeftInverse.isEmbedding (mk_outCLM K) continuous_mk (map_continuous _)

Topological Embedding Property of the Separation Quotient Section Map

Informal description

The continuous linear map $\operatorname{outCLM}_K E : \operatorname{SeparationQuotient} E \to E$ is a topological embedding, meaning it is injective and the topology on $\operatorname{SeparationQuotient} E$ is the coarsest topology that makes $\operatorname{outCLM}_K E$ continuous.

SeparationQuotient.outCLM_injective theorem

: Function.Injective (outCLM K E)

Full source

theorem outCLM_injective : Function.Injective (outCLM K E) :=
  (isEmbedding_outCLM K E).injective

Injectivity of the Separation Quotient Section Map

Informal description

The continuous linear map $\operatorname{outCLM}_K E : \operatorname{SeparationQuotient} E \to E$ is injective.

SeparationQuotient.outCLM_isUniformInducing theorem

: IsUniformInducing (outCLM K E)

Full source

theorem outCLM_isUniformInducing : IsUniformInducing (outCLM K E) := by
  rw [← isUniformInducing_mk.isUniformInducing_comp_iff, mk_comp_outCLM]
  exact .id

Uniform Inducing Property of the Separation Quotient Section Map

Informal description

The continuous linear section map $\operatorname{outCLM}_K E \colon \operatorname{SeparationQuotient} E \to E$ is uniform inducing, meaning that the uniformity on $\operatorname{SeparationQuotient} E$ is the pullback of the uniformity on $E$ under the product map $\operatorname{outCLM}_K E \times \operatorname{outCLM}_K E$.

SeparationQuotient.outCLM_isUniformEmbedding theorem

: IsUniformEmbedding (outCLM K E)

Full source

theorem outCLM_isUniformEmbedding : IsUniformEmbedding (outCLM K E) where
  injective := outCLM_injective K E
  toIsUniformInducing := outCLM_isUniformInducing K E

Uniform Embedding Property of the Separation Quotient Section Map

Informal description

The continuous linear section map $\operatorname{outCLM}_K E \colon \operatorname{SeparationQuotient} E \to E$ is a uniform embedding, meaning it is injective, uniformly continuous, and the uniformity on $\operatorname{SeparationQuotient} E$ is induced by the map from the uniformity on $E$.

SeparationQuotient.outCLM_uniformContinuous theorem

: UniformContinuous (outCLM K E)

Full source

theorem outCLM_uniformContinuous : UniformContinuous (outCLM K E) :=
  (outCLM_isUniformInducing K E).uniformContinuous

Uniform Continuity of the Separation Quotient Section Map

Informal description

The continuous linear section map $\operatorname{outCLM}_K E \colon \operatorname{SeparationQuotient} E \to E$ is uniformly continuous.