# mathlib3documentation

algebraic_topology.dold_kan.compatibility

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 `simplicial_object C ≌ chain_complex C ℕ` for a pseudoabelian category `C` from the equivalence `karoubi (simplicial_object C) ≌ karoubi (chain_complex C ℕ)` and the two equivalences `simplicial_object C ≅ karoubi (simplicial_object C)` and `chain_complex C ℕ ≅ karoubi (chain_complex C ℕ)`.

It is certainly possible to get an equivalence `simplicial_object C ≌ chain_complex 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 `Γ₀ : simplicial_object C ⥤ chain_complex C ℕ` which was constructed in `functor_gamma.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.)

@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₀_functor {A : Type u_1} {A' : Type u_2} {B' : Type u_4} (eA : A A') (e' : A' B') :
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₀_unit_iso_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} (eA : A A') (e' : A' B') (X : A) :
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₀_inverse {A : Type u_1} {A' : Type u_2} {B' : Type u_4} (eA : A A') (e' : A' B') :
def algebraic_topology.dold_kan.compatibility.equivalence₀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} (eA : A A') (e' : A' B') :
A B'

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

Equations
def algebraic_topology.dold_kan.compatibility.equivalence₁ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :
A B'

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

Equations
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₁_functor {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :
theorem algebraic_topology.dold_kan.compatibility.equivalence₁_inverse {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) (X : B') :
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso_inv_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) (X : B') :
def algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :
(e'.inverse eA.inverse) F 𝟭 B'

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

Equations
theorem algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso_eq {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso_inv_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) (X : A) :
def algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :

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

Equations
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) (X : A) :
= eA.unit_iso.hom.app X eA.inverse.map (e'.unit_iso.hom.app (eA.functor.obj X)) eA.inverse.map (e'.inverse.map (hF.hom.app X))
theorem algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso_eq {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₂_functor {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} (eB : B B') {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :
def algebraic_topology.dold_kan.compatibility.equivalence₂ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} (eB : B B') {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :
A B

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

Equations
theorem algebraic_topology.dold_kan.compatibility.equivalence₂_inverse {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} (eB : B B') {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₂_counit_iso_hom_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} (eB : B B') {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) (X : B) :
def algebraic_topology.dold_kan.compatibility.equivalence₂_counit_iso {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} (eB : B B') {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :

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

Equations
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₂_counit_iso_inv_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} (eB : B B') {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) (X : B) :
theorem algebraic_topology.dold_kan.compatibility.equivalence₂_counit_iso_eq {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} (eB : B B') {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :
def algebraic_topology.dold_kan.compatibility.equivalence₂_unit_iso {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} (eB : B B') {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :

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

Equations
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₂_unit_iso_inv_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} (eB : B B') {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) (X : A) :
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence₂_unit_iso_hom_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} (eB : B B') {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) (X : A) :
= eA.unit_iso.hom.app X eA.inverse.map (e'.unit_iso.hom.app (eA.functor.obj X)) eA.inverse.map (e'.inverse.map (hF.hom.app X)) eA.inverse.map (e'.inverse.map (eB.counit_iso.inv.app (F.obj X)))
theorem algebraic_topology.dold_kan.compatibility.equivalence₂_unit_iso_eq {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} (eB : B B') {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :
def algebraic_topology.dold_kan.compatibility.equivalence {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} {eB : B B'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) {G : B A} (hG : eB.functor e'.inverse G eA.functor) :
A B

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

Equations
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence_inverse {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} {eB : B B'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) {G : B A} (hG : eB.functor e'.inverse G eA.functor) :
theorem algebraic_topology.dold_kan.compatibility.equivalence_functor {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} {eB : B B'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) {G : B A} (hG : eB.functor e'.inverse G eA.functor) :
@[simp]
theorem algebraic_topology.dold_kan.compatibility.τ₀_hom_app {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eB : B B'} {e' : A' B'} (X : B) :
def algebraic_topology.dold_kan.compatibility.τ₀ {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eB : B B'} {e' : A' B'} :

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

Equations
@[simp]
theorem algebraic_topology.dold_kan.compatibility.τ₁_hom_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} {eB : B B'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) {G : B A} (hG : eB.functor e'.inverse G eA.functor) (η : G F eB.functor) (X : B) :
X = e'.functor.map (hG.hom.app X) hF.hom.app (G.obj X) η.hom.app X
def algebraic_topology.dold_kan.compatibility.τ₁ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} {eB : B B'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) {G : B A} (hG : eB.functor e'.inverse G eA.functor) (η : G F 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
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence_counit_iso_inv_app {A : Type u_1} {B : Type u_3} {B' : Type u_4} {eB : B B'} {F : A B'} {G : B A} (η : G F eB.functor) (X : B) :
= eB.unit_iso.hom.app X eB.inverse.map (η.inv.app X) (𝟙 (G F eB.inverse)).app X
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence_counit_iso_hom_app {A : Type u_1} {B : Type u_3} {B' : Type u_4} {eB : B B'} {F : A B'} {G : B A} (η : G F eB.functor) (X : B) :
= eB.inverse.map (η.hom.app X) eB.unit_iso.inv.app X
def algebraic_topology.dold_kan.compatibility.equivalence_counit_iso {A : Type u_1} {B : Type u_3} {B' : Type u_4} {eB : B B'} {F : A B'} {G : B A} (η : G F eB.functor) :

The counit isomorphism of `equivalence`.

Equations
theorem algebraic_topology.dold_kan.compatibility.equivalence_counit_iso_eq {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} {eB : B B'} {e' : A' B'} {F : A B'} {hF : eA.functor e'.functor F} {G : B A} {hG : eB.functor e'.inverse G eA.functor} {η : G F eB.functor}  :
@[simp]
theorem algebraic_topology.dold_kan.compatibility.υ_inv_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) (X : A) :
= e'.inverse.map (hF.inv.app X) (𝟙 (eA.functor e'.functor e'.inverse)).app X e'.unit_iso.inv.app (eA.functor.obj X)
def algebraic_topology.dold_kan.compatibility.υ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) :

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

Equations
@[simp]
theorem algebraic_topology.dold_kan.compatibility.υ_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} {eA : A A'} {e' : A' B'} {F : A B'} (hF : eA.functor e'.functor F) (X : A) :
= e'.unit_iso.hom.app (eA.functor.obj X) e'.inverse.map (hF.hom.app X)
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence_unit_iso_inv_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} {eB : B B'} {e' : A' B'} {F : A B'} {G : B A} (hG : eB.functor e'.inverse G eA.functor) (ε : eA.functor F e'.inverse) (X : A) :
= (𝟙 ((F eB.inverse G) 𝟭 A)).app X eA.unit_iso.hom.app (G.obj (eB.inverse.obj (F.obj X))) (𝟙 ((F eB.inverse) (G eA.functor) eA.inverse)).app X eA.inverse.map (hG.inv.app (eB.inverse.obj (F.obj X))) (𝟙 (F (eB.inverse eB.functor) e'.inverse eA.inverse)).app X eA.inverse.map (e'.inverse.map (eB.counit_iso.hom.app (F.obj X))) (𝟙 ((F e'.inverse) eA.inverse)).app X eA.inverse.map (ε.inv.app X) eA.unit_iso.inv.app X
@[simp]
theorem algebraic_topology.dold_kan.compatibility.equivalence_unit_iso_hom_app {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} {eB : B B'} {e' : A' B'} {F : A B'} {G : B A} (hG : eB.functor e'.inverse G eA.functor) (ε : eA.functor F e'.inverse) (X : A) :
= eA.unit_iso.hom.app X eA.inverse.map (ε.hom.app X) eA.inverse.map (e'.inverse.map (eB.counit_iso.inv.app (F.obj X))) eA.inverse.map (hG.hom.app (eB.inverse.obj (F.obj X))) eA.unit_iso.inv.app (G.obj (eB.inverse.obj (F.obj X)))
def algebraic_topology.dold_kan.compatibility.equivalence_unit_iso {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} {eB : B B'} {e' : A' B'} {F : A B'} {G : B A} (hG : eB.functor e'.inverse G eA.functor) (ε : eA.functor F e'.inverse) :
𝟭 A (F eB.inverse) G

The unit isomorphism of `equivalence`.

Equations
theorem algebraic_topology.dold_kan.compatibility.equivalence_unit_iso_eq {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} {eA : A A'} {eB : B B'} {e' : A' B'} {F : A B'} {hF : eA.functor e'.functor F} {G : B A} {hG : eB.functor e'.inverse G eA.functor} {ε : eA.functor F e'.inverse}  :