Example 5.3

Open

QAlgorithms.Papers.Independent.Intakethird100.P07.basedPaths_loopContractible

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

prove2quantum

Let $G$ be any topological group, possibly noncommutative. Give its based path group $PG=\{\gamma\in C([0,1],G):\gamma(0)=e\}$ pointwise multiplication and the subspace topology of the compact-open mapping space. Then

\Phi(\gamma,s)(t)=\gamma(st)

is jointly continuous in $(\gamma,s)$ , satisfies $\Phi(\gamma,0)=1_{PG}$ and $\Phi(\gamma,1)=\gamma$ , and is a group endomorphism for each $s$ . Thus the displayed homotopy makes $PG$ loop contractible.

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

/-- Example 5.3, PDF p. 20: the displayed rescaling is jointly continuous,
has the required endpoints, and is a path-group endomorphism at each time. -/
theorem basedPaths_loopContractible
    (G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    Continuous (fun p : BasedPaths G × UnitTime => pathRescale p.1 p.2) ∧
    (∀ gamma : BasedPaths G, pathRescale gamma timeZero = basedPathOne) ∧
    (∀ gamma : BasedPaths G, pathRescale gamma timeOne = gamma) ∧
    (∀ (s : UnitTime) (gamma eta : BasedPaths G),
      pathRescale (basedPathMul gamma eta) s =
        basedPathMul (pathRescale gamma s) (pathRescale eta s)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P07

end

Source

Cohomology of Local Cochains, arXiv:1110.2661v2, PDF p. 20, Example 5.3

Read-back

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

For every topological group $G$ , let $P(G)$ be the space of continuous paths $\gamma:[0,1]\to G$ satisfying $\gamma(0)=1$ , with the subspace topology inherited from the compact-open topology on continuous maps. Define $R:P(G)\times[0,1]\to P(G)$ by $R(\gamma,s)(t)=\gamma(st)$ . Then $R$ is continuous, $R(\gamma,0)$ is the constant path at $1$ for every $\gamma\in P(G)$ , $R(\gamma,1)=\gamma$ for every $\gamma\in P(G)$ , and for every $s\in[0,1]$ and every $\gamma,\eta\in P(G)$ , rescaling preserves pointwise multiplication: $R(\gamma\eta,s)=R(\gamma,s)R(\eta,s)$ , where $(\gamma\eta)(t)=\gamma(t)\eta(t)$ .

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