The normalization comparison equivalence

This file constructs the homotopy equivalence normalizationComparison : HomotopyEquiv (N₁.obj X) (F₁.obj X) used in the normalized Eilenberg-Zilber argument.

The construction is factored as

N₁(X) ≃ M₁(X) ≃ F₁(X),

where M₁ is outer-unnormalized and inner-normalized.

@[instance_reducible]

instance LeanPool.EilenbergZilber.instTotalComplexShapeSymmetryNatDown : TotalComplexShapeSymmetry (ComplexShape.down ℕ) (ComplexShape.down ℕ) (ComplexShape.down ℕ)

The symmetry of the total complex shape on ChainComplex _ ℕ bicomplexes, with respect to the canonical TotalComplexShape (down ℕ) (down ℕ) (down ℕ). The sign σ i₁ i₂ = (-1)^(i₁ * i₂) (written via the alternating sign ε) is exactly what is needed for the flip symmetry HomologicalComplex₂.totalFlipIso. Mirrors the up ℤ instance in Mathlib.

Equations

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

@[reducible, inline]

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

The intermediate total complex: outer unnormalized and inner normalized.

Equations

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

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

The outer normalization inclusion N₁(X) ⟶ M₁(X).

Equations

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

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

The outer normalization retraction M₁(X) ⟶ N₁(X).

Equations

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

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

The inner normalization inclusion M₁(X) ⟶ F₁(X).

Equations

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

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

The inner normalization retraction F₁(X) ⟶ M₁(X).

Equations

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

theorem LeanPool.EilenbergZilber.BisimplicialObject.inclusionM₁_comp_inclusionF₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : CategoryTheory.CategoryStruct.comp X.inclusionM₁ X.inclusionF₁ = X.inclusionN₁

