Remark 5.4

Open

QAlgorithms.Papers.Independent.Intakethird100.P07.loopContractible_iff_pathExtensionSplits

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

prove2quantum

Let $G$ be a topological group and $PG$ its compact-open based path group. Write $\Omega G$ for the kernel of evaluation $\operatorname{ev}_1:PG\to G$ . Then

G\text{ is loop contractible}\quad\Longleftrightarrow\quad\exists\text{ a continuous group homomorphism }s:G\to PG\text{ with }\operatorname{ev}_1\circ s=\operatorname{id}_G.

This is the continuous splitting meaning of the semidirect-product assertion. With the parameter running from the identity element to the identity map, the section is $s(g)(t)=\Phi(g,t)$ , and a section gives the homotopy $\Phi(g,t)=s(g)(t)$ . No commutativity of $G$ is required.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P07

Formal statement

noncomputable section

universe u v

namespace QAlgorithms.Papers.Independent.Intakethird100.P07

open CategoryTheory Topology TopologicalSpace

/-- Remark 5.4, PDF p. 20: the based-path extension splits by a continuous
group-homomorphic section exactly when G is loop contractible. The section
homotopy is phi(g,t)=s(g)(t), and the section from phi is g↦(t↦phi(g,t)). -/
theorem loopContractible_iff_pathExtensionSplits
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    LoopContractible G ↔
      ∃ s : C(G, BasedPaths G),
        (∀ g, basedPathEndpoint (s g) = g) ∧
        (∀ g h, s (g * h) = basedPathMul (s g) (s h)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P07

end

Source

Cohomology of Local Cochains, arXiv:1110.2661v2, PDF p. 20, Remark 5.4

Read-back

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

For every topological group $G$ , the following are equivalent: there exists a continuous map $\phi:G\times[0,1]\to G$ such that $\phi(g,0)=1$ and $\phi(g,1)=g$ for every $g\in G$ , and $\phi(gh,t)=\phi(g,t)\phi(h,t)$ for every $t\in[0,1]$ and $g,h\in G$ ; and there exists a continuous map $s:G\to P(G)$ , where $P(G)$ is the space of continuous paths $[0,1]\to G$ starting at $1$ , with its subspace topology from the compact-open topology, such that $s(g)(1)=g$ for every $g\in G$ and $s(gh)(t)=s(g)(t)s(h)(t)$ for every $g,h\in G$ and $t\in[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