Construction of projections 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 endomorphisms P q : K[X] ⟶ K[X] for all
q : ℕ. We study how they behave with respect to face maps with the lemmas
higher_faces_vanish.of_P, higher_faces_vanish.comp_P_eq_self and
comp_P_eq_self_iff.
Then, we show that they are projections (see P_f_idem
and P_idem). They are natural transformations (see nat_trans_P
and P_f_naturality) and are compatible with the application
of additive functors (see map_P).
By passing to the limit, these endomorphisms P q shall be used in p_infty.lean
in order to define P_infty : K[X] ⟶ K[X], see equivalence.lean for the general
strategy of proof of the Dold-Kan equivalence.
(See equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)
noncomputable
def
algebraic_topology.dold_kan.P
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C} :
This is the inductive definition of the projections P q : K[X] ⟶ K[X],
with P 0 := 𝟙 _ and P (q+1) := P q ≫ (𝟙 _ + Hσ q).
@[simp]
theorem
algebraic_topology.dold_kan.P_f_0_eq
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q : ℕ) :
All the P q coincide with 𝟙 _ in degree 0.
noncomputable
def
algebraic_topology.dold_kan.Q
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q : ℕ) :
Q q is the complement projection associated to P q
theorem
algebraic_topology.dold_kan.P_add_Q
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q : ℕ) :
theorem
algebraic_topology.dold_kan.P_add_Q_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q n : ℕ) :
(algebraic_topology.dold_kan.P q).f n + (algebraic_topology.dold_kan.Q q).f n = 𝟙 (X.obj (opposite.op (simplex_category.mk n)))
@[simp]
theorem
algebraic_topology.dold_kan.Q_eq_zero
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C} :
theorem
algebraic_topology.dold_kan.Q_eq
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q : ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.Q_f_0_eq
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q : ℕ) :
(algebraic_topology.dold_kan.Q q).f 0 = 0
All the Q q coincide with 0 in degree 0.
theorem
algebraic_topology.dold_kan.higher_faces_vanish.of_P
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q n : ℕ) :
This lemma expresses the vanishing of
(P q).f (n+1) ≫ X.δ k : X _[n+1] ⟶ X _[n] when k≠0 and k≥n-q+2
theorem
algebraic_topology.dold_kan.higher_faces_vanish.comp_P_eq_self
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
{Y : C}
{n q : ℕ}
{φ : Y ⟶ X.obj (opposite.op (simplex_category.mk (n + 1)))}
(v : algebraic_topology.dold_kan.higher_faces_vanish q φ) :
φ ≫ (algebraic_topology.dold_kan.P q).f (n + 1) = φ
theorem
algebraic_topology.dold_kan.higher_faces_vanish.comp_P_eq_self_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
{Y : C}
{n q : ℕ}
{φ : Y ⟶ X.obj (opposite.op (simplex_category.mk (n + 1)))}
(v : algebraic_topology.dold_kan.higher_faces_vanish q φ)
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj X).X (n + 1) ⟶ X') :
theorem
algebraic_topology.dold_kan.comp_P_eq_self_iff
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
{Y : C}
{n q : ℕ}
{φ : Y ⟶ X.obj (opposite.op (simplex_category.mk (n + 1)))} :
φ ≫ (algebraic_topology.dold_kan.P q).f (n + 1) = φ ↔ algebraic_topology.dold_kan.higher_faces_vanish q φ
@[simp]
theorem
algebraic_topology.dold_kan.P_f_idem_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q n : ℕ)
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj X).X n ⟶ X') :
(algebraic_topology.dold_kan.P q).f n ≫ (algebraic_topology.dold_kan.P q).f n ≫ f' = (algebraic_topology.dold_kan.P q).f n ≫ f'
@[simp]
theorem
algebraic_topology.dold_kan.P_f_idem
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q n : ℕ) :
(algebraic_topology.dold_kan.P q).f n ≫ (algebraic_topology.dold_kan.P q).f n = (algebraic_topology.dold_kan.P q).f n
@[simp]
theorem
algebraic_topology.dold_kan.Q_f_idem
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q n : ℕ) :
(algebraic_topology.dold_kan.Q q).f n ≫ (algebraic_topology.dold_kan.Q q).f n = (algebraic_topology.dold_kan.Q q).f n
@[simp]
theorem
algebraic_topology.dold_kan.Q_f_idem_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q n : ℕ)
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj X).X n ⟶ X') :
(algebraic_topology.dold_kan.Q q).f n ≫ (algebraic_topology.dold_kan.Q q).f n ≫ f' = (algebraic_topology.dold_kan.Q q).f n ≫ f'
@[simp]
theorem
algebraic_topology.dold_kan.P_idem
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q : ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.P_idem_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q : ℕ)
{X' : chain_complex C ℕ}
(f' : algebraic_topology.alternating_face_map_complex.obj X ⟶ X') :
@[simp]
theorem
algebraic_topology.dold_kan.Q_idem
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q : ℕ) :
@[simp]
theorem
algebraic_topology.dold_kan.Q_idem_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(q : ℕ)
{X' : chain_complex C ℕ}
(f' : algebraic_topology.alternating_face_map_complex.obj X ⟶ X') :
noncomputable
def
algebraic_topology.dold_kan.nat_trans_P
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(q : ℕ) :
For each q, P q is a natural transformation.
Equations
- algebraic_topology.dold_kan.nat_trans_P q = {app := λ (X : category_theory.simplicial_object C), algebraic_topology.dold_kan.P q, naturality' := _}
@[simp]
theorem
algebraic_topology.dold_kan.nat_trans_P_app
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(q : ℕ)
(X : category_theory.simplicial_object C) :
@[simp]
theorem
algebraic_topology.dold_kan.P_f_naturality_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(q 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 q).f n ≫ f' = (algebraic_topology.dold_kan.P q).f n ≫ f.app (opposite.op (simplex_category.mk n)) ≫ f'
@[simp]
theorem
algebraic_topology.dold_kan.P_f_naturality
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(q n : ℕ)
{X Y : category_theory.simplicial_object C}
(f : X ⟶ Y) :
f.app (opposite.op (simplex_category.mk n)) ≫ (algebraic_topology.dold_kan.P q).f n = (algebraic_topology.dold_kan.P q).f n ≫ f.app (opposite.op (simplex_category.mk n))
@[simp]
theorem
algebraic_topology.dold_kan.Q_f_naturality_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(q 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 q).f n ≫ f' = (algebraic_topology.dold_kan.Q q).f n ≫ f.app (opposite.op (simplex_category.mk n)) ≫ f'
@[simp]
theorem
algebraic_topology.dold_kan.Q_f_naturality
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(q n : ℕ)
{X Y : category_theory.simplicial_object C}
(f : X ⟶ Y) :
f.app (opposite.op (simplex_category.mk n)) ≫ (algebraic_topology.dold_kan.Q q).f n = (algebraic_topology.dold_kan.Q q).f n ≫ f.app (opposite.op (simplex_category.mk n))
@[simp]
theorem
algebraic_topology.dold_kan.nat_trans_Q_app
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(q : ℕ)
(X : category_theory.simplicial_object C) :
noncomputable
def
algebraic_topology.dold_kan.nat_trans_Q
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(q : ℕ) :
For each q, Q q is a natural transformation.
Equations
- algebraic_topology.dold_kan.nat_trans_Q q = {app := λ (X : category_theory.simplicial_object C), algebraic_topology.dold_kan.Q q, naturality' := _}
theorem
algebraic_topology.dold_kan.map_P
{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)
(q n : ℕ) :
G.map ((algebraic_topology.dold_kan.P q).f n) = (algebraic_topology.dold_kan.P q).f n
theorem
algebraic_topology.dold_kan.map_Q
{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)
(q n : ℕ) :
G.map ((algebraic_topology.dold_kan.Q q).f n) = (algebraic_topology.dold_kan.Q q).f n