theorem LeanPool.EilenbergZilber.BisimplicialObject.inclusionM₁_comp_inclusionF₁_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) {Z : ChainComplex C ℕ} (h : (HomologicalComplex₂.totalFunctor C (ComplexShape.down ℕ) (ComplexShape.down ℕ) (ComplexShape.down ℕ)).obj (((AlgebraicTopology.alternatingFaceMapComplex C).mapHomologicalComplex (ComplexShape.down ℕ)).obj ((AlgebraicTopology.alternatingFaceMapComplex (CategoryTheory.SimplicialObject C)).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp X.inclusionM₁ (CategoryTheory.CategoryStruct.comp X.inclusionF₁ h) = CategoryTheory.CategoryStruct.comp X.inclusionN₁ h

theorem LeanPool.EilenbergZilber.BisimplicialObject.retractionF₁_comp_retractionM₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : CategoryTheory.CategoryStruct.comp X.retractionF₁ X.retractionM₁ = X.retractionN₁

theorem LeanPool.EilenbergZilber.BisimplicialObject.retractionF₁_comp_retractionM₁_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) {Z : ChainComplex C ℕ} (h : (HomologicalComplex₂.totalFunctor C (ComplexShape.down ℕ) (ComplexShape.down ℕ) (ComplexShape.down ℕ)).obj (((AlgebraicTopology.normalizedMooreComplex C).mapHomologicalComplex (ComplexShape.down ℕ)).obj ((AlgebraicTopology.normalizedMooreComplex (CategoryTheory.SimplicialObject C)).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp X.retractionF₁ (CategoryTheory.CategoryStruct.comp X.retractionM₁ h) = CategoryTheory.CategoryStruct.comp X.retractionN₁ h

theorem LeanPool.EilenbergZilber.BisimplicialObject.inclusionM₁_comp_retractionM₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : CategoryTheory.CategoryStruct.comp X.inclusionM₁ X.retractionM₁ = CategoryTheory.CategoryStruct.id (N₁.obj X)

theorem LeanPool.EilenbergZilber.BisimplicialObject.inclusionM₁_comp_retractionM₁_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) {Z : ChainComplex C ℕ} (h : (HomologicalComplex₂.totalFunctor C (ComplexShape.down ℕ) (ComplexShape.down ℕ) (ComplexShape.down ℕ)).obj (((AlgebraicTopology.normalizedMooreComplex C).mapHomologicalComplex (ComplexShape.down ℕ)).obj ((AlgebraicTopology.normalizedMooreComplex (CategoryTheory.SimplicialObject C)).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp X.inclusionM₁ (CategoryTheory.CategoryStruct.comp X.retractionM₁ h) = h

theorem LeanPool.EilenbergZilber.BisimplicialObject.inclusionF₁_comp_retractionF₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : CategoryTheory.CategoryStruct.comp X.inclusionF₁ X.retractionF₁ = CategoryTheory.CategoryStruct.id X.M₁

theorem LeanPool.EilenbergZilber.BisimplicialObject.inclusionF₁_comp_retractionF₁_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) {Z : ChainComplex C ℕ} (h : X.M₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp X.inclusionF₁ (CategoryTheory.CategoryStruct.comp X.retractionF₁ h) = h

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.HomologicalComplex₂.totalMapHomotopyHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c : ComplexShape J} [DecidableEq J] [TotalComplexShape c₁ c₂ c] {K L : HomologicalComplex₂ C c₁ c₂} [K.HasTotal c] [L.HasTotal c] {φ ψ : K ⟶ L} (h : Homotopy φ ψ) (j j' : J) : (K.total c).X j ⟶ (L.total c).X j'

The components (K.total c).X j ⟶ (L.total c).X j' of the homotopy on total complexes induced by a homotopy h between maps of bicomplexes that is homotopic in the first direction.

Equations

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

theorem LeanPool.EilenbergZilber.BisimplicialObject.HomologicalComplex₂.totalMapHomotopy_zero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c : ComplexShape J} [DecidableEq J] [TotalComplexShape c₁ c₂ c] {K L : HomologicalComplex₂ C c₁ c₂} [K.HasTotal c] [L.HasTotal c] {φ ψ : K ⟶ L} (h : Homotopy φ ψ) (j j' : J) (hj : ¬c.Rel j' j) : totalMapHomotopyHom h j j' = 0

theorem LeanPool.EilenbergZilber.BisimplicialObject.HomologicalComplex₂.totalMapHomotopy_comm {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c : ComplexShape J} [DecidableEq J] [TotalComplexShape c₁ c₂ c] {K L : HomologicalComplex₂ C c₁ c₂} [K.HasTotal c] [L.HasTotal c] {φ ψ : K ⟶ L} (h : Homotopy φ ψ) (j : J) : (HomologicalComplex₂.total.map φ c).f j = (dNext j) (totalMapHomotopyHom h) + (prevD j) (totalMapHomotopyHom h) + (HomologicalComplex₂.total.map ψ c).f j

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.HomologicalComplex₂.totalMapHomotopy {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c : ComplexShape J} [DecidableEq J] [TotalComplexShape c₁ c₂ c] {K L : HomologicalComplex₂ C c₁ c₂} [K.HasTotal c] [L.HasTotal c] {φ ψ : K ⟶ L} (h : Homotopy φ ψ) : Homotopy (HomologicalComplex₂.total.map φ c) (HomologicalComplex₂.total.map ψ c)

A homotopy of bicomplex morphisms in the outer direction induces a homotopy on total complexes.

Equations

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

def LeanPool.EilenbergZilber.BisimplicialObject.HomologicalComplex₂.flipMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) : K.flip ⟶ L.flip

The flip of a bicomplex morphism, as a morphism between the flipped bicomplexes.

Equations

• LeanPool.EilenbergZilber.BisimplicialObject.HomologicalComplex₂.flipMap φ = (HomologicalComplex₂.flipFunctor C c₁ c₂).map φ

@[simp]

theorem LeanPool.EilenbergZilber.BisimplicialObject.HomologicalComplex₂.flipMap_f_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (i₂ : I₂) (i₁ : I₁) : ((flipMap φ).f i₂).f i₁ = (φ.f i₁).f i₂

theorem LeanPool.EilenbergZilber.BisimplicialObject.HomologicalComplex₂.totalFlipIso_hom_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c : ComplexShape J} [DecidableEq J] [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] {K L : HomologicalComplex₂ C c₁ c₂} [K.HasTotal c] [L.HasTotal c] (φ : K ⟶ L) : CategoryTheory.CategoryStruct.comp (K.totalFlipIso c).hom (HomologicalComplex₂.total.map φ c) = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map (flipMap φ) c) (L.totalFlipIso c).hom

Naturality of the flip symmetry isomorphism totalFlipIso with respect to a bicomplex morphism φ : K ⟶ L: the totalization of φ and of its flip are related by conjugation.

theorem LeanPool.EilenbergZilber.BisimplicialObject.HomologicalComplex₂.totalFlipIso_hom_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c : ComplexShape J} [DecidableEq J] [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] {K L : HomologicalComplex₂ C c₁ c₂} [K.HasTotal c] [L.HasTotal c] (φ : K ⟶ L) {Z : HomologicalComplex C c} (h : L.total c ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.totalFlipIso c).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map φ c) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map (flipMap φ) c) (CategoryTheory.CategoryStruct.comp (L.totalFlipIso c).hom h)

