Canonical unit and contraction isomorphisms

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.lemma_2_7

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

prove2quantum

Let $t:G\to H$ be a topological crossed module, with continuous action $\alpha:H\to\operatorname{Aut}(G)$ . Thus $t(\alpha(h)g)=ht(g)h^{-1}$ and $\alpha(t(g))k=gkg^{-1}$ . Put $G_1=\ker t$ and give both $G/G_1$ and $H/t(G)$ their quotient topologies. Assume their quotient projections admit continuous local sections. All actions, structure maps and isomorphisms below are continuous, all principal bundles are locally trivial, and a bispace has a nonempty principal homogeneous underlying right space.

Let $(X,\psi)$ be an $(H,G)$ -bispace, let $T=G$ with structure map $t$ , and let $X^*$ have the same underlying space with structure map $\psi^{-1}$ and right action $x\cdot g=x\alpha(\psi(x))^{-1}(g^{-1})$ . Tensor products are the balanced quotients $(x,y)k=(xk,k^{-1}y)$ . There are canonical structure-preserving right equivariant homeomorphisms

X\otimes T\cong X,\qquad T\otimes X\cong X,\qquad X\otimes X^*\cong T.

The unit maps send $[x,g]$ to $xg$ and $[g,x]$ to $g\cdot x$ . The contraction sends $[x,y]$ to the unique $g$ such that $g\cdot y=x$ , with $t(g)=\psi(x)\psi(y)^{-1}$ . These specified maps give the unit and dual identifications used in tensor constructions.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P93

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P93

universe u

variable {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

variable (C : CrossedModule G H)

/-- Lemma 2.7, PDF p.6, all three canonical isomorphisms. Their formulas,
right equivariance and structure-map identities are asserted on representatives.
The contraction sends [x,y] to the unique g with gy=x. -/
theorem lemma_2_7 {X : Type u} [TopologicalSpace X] (B : Bispace C X) :
    (∃ e : RightUnitTensor C B ≃ₜ X,
      (∀ x g, e (Quot.mk _ (x, g)) = B.right.act x g) ∧
      (∀ x g k, e (Quot.mk _ (x, g * k)) =
        B.right.act (e (Quot.mk _ (x, g))) k) ∧
      (∀ x g, B.psi (e (Quot.mk _ (x, g))) = B.psi x * C.t g)) ∧
    (∃ e : LeftUnitTensor C B ≃ₜ X,
      (∀ g x, e (Quot.mk _ (g, x)) = inducedLeft C B g x) ∧
      (∀ g x k, e (Quot.mk _ (g, B.right.act x k)) =
        B.right.act (e (Quot.mk _ (g, x))) k) ∧
      (∀ g x, B.psi (e (Quot.mk _ (g, x))) = C.t g * B.psi x)) ∧
    (∃ e : DualTensor C B ≃ₜ G,
      (∀ x y, inducedLeft C B (e (Quot.mk _ (x, y))) y = x) ∧
      (∀ x y k, e (Quot.mk _ (x, inducedLeft C B k⁻¹ y)) =
        e (Quot.mk _ (x, y)) * k) ∧
      (∀ x y, C.t (e (Quot.mk _ (x, y))) = B.psi x * (B.psi y)⁻¹)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 6, Lemma 2.7

Read-back

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

Let $G,H$ be topological groups, and let $C$ consist of a continuous group homomorphism $t:G\to H$ and a group homomorphism $\alpha:H\to\operatorname{Aut}(G)$ such that $(h,g)\mapsto\alpha_h(g)$ is continuous, $t(\alpha_h(g))=h\,t(g)\,h^{-1}$ , and $\alpha_{t(g)}(k)=gkg^{-1}$ for all $h\in H$ and $g,k\in G$ ; assume also that each of the quotient maps $G\to G/\ker t$ and $H\to H/t(G)$ has a continuous right inverse on some open neighborhood of every point of its target. Let $X$ be a topological space and $B$ consist of a continuous right action $x\cdot g$ of $G$ on $X$ , with $x\cdot1=x$ and $(x\cdot g)\cdot k=x\cdot(gk)$ , together with a continuous map $\psi:X\to H$ satisfying $\psi(x\cdot g)=\psi(x)t(g)$ . Assume $X$ is nonempty and, for every $x\in X$ , the map $g\mapsto x\cdot g$ is a homeomorphism $G\to X$ . Define $g\star x=x\cdot\alpha_{\psi(x)}^{-1}(g)$ , where the inverse is the inverse automorphism. Form the quotient spaces $T_R$ of $X\times G$ , $T_L$ of $G\times X$ , and $T_D$ of $X\times X$ by imposing, respectively, $(x,g)\sim(x\cdot a,a^{-1}g)$ , $(g,x)\sim(ga,a^{-1}\star x)$ , and $(x,y)\sim(x\cdot a,y\cdot a)$ for every $a\in G$ . Then there exist homeomorphisms $e_R:T_R\to X$ , $e_L:T_L\to X$ , and $e_D:T_D\to G$ satisfying all the following identities, for every $x,y\in X$ and $g,k\in G$ :

\begin{aligned} e_R([x,g]_R)&=x\cdot g,& e_R([x,gk]_R)&=e_R([x,g]_R)\cdot k,& \psi(e_R([x,g]_R))&=\psi(x)t(g),\\ e_L([g,x]_L)&=g\star x,& e_L([g,x\cdot k]_L)&=e_L([g,x]_L)\cdot k,& \psi(e_L([g,x]_L))&=t(g)\psi(x),\\ e_D([x,y]_D)\star y&=x,& e_D([x,k^{-1}\star y]_D)&=e_D([x,y]_D)k,& t(e_D([x,y]_D))&=\psi(x)\psi(y)^{-1}. \end{aligned}

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