Continuous range frames over singular simplices
Abstract
Continuous range frames over singular simplices
SimplexProjectionData in the formula consists of an arbitrary type B with a TopologicalSpace instance; arbitrary natural numbers n,r,k; a map P:B -> Matrix (Fin n) (Fin n) C; continuity of P; the pointwise equations P(b)*=P(b) and P(b)P(b)=P(b); the pointwise rank equation rank(P(b))=r; a proof k<=3; and a continuous singular simplex sigma:C(SimplexCategory.toTop.obj [k],B). The star means conjugate transpose. All these data, including the dimension bound and sigma, are quantified together as q. No topology on B beyond the given topology is required.
Write X(q)=SimplexCategory.toTop.obj [k], the original ULift of StdSimplex R (Fin (k+1)), and V(m)=EuclideanSpace C (Fin m). Indices(q) is Fin r. Columns(q) is Fin r -> C(X(q),V(n)); Coordinates(q) is C(X(q),V(n) ->L[C] V(r)). Range(q,x) is the actual complex linear range of Matrix.toEuclideanLin(P(sigma(x))) in V(n), and Fiber(q,x) is that range as a subtype. Column(q,s,x,i)=s(i)(x), Coordinate(q,a,x,v)=a(x)(v), and Basis(q,i)=EuclideanSpace.single i (1:C). Ambient(q,v) is the underlying V(n) vector of a fiber element. Reconstruct(q,s,a,x,v) is the finite sum over i:Fin r of (a(x)(Ambient(q,v)))(i) times s(i)(x). Multiplication of a vector by that complex coordinate means scalar multiplication.
Theorem 1.1 (range_projection_simplex_frames).
Proof. Machine-checked in Lean as D5/S3/Geometry/ProjectionRange/SimplexFrames.range_projection_simplex_frames (✓ std3). ∎
Source. Repository-derived.
Commentary.
There are continuous ambient columns s and continuous ambient complex-linear coordinates a. For every x and i the column belongs to the actual projection range and has coordinate vector e_i. For every actual fiber vector v, the coordinate-weighted sum of these columns is v in the ambient Euclidean space. The coordinates are defined on the whole ambient space, while the reconstruction identity is asserted for vectors in the actual range.
Choose the vertex v0 given by the zeroth element of Fin(k+1). On the original ULift simplex define H(t,x) by lifting the convex combination (1-t)v0+t x. Its weights are continuous in t and x, so H is continuous, H(0,x)=v0 and H(1,x)=x. The simplex is compact, including when k=0. This constructs the contraction of the actual singular-simplex domain.
Set E=V(n) ->L[C] V(n). Transport P along sigma and H, then convert each matrix to its continuous linear operator. This gives Q(t,x)=matrixCLE(P(sigma(H(t,x)))). Currying gives a continuous map F:[0,1] -> C(X,E). The compactness of X and completeness of E give the complete normed-ring structure on C(X,E). Matrix multiplication corresponds to operator composition, so F(t)^2=F(t) pointwise. Apply connected_idempotents_intertwiner at 0 and 1 in this map ring.
Let U be the continuous operator-valued map supplied by the resulting unit and W its inverse. Evaluation gives P_x U_x=U_x P_0, U_x W_x=I and W_x U_x=I, where P_x denotes the operator of P(sigma(x)) and P_0 that of P(sigma(v0)). These are identities across the entire simplex. In particular U_x is injective.
At b0=sigma(v0), use the existing actual-range column chart. Let A0:V(r) ->L[C] V(n) be its selected-column operator and C0:V(n) ->L[C] V(r) its inverse-Gram coordinate operator. The chart gives A0(z) in Ran P_0, C0 A0=I, and A0 C0(v)=v for v in Ran P_0. Hermitian idempotence and constant rank provide this chart; no frame is an input.
Define s_i(x)=U_x A0(e_i) and a(x)=C0 W_x. Evaluation and composition of continuous operator maps prove their continuity. Because P_x U_x=U_x P_0 and P_0 A0(e_i)=A0(e_i), each s_i(x) is fixed by P_x. Idempotence identifies this fixed-vector condition with actual range membership. The inverse identity W_x U_x=I and C0 A0=I give a(x)(s_i(x))=e_i.
For an actual range vector v at x, the equation P_x v=v and the intertwining identity imply U_x P_0 W_x v=v=U_x W_x v. Injectivity of U_x gives P_0 W_x v=W_x v, hence W_x v is in Ran P_0. Put z=C0 W_x v. Expand z as the sum of z_i e_i, apply the linear maps A0 and U_x to that sum, and use A0 C0 W_x v=W_x v. The resulting sum is U_x W_x v=v, which proves exactly the ambient reconstruction conjunct.
The parameters n and r may be zero. The same operator identities and the empty Fin r sum apply; no positive-rank or positive-dimension step is used. The vertex exists also for k=0. The bound k<=3 remains part of the statement. An empty B is permitted by the quantified data, although then a singular simplex into B cannot be supplied. Compactness is used for X and the continuous-map algebra, not imposed on B.
This is the standard contraction-and-transport construction for projection ranges. It uses the existing column-chart and inverse-Gram identities, the idempotent transport theorem, and Mathlib’s genuine topological simplex, compact simplex, compact-open currying and continuous-map normed-ring structures. These sources support the argument and its implementation; no claim of literature novelty is made.
Application: integral boundary winding from the supplied range frames.
Keep exactly the data above: an arbitrary topological space B, natural numbers n and r (including zero), and a continuous Hermitian idempotent P with rank(P(b))=r at every b. Put X_k=SimplexCategory.toTop.obj [k]=ULift (StdSimplex ℝ (Fin (k+1))) and V(m)=EuclideanSpace ℂ (Fin m). A genuine singular k-simplex is a continuous map σ:X_k→B. Its fiber at z is the actual range of Matrix.toEuclideanLin(P(σ(z))) in V(n). We use the existing range_projection_simplex_frames for k≤3, with no regularity, compactness or connectedness assumption on B. The construction below is an application of these frames and existing covering-space and singular-chain APIs; it introduces no additional named Lean theorem.
A frame over σ means actual continuous columns s_i:X_k→V(n) and a continuous map a:X_k→(V(n)→L[ℂ]V(r)). At every z the columns lie in that actual range, a(z)(s_i(z))=e_i, and every actual range vector v satisfies ∑_i a(z)(v)_i s_i(z)=v in V(n). Here e_i=EuclideanSpace.single i 1, and a is defined on the entire ambient space. These identities make the columns a basis of the range: applying a proves independence, and reconstruction proves spanning. At a single b∈B we use the same data without a continuity variable. The existing theorem supplies the continuous data separately on each original simplex, including vertices, edges, triangles and tetrahedra. It does not choose a frame varying continuously over all of B, nor does choosing one frame for every vertex or every singular edge assert continuous dependence on that choice index.
Frame multipliers and their direction. For actual frames F and G at the same b, write s_i^F and a_F for their columns and coordinates and define M(F,G)_{ij}=a_F(s_j^G)_i. Reconstruction gives s_j^G=∑i M(F,G){ij}s_i^F, or G=F M(F,G) with columns understood as an operator V(r)→V(n). Applying a_F to the reconstruction of each column of H in the G basis gives M(F,G)M(G,H)=M(F,H). The coordinate identity gives M(F,F)=I, hence M(F,G)M(G,F)=I and det M(F,G)≠0. This is the right multiplier taking F columns to G columns. A receiving ColumnChart transition instead takes F coordinates to G coordinates, and therefore is M(G,F), the inverse matrix. The directions must not be interchanged.
Define φ(F,G)=det M(F,G)/|det M(F,G)|∈Circle, where the denominator is the positive real norm embedded in ℂ. Multiplicativity of determinant and norm gives φ(F,G)φ(G,H)=φ(F,H), φ(F,F)=1 and φ(G,F)=φ(F,G)⁻¹. For frames over a common σ these are pointwise identities. The entries a_F(z)(s_j^G(z))_i are continuous, the determinant is continuous and never zero, so z↦φ(F(z),G(z)) is a genuine continuous Circle-valued map. This uses ambient columns and coordinates rather than supplying a phase cocycle as a hypothesis.
Vertex, edge and path choices. Let v_i=ULift.up(StdSimplex.single i) in X_k. For i≤j, let ι_ij:X_1→X_k be the actual map SimplexCategory.toTop.map(SimplexCategory.mkOfLe i j), and parameterize X_1 by λ(t)=ULift.up((1−t)v_0+t v_1) for 0≤t≤1, with the convex combination understood in StdSimplex before ULift. Thus λ(0)=v_0, λ(1)=v_1, ι_ij(v_0)=v_i and ι_ij(v_1)=v_j. These are the original simplicial maps; repeated vertices are allowed.
Choose an actual vertex frame V_b for every b∈B and an actual continuous edge frame E_e over each genuine singular edge e:X_1→B. For each e choose any correction path β_e in Circle from φ(E_e(v_0),V_{e(v_0)}) to φ(E_e(v_1),V_{e(v_1)}). No integer cochain, cancellation equation or characteristic class is part of these choices. Existence of frames follows from the supplier on dimensions zero and one, and Circle is path connected, so correction paths with these endpoints can be chosen. The choices need not depend continuously on b or e. In particular β_e may traverse extra loops of any integer winding; its endpoints do not determine its increment.
For a surrounding simplex frame F over σ and e_ij=σ∘ι_ij, define the actual coefficient path c^F_ij(t)=φ(F(ι_ij(λ(t))),E_{e_ij}(λ(t))) β_{e_ij}(t). This is a continuous Circle-valued path. The phase composition identity gives exactly c^F_ij(0)=φ(F(v_i),V_{σ(v_i)}) and c^F_ij(1)=φ(F(v_j),V_{σ(v_j)}). Thus on a triangle the composable paths form γ_F=(c^F_01.trans c^F_12).trans (c^F_02.symm), based at φ(F(v_0),V_{σ(v_0)}). The orientations are 01 followed by 12 followed by reverse 02. The endpoint identities, rather than an informal identification of fibers, justify this concatenation.
Period-one lifts and winding. Let h:Circle→AddCircle (1:ℝ)=ℝ/ℤ be the inverse of AddCircle.homeomorphCircle. Its inverse sends [t] to exp(2πit), fixing the positive winding convention. For any continuous interval map c:I→Circle, lift h∘c through the covering q:ℝ→ℝ/ℤ, starting at any real representative of h(c(0)), and call the lift Q. Set Δ(c)=Q(1)−Q(0). If Q and Q′ lift the same map, their difference is a continuous integer-valued map on the connected interval, hence constant. Equivalently apply IsCoveringMap.const_of_comp to Q−Q′. Thus Δ(c) is independent of the chosen starting representative.
The homeomorphism respects the group laws: h(cd)=h(c)+h(d) and h(c/d)=h(c)−h(d). Sums and differences of real lifts therefore give Δ(cd)=Δ(c)+Δ(d) and Δ(c/d)=Δ(c)−Δ(d). Reversing a lift gives Δ(c.symm)=−Δ(c). For composable paths c,d with lifts Q,R, the common endpoint implies s=Q(1)−R(0)∈ℤ. Shift R to R+s, concatenate Q with that shifted lift, and evaluate the endpoints. The result is Δ(c.trans d)=Δ(c)+Δ(d). This is also precisely the existing covering liftPath_trans rule, with eq_liftPath_iff or eq_liftPath_iff’ identifying the shifted second lift. These operations use the ordinary interval reparameterization of Path.trans.
If c is a loop, Q(1) and Q(0) have the same quotient, so Δ(c)∈ℤ. AddCircle.windingNumber_eq_div identifies the real cast of its winding with (Q(1)−Q(0))/1. Write D^F_ij=Δ(c^F_ij). Applying concatenation and reversal to γ_F yields the integer winding o_F(σ), with the exact real identity o_F(σ)=D^F_01+D^F_12−D^F_02. Individual D^F_ij can be nonintegral because the coefficient endpoints can differ. Integrality belongs to the closed boundary loop, not to each edge increment.
Independence of the surrounding frame. For two continuous actual frames F,G on a triangle, put p(z)=φ(F(z),G(z)). Phase composition gives c^G_ij(t)=c^F_ij(t)/p(ι_ij(λ(t))). Obtain a continuous real lift θ:X_2→ℝ of h∘p, with any compatible prescribed value at v_0. The lift is on the exact ULift simplex. To apply the existing general covering theorem, the weights embedding of StdSimplex into the finite real coordinate space identifies it homeomorphically with the nonempty convex standard simplex. The existing convex-set results give contractibility and local path connectedness. Transfer these along that homeomorphism and Homeomorph.ulift; contractibility gives simple connectedness. IsCoveringMap.existsUnique_continuousMap_lifts then supplies θ for the covering q. No new simplex-lifting theorem is needed.
Along edge ij the real lift of p is θ∘ι_ij∘λ, with increment θ(v_j)−θ(v_i). The quotient rule therefore gives D^G_ij=D^F_ij−θ(v_j)+θ(v_i). Subtract the two triangle windings: o_G−o_F=(−θ(v_1)+θ(v_0))+(−θ(v_2)+θ(v_1))−(−θ(v_2)+θ(v_0))=0 in ℝ. Since ℤ→ℝ is injective, the integer windings are equal. Let o_C(σ) denote this common integer for the fixed geometric choices C=(V,E,β), using any supplier frame on σ. This argument lifts a continuous phase on one simplex and never assumes a global continuous choice of vertex frames on B.
Restriction and tetrahedron cancellation. If α:[ℓ]→[k] is a simplicial map, functoriality and the order-map identity give (toTop.map α)∘ι_ij=ι_{α(i),α(j)}. Consequently (σ∘toTop.map α)∘ι_ij=σ∘ι_{α(i),α(j)} as entire continuous edge maps. Since E_e and β_e were selected as functions of that actual map e, the two appearances use exactly the same edge frame and correction path, including their dependent endpoint data. Pulling F back along α therefore gives the identical coefficient path and edge increment for the corresponding edge. Agreement merely at the endpoints would not be sufficient.
Now let τ:X_3→B be a genuine singular tetrahedron and choose one supplier frame T on it. On each face, frame independence lets us compute o_C using the restriction of T instead of that face’s separately chosen supplier frame. By the restriction identity all face increments are the same six numbers D_ij measured in T. For the faces deleting vertices 0,1,2,3 respectively, these windings in ℝ are o_123=D_12+D_23−D_13, o_023=D_02+D_23−D_03, o_013=D_01+D_13−D_03, and o_012=D_01+D_12−D_02. Thus the original signed face sum is o_123−o_023+o_013−o_012=(D_12+D_23−D_13)−(D_02+D_23−D_03)+(D_01+D_13−D_03)−(D_01+D_12−D_02)=0. Every edge occurs twice with opposite signs. Injectivity of the real cast gives the same equation in ℤ.
The original integral singular complex. In the exact source convention the coefficient object is R=ModuleCat.of ℤ (ULift ℤ); ULift only matches universes. Forgetting its ℤ-module structure to AddCommGrp gives the ordinary integral coefficient object. Take C_*(B)=((singularChainComplexFunctor (ModuleCat ℤ)).obj R).obj (TopCat.of B), the existing singular chain functor. Equivalently, for S=TopCat.toSSet.obj (TopCat.of B), degree k is the coproduct of copies of R indexed by S_k, whose elements are the lifted genuine continuous singular k-simplices. This is not a replacement combinatorial chain model. Write ι_σ:R→C_k(B) for its summand inclusion, supplied by SSet.ιChainComplex.
A cochain u of degree k is an actual ℤ-linear map C_k(B)→R, equivalently a homomorphism of the underlying integral chain groups. Define its coboundary by (δu)(c)=u(d_{k+1,k}(c)), using the original differential and no extra sign. On a summand the existing SSet.ιChainComplex_d says d(ι_σ(z))=∑{q=0}^{k+1}(−1)^q ι{∂_qσ}(z). The face ∂_qσ is exactly σ precomposed with toTop.map(δ q), as in the geometric calculation. Thus (δu)(ι_σ(z))=∑q(−1)^q u(ι{∂_qσ}(z)).
Extend o_C to an integral 2-cochain O_C by the coproduct universal property: O_C(ι_σ(z))=o_C(σ)·z, where the dot is integer scalar multiplication in R. For c=∑a ι{σ_a}(z_a), including repeated or degenerate simplices, O_C(c)=∑_a o_C(σ_a)·z_a. On every tetrahedron summand the signed-face calculation gives (δO_C)(ι_τ(z))=(o_123−o_023+o_013−o_012)·z=0 for every z∈R. SSet.chainComplex_hom_ext says that maps out of the chain coproduct are determined by these restrictions. Hence δO_C=0 as a map on C_3(B); explicitly O_C(d c)=∑_a(o_123(τ_a)−o_023(τ_a)+o_013(τ_a)−o_012(τ_a))·z_a=0 for every integral 3-chain c=∑a ι{τ_a}(z_a).
Changing all geometric choices and constructing the integer edge cochain. Let C_old=(V,E,β) and C_new=(V′,E′,β′), with the same P and full assumptions. At a vertex b set ρ_b=φ(V_b,V′_b) and choose a real lift α_b of h(ρ_b), for example the representative from AddCircle.equivIco (1:ℝ) 0. No continuity of b↦α_b is asserted or used. On each actual singular edge e define the new-to-old coefficient ratio r_e(t)=φ(E_e(λ(t)),E′e(λ(t))) β′e(t)/β_e(t). Its endpoints are r_e(0)=ρ{e(v_0)} and r_e(1)=ρ{e(v_1)}: compose the two frame phases with the endpoint of β′ and cancel the endpoint of β. This ratio uses both changed edge frames and arbitrary changed correction paths.
Lift h∘r_e through q to a continuous η_e:I→ℝ with prescribed initial value η_e(0)=α_{e(v_0)}. The existing liftPath, liftPath_zero and liftPath_lifts APIs provide this lift and its endpoint quotient. Because η_e(1) and α_{e(v_1)} represent the same point of ℝ/ℤ, their difference is an integer. Define k(e)∈ℤ by k(e)=η_e(1)−α_{e(v_1)}, understood through ℤ→ℝ. Equivalently k(e)=η_e(1)−η_e(0)−α_{e(v_1)}+α_{e(v_0)}. This constructs an integer from the actual ratio path and prescribed vertex representatives; it does not assume that the obstruction difference is a coboundary.
In any surrounding actual simplex frame F, the phase multiplication identity gives c^{F,new}ij=c^{F,old}ij·r{e_ij}. Therefore D^{F,new}ij−D^{F,old}ij=Δ(r{e_ij})=k(e_ij)+α{σ(v_j)}−α{σ(v_i)}. Use the same F for both triangle windings, which is allowed by frame independence. Their new-minus-old difference is k(e_01)+k(e_12)−k(e_02)+(α_1−α_0)+(α_2−α_1)−(α_2−α_0)=k(e_12)−k(e_02)+k(e_01). The vertex terms cancel and the real-cast equality is an integer equality. This fixes the sign of k for the stated new-minus-old convention.
Extend k by the same original coproduct construction to K∈Hom_ℤ(C_1(B),R), with K(ι_e(z))=k(e)·z. The original differential on a triangle is dσ=e_12−e_02+e_01, so (δK)(ι_σ(z))=(k(e_12)−k(e_02)+k(e_01))·z. Summand extensionality now gives O_new−O_old=δK as an equality of cochains. In full, for every integral 2-chain c=∑a ι{σ_a}(z_a), (O_new−O_old)(c)=∑_a(o_new(σ_a)−o_old(σ_a))·z_a=∑_a(k(e^a_12)−k(e^a_02)+k(e^a_01))·z_a=K(d c)=(δK)(c). Both the cocycle equation and this choice equation apply to all integer coefficients, not just unit generators or real-valued cochains.
Boundary cases and the scope of the construction. If B is empty, each X_k is inhabited by v_0, so no singular simplex into B exists; the chain coproducts are empty and the assertions above are vacuous. If r=0, frames have no columns and their coordinate target V(0) is zero; reconstruction concerns the zero range, and the empty determinant is 1. Nevertheless β_e may be an arbitrary loop at 1, so c_ij=β_{e_ij} can have nonzero integral edge increment. Rank zero does not force the chosen obstruction cochain to vanish. For example on a one-point base take the same correction loop of winding m on its unique singular edge. Its unique singular triangle then has winding m+m−m=m. This is a mathematical illustration of the arbitrary choices, not a separately compiled witness. It is consistent with choice independence up to a coboundary.
All degenerate singular simplices and repeated vertices remain in the original complex. The restriction identity is an identity of actual maps and continues to apply to them. In particular the one-point illustration is allowed; no normalized quotient, vanishing on degeneracies or normalized cochain is claimed. The statements quantify arbitrary natural n and r, including n=0. On an inhabited base an impossible rank value has no P satisfying the hypotheses; for such parameters the conditional assertion may be vacuous. There is no positive-rank or nondegeneracy assumption hidden in the argument.
This application produces an integral singular cocycle and an explicit cochain relating geometric choices. It does not identify that cocycle, or its choice-independent singular cohomology class, with a universal integral first Chern class. It does not construct the actual ambient complex exterior power with its Hermitian metric, a normalized top wedge and its continuity or empty-wedge compatibility; phase normalization of a finite matrix determinant supplies none of those objects. The actual determinant and tensor bundle identifications and their class formulas, the oriented surface cap or integral pairing with its normalization, and the specified Pauli value −1 remain unresolved full ST38 obligations. No global bundle-cohomology identification is inferred from the calculation. The whole original mathematical goal remains active.
Sources for this application. The canonical existing primitive is range_projection_simplex_frames in https://github.com/the-omega-institute/trureturing/blob/7d88bc43ce4dd7e1a411f7b9a8f36a3feffdedd9/D5/S3/Geometry/ProjectionRange/SimplexFrames.lean . Its actual range, columns and receiving chart conventions are in https://github.com/the-omega-institute/trureturing/blob/7d88bc43ce4dd7e1a411f7b9a8f36a3feffdedd9/D5/S3/Geometry/ProjectionRange/Prebundle.lean . These are the retained repository sources; the mathematical labels in this application are prose notation, not additional declaration handles.
All upstream references below are pinned to mathlib 56a005855ea17e0b0958f73ec801ae140b0a1679. For covering lifts use IsCoveringMap.existsUnique_continuousMap_lifts (line 486), liftPath_trans (line 276), eq_liftPath_iff and eq_liftPath_iff’ (lines 262 and 269), together with liftPath_zero and liftPath_lifts in https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/Topology/Homotopy/Lifting.lean . Lift comparison uses IsCoveringMap.const_of_comp in https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/Topology/Covering/Basic.lean . The period-one quotient is AddCircle.isCoveringMap_coe, and winding is AddCircle.windingNumber_eq_div in https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/Topology/Covering/FundamentalGroupCircle.lean . The positive Circle convention and AddCircle.homeomorphCircle are in https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean .
For the exact simplex lift route use StdSimplex.isEmbedding_toFun_comp_weights in https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/Geometry/Convex/ConvexSpace/Topology.lean and StdSimplex.range_toFun_comp_weights in https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean . The range is the stdSimplex of https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/Analysis/Convex/StdSimplex.lean ; use Convex.contractibleSpace in https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/Analysis/Convex/Contractible.lean and Convex.locallyPathConnectedSpace in https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/Topology/Algebra/Module/LocallyConvex.lean . Transfer along Topology.IsEmbedding.toHomeomorph and Homeomorph.ulift in https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/Topology/Homeomorph/Lemmas.lean ; simple connectedness then follows from SimplyConnectedSpace.ofContractible. These existing APIs provide the hypotheses for the general covering lift rather than a new retained lifting lemma.
For actual chains use singularChainComplexFunctor in https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/AlgebraicTopology/SingularHomology/Basic.lean and SSet.ιChainComplex_d and SSet.chainComplex_hom_ext in https://github.com/leanprover-community/mathlib4/blob/56a005855ea17e0b0958f73ec801ae140b0a1679/Mathlib/AlgebraicTopology/SimplicialSet/Homology/Basic.lean . They supply respectively the original alternating face differential and the coproduct extensionality used to pass from the two explicit simplex calculations to equalities on all integral chains.