English
Let X be an object in the derived category, and suppose X is GE in degree a and LE in degree b. Then there exists a cochain complex K with K.IsGE a and K.IsLE b, together with a Nonempty isomorphism X ≅ Q.obj K.
Русский
Пусть X — объект в производной категориe, и X GE в a, LE в b. Тогда существует когопроцесс K, удовлетворяющий K.IsGE a и K.IsLE b, и не пустое изоморование X ≅ Q.obj K.
LaTeX
$$$\forall (X : \text{DerivedCategory } C) (a b : \mathbb{Z}) [X.IsGE a] [X.IsLE b],\; \exists K, K.IsGE a ∧ K.IsLE b ∧ Nonempty (X \cong Q.obj K)$$$
Lean4
theorem exists_iso_Q_obj_of_isGE_of_isLE (X : DerivedCategory C) (a b : ℤ) [X.IsGE a] [X.IsLE b] :
∃ (K : CochainComplex C ℤ) (_ : K.IsStrictlyGE a) (_ : K.IsStrictlyLE b), Nonempty (X ≅ Q.obj K) :=
by
obtain ⟨K, hK, ⟨e⟩⟩ := X.exists_iso_Q_obj_of_isLE b
have : K.IsGE a := by
rw [← isGE_Q_obj_iff]
exact TStructure.t.isGE_of_iso e a
exact ⟨K.truncGE a, inferInstance, inferInstance, ⟨e ≪≫ asIso (Q.map (K.πTruncGE a))⟩⟩
