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

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} [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
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 AB obtained as the composition of equivalence₁ and the inverse of eB : B ≌ B'.

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