English
If K is strictly supported along e and e' is any embedding, then (K.truncGE e).IsStrictlySupported e'.
Русский
Если K строго поддержан вдоль e, то (K.truncGE e) строго поддержан вдоль любого вложения e'.
LaTeX
$$$(K\mathrm{truncGE} e).\mathrm{IsStrictlySupported}(e')$$$
Lean4
instance {ι'' : Type*} {c'' : ComplexShape ι''} (e' : c''.Embedding c') [K.IsStrictlySupported e'] :
(K.truncGE e).IsStrictlySupported e' where
isZero := by
intro i' hi'
by_cases hi'' : ∃ i, e.f i = i'
· obtain ⟨i, hi⟩ := hi''
by_cases hi''' : e.BoundaryGE i
· rw [IsZero.iff_id_eq_zero, ←
cancel_epi ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''').inv, ←
cancel_epi (HomologicalComplex.pOpcycles _ _)]
apply (K.isZero_X_of_isStrictlySupported e' i' hi').eq_of_src
·
exact
(K.isZero_X_of_isStrictlySupported e' i' hi').of_iso
((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIso e hi hi''')
· exact (K.truncGE e).isZero_X_of_isStrictlySupported e _ (by simpa using hi'')
