Lean4
/-- The canonical t-structure on `DerivedCategory C`. -/
def t : TStructure (DerivedCategory C)
where
le n X := ∃ (K : CochainComplex C ℤ) (_ : X ≅ DerivedCategory.Q.obj K), K.IsStrictlyLE n
ge n X := ∃ (K : CochainComplex C ℤ) (_ : X ≅ DerivedCategory.Q.obj K), K.IsStrictlyGE n
le_isClosedUnderIsomorphisms
n :=
{
of_iso := by
rintro X Y e ⟨K, e', _⟩
exact ⟨K, e.symm ≪≫ e', inferInstance⟩ }
ge_isClosedUnderIsomorphisms
n :=
{
of_iso := by
rintro X Y e ⟨K, e', _⟩
exact ⟨K, e.symm ≪≫ e', inferInstance⟩ }
le_shift := by
rintro n a n' h X ⟨K, e, _⟩
exact
⟨(shiftFunctor (CochainComplex C ℤ) a).obj K,
(shiftFunctor (DerivedCategory C) a).mapIso e ≪≫ (Q.commShiftIso a).symm.app K, K.isStrictlyLE_shift n a n' h⟩
ge_shift := by
rintro n a n' h X ⟨K, e, _⟩
exact
⟨(shiftFunctor (CochainComplex C ℤ) a).obj K,
(shiftFunctor (DerivedCategory C) a).mapIso e ≪≫ (Q.commShiftIso a).symm.app K, K.isStrictlyGE_shift n a n' h⟩
zero' X Y
f := by
rintro ⟨K, e₁, _⟩ ⟨L, e₂, _⟩
rw [← cancel_epi e₁.inv, ← cancel_mono e₂.hom, comp_zero, zero_comp]
apply (subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE K L 0 1 (by simp)).elim
le_zero_le := by
rintro X ⟨K, e, _⟩
exact ⟨K, e, K.isStrictlyLE_of_le 0 1 (by omega)⟩
ge_one_le := by
rintro X ⟨K, e, _⟩
exact ⟨K, e, K.isStrictlyGE_of_ge 0 1 (by omega)⟩
exists_triangle_zero_one
X := by
obtain ⟨K, ⟨e₂⟩⟩ : ∃ K, Nonempty (Q.obj K ≅ X) := ⟨_, ⟨Q.objObjPreimageIso X⟩⟩
have h := K.shortComplexTruncLE_shortExact 0
refine
⟨Q.obj (K.truncLE 0), Q.obj (K.truncGE 1), ⟨_, Iso.refl _, inferInstance⟩, ⟨_, Iso.refl _, inferInstance⟩,
Q.map (K.ιTruncLE 0) ≫ e₂.hom, e₂.inv ≫ Q.map (K.πTruncGE 1),
inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 (by omega))) ≫ (triangleOfSES h).mor₃,
isomorphic_distinguished _ (triangleOfSES_distinguished h) _ (Iso.symm ?_)⟩
refine
Triangle.isoMk _ _ (Iso.refl _) e₂ (asIso (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 (by omega)))) ?_ ?_
(by simp)
· dsimp
rw [id_comp]
rfl
· dsimp
rw [← Q.map_comp, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE, Iso.hom_inv_id_assoc]
