English
Let C be a chain complex in V. For any object X and any morphism f: C_0 → X with C.d_{1,0} ; f = 0, there exists a new chain complex C' with C'_0 = X, C'_{n+1} = C_n for n ≥ 0, and differential defined by d'_{1,0} = f and d'_{i+1,j+1} = d_{i,j} (for i,j ≥ 0); all other differentials vanish. Equivalently, augment(C, f, w) is a chain complex built by inserting X at degree 0 and shifting the original complex upward, provided w expresses the condition d_{1,0} ∘ f = 0.
Русский
Пусть C — цепной комплекс в категориях. Пусть X — объект, и дан морфизм f: C_0 → X такой, что d_{1,0} ; f = 0. Тогда существует новый цепной комплекс C' такой, что C'_0 = X, C'_{n+1} = C_n для всех n ≥ 0, и дифференциал задан: d'_{1,0} = f, d'_{i+1,j+1} = d_{i j} (при i,j ≥ 0), остальное равно 0. Эквивалентно, C' = augment(C, f, w) — цепной комплекс, получаемый вставкой X в нулевой степени и сдвигом исходного комплекса вверх, где w выражает условие d_{1,0} ∘ f = 0.
LaTeX
$$$\\text{augment}(C,f,w)$ is the chain complex with $(\\text{augment}(C,f,w))_0 = X$, $(\\text{augment}(C,f,w))_{n+1} = C_n$ for $n\\ge 0$, with $d'_{1,0} = f$ and $d'_{i+1,j+1} = d_{i j}$, $d'_{i j} = 0$ otherwise, where $w: C.d_{1 0} \\circ f = 0$.$$
Lean4
/-- We can "augment" a chain complex by inserting an arbitrary object in degree zero
(shifting everything else up), along with a suitable differential.
-/
def augment (C : ChainComplex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : C.d 1 0 ≫ f = 0) : ChainComplex V ℕ
where
X
| 0 => X
| i + 1 => C.X i
d
| 1, 0 => f
| i + 1, j + 1 => C.d i j
| _, _ => 0
shape
| 1, 0, h => absurd rfl h
| _ + 2, 0, _ => rfl
| 0, _, _ => rfl
| i + 1, j + 1, h => by simp only; exact C.shape i j (Nat.succ_ne_succ.1 h)
d_comp_d'
| _, _, 0, rfl, rfl => w
| _, _, k + 1, rfl, rfl => C.d_comp_d _ _ _
