Documentation

Mathlib.AlgebraicTopology.DoldKan.Compatibility

Tools for compatibilities between Dold-Kan equivalences

The purpose of this file is to introduce tools which will enable the construction of the Dold-Kan equivalence SimplicialObject C ≌ ChainComplex C ℕ for a pseudoabelian category C from the equivalence Karoubi (SimplicialObject C) ≌ Karoubi (ChainComplex C ℕ) and the two equivalences simplicial_object C ≅ Karoubi (SimplicialObject C) and ChainComplex C ℕ ≅ Karoubi (ChainComplex C ℕ).

It is certainly possible to get an equivalence SimplicialObject C ≌ ChainComplex C ℕ using a compositions of the three equivalences above, but then neither the functor nor the inverse would have good definitional properties. For example, it would be better if the inverse functor of the equivalence was exactly the functor Γ₀ : SimplicialObject C ⥤ ChainComplex C ℕ which was constructed in FunctorGamma.lean.

In this file, given four categories A, A', B, B', equivalences eA : A ≅ A', eB : B ≅ B', e' : A' ≅ B', functors F : A ⥤ B', G : B ⥤ A equipped with certain compatibilities, we construct successive equivalences:

When extra assumptions are given, we shall also provide simplification lemmas for the unit and counit isomorphisms of equivalence.

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

