mathlib3 documentation

algebraic_topology.dold_kan.normalized

Comparison with the normalized Moore complex functor #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

TODO (@joelriou) continue adding the various files referenced below

In this file, we show that when the category A is abelian, there is an isomorphism N₁_iso_normalized_Moore_complex_comp_to_karoubi between the functor N₁ : simplicial_object A ⥤ karoubi (chain_complex A ℕ) defined in functor_n.lean and the composition of normalized_Moore_complex A with the inclusion chain_complex A ℕ ⥤ karoubi (chain_complex A ℕ).

This isomorphism shall be used in equivalence.lean in order to obtain the Dold-Kan equivalence category_theory.abelian.dold_kan.equivalence : simplicial_object A ≌ chain_complex A ℕ with a functor (definitionally) equal to normalized_Moore_complex A.

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

source
theorem algebraic_topology.dold_kan.higher_faces_vanish.inclusion_of_Moore_complex_map {A : Type u_1} [category_theory.category A] [category_theory.abelian A] {X : category_theory.simplicial_object A} (n : ℕ) :
algebraic_topology.dold_kan.higher_faces_vanish (n + 1) ((algebraic_topology.inclusion_of_Moore_complex_map X).f (n + 1))
source
theorem algebraic_topology.dold_kan.factors_normalized_Moore_complex_P_infty {A : Type u_1} [category_theory.category A] [category_theory.abelian A] {X : category_theory.simplicial_object A} (n : ℕ) :
(algebraic_topology.normalized_Moore_complex.obj_X X n).factors (algebraic_topology.dold_kan.P_infty.f n)
source
@[simp]
theorem algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex_f {A : Type u_1} [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) (n : ℕ) :
(algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex X).f n = (algebraic_topology.normalized_Moore_complex.obj_X X n).factor_thru (algebraic_topology.dold_kan.P_infty.f n) _
source
noncomputable def algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex {A : Type u_1} [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) :
algebraic_topology.alternating_face_map_complex.obj X ⟶ algebraic_topology.normalized_Moore_complex.obj X

P_infty factors through the normalized Moore complex

Equations
source
@[simp]
theorem algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex_comp_inclusion_of_Moore_complex_map_assoc {A : Type u_1} [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) {X' : chain_complex A ℕ} (f' : (algebraic_topology.alternating_face_map_complex A).obj X ⟶ X') :
algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex X ≫ algebraic_topology.inclusion_of_Moore_complex_map X ≫ f' = algebraic_topology.dold_kan.P_infty ≫ f'
source
@[simp]
theorem algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex_comp_inclusion_of_Moore_complex_map {A : Type u_1} [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) :
algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex X ≫ algebraic_topology.inclusion_of_Moore_complex_map X = algebraic_topology.dold_kan.P_infty
source
@[simp]
theorem algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex_naturality_assoc {A : Type u_1} [category_theory.category A] [category_theory.abelian A] {X Y : category_theory.simplicial_object A} (f : X ⟶ Y) {X' : chain_complex A ℕ} (f' : algebraic_topology.normalized_Moore_complex.obj Y ⟶ X') :
algebraic_topology.alternating_face_map_complex.map f ≫ algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex Y ≫ f' = algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex X ≫ algebraic_topology.normalized_Moore_complex.map f ≫ f'
source
@[simp]
theorem algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex_naturality {A : Type u_1} [category_theory.category A] [category_theory.abelian A] {X Y : category_theory.simplicial_object A} (f : X ⟶ Y) :
algebraic_topology.alternating_face_map_complex.map f ≫ algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex Y = algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex X ≫ algebraic_topology.normalized_Moore_complex.map f
source
@[simp]
theorem algebraic_topology.dold_kan.P_infty_comp_P_infty_to_normalized_Moore_complex {A : Type u_1} [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) :
algebraic_topology.dold_kan.P_infty ≫ algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex X = algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex X
source
@[simp]
theorem algebraic_topology.dold_kan.P_infty_comp_P_infty_to_normalized_Moore_complex_assoc {A : Type u_1} [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) {X' : chain_complex A ℕ} (f' : algebraic_topology.normalized_Moore_complex.obj X ⟶ X') :
algebraic_topology.dold_kan.P_infty ≫ algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex X ≫ f' = algebraic_topology.dold_kan.P_infty_to_normalized_Moore_complex X ≫ f'
source
@[simp]
theorem algebraic_topology.dold_kan.inclusion_of_Moore_complex_map_comp_P_infty_assoc {A : Type u_1} [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) {X' : chain_complex A ℕ} (f' : algebraic_topology.alternating_face_map_complex.obj X ⟶ X') :
algebraic_topology.inclusion_of_Moore_complex_map X ≫ algebraic_topology.dold_kan.P_infty ≫ f' = algebraic_topology.inclusion_of_Moore_complex_map X ≫ f'
source
@[simp]
theorem algebraic_topology.dold_kan.inclusion_of_Moore_complex_map_comp_P_infty {A : Type u_1} [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) :
algebraic_topology.inclusion_of_Moore_complex_map X ≫ algebraic_topology.dold_kan.P_infty = algebraic_topology.inclusion_of_Moore_complex_map X
source
@[protected, instance]
def algebraic_topology.dold_kan.algebraic_topology.inclusion_of_Moore_complex_map.category_theory.mono {A : Type u_1} [category_theory.category A] [category_theory.abelian A] {X : category_theory.simplicial_object A} :
category_theory.mono (algebraic_topology.inclusion_of_Moore_complex_map X)
source
noncomputable def algebraic_topology.dold_kan.split_mono_inclusion_of_Moore_complex_map {A : Type u_1} [category_theory.category A] [category_theory.abelian A] (X : category_theory.simplicial_object A) :
category_theory.split_mono (algebraic_topology.inclusion_of_Moore_complex_map X)

inclusion_of_Moore_complex_map X is a split mono.

Equations
source
noncomputable def algebraic_topology.dold_kan.N₁_iso_normalized_Moore_complex_comp_to_karoubi (A : Type u_1) [category_theory.category A] [category_theory.abelian A] :
algebraic_topology.dold_kan.N₁ ≅ algebraic_topology.normalized_Moore_complex A ⋙ category_theory.idempotents.to_karoubi (chain_complex A ℕ)

When the category A is abelian, the functor N₁ : simplicial_object A ⥤ karoubi (chain_complex A ℕ) defined using P_infty identifies to the composition of the normalized Moore complex functor and the inclusion in the Karoubi envelope.

Equations