isGE_iff — Mathlib

English

For any X in the derived category, X.IsGE n holds if and only if Homology groups in degrees < n vanish.

Русский

Для любых X в производной категории свойство X.IsGE n эквивалентно тому, что гомологии в степенях ниже n равны нулю.

LaTeX

$$$$ X.IsGE(n) \iff \forall i < n,\ IsZero((\mathrm{homologyFunctor}\;C\;i).\mathrmobj X). $$$$

Lean4

theorem isGE_iff (X : DerivedCategory C) (n : ℤ) :
    X.IsGE n ↔ ∀ (i : ℤ) (_ : i < n), IsZero ((homologyFunctor C i).obj X) :=
  by
  constructor
  · rintro ⟨K, e, _⟩ i hi
    apply ((K.exactAt_of_isGE n i hi).isZero_homology).of_iso
    exact (homologyFunctor C i).mapIso e ≪≫ (homologyFunctorFactors C i).app K
  · intro hX
    have : (Q.objPreimage X).IsGE n := by
      rw [CochainComplex.isGE_iff]
      intro i hi
      rw [HomologicalComplex.exactAt_iff_isZero_homology]
      apply (hX i hi).of_iso
      exact (homologyFunctorFactors C i).symm.app _ ≪≫ (homologyFunctor C i).mapIso (Q.objObjPreimageIso X)
    exact
      ⟨(Q.objPreimage X).truncGE n, (Q.objObjPreimageIso X).symm ≪≫ asIso (Q.map ((Q.objPreimage X).πTruncGE n)),
        inferInstance⟩

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