Documentation

Mathlib.AlgebraicTopology.DoldKan.NCompGamma

The unit isomorphism of the Dold-Kan equivalence

In order to construct the unit isomorphism of the Dold-Kan equivalence, we first construct natural transformations Γ₂N₁.natTrans : N₁ ⋙ Γ₂ ⟶ toKaroubi (SimplicialObject C) and Γ₂N₂.natTrans : N₂ ⋙ Γ₂ ⟶ 𝟭 (SimplicialObject C). It is then shown that Γ₂N₂.natTrans is an isomorphism by using that it becomes an isomorphism after the application of the functor N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ) which reflects isomorphisms.

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

source
theorem AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) {n : ℕ} {Δ' : SimplexCategory} (i : Δ' ⟶ SimplexCategory.mk n) [hi : CategoryTheory.Mono i] (h₁ : SimplexCategory.len Δ' ≠ n) (h₂ : ¬AlgebraicTopology.DoldKan.Isδ₀ i) :
CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (X.toPrefunctor.map i.op) = 0
source
theorem AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ ⟶ Δ') [CategoryTheory.Mono i] {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X (SimplexCategory.len Δ) ⟶ Z) :
CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono (AlgebraicTopology.AlternatingFaceMapComplex.obj X) i) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f (SimplexCategory.len Δ)) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f (SimplexCategory.len Δ')) (CategoryTheory.CategoryStruct.comp (X.toPrefunctor.map i.op) h)
source
theorem AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ ⟶ Δ') [CategoryTheory.Mono i] :
CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono (AlgebraicTopology.AlternatingFaceMapComplex.obj X) i) (AlgebraicTopology.DoldKan.PInfty.f (SimplexCategory.len Δ)) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f (SimplexCategory.len Δ')) (X.toPrefunctor.map i.op)
source
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C) (Δ : SimplexCategoryᵒᵖ) :
(AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X).f.app Δ = SimplicialObject.Splitting.desc (AlgebraicTopology.DoldKan.Γ₀.splitting (AlgebraicTopology.AlternatingFaceMapComplex.obj X)) Δ fun (A : SimplicialObject.Splitting.IndexSet Δ) => CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f (SimplexCategory.len A.fst.unop)) (X.toPrefunctor.map (SimplicialObject.Splitting.IndexSet.e A).op)
source
@[irreducible]
def AlgebraicTopology.DoldKan.Γ₂N₁.natTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂ ⟶ CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)

The natural transformation N₁ ⋙ Γ₂ ⟶ toKaroubi (SimplicialObject C).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[irreducible]
    def AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
    CategoryTheory.Functor.comp (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)) (CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂) ≅ CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂

    The compatibility isomorphism relating N₂ ⋙ Γ₂ and N₁ ⋙ Γ₂.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C) :
      AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.hom.app X = AlgebraicTopology.DoldKan.Γ₂.toPrefunctor.map (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.hom.app X)
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C) :
      AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.inv.app X = AlgebraicTopology.DoldKan.Γ₂.toPrefunctor.map (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.inv.app X)
      source
      @[irreducible]
      def AlgebraicTopology.DoldKan.Γ₂N₂.natTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
      CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂ ⟶ CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C))

      The natural transformation N₂ ⋙ Γ₂ ⟶ 𝟭 (SimplicialObject C).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) :
        AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app P = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂).toPrefunctor.map (CategoryTheory.Idempotents.Karoubi.decompId_i P)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.hom AlgebraicTopology.DoldKan.Γ₂N₁.natTrans).app P.X) (CategoryTheory.Idempotents.Karoubi.decompId_p P))
        source
        theorem AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.SimplicialObject C) :
        AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.app X).inv (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app ((CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)).toPrefunctor.obj X))
        source
        theorem AlgebraicTopology.DoldKan.identity_N₂_objectwise {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) :
        CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.N₂Γ₂.inv.app (AlgebraicTopology.DoldKan.N₂.toPrefunctor.obj P)) (AlgebraicTopology.DoldKan.N₂.toPrefunctor.map (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app P)) = CategoryTheory.CategoryStruct.id (AlgebraicTopology.DoldKan.N₂.toPrefunctor.obj P)
        source
        theorem AlgebraicTopology.DoldKan.identity_N₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id AlgebraicTopology.DoldKan.N₂ ◫ AlgebraicTopology.DoldKan.N₂Γ₂.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂ AlgebraicTopology.DoldKan.N₂).inv (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans ◫ CategoryTheory.CategoryStruct.id AlgebraicTopology.DoldKan.N₂)) = CategoryTheory.CategoryStruct.id AlgebraicTopology.DoldKan.N₂
        source
        instance AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectInstCategorySimplicialObjectInstCategoryKaroubiCategoryCompChainComplexPreadditiveHasZeroMorphismsNatToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringInstCategoryHomologicalComplexDownN₂Γ₂IdNatTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        CategoryTheory.IsIso AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
        Equations
        source
        instance AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectInstCategorySimplicialObjectKaroubiInstCategoryKaroubiCategoryCompChainComplexPreadditiveHasZeroMorphismsNatToAddRightCancelSemigroupToAddRightCancelMonoidToAddCancelMonoidToCancelAddCommMonoidToOrderedCancelAddCommMonoidStrictOrderedSemiringToOneCanonicallyOrderedCommSemiringInstCategoryHomologicalComplexDownN₁Γ₂ToKaroubiNatTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        CategoryTheory.IsIso AlgebraicTopology.DoldKan.Γ₂N₁.natTrans
        Equations
        source
        @[simp]
        theorem AlgebraicTopology.DoldKan.Γ₂N₂_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        AlgebraicTopology.DoldKan.Γ₂N₂.inv = AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
        source
        def AlgebraicTopology.DoldKan.Γ₂N₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) ≅ CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₂ AlgebraicTopology.DoldKan.Γ₂

        The unit isomorphism of the Dold-Kan equivalence.

        Equations
        • AlgebraicTopology.DoldKan.Γ₂N₂ = (CategoryTheory.asIso AlgebraicTopology.DoldKan.Γ₂N₂.natTrans).symm
        Instances For
          source
          @[simp]
          theorem AlgebraicTopology.DoldKan.Γ₂N₁_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
          AlgebraicTopology.DoldKan.Γ₂N₁.inv = AlgebraicTopology.DoldKan.Γ₂N₁.natTrans
          source
          def AlgebraicTopology.DoldKan.Γ₂N₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
          CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C) ≅ CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.N₁ AlgebraicTopology.DoldKan.Γ₂

          The natural isomorphism toKaroubi (SimplicialObject C) ≅ N₁ ⋙ Γ₂.

          Equations
          • AlgebraicTopology.DoldKan.Γ₂N₁ = (CategoryTheory.asIso AlgebraicTopology.DoldKan.Γ₂N₁.natTrans).symm
          Instances For