English
For a Karoubi object P in the simplicial setting, the differential respects the Karoubi decomposition, i.e. the d-map commutes with the projection to P.
Русский
Для объекта Карауби в симпликсиальном контексте дифференциал совместим с разложением Карауби; отображение d commuting с проекциями.
LaTeX
$$$((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n+1) n).f = P.p.app (\mathrm{op}\,⟦n+1⟧) \; \circ\; (AlternatingFaceMapComplex.obj P.X).d (n+1) n$$$
Lean4
theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
-- we start by expanding d ≫ d as a double sum
dsimp
simp only [comp_sum, sum_comp, ← Finset.sum_product']
-- then, we decompose the index set P into a subset S and its complement Sᶜ
let P := Fin (n + 2) × Fin (n + 3)
let S : Finset P := {ij : P | (ij.2 : ℕ) ≤ (ij.1 : ℕ)}
rw [Finset.univ_product_univ, ← Finset.sum_add_sum_compl S, ← eq_neg_iff_add_eq_zero, ← Finset.sum_neg_distrib]
/- we are reduced to showing that two sums are equal, and this is obtained
by constructing a bijection φ : S -> Sᶜ, which maps (i,j) to (j,i+1),
and by comparing the terms -/
let φ : ∀ ij : P, ij ∈ S → P := fun ij hij =>
(Fin.castLT ij.2 (lt_of_le_of_lt (Finset.mem_filter.mp hij).right (Fin.is_lt ij.1)), ij.1.succ)
apply Finset.sum_bij φ
· -- φ(S) is contained in Sᶜ
intro ij hij
simp_rw [S, φ, Finset.compl_filter, Finset.mem_filter_univ, Fin.val_succ, Fin.coe_castLT] at hij ⊢
cutsat
· -- φ : S → Sᶜ is injective
rintro ⟨i, j⟩ hij ⟨i', j'⟩ hij' h
rw [Prod.mk_inj]
exact
⟨by simpa [φ] using congr_arg Prod.snd h, by
simpa [φ, Fin.castSucc_castLT] using congr_arg Fin.castSucc (congr_arg Prod.fst h)⟩
· -- φ : S → Sᶜ is surjective
rintro ⟨i', j'⟩ hij'
simp_rw [S, Finset.compl_filter, Finset.mem_filter_univ, not_le] at hij'
refine ⟨(j'.pred <| ?_, Fin.castSucc i'), ?_, ?_⟩
· rintro rfl
simp only [Fin.val_zero, not_lt_zero'] at hij'
· simpa [S] using Nat.le_sub_one_of_lt hij'
· simp only [φ, Fin.castLT_castSucc, Fin.succ_pred]
· -- identification of corresponding terms in both sums
rintro ⟨i, j⟩ hij
dsimp
simp only [zsmul_comp, comp_zsmul, smul_smul, ← neg_smul]
congr 1
· simp only [φ, Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]
apply mul_comm
· rw [CategoryTheory.SimplicialObject.δ_comp_δ'']
simpa [S] using hij