Alexander–Whitney and shuffle maps for bisimplicial objects

For a bisimplicial object X in an abelian category C, this file compares the total complex F₁(X) of the double complex of alternating face maps with the alternating face map complex F₂(X) of the diagonal. It defines the Alexander–Whitney map F₂(X) ⟶ F₁(X) and the shuffle (Eilenberg–Zilber) map F₁(X) ⟶ F₂(X), proves that the shuffle map is a chain map via the boundary formula for its components, and computes alexanderWhitney ≫ shuffleMap degreewise (it is the identity in degree 0). It also sets up the normalized complexes N₁(X) and N₂(X) together with their inclusions and retractions.

@[reducible, inline]

abbrev LeanPool.EilenbergZilber.BisimplicialObject (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] : Type (max u_1 v_1)

A bisimplicial object in C: a simplicial object in simplicial objects in C.

Equations

• LeanPool.EilenbergZilber.BisimplicialObject C = CategoryTheory.SimplicialObject (CategoryTheory.SimplicialObject C)

def LeanPool.EilenbergZilber.BisimplicialObject.diag {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] : CategoryTheory.Functor (BisimplicialObject C) (CategoryTheory.SimplicialObject C)

The diagonal simplicial object [n] ↦ X_{n,n} of a bisimplicial object.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanPool.EilenbergZilber.BisimplicialObject.diag_obj_obj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : BisimplicialObject C) (X✝ : SimplexCategoryᵒᵖ) : (diag.obj X).obj X✝ = (X.obj X✝).obj X✝

@[simp]

theorem LeanPool.EilenbergZilber.BisimplicialObject.diag_obj_map {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : BisimplicialObject C) {X✝ Y✝ : SimplexCategoryᵒᵖ} (f : X✝ ⟶ Y✝) : (diag.obj X).map f = CategoryTheory.CategoryStruct.comp ((X.map f).app X✝) ((X.obj Y✝).map f)

@[simp]

theorem LeanPool.EilenbergZilber.BisimplicialObject.diag_map_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X✝ Y✝ : BisimplicialObject C} (f : X✝ ⟶ Y✝) (X : SimplexCategoryᵒᵖ) : (diag.map f).app X = (f.app X).app X

@[instance_reducible]