Naturality of the flip symmetry isomorphism totalFlipIso with respect to a bicomplex morphism φ : K ⟶ L: the totalization of φ and of its flip are related by conjugation.

theorem LeanPool.EilenbergZilber.BisimplicialObject.HomologicalComplex₂.total_map_eq_flipConjugate {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c : ComplexShape J} [DecidableEq J] [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] {K L : HomologicalComplex₂ C c₁ c₂} [K.HasTotal c] [L.HasTotal c] (φ : K ⟶ L) : HomologicalComplex₂.total.map φ c = CategoryTheory.CategoryStruct.comp (K.totalFlipIso c).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map (flipMap φ) c) (L.totalFlipIso c).hom)

The totalization of a bicomplex morphism is conjugate to the totalization of its flip by totalFlipIso.

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.HomologicalComplex₂.totalMapHomotopy₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c : ComplexShape J} [DecidableEq J] [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] {K L : HomologicalComplex₂ C c₁ c₂} [K.HasTotal c] [L.HasTotal c] {φ ψ : K ⟶ L} (h : Homotopy (flipMap φ) (flipMap ψ)) : Homotopy (HomologicalComplex₂.total.map φ c) (HomologicalComplex₂.total.map ψ c)

The inner-direction analog of totalMapHomotopy.

It is obtained by applying totalMapHomotopy to the flipped bicomplex and transporting the result across totalFlipIso.

Equations

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

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.outerNormalizationComparisonPreTotal {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : HomotopyEquiv (((AlgebraicTopology.normalizedMooreComplex C).mapHomologicalComplex (ComplexShape.down ℕ)).obj ((AlgebraicTopology.normalizedMooreComplex (CategoryTheory.SimplicialObject C)).obj X)) (((AlgebraicTopology.normalizedMooreComplex C).mapHomologicalComplex (ComplexShape.down ℕ)).obj ((AlgebraicTopology.alternatingFaceMapComplex (CategoryTheory.SimplicialObject C)).obj X))

The outer Dold-Kan homotopy equivalence before totalization.

Equations

• X.outerNormalizationComparisonPreTotal = (AlgebraicTopology.normalizedMooreComplex C).mapHomotopyEquiv AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex

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

The outer half of normalizationComparison.

Equations

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

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.flipMapHomologicalComplexHomotopy {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {𝒜 : Type u_2} [CategoryTheory.Category.{v_2, u_2} 𝒜] [CategoryTheory.Preadditive 𝒜] {F G : CategoryTheory.Functor 𝒜 (ChainComplex C ℕ)} [F.Additive] [G.Additive] {α β : F ⟶ G} (h : (Y : 𝒜) → Homotopy (α.app Y) (β.app Y)) (hnat : ∀ {Y Z : 𝒜} (f : Y ⟶ Z) (i j : ℕ), CategoryTheory.CategoryStruct.comp ((F.map f).f i) ((h Z).hom i j) = CategoryTheory.CategoryStruct.comp ((h Y).hom i j) ((G.map f).f j)) (W : HomologicalComplex 𝒜 (ComplexShape.down ℕ)) : Homotopy (HomologicalComplex₂.flipMap ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app W)) (HomologicalComplex₂.flipMap ((CategoryTheory.NatTrans.mapHomologicalComplex β (ComplexShape.down ℕ)).app W))

A natural family of homotopies between chain-complex-valued functors lifts, after flip, to a homotopy between the corresponding mapHomologicalComplex morphisms.

Equations

• LeanPool.EilenbergZilber.BisimplicialObject.flipMapHomologicalComplexHomotopy h hnat W = { hom := fun (m m' : ℕ) => { f := fun (r : ℕ) => (h (W.X r)).hom m m', comm' := ⋯ }, zero := ⋯, comm := ⋯ }

theorem LeanPool.EilenbergZilber.BisimplicialObject.alternatingFaceMapComplex_map_f_comp_homotopyPToId_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {Y Z : CategoryTheory.SimplicialObject C} (f : Y ⟶ Z) (q i j : ℕ) : CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.alternatingFaceMapComplex C).map f).f i) ((AlgebraicTopology.DoldKan.homotopyPToId Z q).hom i j) = CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.homotopyPToId Y q).hom i j) (((AlgebraicTopology.alternatingFaceMapComplex C).map f).f j)

