Eilenberg–Mac Lane derived-operator API for the normalized Eilenberg–Zilber homotopy #
This file builds the tiny, local derived-operator API needed to formalize Eilenberg–Mac Lane's
recursive construction of the Eilenberg–Zilber homotopy Φ (Eilenberg–Mac Lane II, Thm 2.1a,
the identity ∂Φ + Φ∂ = ∇f − i modulo norms). It is the input to
eilenbergZilberNormalized in BisimplicialNormalized.lean.
We deliberately do not use an explicit closed-form homotopy; the literature only ever proves the contraction identity via the recursion + derived operators, so we follow EM directly.
Design #
EM's "natural operators" M : (K×L)_s → (K×L)_q (their (2.10)) are, on a bisimplicial object X,
exactly finite ℤ-linear combinations of letters: a pair of SimplexCategory maps
(β, γ) : ⟦q⟧ ⟶ ⟦s⟧ acting on the diagonal F₂.obj X = diag X by
(X.obj ⟦s⟧).map γ.op ≫ (X.map β.op).app ⟦q⟧ : X_{s,s} ⟶ X_{q,q}.
OpLetter s q— one such pair,DerivedOp s q := OpLetter s q →₀ ℤ— a formalℤ-combination.DerivedOp.realize X— realize a formal operator as an actual degreewise hom onF₂.obj X.DerivedOp.prime— EM's derived operatorM ↦ M'(prepend the 0-th cofaceδ⁰to each letter).DerivedOp.Frontal— every letter fixes the bottom vertex (avoids the 0-th faceF₀).
"Modulo norms" is represented (per the project's PInfty strategy) by postcomposing with
retractionN₂ X = PInftyToNormalizedMooreComplex (diag X): a term is a norm iff it dies after
≫ retractionN₂.
Operators as formal ℤ-combinations of letters #
A letter: a pair of SimplexCategory maps ⟦q⟧ ⟶ ⟦s⟧. The fst map acts on the
horizontal (first / K) simplicial variable and snd on the vertical (second / L) one.
Realized on a bisimplicial object it gives a single summand X_{s,s} ⟶ X_{q,q} of an EM
natural operator (their (2.10)).
Horizontal (
K-side)SimplexCategorymap.Vertical (
L-side)SimplexCategorymap.
Instances For
An EM natural operator (K×L)_s → (K×L)_q (their (2.10)): a finite ℤ-linear combination of
letters, with uniqueness of representation supplied by carrying the representation as data.
Equations
Instances For
Realize a single letter as a degreewise hom on the diagonal complex F₂.obj X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Realize a formal operator as a degreewise hom on F₂.obj X (ℤ-linear extension of
OpLetter.realize).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The derived operator M ↦ M' (EM (2.10)) #
The 0-th-coface shift of a monotone map: 0 ↦ 0, j+1 ↦ θ(j)+1. This is EM's δ⁰
prepending used to define the derived operator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The derived operator on a single letter: prime both SimplexCategory maps.
Equations
Instances For
EM's derived operator M ↦ M' (their (2.10)): prime every letter, ℤ-linearly.
Instances For
Composition of operators (vertical, on the diagonal) #
Composition of letters: comp l₂ l₁ realizes to realize l₁ ≫ realize l₂ (apply l₁ then
l₂). Horizontal and vertical maps compose independently.
Equations
- l₂.comp l₁ = { fst := CategoryTheory.CategoryStruct.comp l₂.fst l₁.fst, snd := CategoryTheory.CategoryStruct.comp l₂.snd l₁.snd }
Instances For
Functoriality / ℤ-linearity of realize #
These let the abstract operator identities (prime_comp_truncBoundary, lastFace_comp_prime,
boundary_comp_D0, …) be pushed to genuine hom identities on F₂.obj X, so the EM induction can
run at the operator level and only be realized at the end.
realize turns operator composition into hom composition (contravariantly: apply M₁ then
M₂). The functoriality fact that drives the operator-level induction. Proved by reducing to the
single-single case (OpLetter.realize_comp) via bilinearity of comp and additivity of
realize.
The identity letter realizes to the identity hom.
Distinguished operators: degeneracy D₀, faces, boundaries #
The 0-th degeneracy operator D₀ = s₀ × s₀ : (K×L)_q → (K×L)_{q+1} of EM (2.13).
Equations
- LeanPool.EilenbergZilber.BisimplicialObject.D0op q = Finsupp.single { fst := SimplexCategory.σ 0, snd := SimplexCategory.σ 0 } 1
Instances For
The i-th face operator F_i = δ_i × δ_i : (K×L)_{q+1} → (K×L)_q.
Equations
- LeanPool.EilenbergZilber.BisimplicialObject.faceOp q i = Finsupp.single { fst := SimplexCategory.δ i, snd := SimplexCategory.δ i } 1
Instances For
The last face F₀ in EM's ∂ = F₀ − ∂' decomposition — here the 0-th face F_0.
Equations
Instances For
The truncated boundary ∂' = Σ_{i≥1} (-1)^{i-1} F_i (the part of the boundary omitting the
0-th face), so that the full boundary is ∂ = F₀ − ∂'.
Equations
- LeanPool.EilenbergZilber.BisimplicialObject.truncBoundaryOp q = ∑ i : Fin (q + 1), (-1) ^ ↑i • LeanPool.EilenbergZilber.BisimplicialObject.faceOp q i.succ
Instances For
The full simplicial boundary operator ∂ = Σ_i (-1)^i F_i : (K×L)_{q+1} → (K×L)_q.
Equations
- LeanPool.EilenbergZilber.BisimplicialObject.boundaryOp q = ∑ i : Fin (q + 2), (-1) ^ ↑i • LeanPool.EilenbergZilber.BisimplicialObject.faceOp q i
Instances For
Frontality #
A SimplexCategory map is frontal if it fixes the bottom vertex 0 (equivalently its
operator word avoids the 0-th face F₀).
Equations
Instances For
An operator is frontal (EM) if every letter in its support is frontal in both variables.
This is the property of derived (primed) operators — primeHom fixes 0, so any M.prime is
frontal in this strong sense (prime_frontal). It is what the homotopy identity (2.3) consumes
(via prime_comp_D0_of_frontal).
Equations
Instances For
The realized operators agree with the chain-complex data #
These tie the formal operators to the actual differentials / maps on F₂.obj X, so the abstract
operator identities below can be transported to statements about Homotopy.comm.
The realized i-th face is the i-th face of the diagonal simplicial object: the
horizontal/vertical legs of ⟨δ i, δ i⟩ reassemble into (diag X).δ i via naturality of
X.map (δ i).op.
The realized boundary operator is the differential of F₂.obj X.
∂ = F₀ − ∂' (EM, just above (2.13)): the full boundary splits as the 0-th face minus the
truncated boundary.
Algebra of the derived operator prime #
prime is additive and multiplicative ((β∘γ)' = β'∘γ'), and on faces it shifts the index
(prime(δ_i) = δ_{i+1}). Consequently EM's truncated boundary is literally the derived operator
of the boundary: ∂' = prime(∂) (prime_boundaryOp). These are exactly what make EM's family
identity ∂'M' = M'∂' hold — it is just prime applied (via prime_comp) to the chain-map
condition ∂M = M∂, with no ad-hoc index juggling. This is why we no longer state a separate
(mis-indexed) prime_comp_truncBoundary.
prime is multiplicative ((β∘γ)' = β'∘γ'), so (M₂ ∘ M₁)' = M₂' ∘ M₁'. The key fact
behind EM's ∂'M' = M'∂'. Reduced to the single–single case OpLetter.prime_comp by bilinearity
of comp and additivity of prime.
primeHom shifts the face map index: prime(δ_i) = δ_{i+1}. The combinatorial core of
prime_faceOp.
primeHom shifts the degeneracy map index: prime(σ_i) = σ_{i+1} (prepending the 0-th vertex
pushes the doubled vertex up by one). The degeneracy analog of primeHom_δ.
∂' = prime(∂) (EM): the truncated boundary is the derived operator of the full boundary.
Note the degree shift — prime of the degree-q boundary is the truncated boundary at degree
q+1 (this is the index offset that the literal EM transcription hides).
Core derived-operator identities (EM I.3, used in the (2.13) induction) #
For a frontal map (θ 0 = 0), the prepended vertex collapses against σ 0:
primeHom θ ≫ σ 0 = σ 0 ≫ θ. The combinatorial core of prime_comp_D0_of_frontal; frontality
is exactly what makes the two sides agree at the bottom vertex.
F₀ M' = M F₀ (EM, Lemma I.3.3): dropping the bottom face commutes with priming. The one
derived-operator/boundary identity that is not a consequence of multiplicativity, since the
outer F₀ is unprimed.
Simplicial identity ∂ D₀ = D₀ ∂' at the operator level.
Writing ∂ = F₀ - ∂', the terms F₀ D₀ and F₁ D₀ both equal the identity, so the remaining
faces assemble to D₀ ∂'.
Killing norms with PInfty #
For the homotopy identity, the relevant norms are the diagonal degenerate terms in D(K×L).
They are detected by postcomposing with
retractionN₂ = PInftyToNormalizedMooreComplex (diag X), which kills diagonal degeneracies of the
diagonal simplicial object.
The lemmas in this section package that kill mechanism in the forms used later by the EM induction.
The realization of a diagonal letter ⟨θ, θ⟩ is the diagonal map (diag X).map θ.op
(realize_faceOp generalized off the face case): the horizontal/vertical legs reassemble by
naturality of X.map θ.op.
A diagonal degeneracy ⟨θ, θ⟩ with θ non-monic is killed by retractionN₂.
Its realization is the diagonal map (diag X).map θ.op, and a non-monic θ is a simplicial
degeneracy, so degeneracy_comp_PInfty applies after factoring PInfty through the Moore
inclusion.
A diagonal degeneracy on the output side kills any composite after retractionN₂.
If M = ⟨θ, θ⟩ ∘ N with θ non-monic, then realize M ≫ retractionN₂ = 0. This is the form
used later, where the norm term is expressed as a diagonal degeneracy postcomposed with an
arbitrary operator.
The Eilenberg–Mac Lane homotopy h = ∇f and the recursion (2.13) #
A single summand of h = ∇f: split q = p + (q - p), apply the AW front/back
faces, then apply one (p, q-p) shuffle. The two eqToHoms transport across
p + (q-p) = q.
Equations
- One or more equations did not get rendered due to their size.
Instances For
h = ∇f as a derived operator: sum over the Alexander-Whitney split and then over
shuffles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Realization of one hLetter summand is the corresponding awComponent ≫ ezComponent shuffle
summand. This is the Pattern-5 merge of the AW front/back faces with the shuffle degeneracies.
hOp realizes to the composite alexanderWhitney ≫ shuffleMap = ∇f on F₂.obj X.
The Eilenberg–Mac Lane homotopy Φ as a derived operator, defined by EM's recursion (2.13):
Φ₀ = 0 and Φ_{q} = − Φ'_{q-1} + h'_{q} D₀ for q > 0. Here Φ_q : (K×L)_q → (K×L)_{q+1}.
Equations
- One or more equations did not get rendered due to their size.
- LeanPool.EilenbergZilber.BisimplicialObject.phiOp 0 = 0
Instances For
Composition of frontal SimplexCategory maps is frontal (0 ↦ 0 ↦ 0).
The zero operator is (vacuously) frontal.
A single frontal letter gives a frontal operator.
Packaging the homotopy on F₂ (raw, modulo norms) #
Φ packaged as a degree-+1 Homotopy.hom family on F₂.obj X (the unnormalized diagonal):
phiOp i realized (transported along j = i+1) on the single nonzero entry, 0 elsewhere.
Equations
- One or more equations did not get rendered due to their size.
Instances For
prevD of phiHomRaw is the realized operator ∂Φ (apply Φ then ∂):
prevD n (phiHomRaw X) = (phiOp n).realize X ≫ (boundaryOp n).realize X.
dNext of phiHomRaw (at n+1) is the realized operator Φ∂ (apply ∂ then Φ):
dNext (n+1) (phiHomRaw X) = (boundaryOp n).realize X ≫ (phiOp n).realize X.
The identity operator i = 𝟙 × 𝟙 : (K×L)_q → (K×L)_q (EM's i). Realizes to 𝟙
(realize_single_id).
Equations
- LeanPool.EilenbergZilber.BisimplicialObject.idOp q = Finsupp.single { fst := CategoryTheory.CategoryStruct.id { len := q }, snd := CategoryTheory.CategoryStruct.id { len := q } } 1
Instances For
Abstract properties of h = ∇f used by the EM induction #
From this point on, the induction uses hOp only through formal operator identities, not by
unfolding its explicit summands.
The represented simplicial type Δ[s] : b ↦ (⦋b⦌ ⟶ ⦋s⦌) (the SimplexCategory Yoneda).
Equations
Instances For
The bi-represented bisimplicial type at (s, s): (a, b) ↦ (⦋a⦌ ⟶ ⦋s⦌) × (⦋b⦌ ⟶ ⦋s⦌),
the horizontal map acting on the first factor and the vertical on the second.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Postcompose a (bi)simplicial type with the free ℤ-module functor.
Equations
Instances For
A universal bisimplicial object detecting all derived operators out of degree s:
the free ℤ-module on the bi-represented bisimplicial set at (s, s). Realizing a derived
operator against it recovers it as a Finsupp, so realize (univOp s) is injective
(realize_univOp_injective).
Equations
Instances For
realize against the universal object is injective: a derived operator is determined by
its realization on univOp. This is the faithfulness principle that lets us deduce formal
DerivedOp identities from their (realized) chain-level counterparts.
∂ h = h ∂ (EM line 155, ∂*h' = h'∂*). h = ∇f is a chain map, so boundaryOp commutes
with hOp. Proof: realize against the universal object is injective, and on the realized side
this is just the chain-map condition comm of alexanderWhitney ≫ shuffleMap.
F₀ h' = h F₀ (EM, Lemma I.3.3). Just lastFace_comp_prime specialized to hOp.
Base degree: hOp 0 agrees with the identity after postcomposing with retractionN₂.
Exact-identity backbone for the EM induction #
The induction is organized at the formal DerivedOp level. We encode the error term
Φ∂ + ∂Φ + i - h as a structural norm class IsNorm, prove that this class is closed under
prime, and only at the end convert structural norms into vanishing statements after
postcomposing with retractionN₂.
Structural norm class for diagonal degeneracies, closed under + and neg.
The point of this definition is that closure under prime is formal, so the induction can be run
before realizing operators on a bisimplicial object.
- zero {s q : ℕ} : IsNorm 0
- add {s q : ℕ} {M N : DerivedOp s q} : IsNorm M → IsNorm N → IsNorm (M + N)
- neg {s q : ℕ} {M : DerivedOp s q} : IsNorm M → IsNorm (-M)
- diagDegen {r s q : ℕ} (θ : { len := q } ⟶ { len := s }) (hθ : ¬CategoryTheory.Mono θ) (N : DerivedOp r s) : IsNorm (DerivedOp.comp (Finsupp.single { fst := θ, snd := θ } 1) N)
Instances For
prime of a diagonal letter ⟨θ,θ⟩ is the diagonal of primeHom θ.
primeHom preserves non-monicity: primeHom θ is injective iff θ is, and Mono in
SimplexCategory is injectivity.
prime fixes the identity map: primeHom 𝟙 = 𝟙 (0 ↦ 0, j+1 ↦ 𝟙(j)+1 = j+1).
F₀ D₀ = i (δ_0 ≫ σ_0 = 𝟙): the last face undoes the 0-th degeneracy. Repackages the
existing face_zero_comp_D0 (lastFaceOp = faceOp _ 0).
Right unit for DerivedOp.comp: M ∘ i = M (l ≫ 𝟙 = l in each coordinate).
F₀ h' D₀ = h (EM line 192). F₀ h' D₀ = (h F₀) D₀ = h (F₀ D₀) = h, using
lastFace_comp_hPrime and F₀ D₀ = i (δ_0 ≫ σ_0 = 𝟙).
EM (2.12): f and ∇ preserve norms ⟹ h = ∇f preserves norms #
EM (2.12) is a composition fact: f = AW and ∇ = shuffleMap each carry the (diagonal)
degenerate subcomplex into the (bi-)degenerate subcomplex, so h = ∇f does too. The two halves are
genuine Dold–Kan combinatorial inputs (Phase-4-level); the composite h-statement then follows
for free via realize_hOp.
∇-half (6b):retractionN₁_inclusionN₁_shuffleMap_retractionN₂— a degenerate-F₁element (image of1 − retractionN₁ ≫ inclusionN₁) is sent by∇to a degenerate diagonal element, killed byretractionN₂.f-half:alexanderWhitney_diagDegen_comp_retractionN₁— a diagonal degeneracy⟨θ,θ⟩followed byAWlands in the degenerate part ofF₁, killed byretractionN₁.
PInfty of the diagonal in degree n, typed on the (n, n) entry of X.
Equations
Instances For
EZ–degeneracy kill, inner (vertical) direction (the per-summand combinatorial core).
A (p, m+1)-shuffle component of a chain that is degenerate in the inner simplicial direction
(in the image of the inner degeneracy s_i = (X_⦋p⦌).map (σ i).op : X_{p,m} → X_{p,m+1}) is sent by
the Eilenberg–Zilber component to a diagonally degenerate chain, hence annihilated by PInfty.
EM Lemma I.5.3 content: ∇ ∘ (1 ⊗ s_i) = s_? ∘ ∇' lands in a diagonal degeneracy.
EZ–degeneracy kill, outer (horizontal) direction (the per-summand combinatorial core).
An (a+1, q)-shuffle component of a chain that is degenerate in the outer simplicial direction
(in the image of the outer degeneracy s_i = (X.map (σ i).op).app ⦋q⦌ : X_{a,q} → X_{a+1,q})
is sent
by the Eilenberg–Zilber component to a diagonally degenerate chain, hence annihilated by PInfty.
EM Lemma I.5.3 content: ∇ ∘ (s_i ⊗ 1) = s_? ∘ ∇' lands in a diagonal degeneracy.
The degenerate part of F₁ is sent by shuffleMap to a diagonal degeneracy, hence is killed by
PInfty.
Concretely, after decomposing the complementary projector
𝟙 - retractionN₁ ≫ inclusionN₁ bidegreewise, the resulting inner- and outer-degenerate pieces are
annihilated by ezComponent_inner_degeneracy_comp_PInfty and
ezComponent_outer_degeneracy_comp_PInfty.
The round trip retractionN₁ ≫ inclusionN₁ is absorbed under shuffleMap ≫ PInfty.
The correction term 1 - retractionN₁ ≫ inclusionN₁ lands in the degenerate part of the diagonal,
which PInfty kills.
The round trip retractionN₁ ≫ inclusionN₁ is absorbed under shuffleMap ≫ PInfty.
The correction term 1 - retractionN₁ ≫ inclusionN₁ lands in the degenerate part of the diagonal,
which PInfty kills.
The corresponding absorption identity after replacing PInfty by retractionN₂.
The corresponding absorption identity after replacing PInfty by retractionN₂.
Every norm dies under retractionN₂ (for every X). Structural induction: linear cases are
realize-linearity; the two generators are the (2)-diagonal kill and EM (2.12).
Base case for the exact induction: the degree-1 error term is a norm.
The error term Φ∂ + ∂Φ + i - h satisfies the same prime recursion as Φ.
After rewriting ∂ = F₀ - ∂' and Φ = -Φ' + h' D₀, the remaining identity is a formal operator
calculation using lastFace_comp_prime, boundaryOp_comp_hOp, and boundary_comp_D0.
Operator-level form of the EM homotopy identity, modulo norms.
This is the realized statement corresponding to Φ∂ + ∂Φ + i ≡ h, obtained by killing the
structural norm term from phi_op_isNorm with retractionN₂.
EM's homotopy identity ∂Φ + Φ∂ = ∇f - i, after postcomposing with retractionN₂.
Descent to the normalized diagonal N₂ #
The normalized Moore complex N₂ is a retract of F₂: inclusionN₂ ≫ retractionN₂ = 𝟙.
The normalized Moore complex N₂ is a retract of F₂: inclusionN₂ ≫ retractionN₂ = 𝟙.
Φ conjugated onto the normalized diagonal N₂.obj X (EM's homotopy on K ×_N L):
inclusionN₂ ≫ phiOp.realize ≫ retractionN₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
phiHomNorm is the conjugate of phiHomRaw by inclusionN₂ … retractionN₂.
dNext commutes with the inclusionN₂ … retractionN₂ conjugation (both are chain maps).
prevD commutes with the inclusionN₂ … retractionN₂ conjugation (both are chain maps).
(6b) The normalized AW ≫ ∇ is the N₂-conjugate of the unnormalized AW ≫ ∇.
Unfolding the definitions, normalizedAlexanderWhitney ≫ normalizedShuffleMap
= ι₂ ≫ AW ≫ (retractionN₁ ≫ inclusionN₁) ≫ ∇ ≫ ρ₂; the inner Dold–Kan round-trip
retractionN₁ ≫ inclusionN₁ (the PInfty idempotent on F₁) is absorbed, leaving
ι₂ ≫ (AW ≫ ∇) ≫ ρ₂.
AW ≫ ∇ ≃ 𝟙 on the normalized diagonal N₂ via the Eilenberg–Mac Lane homotopy Φ
(EM Thm 2.1a, ∂Φ + Φ∂ = ∇f − i). This is the contraction homotopy used by
eilenbergZilberNormalized (BisimplicialNormalized.lean).
Equations
- X.homotopyAWShuffleNormalized = { hom := X.phiHomNorm, zero := ⋯, comm := ⋯ }