noncomputable instance LeanPool.EilenbergZilber.BisimplicialObject.instAbelianSimplicialObject {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Abelian (CategoryTheory.SimplicialObject C)

Equations

• LeanPool.EilenbergZilber.BisimplicialObject.instAbelianSimplicialObject = CategoryTheory.Abelian.functorCategoryAbelian

instance LeanPool.EilenbergZilber.BisimplicialObject.instAdditiveSimplicialObjectChainComplexNatAlternatingFaceMapComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : (AlgebraicTopology.alternatingFaceMapComplex C).Additive

instance LeanPool.EilenbergZilber.BisimplicialObject.instHasTotalNatDown {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : ChainComplex (ChainComplex C ℕ) ℕ) : HomologicalComplex₂.HasTotal K (ComplexShape.down ℕ)

@[reducible, inline]

noncomputable abbrev LeanPool.EilenbergZilber.BisimplicialObject.F₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (BisimplicialObject C) (ChainComplex C ℕ)

The total complex of the double complex obtained by taking alternating face map complexes in both simplicial directions.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LeanPool.EilenbergZilber.BisimplicialObject.F₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (BisimplicialObject C) (ChainComplex C ℕ)

The alternating face map complex of the diagonal simplicial object.

Equations

• LeanPool.EilenbergZilber.BisimplicialObject.F₂ = LeanPool.EilenbergZilber.BisimplicialObject.diag.comp (AlgebraicTopology.alternatingFaceMapComplex C)

@[reducible, inline]

noncomputable abbrev LeanPool.EilenbergZilber.BisimplicialObject.doubleComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : HomologicalComplex (ChainComplex C ℕ) (ComplexShape.down ℕ)

The double complex obtained by applying alternatingFaceMapComplex in both simplicial directions. Its (p, q) entry is X_{p,q}.

Equations

• One or more equations did not get rendered due to their size.

Basic simplicial maps

The Alexander-Whitney and shuffle maps are built from the standard front and back inclusions ιFront and ιBack.

def LeanPool.EilenbergZilber.BisimplicialObject.ιFront (p q : ℕ) : { len := p } ⟶ { len := p + q }

Front face inclusion [p] ⟶ [p+q]: the unique monotone map sending i ↦ i.

Equations

• LeanPool.EilenbergZilber.BisimplicialObject.ιFront p q = SimplexCategory.mkHom { toFun := fun (i : Fin (p + 1)) => ⟨↑i, ⋯⟩, monotone' := ⋯ }

def LeanPool.EilenbergZilber.BisimplicialObject.ιBack (p q : ℕ) : { len := q } ⟶ { len := p + q }

Back face inclusion [q] ⟶ [p+q]: the unique monotone map sending j ↦ p + j.

Equations

• LeanPool.EilenbergZilber.BisimplicialObject.ιBack p q = SimplexCategory.mkHom { toFun := fun (j : Fin (q + 1)) => ⟨p + ↑j, ⋯⟩, monotone' := ⋯ }

theorem LeanPool.EilenbergZilber.BisimplicialObject.ιFront_comp_δ_of_le (p q : ℕ) (k : Fin (p + q + 2)) (hk : ↑k ≤ p) : CategoryTheory.CategoryStruct.comp (ιFront p q) (SimplexCategory.δ k) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ ⟨↑k, ⋯⟩) (CategoryTheory.CategoryStruct.comp (ιFront (p + 1) q) (CategoryTheory.eqToHom ⋯))

ιFront(p, q) ≫ δ k = δ k ≫ ιFront(p+1, q) when k ≤ p, i.e., the face map acts within the front range. Here δ k on the left is [p+q] → [p+q+1] and δ k on the right is [p] → [p+1].

theorem LeanPool.EilenbergZilber.BisimplicialObject.ιFront_comp_δ_of_gt (p q : ℕ) (k : Fin (p + q + 2)) (hk : p < ↑k) : CategoryTheory.CategoryStruct.comp (ιFront p q) (SimplexCategory.δ k) = CategoryTheory.CategoryStruct.comp (ιFront p (q + 1)) (CategoryTheory.eqToHom ⋯)

ιFront(p, q) ≫ δ k = ιFront(p, q+1) when k > p, i.e., the face map acts beyond the front range — all front vertices stay below the skipped index.

theorem LeanPool.EilenbergZilber.BisimplicialObject.ιBack_comp_δ_of_le (p q : ℕ) (k : Fin (p + q + 2)) (hk : ↑k ≤ p) : CategoryTheory.CategoryStruct.comp (ιBack p q) (SimplexCategory.δ k) = CategoryTheory.CategoryStruct.comp (ιBack (p + 1) q) (CategoryTheory.eqToHom ⋯)

ιBack(p, q) ≫ δ k = ιBack(p+1, q) when k ≤ p, i.e., the face map acts before the back range — all back vertices shift by one.

theorem LeanPool.EilenbergZilber.BisimplicialObject.ιBack_comp_δ_of_gt (p q : ℕ) (k : Fin (p + q + 2)) (hk : p < ↑k) : CategoryTheory.CategoryStruct.comp (ιBack p q) (SimplexCategory.δ k) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ ⟨↑k - p, ⋯⟩) (CategoryTheory.CategoryStruct.comp (ιBack p (q + 1)) (CategoryTheory.eqToHom ⋯))

ιBack(p, q) ≫ δ k = δ (k - p) ≫ ιBack(p, q+1) when k > p, i.e., the face map acts within the back range. Here δ (k-p) is the face map on [q].

Alexander-Whitney map

The Alexander-Whitney map F₂(X) ⟶ F₁(X) sends the diagonal chain complex to the total complex by copairing the component maps awComponent X p q over all decompositions p + q = n.

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.awComponent {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : BisimplicialObject C) (p q : ℕ) : (X.obj (Opposite.op { len := p + q })).obj (Opposite.op { len := p + q }) ⟶ (X.obj (Opposite.op { len := p })).obj (Opposite.op { len := q })

The (p, q) component of the Alexander-Whitney map.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.alexanderWhitney {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : F₂.obj X ⟶ F₁.obj X

The Alexander-Whitney chain map F₂(X) ⟶ F₁(X).

Equations

• One or more equations did not get rendered due to their size.

Shuffle map

The shuffle map F₁(X) ⟶ F₂(X) is defined on each bidegree (p, q) by the signed sum over (p, q)-shuffles, and then assembled with totalDesc.

def LeanPool.EilenbergZilber.BisimplicialObject.shuffleFstHom {p q : ℕ} (μ : Shuffle p q) : { len := p + q } ⟶ { len := p }

First projection of a shuffle as a SimplexCategory morphism ⦋p+q⦌ ⟶ ⦋p⦌.

Equations

• LeanPool.EilenbergZilber.BisimplicialObject.shuffleFstHom μ = SimplexCategory.Hom.mk (OrderHom.fst.comp ↑μ)

def LeanPool.EilenbergZilber.BisimplicialObject.shuffleSndHom {p q : ℕ} (μ : Shuffle p q) : { len := p + q } ⟶ { len := q }

Second projection of a shuffle as a SimplexCategory morphism ⦋p+q⦌ ⟶ ⦋q⦌.

Equations

• LeanPool.EilenbergZilber.BisimplicialObject.shuffleSndHom μ = SimplexCategory.Hom.mk (OrderHom.snd.comp ↑μ)

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.ezComponent {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) (p q : ℕ) : (X.obj (Opposite.op { len := p })).obj (Opposite.op { len := q }) ⟶ (X.obj (Opposite.op { len := p + q })).obj (Opposite.op { len := p + q })

The (p, q) component of the shuffle map.

Equations

• One or more equations did not get rendered due to their size.

Boundary formula for the shuffle components

The chain map condition for shuffleMap is reduced to a componentwise identity for ezComponent: composing with the diagonal differential splits into the expected vertical and horizontal boundary terms.

theorem LeanPool.EilenbergZilber.BisimplicialObject.fstHom_insertLeftStep_comp_δ {p q n : ℕ} (ν : Shuffle p q) (j : Fin (p + 2)) (hn : n + 1 = p + 1 + q) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.cast ⋯ (ν.insertLeftIndex j))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (shuffleFstHom (ν.insertLeftStep j))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (shuffleFstHom ν) (SimplexCategory.δ j))