Naturality of the homotopy operator in homotopyPToId.

theorem LeanPool.EilenbergZilber.BisimplicialObject.homotopyInvHomId_hom_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {Y Z : CategoryTheory.SimplicialObject C} (f : Y ⟶ Z) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.alternatingFaceMapComplex C).map f).f i) (AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyInvHomId.hom i j) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyInvHomId.hom i j) (((AlgebraicTopology.alternatingFaceMapComplex C).map f).f j)

Naturality, in the simplicial object, of the Dold–Kan contraction homotopy operator for PInfty ≃ 𝟙 (i.e. homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex.homotopyInvHomId). This is the hnat input to flipMapHomologicalComplexHomotopy for the inner normalization comparison.

noncomputable def LeanPool.EilenbergZilber.BisimplicialObject.retractionF₁InclusionF₁FlipHomotopy {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : Homotopy (HomologicalComplex₂.flipMap (CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex mooreRetraction (ComplexShape.down ℕ)).app ((AlgebraicTopology.alternatingFaceMapComplex (CategoryTheory.SimplicialObject C)).obj X)) ((CategoryTheory.NatTrans.mapHomologicalComplex mooreInclusion (ComplexShape.down ℕ)).app ((AlgebraicTopology.alternatingFaceMapComplex (CategoryTheory.SimplicialObject C)).obj X)))) (HomologicalComplex₂.flipMap (CategoryTheory.CategoryStruct.id (((AlgebraicTopology.alternatingFaceMapComplex C).mapHomologicalComplex (ComplexShape.down ℕ)).obj ((AlgebraicTopology.alternatingFaceMapComplex (CategoryTheory.SimplicialObject C)).obj X))))

The flipped inner Dold-Kan homotopy used in innerNormalizationComparison.

Equations

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

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

The inner half of normalizationComparison.

Equations

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

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

The full comparison between the normalized and unnormalized total complexes.

Equations

• X.normalizationComparison = X.outerNormalizationComparison.trans X.innerNormalizationComparison

theorem LeanPool.EilenbergZilber.BisimplicialObject.normalizationComparison_hom_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : X.normalizationComparison.hom = X.inclusionN₁

theorem LeanPool.EilenbergZilber.BisimplicialObject.normalizationComparison_hom_eq_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : (HomologicalComplex₂.totalFunctor C (ComplexShape.down ℕ) (ComplexShape.down ℕ) (ComplexShape.down ℕ)).obj (((AlgebraicTopology.alternatingFaceMapComplex C).mapHomologicalComplex (ComplexShape.down ℕ)).obj ((AlgebraicTopology.alternatingFaceMapComplex (CategoryTheory.SimplicialObject C)).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp X.normalizationComparison.hom h = CategoryTheory.CategoryStruct.comp X.inclusionN₁ h

theorem LeanPool.EilenbergZilber.BisimplicialObject.normalizationComparison_inv_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) : X.normalizationComparison.inv = X.retractionN₁

theorem LeanPool.EilenbergZilber.BisimplicialObject.normalizationComparison_inv_eq_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (X : BisimplicialObject C) {Z : HomologicalComplex C (ComplexShape.down ℕ)} (h : (HomologicalComplex₂.totalFunctor C (ComplexShape.down ℕ) (ComplexShape.down ℕ) (ComplexShape.down ℕ)).obj (((AlgebraicTopology.normalizedMooreComplex C).mapHomologicalComplex (ComplexShape.down ℕ)).obj ((AlgebraicTopology.normalizedMooreComplex (CategoryTheory.SimplicialObject C)).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp X.normalizationComparison.inv h = CategoryTheory.CategoryStruct.comp X.retractionN₁ h