@[simp]
theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₀_unitIso_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_4} B'] (eA : A A') (e' : A' B') (X : A) :
(AlgebraicTopology.DoldKan.Compatibility.equivalence₀ eA e').unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (eA.unitIso.hom.app X) (eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X)))

A basic equivalence A ≅ B' obtained by composing eA : A ≅ A' and e' : A' ≅ B'.

Equations
Instances For

    An intermediate equivalence A ≅ B' whose functor is F and whose inverse is e'.inverse ⋙ eA.inverse.

    Equations
    Instances For
      @[simp]
      theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_inv_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_4} B'] {eA : A A'} {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) (X : B') :
      (AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso hF).inv.app X = CategoryTheory.CategoryStruct.comp (e'.counitIso.inv.app X) (CategoryTheory.CategoryStruct.comp (e'.functor.map (eA.counitIso.inv.app (e'.inverse.obj X))) (hF.hom.app (eA.inverse.obj (e'.inverse.obj X))))
      @[simp]
      theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_4} B'] {eA : A A'} {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) (X : B') :
      (AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso hF).hom.app X = CategoryTheory.CategoryStruct.comp (hF.inv.app (eA.inverse.obj (e'.inverse.obj X))) (CategoryTheory.CategoryStruct.comp (e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj X))) (e'.counitIso.hom.app X))

      The counit isomorphism of the equivalence equivalence₁ between A and B'.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_inv_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_4} B'] {eA : A A'} {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) (X : A) :
        (AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso hF).inv.app X = CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (hF.inv.app X))) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.unitIso.inv.app (eA.functor.obj X))) (eA.unitIso.inv.app X))
        @[simp]
        theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_4} B'] {eA : A A'} {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) (X : A) :
        (AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso hF).hom.app X = CategoryTheory.CategoryStruct.comp (eA.unitIso.hom.app X) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X))) (eA.inverse.map (e'.inverse.map (hF.hom.app X))))

        The unit isomorphism of the equivalence equivalence₁ between A and B'.

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

          An intermediate equivalence A ≅ B obtained as the composition of equivalence₁ and the inverse of eB : B ≌ B'.

          Equations
          Instances For
            @[simp]
            theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_hom_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_3} B] [CategoryTheory.Category.{u_8, u_4} B'] {eA : A A'} (eB : B B') {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) (X : B) :
            (AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso eB hF).hom.app X = CategoryTheory.CategoryStruct.comp (eB.inverse.map (hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj X))))) (CategoryTheory.CategoryStruct.comp (eB.inverse.map (e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj X))))) (CategoryTheory.CategoryStruct.comp (eB.inverse.map (e'.counitIso.hom.app (eB.functor.obj X))) (eB.unitIso.inv.app X)))
            @[simp]
            theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_inv_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_3} B] [CategoryTheory.Category.{u_8, u_4} B'] {eA : A A'} (eB : B B') {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) (X : B) :
            (AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso eB hF).inv.app X = CategoryTheory.CategoryStruct.comp (eB.unitIso.hom.app X) (CategoryTheory.CategoryStruct.comp (eB.inverse.map (e'.counitIso.inv.app (eB.functor.obj X))) (CategoryTheory.CategoryStruct.comp (eB.inverse.map (e'.functor.map (eA.counitIso.inv.app (e'.inverse.obj (eB.functor.obj X))))) (eB.inverse.map (hF.hom.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj X)))))))

            The counit isomorphism of the equivalence equivalence₂ between A and B.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_hom_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_3} B] [CategoryTheory.Category.{u_8, u_4} B'] {eA : A A'} (eB : B B') {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) (X : A) :
              (AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso eB hF).hom.app X = CategoryTheory.CategoryStruct.comp (eA.unitIso.hom.app X) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.unitIso.hom.app (eA.functor.obj X))) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (hF.hom.app X))) (eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X))))))
              @[simp]
              theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_inv_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_3} B] [CategoryTheory.Category.{u_8, u_4} B'] {eA : A A'} (eB : B B') {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) (X : A) :
              (AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso eB hF).inv.app X = CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (eB.counitIso.hom.app (F.obj X)))) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (hF.inv.app X))) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.unitIso.inv.app (eA.functor.obj X))) (eA.unitIso.inv.app X)))

              The unit isomorphism of the equivalence equivalence₂ between A and B.

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

                The equivalence A ≅ B whose functor is F ⋙ eB.inverse and whose inverse is G : B ≅ A.

                Equations
                Instances For
                  @[simp]
                  theorem AlgebraicTopology.DoldKan.Compatibility.τ₀_hom_app {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_2} A'] [CategoryTheory.Category.{u_6, u_3} B] [CategoryTheory.Category.{u_7, u_4} B'] {eB : B B'} {e' : A' B'} (X : B) :
                  AlgebraicTopology.DoldKan.Compatibility.τ₀.hom.app X = e'.counitIso.hom.app (eB.functor.obj X)

                  The isomorphism eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor deduced from the counit isomorphism of e'.

                  Equations
                  Instances For
                    @[simp]
                    theorem AlgebraicTopology.DoldKan.Compatibility.τ₁_hom_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_3} B] [CategoryTheory.Category.{u_8, u_4} B'] {eA : A A'} {eB : B B'} {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) {G : CategoryTheory.Functor B A} (hG : CategoryTheory.Functor.comp eB.functor e'.inverse CategoryTheory.Functor.comp G eA.functor) (η : CategoryTheory.Functor.comp G F eB.functor) (X : B) :
                    (AlgebraicTopology.DoldKan.Compatibility.τ₁ hF hG η).hom.app X = CategoryTheory.CategoryStruct.comp (e'.functor.map (hG.hom.app X)) (CategoryTheory.CategoryStruct.comp (hF.hom.app (G.obj X)) (η.hom.app X))
                    def AlgebraicTopology.DoldKan.Compatibility.τ₁ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_3} B] [CategoryTheory.Category.{u_8, u_4} B'] {eA : A A'} {eB : B B'} {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) {G : CategoryTheory.Functor B A} (hG : CategoryTheory.Functor.comp eB.functor e'.inverse CategoryTheory.Functor.comp G eA.functor) (η : CategoryTheory.Functor.comp G F eB.functor) :
                    CategoryTheory.Functor.comp eB.functor (CategoryTheory.Functor.comp e'.inverse e'.functor) eB.functor

                    The isomorphism eB.functor ⋙ e'.inverse ⋙ e'.functor ≅ eB.functor deduced from the isomorphisms hF : eA.functor ⋙ e'.functor ≅ F, hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor and the datum of an isomorphism η : G ⋙ F ≅ eB.functor.

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

                      The counit isomorphism of equivalence.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem AlgebraicTopology.DoldKan.Compatibility.υ_inv_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_4} B'] {eA : A A'} {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) (X : A) :
                        (AlgebraicTopology.DoldKan.Compatibility.υ hF).inv.app X = CategoryTheory.CategoryStruct.comp (e'.inverse.map (hF.inv.app X)) (e'.unitIso.inv.app (eA.functor.obj X))
                        @[simp]
                        theorem AlgebraicTopology.DoldKan.Compatibility.υ_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_4} B'] {eA : A A'} {e' : A' B'} {F : CategoryTheory.Functor A B'} (hF : CategoryTheory.Functor.comp eA.functor e'.functor F) (X : A) :
                        (AlgebraicTopology.DoldKan.Compatibility.υ hF).hom.app X = CategoryTheory.CategoryStruct.comp (e'.unitIso.hom.app (eA.functor.obj X)) (e'.inverse.map (hF.hom.app X))

                        The isomorphism eA.functor ≅ F ⋙ e'.inverse deduced from the unit isomorphism of e' and the isomorphism hF : eA.functor ⋙ e'.functor ≅ F.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_hom_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_3} B] [CategoryTheory.Category.{u_8, u_4} B'] {eA : A A'} {eB : B B'} {e' : A' B'} {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A} (hG : CategoryTheory.Functor.comp eB.functor e'.inverse CategoryTheory.Functor.comp G eA.functor) (ε : eA.functor CategoryTheory.Functor.comp F e'.inverse) (X : A) :
                          (AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso hG ε).hom.app X = CategoryTheory.CategoryStruct.comp (eA.unitIso.hom.app X) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (ε.hom.app X)) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (eB.counitIso.inv.app (F.obj X)))) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X)))) (eA.unitIso.inv.app (G.obj (eB.inverse.obj (F.obj X)))))))
                          @[simp]
                          theorem AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_inv_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{u_5, u_1} A] [CategoryTheory.Category.{u_6, u_2} A'] [CategoryTheory.Category.{u_7, u_3} B] [CategoryTheory.Category.{u_8, u_4} B'] {eA : A A'} {eB : B B'} {e' : A' B'} {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A} (hG : CategoryTheory.Functor.comp eB.functor e'.inverse CategoryTheory.Functor.comp G eA.functor) (ε : eA.functor CategoryTheory.Functor.comp F e'.inverse) (X : A) :
                          (AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso hG ε).inv.app X = CategoryTheory.CategoryStruct.comp (eA.unitIso.hom.app (G.obj (eB.inverse.obj (F.obj X)))) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (hG.inv.app (eB.inverse.obj (F.obj X)))) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (e'.inverse.map (eB.counitIso.hom.app (F.obj X)))) (CategoryTheory.CategoryStruct.comp (eA.inverse.map (ε.inv.app X)) (eA.unitIso.inv.app X))))

                          The unit isomorphism of equivalence.

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