mathlib documentation

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

@[simp]

theorem algebraic_topology.dold_kan.compatibility.equivalence₀_functor {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] (eA : A ≌ A') (e' : A' ≌ B') :

(algebraic_topology.dold_kan.compatibility.equivalence₀ eA e').functor = eA.functor ⋙ e'.functor

@[simp]

theorem algebraic_topology.dold_kan.compatibility.equivalence₀_unit_iso_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] (eA : A ≌ A') (e' : A' ≌ B') (X : A) :

(algebraic_topology.dold_kan.compatibility.equivalence₀ eA e').unit_iso.hom.app X = eA.unit_iso.hom.app X ≫ eA.inverse.map (e'.unit_iso.hom.app (eA.functor.obj X))

@[simp]

theorem algebraic_topology.dold_kan.compatibility.equivalence₀_inverse {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] (eA : A ≌ A') (e' : A' ≌ B') :

(algebraic_topology.dold_kan.compatibility.equivalence₀ eA e').inverse = e'.inverse ⋙ eA.inverse

def algebraic_topology.dold_kan.compatibility.equivalence₀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] (eA : A ≌ A') (e' : A' ≌ B') :

A ≌ B'

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

Equations

algebraic_topology.dold_kan.compatibility.equivalence₀ eA e' = eA.trans e'

def algebraic_topology.dold_kan.compatibility.equivalence₁ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] {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

algebraic_topology.dold_kan.compatibility.equivalence₁ hF = let _inst : category_theory.is_equivalence F := category_theory.is_equivalence.of_iso hF (category_theory.is_equivalence.of_equivalence (algebraic_topology.dold_kan.compatibility.equivalence₀ eA e')) in F.as_equivalence

@[simp]

theorem algebraic_topology.dold_kan.compatibility.equivalence₁_functor {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) :

(algebraic_topology.dold_kan.compatibility.equivalence₁ hF).functor = F

theorem algebraic_topology.dold_kan.compatibility.equivalence₁_inverse {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) :

(algebraic_topology.dold_kan.compatibility.equivalence₁ hF).inverse = e'.inverse ⋙ eA.inverse

@[simp]

theorem algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) (X : B') :

(algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso hF).hom.app X = hF.inv.app (eA.inverse.obj (e'.inverse.obj X)) ≫ e'.functor.map (eA.counit_iso.hom.app (e'.inverse.obj X)) ≫ e'.counit_iso.hom.app X

@[simp]

theorem algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso_inv_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) (X : B') :

(algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso hF).inv.app X = e'.counit_iso.inv.app X ≫ (𝟙 (e'.inverse ⋙ 𝟭 A' ⋙ e'.functor)).app X ≫ e'.functor.map (eA.counit_iso.inv.app (e'.inverse.obj X)) ≫ (𝟙 ((e'.inverse ⋙ eA.inverse) ⋙ eA.functor ⋙ e'.functor)).app X ≫ hF.hom.app (eA.inverse.obj (e'.inverse.obj X))

def algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] {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

algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso hF = (((category_theory.iso_whisker_left (e'.inverse ⋙ eA.inverse) hF.symm ≪≫ category_theory.iso.refl ((e'.inverse ⋙ eA.inverse) ⋙ eA.functor ⋙ e'.functor)) ≪≫ category_theory.iso_whisker_left e'.inverse (category_theory.iso_whisker_right eA.counit_iso e'.functor)) ≪≫ category_theory.iso.refl (e'.inverse ⋙ 𝟭 A' ⋙ e'.functor)) ≪≫ e'.counit_iso

theorem algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso_eq {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) :

(algebraic_topology.dold_kan.compatibility.equivalence₁ hF).counit_iso = algebraic_topology.dold_kan.compatibility.equivalence₁_counit_iso hF

@[simp]

theorem algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso_inv_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) (X : A) :

(algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso hF).inv.app X = eA.inverse.map (e'.inverse.map (hF.inv.app X)) ≫ (𝟙 (eA.functor ⋙ (e'.functor ⋙ e'.inverse) ⋙ eA.inverse)).app X ≫ eA.inverse.map (e'.unit_iso.inv.app (eA.functor.obj X)) ≫ (𝟙 (eA.functor ⋙ eA.inverse)).app X ≫ eA.unit_iso.inv.app X

def algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) :

𝟭 A ≅ F ⋙ e'.inverse ⋙ eA.inverse

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

Equations

algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso hF = (((eA.unit_iso ≪≫ category_theory.iso.refl (eA.functor ⋙ eA.inverse)) ≪≫ category_theory.iso_whisker_left eA.functor (category_theory.iso_whisker_right e'.unit_iso eA.inverse)) ≪≫ category_theory.iso.refl (eA.functor ⋙ (e'.functor ⋙ e'.inverse) ⋙ eA.inverse)) ≪≫ category_theory.iso_whisker_right hF (e'.inverse ⋙ eA.inverse)

@[simp]

theorem algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso_hom_app {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) (X : A) :

(algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso hF).hom.app X = 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} [category_theory.category A] [category_theory.category A'] [category_theory.category B'] {eA : A ≌ A'} {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) :

(algebraic_topology.dold_kan.compatibility.equivalence₁ hF).unit_iso = algebraic_topology.dold_kan.compatibility.equivalence₁_unit_iso hF

@[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} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) :

(algebraic_topology.dold_kan.compatibility.equivalence₂ eB hF).functor = F ⋙ eB.inverse

def algebraic_topology.dold_kan.compatibility.equivalence₂ {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {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

algebraic_topology.dold_kan.compatibility.equivalence₂ eB hF = (algebraic_topology.dold_kan.compatibility.equivalence₁ hF).trans eB.symm

theorem algebraic_topology.dold_kan.compatibility.equivalence₂_inverse {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) :

(algebraic_topology.dold_kan.compatibility.equivalence₂ eB hF).inverse = eB.functor ⋙ e'.inverse ⋙ eA.inverse

@[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} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) (X : B) :

(algebraic_topology.dold_kan.compatibility.equivalence₂_counit_iso eB hF).hom.app X = eB.inverse.map (hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj X)))) ≫ eB.inverse.map (e'.functor.map (eA.counit_iso.hom.app (e'.inverse.obj (eB.functor.obj X)))) ≫ eB.inverse.map (e'.counit_iso.hom.app (eB.functor.obj X)) ≫ eB.unit_iso.inv.app X

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} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) :

(eB.functor ⋙ e'.inverse ⋙ eA.inverse) ⋙ F ⋙ eB.inverse ≅ 𝟭 B

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} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) (X : B) :

(algebraic_topology.dold_kan.compatibility.equivalence₂_counit_iso eB hF).inv.app X = eB.unit_iso.hom.app X ≫ (𝟙 (eB.functor ⋙ 𝟭 B' ⋙ eB.inverse)).app X ≫ eB.inverse.map (e'.counit_iso.inv.app (eB.functor.obj X)) ≫ eB.inverse.map ((𝟙 (e'.inverse ⋙ 𝟭 A' ⋙ e'.functor)).app (eB.functor.obj X)) ≫ eB.inverse.map (e'.functor.map (eA.counit_iso.inv.app (e'.inverse.obj (eB.functor.obj X)))) ≫ eB.inverse.map ((𝟙 ((e'.inverse ⋙ eA.inverse) ⋙ eA.functor ⋙ e'.functor)).app (eB.functor.obj X)) ≫ eB.inverse.map (hF.hom.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj X)))) ≫ (𝟙 ((eB.functor ⋙ e'.inverse ⋙ eA.inverse) ⋙ F ⋙ eB.inverse)).app X

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} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) :

(algebraic_topology.dold_kan.compatibility.equivalence₂ eB hF).counit_iso = algebraic_topology.dold_kan.compatibility.equivalence₂_counit_iso eB hF

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} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) :

