Documentation

Mathlib.AlgebraicTopology.DoldKan.Normalized

Comparison with the normalized Moore complex functor #

In this file, we show that when the category A is abelian, there is an isomorphism N₁_iso_normalizedMooreComplex_comp_toKaroubi between the functor N₁ : SimplicialObject A ⥤ Karoubi (ChainComplex A ℕ) defined in FunctorN.lean and the composition of normalizedMooreComplex A with the inclusion ChainComplex A ℕ ⥤ Karoubi (ChainComplex A ℕ).

This isomorphism shall be used in Equivalence.lean in order to obtain the Dold-Kan equivalence CategoryTheory.Abelian.DoldKan.equivalence : SimplicialObject A ≌ ChainComplex A ℕ with a functor (definitionally) equal to normalizedMooreComplex A.

(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

source
theorem AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] {X : CategoryTheory.SimplicialObject A} (n : ℕ) :
AlgebraicTopology.DoldKan.HigherFacesVanish (n + 1) ((AlgebraicTopology.inclusionOfMooreComplexMap X).f (n + 1))
source
theorem AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] {X : CategoryTheory.SimplicialObject A} (n : ℕ) :
CategoryTheory.Subobject.Factors (AlgebraicTopology.NormalizedMooreComplex.objX X n) (AlgebraicTopology.DoldKan.PInfty.f n)
source
@[simp]
theorem AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) (n : ℕ) :
(AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X).f n = CategoryTheory.Subobject.factorThru (AlgebraicTopology.NormalizedMooreComplex.objX X n) (AlgebraicTopology.DoldKan.PInfty.f n) ⋯
source
def AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) :
AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.NormalizedMooreComplex.obj X

PInfty factors through the normalized Moore complex

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) {Z : ChainComplex A ℕ} (h : (AlgebraicTopology.alternatingFaceMapComplex A).obj X ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.inclusionOfMooreComplexMap X) h) = CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) :
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X) (AlgebraicTopology.inclusionOfMooreComplexMap X) = AlgebraicTopology.DoldKan.PInfty
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] {X : CategoryTheory.SimplicialObject A} {Y : CategoryTheory.SimplicialObject A} (f : X ⟶ Y) {Z : ChainComplex A ℕ} (h : AlgebraicTopology.NormalizedMooreComplex.obj Y ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.AlternatingFaceMapComplex.map f) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex Y) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.NormalizedMooreComplex.map f) h)
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] {X : CategoryTheory.SimplicialObject A} {Y : CategoryTheory.SimplicialObject A} (f : X ⟶ Y) :
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.AlternatingFaceMapComplex.map f) (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex Y) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X) (AlgebraicTopology.NormalizedMooreComplex.map f)
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) {Z : ChainComplex A ℕ} (h : AlgebraicTopology.NormalizedMooreComplex.obj X ⟶ Z) :
    CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X) h
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) :
    CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X) = AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) {Z : ChainComplex A ℕ} (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.inclusionOfMooreComplexMap X) (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.inclusionOfMooreComplexMap X) h
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) :
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.inclusionOfMooreComplexMap X) AlgebraicTopology.DoldKan.PInfty = AlgebraicTopology.inclusionOfMooreComplexMap X
    source
    instance AlgebraicTopology.DoldKan.instMonoChainComplexPreadditiveHasZeroMorphismsToPreadditiveNatToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringInstCategoryHomologicalComplexDownObjSimplicialObjectToQuiverToCategoryStructInstCategorySimplicialObjectToPrefunctorNormalizedMooreComplexAlternatingFaceMapComplexInclusionOfMooreComplexMap {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] {X : CategoryTheory.SimplicialObject A} :
    CategoryTheory.Mono (AlgebraicTopology.inclusionOfMooreComplexMap X)
    Equations
    • ⋯ = ⋯
    source
    def AlgebraicTopology.DoldKan.splitMonoInclusionOfMooreComplexMap {A : Type u_1} [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) :
    CategoryTheory.SplitMono (AlgebraicTopology.inclusionOfMooreComplexMap X)

    inclusionOfMooreComplexMap X is a split mono.

    Equations
    Instances For
      source
      def AlgebraicTopology.DoldKan.N₁_iso_normalizedMooreComplex_comp_toKaroubi (A : Type u_1) [CategoryTheory.Category.{u_2, u_1} A] [CategoryTheory.Abelian A] :
      AlgebraicTopology.DoldKan.N₁ ≅ CategoryTheory.Functor.comp (AlgebraicTopology.normalizedMooreComplex A) (CategoryTheory.Idempotents.toKaroubi (ChainComplex A ℕ))

      When the category A is abelian, the functor N₁ : SimplicialObject A ⥤ Karoubi (ChainComplex A ℕ) defined using PInfty identifies to the composition of the normalized Moore complex functor and the inclusion in the Karoubi envelope.

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