English
CanonicalDescShortComplex morphism is a quasi-isomorphism in the short exact context.
Русский
Канонический морфизм DescShortComplex является квазиизоморфизмом в контексте краткой точной последовательности.
LaTeX
$$$\text{QuasiIso}(\operatorname{descShortComplex} S)$$$
Lean4
/-- The collection of all single functors `C ⥤ CochainComplex C ℤ` along with
their compatibilites with shifts. (This definition has purposely no `simps`
attribute, as the generated lemmas would not be very useful.) -/
noncomputable def singleFunctors : SingleFunctors C (CochainComplex C ℤ) ℤ
where
functor n := single _ _ n
shiftIso n a a'
ha' :=
NatIso.ofComponents
(fun X =>
Hom.isoOfComponents
(fun i =>
eqToIso
(by
obtain rfl : a' = a + n := by omega
by_cases h : i = a
· subst h
simp only [Functor.comp_obj, shiftFunctor_obj_X', single_obj_X_self]
· dsimp [single]
rw [if_neg h, if_neg (fun h' => h (by omega))])))
(fun {X Y} f => by
obtain rfl : a' = a + n := by omega
ext
simp [single])
shiftIso_zero
a := by
ext
dsimp
simp only [single, shiftFunctorZero_eq, shiftFunctorZero'_hom_app_f, XIsoOfEq, eqToIso.hom]
shiftIso_add n m a a' a'' ha'
ha'' := by
ext
dsimp
simp only [shiftFunctorAdd_eq, shiftFunctorAdd'_hom_app_f, XIsoOfEq, eqToIso.hom, eqToHom_trans, id_comp]
