Lemma 10: equivariant fiberwise NDR criterion

Open

QAlgorithms.Papers.Independent.Intakethird100.P73.equivariant_strongFCofibration_iff_ndr

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

prove2quantum

Let $B$ be a weakly Hausdorff k-space, let $G$ be a group object in $\mathcal K/B$ , and let $i:A\hookrightarrow X$ be an equivariant inclusion of right $G$ -spaces over $B$ . A strong $\bar f$ -cofibration means a map with the left lifting property against every equivariant map that is both a fiberwise homotopy equivalence and a fiberwise covering-homotopy fibration. Then

i\text{ is a strong }\bar f\text{-cofibration}\quad\Longleftrightarrow\quad i(A)\text{ is closed in }X\text{ and }(X,i(A))\text{ is a }G\text{-fiberwise NDR pair}.

Here an NDR representation consists of continuous maps $u:X\to I$ and $H:X\times I\to X$ , with $I=[0,1]$ , such that $i(A)=u^{-1}(0)$ , $H(x,0)=x$ , $H(a,t)=a$ for every $a\in i(A)$ and every $t\in I$ , and $u(x)<1$ implies $H(x,1)\in i(A)$ . The homotopy stays over $B$ , $u(xg)=u(x)$ , and $H(xg,t)=H(x,t)g$ for elements in a common fiber. Tensor and action domains have k-space topology. No fibrancy of $G$ is assumed.

This characterizes equivariant strong cofibrations by geometric deformation data.

Formalization Note An inclusion is represented by an embedding, with its image used as the subspace. The two sides of the equivalence have independent definitions.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P73

Formal statement

noncomputable section

universe u

namespace QAlgorithms.Papers.Independent.Intakethird100.P73

open CategoryTheory

open scoped Topology

/-- Roberts--Stevenson, Lemma 10, arXiv:1203.2460v4, PDF p. 7.
An equivariant inclusion over B is a strong fbar-cofibration exactly when
its image is closed and the pair has an equivariant fiberwise NDR
representation. No fibrancy assumption on the group is made. -/
theorem equivariant_strongFCofibration_iff_ndr
    (B : KSpace) (hB : IsWeaklyHausdorff B) (G : ParametrizedGroup B)
    (A X : EquivariantSpace G) (i : EquivariantMap A X)
    (hi : Topology.IsEmbedding i.map.map) :
    IsEquivariantStrongFCofibration i ↔
      IsClosed (Set.range i.map.map) ∧
      IsEquivariantFiberwiseNDR X (Set.range i.map.map) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P73

end

Source

Simplicial principal bundles in parametrized spaces, arXiv:1203.2460v4, PDF p. 7, Lemma 10

Read-back

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

Let $B$ be a compactly generated topological space such that the image of every continuous map $S\to B$ from a compact Hausdorff space $S$ is closed in $B$ . Let $G$ be any parametrized group over $B$ , with compactly generated total space, continuous projection, unit section and inverse, and fiberwise group multiplication continuous on the kified fiber product. Let $A,X$ be compactly generated right $G$ -spaces over $B$ , whose actions preserve their continuous projections, satisfy the unit and associativity laws, and are continuous on the kified fiber products. Let $i:A\to X$ be continuous, projection-preserving and action-preserving, and assume that $i$ is a topological embedding, meaning an injective map that is a homeomorphism onto its image with the subspace topology. Write $K(T)$ for the same underlying set as $T$ , with subsets open exactly when all continuous compact Hausdorff probes into $T$ have open inverse images; call a map equivariant when it is continuous, preserves the base projection and commutes with the action on compatible pairs, and call a homotopy equivariant when it is continuous from $K(D\times[0,1])$ , preserves the base projection and commutes with the action at every time. Then the following are equivalent: (i) for every pair of right $G$ -spaces $U,V$ and equivariant map $p:U\to V$ satisfying both the lifting condition that, for every right $G$ -space $Z$ , equivariant $a_0:Z\to U$ , and equivariant homotopy $F:K(Z\times[0,1])\to V$ with $F(z,0)=p(a_0(z))$ , there is an equivariant homotopy $L$ with $L(z,0)=a_0(z)$ and $p(L(z,t))=F(z,t)$ , and the condition that some equivariant $q:V\to U$ has equivariant homotopies from $q\circ p$ to $\operatorname{id}_U$ and from $p\circ q$ to $\operatorname{id}_V$ , every equivariant $a:A\to U$ , $b:X\to V$ with $p\circ a=b\circ i$ admits an equivariant $\ell:X\to U$ with $\ell\circ i=a$ and $p\circ\ell=b$ ; (ii) the image $I=\{i(a):a\in A\}$ is closed in $X$ , and there exist a continuous $u:X\to[0,1]$ and an equivariant homotopy $H:K(X\times[0,1])\to X$ such that

x\in I\ \Longleftrightarrow\ u(x)=0,\qquad H(x,0)=x,\qquad H(x,t)=x\ \text{for }x\in I,\qquad u(x)<1\ \Longrightarrow\ H(x,1)\in I,

and $u(x\cdot g)=u(x)$ for every compatible $x,g$ . All time variables range over $[0,1]$ , no endpoint inclusion is required where $u(x)=1$ , and no nonemptiness assumptions are imposed.

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