Local one-cocycles are globally continuous

Proved

QAlgorithms.Papers.Independent.Intakethird100.P08.proposition3

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

prove2quantum

Let $G$ be a topological group and $A$ an abelian topological group with a continuous $G$ -action by automorphisms. Let $Z_{\rm lcm}^1(G,A)$ consist of all everywhere-defined Borel maps $c:G\to A$ continuous on some open identity neighborhood and satisfying the pointwise crossed identity. Then

Z_{\rm lcm}^1(G,A)=\{c:G\to A:\ c\text{ is continuous and }c(st)=c(s)+s\cdot c(t)\text{ for all }s,t\in G\}=Z_{\rm cont}^1(G,A).

This identifies cocycles themselves; no quotient by principal crossed homomorphisms is taken.

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 DegreeOne

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

/-- Proposition 3, PDF p. 11: local one-cocycles are globally continuous.
No local compactness, countability, or trivial action is assumed. -/
theorem proposition3 (rho : ContinuousModule G A) :
    locallyContinuousOneCocycles rho = continuousOneCocycles rho := by sorry

end DegreeOne

end QAlgorithms.Papers.Independent.Intakethird100.P08

Source

On Cohomology theory for topological groups, arXiv:1009.4519v1, PDF p. 11, Proposition 3: local one-cocycles are globally continuous

Read-back

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

For the given topological group $G$ , topological abelian group $A$ , and measurable structures, let $\rho$ specify additive automorphisms $\alpha_g$ of $A$ satisfying $\alpha_1=\operatorname{id}_A$ and $\alpha_{gh}=\alpha_g\circ\alpha_h$ , with $(g,a)\mapsto\alpha_g(a)$ continuous. The set of measurable functions $c:G\to A$ that are continuous on some open neighborhood of $1$ and satisfy $c(st)=c(s)+\alpha_s(c(t))$ for every $s,t\in G$ equals the set of globally continuous functions satisfying that same identity. Thus, for every function $c:G\to A$ , membership in either of these two explicitly described sets is equivalent to membership in the other.

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