English
There exists a natural isomorphism between the truncation of an augmented complex and the original, with explicit inverse and compatibility data.
Русский
Существует натуральное изоморфование между усечением дополненного комплекса и исходным, с явными обратными данными и совместимостью.
LaTeX
$$$\\exists \\; \\alpha: \\text{truncate}(\\text{augment}(C,f,w)) \\cong C$ with compatible inverse$$
Lean4
/-- Augmenting a truncated complex with the original object and morphism is isomorphic
(with components the identity) to the original complex.
-/
def augmentTruncate (C : ChainComplex V ℕ) : augment (truncate.obj C) (C.d 1 0) (C.d_comp_d _ _ _) ≅ C
where
hom :=
{ f := fun
| 0 => 𝟙 _
| _ + 1 => 𝟙 _
comm' := fun i j => by
match i with
| 0 | 1 | n + 2 => rcases j with - | j <;> dsimp [augment, truncate] <;> simp }
inv :=
{ f := fun
| 0 => 𝟙 _
| _ + 1 => 𝟙 _
comm' := fun i j => by
match i with
| 0 | 1 | n + 2 => rcases j with - | j <;> dsimp [augment, truncate] <;> simp }
hom_inv_id := by
ext i
cases i <;> simp
inv_hom_id := by
ext i
cases i <;> simp
