Construction of the projection P_infty for the Dold-Kan correspondence #
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 construct the projection P_infty : K[X] ⟶ K[X] by passing
to the limit the projections P q defined in projections.lean. This
projection is a critical tool in this formalisation of the Dold-Kan correspondence,
because in the case of abelian categories, P_infty corresponds to the
projection on the normalized Moore subcomplex, with kernel the degenerate subcomplex.
(See equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)
theorem
algebraic_topology.dold_kan.P_is_eventually_constant
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
{q n : ℕ}
(hqn : n ≤ q) :
(algebraic_topology.dold_kan.P (q + 1)).f n = (algebraic_topology.dold_kan.P q).f n
theorem
algebraic_topology.dold_kan.Q_is_eventually_constant
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
{q n : ℕ}
(hqn : n ≤ q) :
(algebraic_topology.dold_kan.Q (q + 1)).f n = (algebraic_topology.dold_kan.Q q).f n
noncomputable
def
algebraic_topology.dold_kan.P_infty
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C} :
The endomorphism P_infty : K[X] ⟶ K[X] obtained from the P q by passing to the limit.
Equations
- algebraic_topology.dold_kan.P_infty = chain_complex.of_hom (λ (n : ℕ), X.obj (opposite.op (simplex_category.mk n))) (algebraic_topology.alternating_face_map_complex.obj_d X) _ (λ (n : ℕ), X.obj (opposite.op (simplex_category.mk n))) (algebraic_topology.alternating_face_map_complex.obj_d X) _ (λ (n : ℕ), (algebraic_topology.dold_kan.P n).f n) algebraic_topology.dold_kan.P_infty._proof_1
noncomputable
def
algebraic_topology.dold_kan.Q_infty
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C} :
The endomorphism Q_infty : K[X] ⟶ K[X] obtained from the Q q by passing to the limit.
@[simp]
theorem
algebraic_topology.dold_kan.P_infty_f_0
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C} :
theorem
algebraic_topology.dold_kan.P_infty_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(n : ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.Q_infty_f_0
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C} :
theorem
algebraic_topology.dold_kan.Q_infty_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(n : ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.P_infty_f_naturality
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(n : ℕ)
{X Y : category_theory.simplicial_object C}
(f : X ⟶ Y) :
@[simp]
theorem
algebraic_topology.dold_kan.P_infty_f_naturality_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(n : ℕ)
{X Y : category_theory.simplicial_object C}
(f : X ⟶ Y)
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj Y).X n ⟶ X') :
f.app (opposite.op (simplex_category.mk n)) ≫ algebraic_topology.dold_kan.P_infty.f n ≫ f' = algebraic_topology.dold_kan.P_infty.f n ≫ f.app (opposite.op (simplex_category.mk n)) ≫ f'
@[simp]
theorem
algebraic_topology.dold_kan.Q_infty_f_naturality
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(n : ℕ)
{X Y : category_theory.simplicial_object C}
(f : X ⟶ Y) :
@[simp]
theorem
algebraic_topology.dold_kan.Q_infty_f_naturality_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(n : ℕ)
{X Y : category_theory.simplicial_object C}
(f : X ⟶ Y)
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj Y).X n ⟶ X') :
f.app (opposite.op (simplex_category.mk n)) ≫ algebraic_topology.dold_kan.Q_infty.f n ≫ f' = algebraic_topology.dold_kan.Q_infty.f n ≫ f.app (opposite.op (simplex_category.mk n)) ≫ f'
@[simp]
theorem
algebraic_topology.dold_kan.P_infty_f_idem_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(n : ℕ)
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj X).X n ⟶ X') :
@[simp]
theorem
algebraic_topology.dold_kan.P_infty_f_idem
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(n : ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.P_infty_idem_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
{X' : chain_complex C ℕ}
(f' : algebraic_topology.alternating_face_map_complex.obj X ⟶ X') :
@[simp]
theorem
algebraic_topology.dold_kan.Q_infty_f_idem_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(n : ℕ)
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj X).X n ⟶ X') :
@[simp]
theorem
algebraic_topology.dold_kan.Q_infty_f_idem
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(n : ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.Q_infty_idem_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
{X' : chain_complex C ℕ}
(f' : algebraic_topology.alternating_face_map_complex.obj X ⟶ X') :
@[simp]
theorem
algebraic_topology.dold_kan.P_infty_f_comp_Q_infty_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(n : ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.P_infty_f_comp_Q_infty_f_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(n : ℕ)
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj X).X n ⟶ X') :
algebraic_topology.dold_kan.P_infty.f n ≫ algebraic_topology.dold_kan.Q_infty.f n ≫ f' = 0 ≫ f'
@[simp]
@[simp]
theorem
algebraic_topology.dold_kan.P_infty_comp_Q_infty_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
{X' : chain_complex C ℕ}
(f' : algebraic_topology.alternating_face_map_complex.obj X ⟶ X') :
@[simp]
theorem
algebraic_topology.dold_kan.Q_infty_f_comp_P_infty_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(n : ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.Q_infty_f_comp_P_infty_f_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(n : ℕ)
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj X).X n ⟶ X') :
algebraic_topology.dold_kan.Q_infty.f n ≫ algebraic_topology.dold_kan.P_infty.f n ≫ f' = 0 ≫ f'
@[simp]
@[simp]
theorem
algebraic_topology.dold_kan.Q_infty_comp_P_infty_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
{X' : chain_complex C ℕ}
(f' : algebraic_topology.alternating_face_map_complex.obj X ⟶ X') :
@[simp]
theorem
algebraic_topology.dold_kan.P_infty_add_Q_infty
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C} :
theorem
algebraic_topology.dold_kan.P_infty_f_add_Q_infty_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(n : ℕ) :
noncomputable
def
algebraic_topology.dold_kan.nat_trans_P_infty
(C : Type u_1)
[category_theory.category C]
[category_theory.preadditive C] :
P_infty induces a natural transformation, i.e. an endomorphism of
the functor alternating_face_map_complex C.
Equations
@[simp]
noncomputable
def
algebraic_topology.dold_kan.nat_trans_P_infty_f
(C : Type u_1)
[category_theory.category C]
[category_theory.preadditive C]
(n : ℕ) :
The natural transformation in each degree that is induced by nat_trans_P_infty.
@[simp]
theorem
algebraic_topology.dold_kan.nat_trans_P_infty_f_app
(C : Type u_1)
[category_theory.category C]
[category_theory.preadditive C]
(n : ℕ)
(X : category_theory.simplicial_object C) :
@[simp]
theorem
algebraic_topology.dold_kan.map_P_infty_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u_3}
[category_theory.category D]
[category_theory.preadditive D]
(G : C ⥤ D)
[G.additive]
(X : category_theory.simplicial_object C)
(n : ℕ) :
theorem
algebraic_topology.dold_kan.karoubi_P_infty_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{Y : category_theory.idempotents.karoubi (category_theory.simplicial_object C)}
(n : ℕ) :
Given an object Y : karoubi (simplicial_object C), this lemma
computes P_infty for the associated object in simplicial_object (karoubi C)
in terms of P_infty for Y.X : simplicial_object C and Y.p.