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 SimplicialObject C ≌ Karoubi (SimplicialObject C) and ChainComplex C ℕ ≌ Karoubi (ChainComplex C ℕ).

It is certainly possible to get an equivalence SimplicialObject C ≌ ChainComplex C ℕ using a composition 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 Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject 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:

• equivalence₀ from A to B', which is the composition of eA and e'.
• equivalence₁ from A to B', with the same inverse functor as equivalence₀, but whose functor is F.
• equivalence₂ from A to B, which is the composition of equivalence₁ and the inverse of eB:
• equivalence from A to B, which has the same functor F ⋙ eB.inverse as equivalence₂, but whose inverse functor is G.

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.)

def AlgebraicTopology.DoldKan.Compatibility.equivalence₀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] (eA : A ≌ A') (e' : A' ≌ B') : A ≌ B'

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

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₀_unitIso_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] (eA : A ≌ A') (e' : A' ≌ B') (X : A) : (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)))

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₀_inverse {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] (eA : A ≌ A') (e' : A' ≌ B') : (equivalence₀ eA e').inverse = e'.inverse.comp eA.inverse

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₀_functor {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] (eA : A ≌ A') (e' : A' ≌ B') : (equivalence₀ eA e').functor = eA.functor.comp e'.functor

def AlgebraicTopology.DoldKan.Compatibility.equivalence₁ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : A ≌ B'

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

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁_functor {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : (equivalence₁ hF).functor = F

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁_inverse {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : (equivalence₁ hF).inverse = e'.inverse.comp eA.inverse

def AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : (e'.inverse.comp eA.inverse).comp F ≅ CategoryTheory.Functor.id B'

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

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : B') : (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))

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_inv_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : B') : (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))))

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_eq {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : (equivalence₁ hF).counitIso = equivalence₁CounitIso hF

def AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : CategoryTheory.Functor.id A ≅ F.comp (e'.inverse.comp eA.inverse)

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

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_inv_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A) : (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.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A) : (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))))

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₁UnitIso_eq {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : (equivalence₁ hF).unitIso = equivalence₁UnitIso hF

def AlgebraicTopology.DoldKan.Compatibility.equivalence₂ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : A ≌ B

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

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₂_functor {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : (equivalence₂ eB hF).functor = F.comp eB.inverse

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₂_inverse {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : (equivalence₂ eB hF).inverse = eB.functor.comp (e'.inverse.comp eA.inverse)

def AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : (eB.functor.comp (e'.inverse.comp eA.inverse)).comp (F.comp eB.inverse) ≅ CategoryTheory.Functor.id B

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

@[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.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : B) : (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)))))))

@[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.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : B) : (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)))

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₂CounitIso_eq {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : (equivalence₂ eB hF).counitIso = equivalence₂CounitIso eB hF

def AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : CategoryTheory.Functor.id A ≅ (F.comp eB.inverse).comp (eB.functor.comp (e'.inverse.comp eA.inverse))

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

@[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.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A) : (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)))

@[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.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A) : (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))))))

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence₂UnitIso_eq {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : (equivalence₂ eB hF).unitIso = equivalence₂UnitIso eB hF

def AlgebraicTopology.DoldKan.Compatibility.equivalence {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) {G : CategoryTheory.Functor B A} (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor) : A ≌ B

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

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence_inverse {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) {G : CategoryTheory.Functor B A} (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor) : (equivalence hF hG).inverse = G

theorem AlgebraicTopology.DoldKan.Compatibility.equivalence_functor {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) {G : CategoryTheory.Functor B A} (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor) : (equivalence hF hG).functor = F.comp eB.inverse

def AlgebraicTopology.DoldKan.Compatibility.τ₀ {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eB : B ≌ B'} {e' : A' ≌ B'} : eB.functor.comp (e'.inverse.comp e'.functor) ≅ eB.functor

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

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.τ₀_hom_app {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eB : B ≌ B'} {e' : A' ≌ B'} (X : B) : τ₀.hom.app X = e'.counitIso.hom.app (eB.functor.obj X)

def AlgebraicTopology.DoldKan.Compatibility.τ₁ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) {G : CategoryTheory.Functor B A} (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor) (η : G.comp F ≅ eB.functor) : eB.functor.comp (e'.inverse.comp 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.

@[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.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) {G : CategoryTheory.Functor B A} (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor) (η : G.comp F ≅ eB.functor) (X : B) : (τ₁ 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.equivalenceCounitIso {A : Type u_1} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eB : B ≌ B'} {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A} (η : G.comp F ≅ eB.functor) : G.comp (F.comp eB.inverse) ≅ CategoryTheory.Functor.id B

The counit isomorphism of equivalence.

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_hom_app {A : Type u_1} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eB : B ≌ B'} {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A} (η : G.comp F ≅ eB.functor) (X : B) : (equivalenceCounitIso η).hom.app X = CategoryTheory.CategoryStruct.comp (eB.inverse.map (η.hom.app X)) (eB.unitIso.inv.app X)

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_inv_app {A : Type u_1} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eB : B ≌ B'} {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A} (η : G.comp F ≅ eB.functor) (X : B) : (equivalenceCounitIso η).inv.app X = CategoryTheory.CategoryStruct.comp (eB.unitIso.hom.app X) (eB.inverse.map (η.inv.app X))

theorem AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso_eq {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} {hF : eA.functor.comp e'.functor ≅ F} {G : CategoryTheory.Functor B A} {hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor} {η : G.comp F ≅ eB.functor} (hη : τ₀ = τ₁ hF hG η) : (equivalence hF hG).counitIso = equivalenceCounitIso η

def AlgebraicTopology.DoldKan.Compatibility.υ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) : eA.functor ≅ F.comp e'.inverse

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

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.υ_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A) : (υ hF).hom.app X = CategoryTheory.CategoryStruct.comp (e'.unitIso.hom.app (eA.functor.obj X)) (e'.inverse.map (hF.hom.app X))

@[simp]

theorem AlgebraicTopology.DoldKan.Compatibility.υ_inv_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : A) : (υ hF).inv.app X = CategoryTheory.CategoryStruct.comp (e'.inverse.map (hF.inv.app X)) (e'.unitIso.inv.app (eA.functor.obj X))

def AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A} (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor) (ε : eA.functor ≅ F.comp e'.inverse) : CategoryTheory.Functor.id A ≅ (F.comp eB.inverse).comp G

The unit isomorphism of equivalence.

@[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.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A} (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor) (ε : eA.functor ≅ F.comp e'.inverse) (X : A) : (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.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} {G : CategoryTheory.Functor B A} (hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor) (ε : eA.functor ≅ F.comp e'.inverse) (X : A) : (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))))

theorem AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso_eq {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} A'] [CategoryTheory.Category.{v_3, u_3} B] [CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'} {eB : B ≌ B'} {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} {hF : eA.functor.comp e'.functor ≅ F} {G : CategoryTheory.Functor B A} {hG : eB.functor.comp e'.inverse ≅ G.comp eA.functor} {ε : eA.functor ≅ F.comp e'.inverse} (hε : υ hF = ε) : (equivalence hF hG).unitIso = equivalenceUnitIso hG ε