Based twisted loops take values in the identity path component

Open

QAlgorithms.Papers.Independent.Intakethird100.P59.based_twisted_loops_identity_component

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

prove2quantum

Let $G$ be a compactly generated topological group, let $\alpha\in G$ , and let $G^0$ denote the path component of its identity. Define

\Omega_{(\alpha)}G=\{\gamma\in C(\mathbb R,G):\gamma(t+1)=\alpha\gamma(t)\alpha^{-1}\text{ for every }t\in\mathbb R,\ \gamma(0)=1\}.

Every such loop takes values in $G^0$ . Restricting its codomain gives the canonical identification

\Omega_{(\alpha)}G\cong\Omega_{\operatorname{Ad}(\alpha)|_{G^0}}G^0.

This is an identification of topological groups, with compactly generated compact-open topologies and pointwise operations. If $G$ is discrete, $\Omega_{(\alpha)}G$ consists solely of the constant identity loop. The twist $\alpha$ is arbitrary and need not lie in $G^0$ .

Formalization Note Lean states equality of the sets after inclusion in $C(\mathbb R,G)$ , together with a homeomorphism that preserves every evaluation. Evaluation preservation also preserves the pointwise group operations. No connected component is substituted for the path component.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P59

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P59

universe u v

/-- Unnumbered identity-component assertion, PDF p.14. The equality is via
inclusion of G0 into G, with Ad(alpha) restricted to G0. Both groups are the
same set of continuous G-valued functions, hence have the same induced
compact-open (and compactly generated compact-open) topology and pointwise
operations. The discrete specialization asserts the entire group is trivial. -/
theorem based_twisted_loops_identity_component
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactlyGeneratedSpace G] (alpha : G) :
    basedTwistedLoopSet alpha =
      includeIdentityLoop '' identityBasedTwistedLoopSet alpha ∧
    (∃ e : KSubspace C(ℝ, G) (basedTwistedLoopSet alpha) ≃ₜ
        KSubspace C(ℝ, pathComponent (1 : G)) (identityBasedTwistedLoopSet alpha),
      ∀ gamma t, ((e gamma).1 t).1 = gamma.1 t) ∧
    (DiscreteTopology G → basedTwistedLoopSet alpha = {1}) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P59

Source

Mapping stacks of topological stacks, arXiv:0809.2373v2, PDF p. 14, Unnumbered §7: based twisted loops see only G0

Read-back

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

For every group $G$ equipped with a topology making it a topological group and a compactly generated space, and every $\alpha\in G$ , let $G_1$ be the path component of $1$ , with its subspace topology. Define $L_\alpha$ to be the set of continuous maps $\gamma:\mathbb R\to G$ such that $\gamma(0)=1$ and $\gamma(t+1)=\alpha\gamma(t)\alpha^{-1}$ for every real $t$ . Define $L_\alpha^1$ to be the set of continuous maps $\eta:\mathbb R\to G_1$ satisfying the same two equations after their values are viewed in $G$ . Then all three assertions hold: $L_\alpha$ is exactly the image of $L_\alpha^1$ under composition with the inclusion $G_1\hookrightarrow G$ ; there exists a homeomorphism $e:L_\alpha\to L_\alpha^1$ , where each set carries the compactly generated modification of its subspace topology in the corresponding continuous-map space with the compact-open topology, such that for every $\gamma\in L_\alpha$ and every $t\in\mathbb R$ , the value $e(\gamma)(t)$ , viewed in $G$ , equals $\gamma(t)$ ; and, if the given topology on $G$ is discrete, then $L_\alpha$ is the singleton consisting of the constant map $t\mapsto1$ . The defining equations apply to all real times, including negative times, and both sets contain the constant identity map.

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