Normalized Eilenberg–Zilber for bisimplicial objects #
The literature (Eilenberg–Mac Lane II, Thm 2.1a) proves the Eilenberg–Zilber contraction on the
normalized complexes, where one direction is a strict identity and the other is a chain
homotopy via the explicit Eilenberg–Mac Lane homotopy. We assemble that here on the bi-normalized
total complex N₁ and the normalized Moore complex of the diagonal N₂ (both defined in
Bisimplicial.lean).
This normalized equivalence is then transported to the unnormalized F₁/F₂
(in Bisimplicial.lean) along the normalization comparisons
normalizationComparison and diagonalNormalizationComparison,
to obtain eilenbergZilber : HomotopyEquiv (F₁.obj X) (F₂.obj X).
Glue (split mono, lifted to the total complex). The bi-normalized inclusion is a section
of the retraction. This lifts the Mathlib split-mono identity (splitMonoInclusionOfMooreComplexMap _).id through totalFunctor in both simplicial directions. (Reused by
normalizationComparison.)
Glue (split mono, lifted to the total complex). The bi-normalized inclusion is a section
of the retraction. This lifts the Mathlib split-mono identity (splitMonoInclusionOfMooreComplexMap _).id through totalFunctor in both simplicial directions. (Reused by
normalizationComparison.)
(B) ∇ preserves normalization (EM Lemma I.5.3). Precomposed with the bi-normalized
inclusion, the shuffle map already lands in the normalized diagonal, so the diagonal
renormalization round-trip retractionN₂ ≫ inclusionN₂ (which equals PInfty) is a no-op.
@[reassoc] so it rewrites underneath the trailing alexanderWhitney ≫ retractionN₁.
(B) ∇ preserves normalization (EM Lemma I.5.3). Precomposed with the bi-normalized
inclusion, the shuffle map already lands in the normalized diagonal, so the diagonal
renormalization round-trip retractionN₂ ≫ inclusionN₂ (which equals PInfty) is a no-op.
@[reassoc] so it rewrites underneath the trailing alexanderWhitney ≫ retractionN₁.
A-diag: the diagonal Eilenberg–MacLane identity. On the diagonal (p,q) = (r,m) the
shuffle/Alexander–Whitney pairing ezComponent ≫ awComponent is the identity plus degenerate
cross-terms; the bi-normalized retraction component R' (the Dold–Kan PInfty projection in
both simplicial directions, taken at bidegree (r,m)) annihilates the degenerate part, so
ez ≫ aw ≫ R' = R'. Non-staircase summands vanish via ezawSummand_merge, the combinatorial
non-mono front face, and the outer kill lemma. This is the combinatorial heart of
(A).
(A) EM f∇ = i modulo norms. Unnormalized, shuffleMap ≫ alexanderWhitney = 𝟙 + D with
D landing in the degenerate subcomplex; the bi-normalized retraction retractionN₁ annihilates
D, leaving retractionN₁. The combinatorial core is the shuffle pairing
ezComponent ≫ awComponent (diagonal (r,s) = (p,q) ↦ identity; off-diagonal ↦ degenerate).
EM Thm 2.1a, first half (f∇ = i). On normalized complexes the composite ∇ ≫ AW
is the identity strictly — the degenerate cross-terms that obstruct this on the unnormalized
complex vanish modulo norms.
Eilenberg–Zilber theorem on normalized complexes (Eilenberg–Mac Lane II, Thm 2.1a). The bi-normalized total complex is homotopy equivalent to the normalized Moore complex of the diagonal. One direction is a strict identity; the other uses the EM homotopy.
Equations
- X.eilenbergZilberNormalized = { hom := X.normalizedShuffleMap, inv := X.normalizedAlexanderWhitney, homotopyHomInvId := Homotopy.ofEq ⋯, homotopyInvHomId := X.homotopyAWShuffleNormalized }
Instances For
The normalization comparison on the diagonal simplicial object.
Equations
Instances For
The unnormalized Eilenberg–Zilber homotopy equivalence F₁(X) ≃ F₂(X), obtained by
transporting the normalized equivalence eilenbergZilberNormalized across the normalization
comparisons:
F₁(X) ≃ N₁(X) ≃ N₂(X) ≃ F₂(X),
where normalizationComparison is the inner/outer Moore normalization of the total complex
(BisimplicialNormalizationComparison),
and diagonalNormalizationComparison is the corresponding comparison for the diagonal simplicial
object.