Documentation

Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive

The Dold-Kan equivalence for additive categories.

This file defines Preadditive.DoldKan.equivalence which is the equivalence of categories Karoubi (SimplicialObject C) ā‰Œ Karoubi (ChainComplex C ā„•).

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

source
šŸ”ø coverage
def CategoryTheory.Preadditive.DoldKan.N {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] :
Functor (Idempotents.Karoubi (SimplicialObject C)) (Idempotents.Karoubi (ChainComplex C ā„•))

The functor Karoubi (SimplicialObject C) ā„¤ Karoubi (ChainComplex C ā„•) of the Dold-Kan equivalence for additive categories.

Equations
    Instances For
      source
      šŸ”ø coverage
      def CategoryTheory.Preadditive.DoldKan.Ī“ {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasFiniteCoproducts C] :
      Functor (Idempotents.Karoubi (ChainComplex C ā„•)) (Idempotents.Karoubi (SimplicialObject C))

      The inverse functor Karoubi (ChainComplex C ā„•) ā„¤ Karoubi (SimplicialObject C) of the Dold-Kan equivalence for additive categories.

      Equations
        Instances For
          source
          šŸ”ø coverage
          def CategoryTheory.Preadditive.DoldKan.equivalence {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasFiniteCoproducts C] :
          Idempotents.Karoubi (SimplicialObject C) ā‰Œ Idempotents.Karoubi (ChainComplex C ā„•)

          The Dold-Kan equivalence Karoubi (SimplicialObject C) ā‰Œ Karoubi (ChainComplex C ā„•) for additive categories.

          Equations
            Instances For
              source
              šŸ“ coverage
              @[simp]
              theorem CategoryTheory.Preadditive.DoldKan.equivalence_counitIso {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasFiniteCoproducts C] :
              equivalence.counitIso = AlgebraicTopology.DoldKan.Nā‚‚Ī“ā‚‚
              source
              šŸ“ coverage
              @[simp]
              theorem CategoryTheory.Preadditive.DoldKan.equivalence_unitIso {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasFiniteCoproducts C] :
              equivalence.unitIso = AlgebraicTopology.DoldKan.Ī“ā‚‚Nā‚‚
              source
              šŸ“ coverage
              @[simp]
              theorem CategoryTheory.Preadditive.DoldKan.equivalence_inverse {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasFiniteCoproducts C] :
              equivalence.inverse = Ī“
              source
              šŸ“ coverage
              @[simp]
              theorem CategoryTheory.Preadditive.DoldKan.equivalence_functor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasFiniteCoproducts C] :
              equivalence.functor = N