Theorems · Theorem · category theory

CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f

∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A) (i : ℕ),
  (CategoryTheory.Abelian.DoldKan.comparisonN.inv.app X).f i =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex A ℕ)).inverse.map
            ((AlgebraicTopology.DoldKan.N₁_iso_normalizedMooreComplex_comp_toKaroubi A).hom.app X)).f
        i)
      (((CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex A ℕ)).unitIso.inv.app
            (CategoryTheory.Abelian.DoldKan.N.obj X)).f
        i)

Defined in

Mathlib.AlgebraicTopology.DoldKan.Equivalence

Cited by

0 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian