CategoryTheory.Idempotents.DoldKan.hη

theorem CategoryTheory.Idempotents.DoldKan.hη : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C], AlgebraicTopology.DoldKan.Compatibility.τ₀ = AlgebraicTopology.DoldKan.Compatibility.τ₁ CategoryTheory.Idempotents.DoldKan.isoN₁ CategoryTheory.Idempotents.DoldKan.isoΓ₀ AlgebraicTopology.DoldKan.N₁Γ₀

This theorem states that for any type C, which is a category, is preadditive, is idempotent complete, and has finite coproducts, the natural isomorphism `NΓ'` in the Dold-Kan correspondence satisfies a specific compatibility condition. This condition is crucial for constructing the counit isomorphism `η`. Specifically, the theorem asserts that the compatibility τ₀ is equal to the compatibility τ₁ when applied to `DoldKan.isoN₁`, `DoldKan.isoΓ₀`, and `DoldKan.N₁Γ₀`.

More concisely: In the category C with finite coproducts, preadditive and idempotent complete structure, the natural isomorphisms in the Dold-Kan correspondence `NΓ'`, `DoldKan.isoN₁`, `DoldKan.isoΓ₀`, and `DoldKan.N₁Γ₀` satisfy the compatibility condition τ₀ = τ₁.