Left insertion face factorization (fst component): δ_{insertLeftIndex} ≫ eqToHom ≫ fstHom(insertLeftStep ν j) = fstHom(ν) ≫ δ(j).

theorem LeanPool.EilenbergZilber.BisimplicialObject.sndHom_insertRightStep_comp_δ {p q n : ℕ} (ν : Shuffle p q) (k : Fin (q + 2)) (hn : n + 1 = p + (q + 1)) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.cast ⋯ (ν.insertRightIndex k))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (shuffleSndHom (ν.insertRightStep k))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (shuffleSndHom ν) (SimplexCategory.δ k))

Right insertion face factorization (snd component): δ_{insertRightIndex} ≫ eqToHom ≫ sndHom(insertRightStep ν k) = sndHom(ν) ≫ δ(k).

theorem LeanPool.EilenbergZilber.BisimplicialObject.fstHom_swapDiagonalSteps_comp_δ {p q n : ℕ} (μ : Shuffle p q) (r : Fin (n + 2)) (hn : n + 1 = p + q) (h : μ.isDiagonalVertex (Fin.cast ⋯ r)) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ r) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (shuffleFstHom (μ.swapDiagonalSteps (Fin.cast ⋯ r) h))) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ r) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (shuffleFstHom μ))

Composing δ r ≫ eqToHom ≫ shuffleFstHom of swapDiagonalSteps μ gives the same result as for μ, because δ r maps via succAbove r which avoids vertex r, and swapDiagonalSteps only changes the value at r.

theorem LeanPool.EilenbergZilber.BisimplicialObject.sndHom_swapDiagonalSteps_comp_δ {p q n : ℕ} (μ : Shuffle p q) (r : Fin (n + 2)) (hn : n + 1 = p + q) (h : μ.isDiagonalVertex (Fin.cast ⋯ r)) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ r) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (shuffleSndHom (μ.swapDiagonalSteps (Fin.cast ⋯ r) h))) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ r) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (shuffleSndHom μ))

theorem LeanPool.EilenbergZilber.BisimplicialObject.ezComponent_boundary {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) (p q j : ℕ) (h : (ComplexShape.down ℕ).Rel (p + q) j) : CategoryTheory.CategoryStruct.comp (X.ezComponent p q) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (((AlgebraicTopology.alternatingFaceMapComplex C).obj (diag.obj X)).d (p + q) j)) = (match p, h with | 0, h => 0 | p'.succ, h => ∑ k : Fin (p' + 2), (-1) ^ ↑k • CategoryTheory.CategoryStruct.comp ((X.map (SimplexCategory.δ k).op).app (Opposite.op { len := q })) (CategoryTheory.CategoryStruct.comp (X.ezComponent p' q) (CategoryTheory.eqToHom ⋯))) + match q, h with | 0, h => 0 | q'.succ, h => (-1) ^ p • ∑ k : Fin (q' + 2), (-1) ^ ↑k • CategoryTheory.CategoryStruct.comp ((X.obj (Opposite.op { len := p })).map (SimplexCategory.δ k).op) (CategoryTheory.CategoryStruct.comp (X.ezComponent p q') (CategoryTheory.eqToHom ⋯))

Boundary formula for ezComponent.

Composing ezComponent X p q with the diagonal differential splits into the vertical boundary term coming from the first simplicial direction and the horizontal boundary term coming from the second. The differential is written as .d rather than objD to avoid index-cast noise.

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.shuffleMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : F₁.obj X ⟶ F₂.obj X

The shuffle chain map F₁(X) ⟶ F₂(X).

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.EilenbergZilber.BisimplicialObject.alexanderWhitney_comp_shuffleMap_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) (q : ℕ) : (CategoryTheory.CategoryStruct.comp X.alexanderWhitney X.shuffleMap).f q = ∑ p : Fin (q + 1), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (X.awComponent (↑p) (q - ↑p)) (CategoryTheory.CategoryStruct.comp (X.ezComponent (↑p) (q - ↑p)) (CategoryTheory.eqToHom ⋯)))

Degreewise formula for alexanderWhitney ≫ shuffleMap.

theorem LeanPool.EilenbergZilber.BisimplicialObject.awShuffle_f_zero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : (CategoryTheory.CategoryStruct.comp X.alexanderWhitney X.shuffleMap).f 0 = (CategoryTheory.CategoryStruct.id (F₂.obj X)).f 0

In degree 0, the composite alexanderWhitney ≫ shuffleMap is the identity.

instance LeanPool.EilenbergZilber.BisimplicialObject.instAdditiveSimplicialObjectChainComplexNatNormalizedMooreComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : (AlgebraicTopology.normalizedMooreComplex C).Additive

@[reducible, inline]

noncomputable abbrev LeanPool.EilenbergZilber.BisimplicialObject.N₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (BisimplicialObject C) (ChainComplex C ℕ)

