Example 1.5

Proved

QAlgorithms.Papers.Independent.Intakenext100.P09.example_1_5

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $G$ be a topological group and $U\subseteq G$ an open set containing the identity. Define $\mathcal U_U=\{gU:g\in G\}$ . Then $\mathcal U_U$ is an invariant open cover of $G$ . In each degree $n\ge0$ , let

\mathcal U_U[n]=\bigcup_{g\in G}(gU)^{n+1}.

These sets are open and invariant under simultaneous left translation. Every coordinate-selection map, including every face and degeneracy map, sends the corresponding set into the set in its target degree. Thus they form an open simplicial $G$ -subspace of $G^{\bullet+1}$ . Invariance refers to the translated family; its individual members need not be invariant.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P09

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakenext100.P09

universe u v w

/-- PDF p. 3, Example 1.5: translated identity neighborhoods cover the group,
are invariant as a family, and give an open simplicial invariant subspace.
All coordinate maps include faces and degeneracies. -/
theorem example_1_5 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : Set G) (hU : IsOpen U) (h1 : (1 : G) ∈ U) :
    ∃ C : OpenCover G, C.sets = translatedFamily U ∧ InvariantCover G C ∧
      (∀ n : ℕ, IsOpen (coverDiagonal C n)) ∧
      (∀ (n : ℕ) (x : Fin (n + 1) → G), x ∈ coverDiagonal C n →
        ∀ g : G, (fun i => g * x i) ∈ coverDiagonal C n) ∧
      (∀ (n m : ℕ) (a : Fin (m + 1) → Fin (n + 1)) (x : Fin (n + 1) → G),
        x ∈ coverDiagonal C n → x ∘ a ∈ coverDiagonal C m) := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P09

end

Source

A Spectral Sequence Connecting Continuous With Locally Continuous Group Cohomology, arXiv:1110.0994v1, PDF p. 3, Example 1.5

Read-back

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

Let $G$ be a topological group and let $U\subseteq G$ be open and contain the identity element. There exists an open cover $C$ of $G$ , meaning a family of open subsets whose union is $G$ , whose family of members is exactly $\{gU:g\in G\}$ , where $gU=\{gu:u\in U\}$ . This cover is invariant under left translation: for every $g\in G$ and every member $W$ of $C$ , the set $gW$ is also a member of $C$ . For each natural number $n\geq 0$ , define

D_n=\{(x_0,\ldots,x_n)\in G^{n+1}:\text{all }x_i\text{ lie in one member of }C\}.

Every $D_n$ is open in the product topology; whenever $x\in D_n$ and $g\in G$ , the tuple $(gx_0,\ldots,gx_n)$ also belongs to $D_n$ ; and for all natural numbers $n,m\geq 0$ , every map $a:\{0,\ldots,m\}\to\{0,\ldots,n\}$ , and every $x\in D_n$ , the tuple $(x_{a(0)},\ldots,x_{a(m)})$ belongs to $D_m$ . The map $a$ need not be injective or surjective, so repetitions and omissions are included. In degree $0$ , $D_0=G^1$ .

Human review

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

View graph