Lemma 24: fiberwise products of strong cofibrations

Open

QAlgorithms.Papers.Independent.Intakethird100.P73.fiberProduct_strongFCofibration

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

prove2quantum

Let $B$ be a weakly Hausdorff k-space. Let $i_1:A_1\to X$ and $i_2:A_2\to Y$ be strong $\bar f$ -cofibrations in $\mathcal K/B$ , where all four spaces are k-spaces over $B$ and all maps commute with their projections. A strong $\bar f$ -cofibration has the left lifting property against every map over $B$ that is both a fiberwise homotopy equivalence and a fiberwise covering-homotopy fibration. Then

i_1\times_B i_2:A_1\times_B A_2\longrightarrow X\times_B Y \quad\text{is a strong }\bar f\text{-cofibration}.

The displayed map sends $(a_1,a_2)$ to $(i_1(a_1),i_2(a_2))$ . Each fiber product is formed with the kification of the subspace topology on the equal-base pairs. No separation assumption on the total spaces is imposed.

This gives stability of strong fiberwise cofibrations under products over the fixed base.

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 24, arXiv:1203.2460v4, PDF p. 20.
The fiberwise product of two strong fbar-cofibrations is a strong
fbar-cofibration. All objects are k-spaces over a weakly Hausdorff k-space B. -/
theorem fiberProduct_strongFCofibration
    (B : KSpace) (hB : IsWeaklyHausdorff B)
    (A X D Y : SpaceOver B) (i : MapOver A X) (j : MapOver D Y)
    (hi : IsStrongFCofibration i) (hj : IsStrongFCofibration j) :
    IsStrongFCofibration (fiberProductMap i j) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P73

end

Source

Simplicial principal bundles in parametrized spaces, arXiv:1203.2460v4, PDF p. 20, Lemma 24

Read-back

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

Let $B$ be a compactly generated space such that the image of every continuous map from any compact Hausdorff space in the same universe to $B$ is closed. Let $A,X,D,Y$ be compactly generated spaces with continuous projections $\pi_A,\pi_X,\pi_D,\pi_Y$ to $B$ , and let $i:A\to X$ and $j:D\to Y$ be continuous maps with $\pi_X(i(a))=\pi_A(a)$ and $\pi_Y(j(d))=\pi_D(d)$ for every $a,d$ . Write $I=[0,1]$ , and let $k(T)$ retain the set of $T$ with the finest topology making every originally continuous map from a compact Hausdorff space in the same universe continuous. A map over $B$ is continuous and commutes with projections, and a homotopy over $B$ from $f_0:S\to T$ to $f_1:S\to T$ is a continuous $F:k(S\times I)\to T$ with $F(s,0)=f_0(s)$ , $F(s,1)=f_1(s)$ , and $\pi_T(F(s,t))=\pi_S(s)$ . For a map $r:P\to Q$ over $B$ , define the property $\mathcal C(r)$ as follows: for every pair of compactly generated spaces $U,V$ over $B$ and every map $p:U\to V$ over $B$ satisfying both conditions below, any maps $a:P\to U$ and $b:Q\to V$ over $B$ with $p\circ a=b\circ r$ admit a map $\ell:Q\to U$ over $B$ with $\ell\circ r=a$ and $p\circ\ell=b$ . The first condition on $p$ is that, for every compactly generated space $Z$ over $B$ , map $c:Z\to U$ over $B$ , and continuous $H:k(Z\times I)\to V$ with $\pi_V(H(z,t))=\pi_Z(z)$ and $H(z,0)=p(c(z))$ , there exists a continuous $L:k(Z\times I)\to U$ with $\pi_U(L(z,t))=\pi_Z(z)$ , $L(z,0)=c(z)$ , and $p(L(z,t))=H(z,t)$ for all $z,t$ . The second condition is that there exists a map $q:V\to U$ over $B$ with homotopies over $B$ from $q\circ p$ to $\mathrm{id}_U$ and from $p\circ q$ to $\mathrm{id}_V$ . Assuming $\mathcal C(i)$ and $\mathcal C(j)$ , the theorem asserts $\mathcal C(i\times_B j)$ , where

i\times_B j: k\bigl(\{(a,d)\in A\times D:\pi_A(a)=\pi_D(d)\}\bigr) \longrightarrow k\bigl(\{(x,y)\in X\times Y:\pi_X(x)=\pi_Y(y)\}\bigr), \qquad (a,d)\longmapsto(i(a),j(d)).

The sets inside $k$ carry their subspace topologies from the ordinary products, and their projections to $B$ are given by the first coordinate’s projection. No nonemptiness or injectivity assumptions are imposed; empty spaces and empty fiber products are included.

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