The bi-normalized total complex: normalize both simplicial directions (via the normalized Moore complex), then take the total complex. The normalized analogue of F₁.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev LeanPool.EilenbergZilber.BisimplicialObject.N₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (BisimplicialObject C) (ChainComplex C ℕ)

The normalized Moore complex of the diagonal. The normalized analogue of F₂.

Equations

• LeanPool.EilenbergZilber.BisimplicialObject.N₂ = LeanPool.EilenbergZilber.BisimplicialObject.diag.comp (AlgebraicTopology.normalizedMooreComplex C)

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.mooreInclusion {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : AlgebraicTopology.normalizedMooreComplex C ⟶ AlgebraicTopology.alternatingFaceMapComplex C

The Moore inclusion N[-] ⟶ K[-] packaged as a natural transformation. Needed to lift the inner-direction normalization through mapHomologicalComplex.

Equations

• LeanPool.EilenbergZilber.BisimplicialObject.mooreInclusion = { app := fun (Y : CategoryTheory.SimplicialObject C) => AlgebraicTopology.inclusionOfMooreComplexMap Y, naturality := ⋯ }

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.mooreRetraction {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : AlgebraicTopology.alternatingFaceMapComplex C ⟶ AlgebraicTopology.normalizedMooreComplex C

The Dold–Kan retraction K[-] ⟶ N[-] (via PInfty) as a natural transformation.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.EilenbergZilber.BisimplicialObject.mooreInclusion_comp_mooreRetraction {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.CategoryStruct.comp mooreInclusion mooreRetraction = CategoryTheory.CategoryStruct.id (AlgebraicTopology.normalizedMooreComplex C)

The Moore inclusion is a section of the Dold–Kan retraction.

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.inclusionN₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : N₁.obj X ⟶ F₁.obj X

Inclusion N₁ ↪ F₁ of the bi-normalized total complex into the unnormalized total complex, obtained by including both simplicial directions (inclusionOfMooreComplexMap outer, mooreInclusion inner) and totalizing.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.retractionN₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : F₁.obj X ⟶ N₁.obj X

Retraction F₁ ↠ N₁ onto the bi-normalized total complex (via PInfty in both directions).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.inclusionN₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : N₂.obj X ⟶ F₂.obj X

Inclusion N₂ ↪ F₂ for the diagonal (the Moore inclusion).

Equations

• X.inclusionN₂ = AlgebraicTopology.inclusionOfMooreComplexMap (LeanPool.EilenbergZilber.BisimplicialObject.diag.obj X)

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.retractionN₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : F₂.obj X ⟶ N₂.obj X

Retraction F₂ ↠ N₂ for the diagonal (the PInfty retraction).

Equations

• X.retractionN₂ = AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex (LeanPool.EilenbergZilber.BisimplicialObject.diag.obj X)

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.normalizedShuffleMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : N₁.obj X ⟶ N₂.obj X

The shuffle map on normalized complexes, ∇ : N₁ → N₂.

Option 3: the unnormalized shuffleMap conjugated by the Dold–Kan inclusion N₁ ↪ F₁ and the retraction F₂ ↠ N₂, so it is levelwise-concrete.

Equations

• X.normalizedShuffleMap = CategoryTheory.CategoryStruct.comp X.inclusionN₁ (CategoryTheory.CategoryStruct.comp X.shuffleMap X.retractionN₂)

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.normalizedAlexanderWhitney {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : N₂.obj X ⟶ N₁.obj X

The Alexander–Whitney map on normalized complexes, AW : N₂ → N₁.

Option 3: the unnormalized alexanderWhitney conjugated by the Dold–Kan inclusion N₂ ↪ F₂ and the retraction F₁ ↠ N₁, so it is levelwise-concrete.

Equations

• X.normalizedAlexanderWhitney = CategoryTheory.CategoryStruct.comp X.inclusionN₂ (CategoryTheory.CategoryStruct.comp X.alexanderWhitney X.retractionN₁)