Continuity of inner conjugation in the constructed extension

Open

QAlgorithms.Papers.Independent.Intakethird100.P08.theorem6

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

For each $x\in E$ define $i_x(y)=xyx^{-1}$ . Then

\text{for every }x\in E,\quad i_x:E\to E\text{ is continuous at }e.

This is the continuity assertion needed for compatibility of the constructed topology with the group law.

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]

/-- Theorem 6, PDF p. 13: continuity of every inner conjugation at identity,
without assuming a topological-group structure on the extension. -/
theorem theorem6 (D : LocalCocycle G A) :
    ∀ x : ExtensionPoint D,
      ContinuousAt (innerConjugation D x) (identityPoint D) := by sorry

end ConstructedExtension

end QAlgorithms.Papers.Independent.Intakethird100.P08

Source

On Cohomology theory for topological groups, arXiv:1009.4519v1, PDF p. 13, Theorem 6: continuity of inner conjugation in the constructed extension

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$ . Equip the set $E_D=A\times G$ with the topology generated by all sets $\{(a+\rho_g(b)+c(g,h),gh):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$ . The theorem asserts that, for every fixed $x=(a,g)\in E_D$ , the function

(b,h)\longmapsto \left( a+\rho_g(b)+c(g,h) +\rho_{gh}\!\left(\rho_{g^{-1}}\bigl(-(a+c(g,g^{-1}))\bigr)\right) +c(gh,g^{-1}), \ ghg^{-1} \right)

from $E_D$ to $E_D$ is continuous at the point $(0,1)$ .

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