Extension of a local section to an open dense domain

Open

QAlgorithms.Papers.Independent.Intakethird100.P08.denseOpenSection

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$ .

Fix an open identity neighborhood $U\subseteq Q$ and a continuous section $\sigma:U\to E$ . There exist an open dense subset $V\subseteq Q$ containing $U$ and a continuous section $\tau:V\to E$ extending $\sigma$ :

U\subseteq V,\qquad \overline V=Q,\qquad p\circ\tau=\operatorname{id}_V,\qquad \tau|_U=\sigma.

The domain may omit a closed nowhere dense subset of the quotient.

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]

/-- Section 3.4, PDF p. 11: a continuous local section extends continuously to
an open dense domain, retaining its original values. No measurable gluing of
an uncountable cover of the entire quotient is asserted. -/
theorem denseOpenSection (i : K →* E) (p : E →* Q)
    (h : IsLocallySplitSequence i p) (U : Set Q) (hU : IsOpen U) (h1 : 1 ∈ U)
    (sigma : U → E) (hc : Continuous sigma) (hs : ∀ u, p (sigma u) = u.val) :
    ∃ V : Set Q, IsOpen V ∧ Dense V ∧ ∃ hUV : U ⊆ V,
      ∃ tau : V → E, Continuous tau ∧ (∀ v, p (tau v) = v.val) ∧
        ∀ u : U, tau ⟨u.val, hUV u.property⟩ = sigma u := by sorry

end Sections

end QAlgorithms.Papers.Independent.Intakethird100.P08

Source

On Cohomology theory for topological groups, arXiv:1009.4519v1, PDF p. 11, Section 3.4: extension to a dense open set

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. 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 $p$ has a continuous section on some open neighborhood of $1$ . For every open set $U\subseteq Q$ containing $1$ and every continuous map $\sigma:U\to E$ satisfying $p(\sigma(u))=u$ for every $u\in U$ , there exist an open dense set $V\subseteq Q$ containing $U$ and a continuous map $\tau:V\to E$ such that $p(\tau(v))=v$ for every $v\in V$ and $\tau(u)=\sigma(u)$ for every $u\in U$ , viewing $u$ as a point of $V$ through the inclusion $U\subseteq V$ .

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