isGE_Q_obj_iff — Mathlib

English

For a cochain complex K, (Q.obj K).IsGE n holds iff K.IsGE n.

Русский

Для коchain-комплекса K верно: (Q.obj K).IsGE n тогда и только тогда K.IsGE n.

LaTeX

$$$$ (\mathrm{Q.obj} K).IsGE(n) \iff K.IsGE(n). $$$$

Lean4

theorem isGE_Q_obj_iff (K : CochainComplex C ℤ) (n : ℤ) : (Q.obj K).IsGE n ↔ K.IsGE n :=
  by
  have eq := fun i ↦ ((homologyFunctorFactors C i).app K).isZero_iff
  simp only [Functor.comp_obj, HomologicalComplex.homologyFunctor_obj] at eq
  simp only [isGE_iff, CochainComplex.isGE_iff, HomologicalComplex.exactAt_iff_isZero_homology, eq]

Похожие утверждения