𝟭 A ≅ (F ⋙ eB.inverse) ⋙ eB.functor ⋙ e'.inverse ⋙ eA.inverse

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} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) (X : A) :

(algebraic_topology.dold_kan.compatibility.equivalence₂_unit_iso eB hF).inv.app 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 (e'.inverse.map (hF.inv.app X)) ≫ (𝟙 (eA.functor ⋙ (e'.functor ⋙ e'.inverse) ⋙ eA.inverse)).app X ≫ eA.inverse.map (e'.unit_iso.inv.app (eA.functor.obj X)) ≫ (𝟙 (eA.functor ⋙ eA.inverse)).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} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) (X : A) :

(algebraic_topology.dold_kan.compatibility.equivalence₂_unit_iso eB hF).hom.app X = 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} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {eA : A ≌ A'} (eB : B ≌ B') {e' : A' ≌ B'} {F : A ⥤ B'} (hF : eA.functor ⋙ e'.functor ≅ F) :

(algebraic_topology.dold_kan.compatibility.equivalence₂ eB hF).unit_iso = algebraic_topology.dold_kan.compatibility.equivalence₂_unit_iso eB hF

def algebraic_topology.dold_kan.compatibility.equivalence {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {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} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {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) :

(algebraic_topology.dold_kan.compatibility.equivalence hF hG).inverse = G

theorem algebraic_topology.dold_kan.compatibility.equivalence_functor {A : Type u_1} {A' : Type u_2} {B : Type u_3} {B' : Type u_4} [category_theory.category A] [category_theory.category A'] [category_theory.category B] [category_theory.category B'] {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) :

(algebraic_topology.dold_kan.compatibility.equivalence hF hG).functor = F ⋙ eB.inverse