Six properties of the constructed extension space

Open

QAlgorithms.Papers.Independent.Intakethird100.P08.proposition4

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

prove2quantum

Let $G$ be a Hausdorff locally compact second-countable topological group and let $A$ be a Hausdorff locally compact second-countable abelian topological group with a continuous action of $G$ by automorphisms, written $g\cdot a$ . Let $F:G\times G\to A$ be a Borel measurable two-cocycle, with pointwise identity

F(g,h)+F(gh,k)=g\cdot F(h,k)+F(g,hk),\qquad F(1,g)=F(g,1)=0.

Assume that $F$ is continuous on $U_F\times U_F$ , where $U_F$ is an open identity neighborhood. Let $E=A\times_F G$ , with multiplication $(a,g)(b,h)=(a+g\cdot b+F(g,h),gh)$ and inverse $(a,g)^{-1}=(-g^{-1}\cdot(a+F(g,g^{-1})),g^{-1})$ . Equip $E$ with the topology generated by left translates of the rectangles $U_A\times U_G$ , where $U_A,U_G$ are open identity neighborhoods and $F$ is continuous on $U_G\times U_G$ . Write $e=(0,1)$ and $\pi(a,g)=g$ .

Let $\iota(a)=(a,1)$ . The following all hold.

The maps $\iota$ and $\pi$ are continuous, and $\pi$ is open.
On an open identity neighborhood $U\subseteq G$ , $\pi$ admits a continuous section.
The map $\iota$ is a homeomorphism onto its image, and its image is closed.
The space $E$ is locally compact, second-countable and Hausdorff.
The Borel sigma algebra is generated by the translated rectangles and, under the coordinate bijection $E\to A\times G$ , equals the product Borel sigma algebra.
Multiplication, inversion and every inner conjugation are Borel measurable.

In particular, writing $\mathcal B$ for the rectangular identity neighborhood base,

\operatorname{Borel}(E)=\sigma\{xB:x\in E,\ B\in\mathcal B\}=\operatorname{Borel}(A)\otimes\operatorname{Borel}(G).

These properties supply the topological and measurable substrate before Theorem 6 is established.

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 ConstructedExtension

variable {G A : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [T2Space G] [LocallyCompactSpace G] [SecondCountableTopology G]
  [MeasurableSpace G] [BorelSpace G]
  [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A]
  [T2Space A] [LocallyCompactSpace A] [SecondCountableTopology A]
  [MeasurableSpace A] [BorelSpace A]

/-- Proposition 4(i)--(vi), PDF pp. 13--14, retaining all six clauses.
The inverse used here corrects the printed p. 14 error documented at twistedInv.
Product measure structure means equality of sigma algebras, not Haar measures. -/
theorem proposition4 (D : LocalCocycle G A) :
    Continuous (kernelInclusion D) ∧ Continuous (quotientProjection D) ∧
    IsOpenMap (quotientProjection D) ∧
    (∃ U : Set G, IsOpen U ∧ 1 ∈ U ∧
      ∃ sigma : U → ExtensionPoint D,
        Continuous sigma ∧ ∀ u, quotientProjection D (sigma u) = u.val) ∧
    Topology.IsClosedEmbedding (kernelInclusion D) ∧
    LocallyCompactSpace (ExtensionPoint D) ∧
    SecondCountableTopology (ExtensionPoint D) ∧ T2Space (ExtensionPoint D) ∧
    (borel (ExtensionPoint D) = MeasurableSpace.generateFrom (translatedRectangles D)) ∧
    (MeasurableSpace.comap (extensionCoordinates D)
      (inferInstance : MeasurableSpace (A × G)) = borel (ExtensionPoint D)) ∧
    Measurable (fun p : ExtensionPoint D × ExtensionPoint D => actionTwistedMul D p.1 p.2) ∧
    Measurable (twistedInv D) ∧
    (∀ x : ExtensionPoint D, Measurable (innerConjugation D x)) := by sorry

end ConstructedExtension

end QAlgorithms.Papers.Independent.Intakethird100.P08

Source

On Cohomology theory for topological groups, arXiv:1009.4519v1, PDF p. 13, Proposition 4: six properties of the constructed extension space

Read-back

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

Let $G$ be a Hausdorff, locally compact, second-countable topological group, and let $A$ be a Hausdorff, locally compact, second-countable abelian topological group, both equipped with their Borel $\sigma$ -algebras; either group may be trivial. Let $D=(\rho,c,N)$ consist of additive automorphisms $\rho_g:A\to A$ satisfying $\rho_1=\mathrm{id}$ and $\rho_{gh}=\rho_g\circ\rho_h$ , with $(g,a)\mapsto\rho_g(a)$ continuous, a measurable map $c:G\times G\to A$ satisfying $\rho_g(c(h,k))+c(g,hk)=c(g,h)+c(gh,k)$ and $c(1,g)=c(g,1)=0$ for all $g,h,k\in G$ , and an open set $N\subseteq G$ containing $1$ such that $c$ is continuous on $N\times N$ . Write $E_D$ for the set of pairs $(a,g)$ , and define

(a,g)\star(b,h)=(a+\rho_g(b)+c(g,h),gh), \qquad j(a,g)=\left(\rho_{g^{-1}}\bigl(-(a+c(g,g^{-1}))\bigr),g^{-1}\right).

Let $\mathcal R_D$ consist of all sets $\{(a,g)\star(b,h):b\in U_A,\ h\in U_G\}$ , where $(a,g)\in E_D$ , $U_A\subseteq A$ is open and contains $0$ , and $U_G\subseteq G$ is open, contains $1$ , and has $c$ continuous on $U_G\times U_G$ . Give $E_D$ the topology generated by $\mathcal R_D$ and its Borel $\sigma$ -algebra. Define $i:A\to E_D$ by $i(a)=(a,1)$ , $p:E_D\to G$ by $p(a,g)=g$ , and $q:E_D\to A\times G$ by $q(a,g)=(a,g)$ . The proposition asserts all of the following simultaneously: $i$ and $p$ are continuous; $p$ maps every open subset of $E_D$ to an open subset of $G$ ; there exist an open set $U\subseteq G$ containing $1$ and a continuous function $\sigma:U\to E_D$ , with $U$ carrying its subspace topology, such that $p(\sigma(u))=u$ for every $u\in U$ ; $i$ is a closed embedding, meaning it is a homeomorphism onto its image and that image is closed in $E_D$ ; $E_D$ is locally compact, second-countable, and Hausdorff; its Borel $\sigma$ -algebra equals the $\sigma$ -algebra generated by $\mathcal R_D$ ; the $\sigma$ -algebra on $E_D$ consisting of preimages under $q$ of sets measurable for the product $\sigma$ -algebra $\mathcal B(A)\otimes\mathcal B(G)$ also equals $\mathcal B(E_D)$ ; the function $(x,y)\mapsto x\star y$ is measurable from $E_D\times E_D$ , with the product measurable structure, to $E_D$ ; $j:E_D\to E_D$ is measurable; and, for every $x\in E_D$ , the function $y\mapsto(x\star y)\star j(x)$ is measurable.

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