Split simplicial objects in preadditive categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define a functor nondeg_complex : simplicial_object.split C ⥤ chain_complex C ℕ
when C is a preadditive category with finite coproducts, and get an isomorphism
to_karoubi_nondeg_complex_iso_N₁ : nondeg_complex ⋙ to_karoubi _ ≅ forget C ⋙ dold_kan.N₁.
(See equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)
noncomputable
def
simplicial_object.splitting.π_summand
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.limits.has_zero_morphisms C]
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
The projection on a summand of the coproduct decomposition given by a splitting of a simplicial object.
Equations
- s.π_summand A = (s.iso Δ).inv ≫ category_theory.limits.sigma.desc (λ (B : simplicial_object.splitting.index_set Δ), dite (B = A) (λ (h : B = A), category_theory.eq_to_hom _) (λ (h : ¬B = A), 0))
@[simp]
theorem
simplicial_object.splitting.ι_π_summand_eq_id
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.limits.has_zero_morphisms C]
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ) :
@[simp]
theorem
simplicial_object.splitting.ι_π_summand_eq_id_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.limits.has_zero_morphisms C]
{Δ : simplex_categoryᵒᵖ}
(A : simplicial_object.splitting.index_set Δ)
{X' : C}
(f' : s.N (opposite.unop A.fst).len ⟶ X') :
@[simp]
theorem
simplicial_object.splitting.ι_π_summand_eq_zero_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.limits.has_zero_morphisms C]
{Δ : simplex_categoryᵒᵖ}
(A B : simplicial_object.splitting.index_set Δ)
(h : B ≠ A)
{X' : C}
(f' : s.N (opposite.unop B.fst).len ⟶ X') :
@[simp]
theorem
simplicial_object.splitting.ι_π_summand_eq_zero
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.limits.has_zero_morphisms C]
{Δ : simplex_categoryᵒᵖ}
(A B : simplicial_object.splitting.index_set Δ)
(h : B ≠ A) :
theorem
simplicial_object.splitting.decomposition_id
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
(Δ : simplex_categoryᵒᵖ) :
𝟙 (X.obj Δ) = finset.univ.sum (λ (A : simplicial_object.splitting.index_set Δ), s.π_summand A ≫ s.ι_summand A)
@[simp]
theorem
simplicial_object.splitting.σ_comp_π_summand_id_eq_zero_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
{n : ℕ}
(i : fin (n + 1))
{X' : C}
(f' : s.N (opposite.unop (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk (n + 1)))).fst).len ⟶ X') :
X.σ i ≫ s.π_summand (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk (n + 1)))) ≫ f' = 0 ≫ f'
@[simp]
theorem
simplicial_object.splitting.σ_comp_π_summand_id_eq_zero
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
{n : ℕ}
(i : fin (n + 1)) :
X.σ i ≫ s.π_summand (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk (n + 1)))) = 0
theorem
simplicial_object.splitting.ι_summand_comp_P_infty_eq_zero
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
[category_theory.preadditive C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
{n : ℕ}
(A : simplicial_object.splitting.index_set (opposite.op (simplex_category.mk n)))
(hA : ¬A.eq_id) :
s.ι_summand A ≫ algebraic_topology.dold_kan.P_infty.f n = 0
If a simplicial object X in an additive category is split,
then P_infty vanishes on all the summands of X _[n] which do
not correspond to the identity of [n].
theorem
simplicial_object.splitting.comp_P_infty_eq_zero_iff
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
{Z : C}
{n : ℕ}
(f : Z ⟶ X.obj (opposite.op (simplex_category.mk n))) :
f ≫ algebraic_topology.dold_kan.P_infty.f n = 0 ↔ f ≫ s.π_summand (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n))) = 0
@[simp]
theorem
simplicial_object.splitting.P_infty_comp_π_summand_id
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
(n : ℕ) :
@[simp]
theorem
simplicial_object.splitting.P_infty_comp_π_summand_id_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
(n : ℕ)
{X' : C}
(f' : s.N (opposite.unop (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n))).fst).len ⟶ X') :
@[simp]
theorem
simplicial_object.splitting.π_summand_comp_ι_summand_comp_P_infty_eq_P_infty
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
(n : ℕ) :
@[simp]
theorem
simplicial_object.splitting.π_summand_comp_ι_summand_comp_P_infty_eq_P_infty_assoc
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
(n : ℕ)
{X' : C}
(f' : (algebraic_topology.alternating_face_map_complex.obj X).X n ⟶ X') :
@[simp]
noncomputable
def
simplicial_object.splitting.d
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
(i j : ℕ) :
The differentials s.d i j : s.N i ⟶ s.N j on nondegenerate simplices of a split
simplicial object are induced by the differentials on the alternating face map complex.
Equations
theorem
simplicial_object.splitting.ι_summand_comp_d_comp_π_summand_eq_zero
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
(j k : ℕ)
(A : simplicial_object.splitting.index_set (opposite.op (simplex_category.mk j)))
(hA : ¬A.eq_id) :
@[simp]
theorem
simplicial_object.splitting.nondeg_complex_X
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
(ᾰ : ℕ) :
s.nondeg_complex.X ᾰ = s.N ᾰ
noncomputable
def
simplicial_object.splitting.nondeg_complex
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C] :
If s is a splitting of a simplicial object X in a preadditive category,
s.nondeg_complex is a chain complex which is given in degree n by
the nondegenerate n-simplices of X.
@[simp]
theorem
simplicial_object.splitting.nondeg_complex_d
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
(i j : ℕ) :
s.nondeg_complex.d i j = s.d i j
noncomputable
def
simplicial_object.splitting.to_karoubi_nondeg_complex_iso_N₁
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C] :
The chain complex s.nondeg_complex attached to a splitting of a simplicial object X
becomes isomorphic to the normalized Moore complex N₁.obj X defined as a formal direct
factor in the category karoubi (chain_complex C ℕ).
Equations
- s.to_karoubi_nondeg_complex_iso_N₁ = {hom := {f := {f := λ (n : ℕ), s.ι_summand (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n))) ≫ algebraic_topology.dold_kan.P_infty.f n, comm' := _}, comm := _}, inv := {f := {f := λ (n : ℕ), s.π_summand (simplicial_object.splitting.index_set.id (opposite.op (simplex_category.mk n))), comm' := _}, comm := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
simplicial_object.splitting.to_karoubi_nondeg_complex_iso_N₁_inv_f_f
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
(n : ℕ) :
@[simp]
theorem
simplicial_object.splitting.to_karoubi_nondeg_complex_iso_N₁_hom_f_f
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_finite_coproducts C]
{X : category_theory.simplicial_object C}
(s : simplicial_object.splitting X)
[category_theory.preadditive C]
(n : ℕ) :
@[simp]
noncomputable
def
simplicial_object.split.nondeg_complex_functor
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The functor which sends a split simplicial object in a preadditive category to the chain complex which consists of nondegenerate simplices.
Equations
- simplicial_object.split.nondeg_complex_functor = {obj := λ (S : simplicial_object.split C), S.s.nondeg_complex, map := λ (S₁ S₂ : simplicial_object.split C) (Φ : S₁ ⟶ S₂), {f := Φ.f, comm' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
simplicial_object.split.nondeg_complex_functor_map_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(S₁ S₂ : simplicial_object.split C)
(Φ : S₁ ⟶ S₂)
(n : ℕ) :
(simplicial_object.split.nondeg_complex_functor.map Φ).f n = Φ.f n
@[simp]
theorem
simplicial_object.split.to_karoubi_nondeg_complex_functor_iso_N₁_hom_app_f_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(X : simplicial_object.split C)
(n : ℕ) :
@[simp]
theorem
simplicial_object.split.to_karoubi_nondeg_complex_functor_iso_N₁_inv_app_f_f
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C]
(X : simplicial_object.split C)
(n : ℕ) :
noncomputable
def
simplicial_object.split.to_karoubi_nondeg_complex_functor_iso_N₁
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_coproducts C] :
The natural isomorphism (in karoubi (chain_complex C ℕ)) between the chain complex
of nondegenerate simplices of a split simplicial object and the normalized Moore complex
defined as a formal direct factor of the alternating face map complex.
Equations
- simplicial_object.split.to_karoubi_nondeg_complex_functor_iso_N₁ = category_theory.nat_iso.of_components (λ (S : simplicial_object.split C), S.s.to_karoubi_nondeg_complex_iso_N₁) simplicial_object.split.to_karoubi_nondeg_complex_functor_iso_N₁._proof_1