A Borel section continuous near identity for Lindelof quotient

Open

QAlgorithms.Papers.Independent.Intakethird100.P08.remark2

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $K,E,Q$ be topological groups in a locally split short exact sequence $1\to K\xrightarrow{i}E\xrightarrow{p}Q\to1$ . Thus $i$ is a continuous closed embedding, $p$ is continuous, open and surjective, $i(K)=\ker p$ , and $p$ admits a continuous section on an open neighborhood of the identity of $Q$ .

Assume that $Q$ is Lindelof, meaning that every open cover has a countable subcover, and use the Borel sigma algebras. There is an everywhere-defined map $\sigma:Q\to E$ such that

p\circ\sigma=\operatorname{id}_Q,\qquad \sigma\text{ is Borel measurable},\qquad \sigma|_U\text{ is continuous for some open }U\ni1.

This is the countable-cover form of the global section construction.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P08

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P08

open Set MeasureTheory

open scoped BigOperators Topology CompactlySupported

section Sections

variable {K E Q : Type*} [Group K] [Group E] [Group Q]
  [TopologicalSpace K] [TopologicalSpace E] [TopologicalSpace Q]
  [IsTopologicalGroup K] [IsTopologicalGroup E] [IsTopologicalGroup Q]

/-- Remark 2, PDF p. 10: the Lindelof version of Lemma 1. The section is
Borel measurable globally, is continuous near identity, and is a right inverse;
it is not required to be a homomorphism. -/
theorem remark2 [MeasurableSpace E] [BorelSpace E]
    [MeasurableSpace Q] [BorelSpace Q] [LindelofSpace Q]
    (i : K →* E) (p : E →* Q) (h : IsLocallySplitSequence i p) :
    ∃ sigma : Q → E, Measurable sigma ∧ (∀ q, p (sigma q) = q) ∧
      ∃ U : Set Q, IsOpen U ∧ 1 ∈ U ∧ ContinuousOn sigma U := by sorry

end Sections

end QAlgorithms.Papers.Independent.Intakethird100.P08

Source

On Cohomology theory for topological groups, arXiv:1009.4519v1, PDF p. 10, Remark 2: the Lindelof section construction

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $i:K\to E$ and $p:E\to Q$ be identity-preserving multiplicative homomorphisms with the given topologies, suppose $E$ and $Q$ have measurable structures equal to their Borel $\sigma$ -algebras, and suppose $Q$ is Lindelöf, meaning that every open cover has a countable subcover. Assume $i$ and $p$ are continuous, $i$ is a closed embedding, $p$ is an open surjection, $i(K)=\{x\in E:p(x)=1\}$ , and there exist an open neighborhood $U_0$ of $1$ in $Q$ and a continuous map $\sigma_0:U_0\to E$ satisfying $p(\sigma_0(u))=u$ for every $u\in U_0$ . Then there exists a measurable map $\sigma:Q\to E$ satisfying $p(\sigma(q))=q$ for every $q\in Q$ , and there exists an open neighborhood $U$ of $1$ on which $\sigma$ is continuous.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph