English
Let X be a simplicial object in an abelian category C. For every n ∈ N there is a differential d_n: objX X (n+1) → objX X n in the normalized Moore complex. The case n = 0 is given by the composite Subobject.arrow followed by the face map X.δ(0) and the inverse of the top subobject arrow; for n ≥ 1 the differential d_n factors through the intersection of kernels of X.δ i for i = 1, … , n+1, in a canonical way, using δ(0) to induce the map to the next level.
Русский
Пусть X — симплициальный объект в абельевой категории C. Для каждого n ∈ N существует дифференциал d_n: objX X (n+1) → objX X n в нормализованном Moore-комплексе. Случай n = 0 задаётся как композиция Subobject.arrow, X.δ(0) и обратного away верхнего подобъекта; для n ≥ 1 дифференциал d_n факторизуется через пересечение ядер X.δ_i при i = 1, …, n+1 в каноническом виде, используя δ(0) для перехода к следующему уровню.
LaTeX
$$$\forall n:\mathbb{N},\; d_n : (\mathrm{objX}\,X\,(n+1)) \to (\mathrm{objX}\,X\,n)$.
- $d_0 = \mathrm{Subobject.arrow} \;\; \circ \; X.\delta(0) \; \circ \; (\top)^{-1}$.
- For n ≥ 1, $d_n$ factors through $\bigcap_{i=1}^{n+1} \ker( X.\delta(i) )$ and is induced by $X.\delta(0)$ through that intersection.$$
Lean4
/-- The differentials in the normalized Moore complex.
-/
@[simp]
def objD : ∀ n : ℕ, (objX X (n + 1) : C) ⟶ (objX X n : C)
| 0 => Subobject.arrow _ ≫ X.δ (0 : Fin 2) ≫ inv (⊤ : Subobject _).arrow
| n + 1 => by
-- The differential is `Subobject.arrow _ ≫ X.δ (0 : Fin (n+3))`,
-- factored through the intersection of the kernels.
refine
factorThru _ (arrow _ ≫ X.δ (0 : Fin (n + 3)))
?_
-- We now need to show that it factors!
-- A morphism factors through an intersection of subobjects if it factors through each.
refine
(finset_inf_factors _).mpr fun i _ =>
?_
-- A morphism `f` factors through the kernel of `g` exactly if `f ≫ g = 0`.
apply kernelSubobject_factors
dsimp [objX]
-- Use a simplicial identity
rw [Category.assoc, ← Fin.castSucc_zero, ← X.δ_comp_δ (Fin.zero_le i.succ)]
-- We can rewrite the arrow out of the intersection of all the kernels as a composition
-- of a morphism we don't care about with the arrow out of the kernel of `X.δ i.succ.succ`.
rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i.succ (by simp)), Category.assoc,
kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
