From 870ef7aa0b0738f861589ff2ced7af997db10fb8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 15 Feb 2026 17:03:56 +0100 Subject: [PATCH 1/7] truncltge-1 --- .../Triangulated/TStructure/TruncLTGE.lean | 338 +++++++++++++++++- 1 file changed, 331 insertions(+), 7 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean b/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean index 44036a78497de9..81fb6918e516eb 100644 --- a/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean +++ b/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean @@ -19,13 +19,21 @@ part of a distinguished triangle `(t.truncLT n).obj X ⟶ X ⟶ (t.truncGE n).obj X ⟶ ((t.truncLT n).obj X)⟦1⟧` for any `X : C`, with `(t.truncLT n).obj X < n` and `(t.truncGE n).obj X ≥ n`. +We obtain various properties of these truncation functors. +Variants `truncGT` and `truncLE` are introduced in the file +`Mathlib/CategoryTheory/Triangulated/TStucture/TruncLEGT.lean`. +Extensions to indices in `EInt` instead of `ℤ` are introduced in the file +`Mathlib/CategoryTheory/Triangulated/TStucture/ETrunc.lean`. +The spectral object attached to an object `X : C` is constructed in the file +`Mathlib/CategoryTheory/Triangulated/TStucture/SpectralObject.lean`. + -/ universe v u namespace CategoryTheory -open Limits Pretriangulated +open Limits Pretriangulated ZeroObject variable {C : Type u} [Category.{v} C] [Preadditive C] [HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] @@ -163,6 +171,43 @@ instance isGE_triangleFunctor_obj_obj₃ : dsimp [triangleFunctor] infer_instance +noncomputable def triangleMapOfLE (a b : ℤ) (h : a ≤ b) : triangle t a A ⟶ triangle t b A := + have H := triangle_map_exists t (triangle_distinguished t a A) + (triangle_distinguished t b A) (𝟙 _) (a-1) b inferInstance inferInstance + { hom₁ := H.choose.hom₁ + hom₂ := 𝟙 _ + hom₃ := H.choose.hom₃ + comm₁ := by rw [← H.choose.comm₁, H.choose_spec] + comm₂ := by rw [H.choose.comm₂, H.choose_spec] + comm₃ := H.choose.comm₃ } + +noncomputable def triangleFunctorNatTransOfLE (a b : ℤ) (h : a ≤ b) : + triangleFunctor t a ⟶ triangleFunctor t b where + app X := triangleMapOfLE t X a b h + naturality {X₁ X₂} φ := + triangle_map_ext t (triangleFunctor_obj_distinguished _ _ _) + (triangleFunctor_obj_distinguished _ _ _) (a - 1) b inferInstance inferInstance + (by simp [triangleMapOfLE]) + +@[simp] +lemma triangleFunctorNatTransOfLE_app_hom₂ (a b : ℤ) (h : a ≤ b) (X : C) : + ((triangleFunctorNatTransOfLE t a b h).app X).hom₂ = 𝟙 X := rfl + +lemma triangleFunctorNatTransOfLE_trans (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) : + triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc = + triangleFunctorNatTransOfLE t a c (hab.trans hbc) := by + apply NatTrans.ext + ext1 X + exact triangle_map_ext t (triangleFunctor_obj_distinguished _ _ _) + (triangleFunctor_obj_distinguished _ _ _) (a - 1) c inferInstance inferInstance (by simp) + +lemma triangleFunctorNatTransOfLE_refl (a : ℤ) : + triangleFunctorNatTransOfLE t a a (by rfl) = 𝟙 _ := by + apply NatTrans.ext + ext1 X + exact triangle_map_ext t (triangleFunctor_obj_distinguished _ _ _) + (triangleFunctor_obj_distinguished _ _ _) (a - 1) a inferInstance inferInstance (by simp) + instance : (triangleFunctor t n).Additive where end TruncAux @@ -201,13 +246,29 @@ on a category `C` and `n : ℤ`. -/ noncomputable def truncGEπ (n : ℤ) : 𝟭 _ ⟶ t.truncGE n := Functor.whiskerLeft (TruncAux.triangleFunctor t n) Triangle.π₂Toπ₃ -instance (X : C) (n : ℤ) : t.IsLE ((t.truncLT n).obj X) (n - 1) := by - dsimp [truncLT] - infer_instance +@[reassoc (attr := simp)] +lemma truncGEπ_naturality (n : ℤ) {X Y : C} (f : X ⟶ Y) : + (t.truncGEπ n).app X ≫ (t.truncGE n).map f = f ≫ (t.truncGEπ n).app Y := + ((t.truncGEπ n).naturality f).symm -instance (X : C) (n : ℤ) : t.IsGE ((t.truncGE n).obj X) n := by - dsimp [truncGE] - infer_instance +lemma isLE_truncLT_obj (X : C) (a b : ℤ) (hn : a ≤ b + 1 := by lia) : + t.IsLE ((t.truncLT a).obj X) b := by + have : t.IsLE ((t.truncLT a).obj X) (a - 1) := by dsimp [truncLT]; infer_instance + exact t.isLE_of_le _ (a - 1) _ (by lia) + +instance (X : C) (n : ℤ) : t.IsLE ((t.truncLT n).obj X) (n - 1) := + t.isLE_truncLT_obj .. + +instance (X : C) (n : ℤ) : t.IsLE ((t.truncLT (n + 1)).obj X) n := + t.isLE_truncLT_obj .. + +lemma isGE_truncGE_obj (X : C) (a b : ℤ) (hn : b ≤ a := by lia) : + t.IsGE ((t.truncGE a).obj X) b := by + have : t.IsGE ((t.truncGE a).obj X) a := by dsimp [truncGE]; infer_instance + exact t.isGE_of_ge _ _ a (by lia) + +instance (X : C) (n : ℤ) : t.IsGE ((t.truncGE n).obj X) n := + t.isGE_truncGE_obj .. /-- The connecting morphism `t.truncGE n ⟶ t.truncLT n ⋙ shiftFunctor C (1 : ℤ)` when `t` is a t-structure on a pretriangulated category and `n : ℤ`. -/ @@ -234,6 +295,269 @@ instance (X : C) (n : ℤ) : t.IsGE ((t.triangleLTGE n).obj X).obj₃ n := by dsimp infer_instance +@[reassoc (attr := simp)] +lemma truncLTι_comp_truncGEπ_app (n : ℤ) (X : C) : + (t.truncLTι n).app X ≫ (t.truncGEπ n).app X = 0 := + comp_distTriang_mor_zero₁₂ _ (t.triangleLTGE_distinguished n X) + +@[reassoc (attr := simp)] +lemma truncGEπ_comp_truncGEδLT_app (n : ℤ) (X : C) : + (t.truncGEπ n).app X ≫ (t.truncGEδLT n).app X = 0 := + comp_distTriang_mor_zero₂₃ _ (t.triangleLTGE_distinguished n X) + +@[reassoc (attr := simp)] +lemma truncGEδLT_comp_truncLTι_app (n : ℤ) (X : C) : + (t.truncGEδLT n).app X ≫ ((t.truncLTι n).app X)⟦(1 : ℤ)⟧' = 0 := + comp_distTriang_mor_zero₃₁ _ (t.triangleLTGE_distinguished n X) + +@[reassoc (attr := simp)] +lemma truncLTι_comp_truncGEπ (n : ℤ) : + t.truncLTι n ≫ t.truncGEπ n = 0 := by cat_disch + +@[reassoc (attr := simp)] +lemma truncGEπ_comp_truncGEδLT (n : ℤ) : + t.truncGEπ n ≫ t.truncGEδLT n = 0 := by cat_disch + +@[reassoc (attr := simp)] +lemma truncGEδLT_comp_truncLTι (n : ℤ) : + t.truncGEδLT n ≫ Functor.whiskerRight (t.truncLTι n) (shiftFunctor C (1 : ℤ)) = 0 := by + cat_disch + +/-- The natural transformation `t.truncLT a ⟶ t.truncLT b` when `a ≤ b`. -/ +noncomputable def natTransTruncLTOfLE (a b : ℤ) (h : a ≤ b) : + t.truncLT a ⟶ t.truncLT b := + Functor.whiskerRight (TruncAux.triangleFunctorNatTransOfLE t a b h) Triangle.π₁ + +/-- The natural transformation `t.truncGE a ⟶ t.truncGE b` when `a ≤ b`. -/ +noncomputable def natTransTruncGEOfLE (a b : ℤ) (h : a ≤ b) : + t.truncGE a ⟶ t.truncGE b := + Functor.whiskerRight (TruncAux.triangleFunctorNatTransOfLE t a b h) Triangle.π₃ + +@[reassoc (attr := simp)] +lemma natTransTruncLTOfLE_ι_app (a b : ℤ) (h : a ≤ b) (X : C) : + (t.natTransTruncLTOfLE a b h).app X ≫ (t.truncLTι b).app X = (t.truncLTι a).app X := by + simpa using ((TruncAux.triangleFunctorNatTransOfLE t a b h).app X).comm₁.symm + +@[reassoc (attr := simp)] +lemma natTransTruncLTOfLE_ι (a b : ℤ) (h : a ≤ b) : + t.natTransTruncLTOfLE a b h ≫ t.truncLTι b = t.truncLTι a := by cat_disch + +@[reassoc (attr := simp)] +lemma π_natTransTruncGEOfLE_app (a b : ℤ) (h : a ≤ b) (X : C) : + (t.truncGEπ a).app X ≫ (t.natTransTruncGEOfLE a b h).app X = (t.truncGEπ b).app X := by + simpa only [TruncAux.triangleFunctor_obj, TruncAux.triangle_obj₂, + TruncAux.triangleFunctorNatTransOfLE_app_hom₂, Category.id_comp] using + ((TruncAux.triangleFunctorNatTransOfLE t a b h).app X).comm₂ + +@[reassoc] +lemma truncGEδLT_comp_natTransTruncLTOfLE_app (a b : ℤ) (h : a ≤ b) (X : C) : + (t.truncGEδLT a).app X ≫ ((natTransTruncLTOfLE t a b h).app X)⟦(1 :ℤ)⟧' = + (t.natTransTruncGEOfLE a b h).app X ≫ (t.truncGEδLT b).app X := + ((TruncAux.triangleFunctorNatTransOfLE t a b h).app X).comm₃ + +@[reassoc] +lemma truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE (a b : ℤ) (h : a ≤ b) : + t.truncGEδLT a ≫ Functor.whiskerRight (natTransTruncLTOfLE t a b h) (shiftFunctor C (1 : ℤ)) = + t.natTransTruncGEOfLE a b h ≫ t.truncGEδLT b := by + ext X + exact t.truncGEδLT_comp_natTransTruncLTOfLE_app a b h X + +@[reassoc (attr := simp)] +lemma π_natTransTruncGEOfLE (a b : ℤ) (h : a ≤ b) : + t.truncGEπ a ≫ t.natTransTruncGEOfLE a b h = t.truncGEπ b := by cat_disch + +/-- The natural transformation `t.triangleLTGE a ⟶ t.triangleLTGE b` +when `a ≤ b`. -/ +noncomputable def natTransTriangleLTGEOfLE (a b : ℤ) (h : a ≤ b) : + t.triangleLTGE a ⟶ t.triangleLTGE b := by + refine Triangle.functorHomMk' (t.natTransTruncLTOfLE a b h) (𝟙 _) + ((t.natTransTruncGEOfLE a b h)) ?_ ?_ ?_ + · simp + · simp + · exact t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE a b h + +@[simp] +lemma natTransTriangleLTGEOfLE_refl (a : ℤ) : + t.natTransTriangleLTGEOfLE a a (by rfl) = 𝟙 _ := + TruncAux.triangleFunctorNatTransOfLE_refl t a + +lemma natTransTriangleLTGEOfLE_trans (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) : + t.natTransTriangleLTGEOfLE a b hab ≫ t.natTransTriangleLTGEOfLE b c hbc = + t.natTransTriangleLTGEOfLE a c (hab.trans hbc) := + TruncAux.triangleFunctorNatTransOfLE_trans t a b c hab hbc + +@[simp] +lemma natTransTruncLTOfLE_refl (a : ℤ) : + t.natTransTruncLTOfLE a a (by rfl) = 𝟙 _ := + congr_arg (fun x ↦ Functor.whiskerRight x (Triangle.π₁)) (t.natTransTriangleLTGEOfLE_refl a) + +@[simp] +lemma natTransTruncLTOfLE_trans (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) : + t.natTransTruncLTOfLE a b hab ≫ t.natTransTruncLTOfLE b c hbc = + t.natTransTruncLTOfLE a c (hab.trans hbc) := + congr_arg (fun x ↦ Functor.whiskerRight x Triangle.π₁) + (t.natTransTriangleLTGEOfLE_trans a b c hab hbc) + +@[simp] +lemma natTransTruncGEOfLE_refl (a : ℤ) : + t.natTransTruncGEOfLE a a (by rfl) = 𝟙 _ := + congr_arg (fun x ↦ Functor.whiskerRight x (Triangle.π₃)) (t.natTransTriangleLTGEOfLE_refl a) + +@[simp] +lemma natTransTruncGEOfLE_trans (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) : + t.natTransTruncGEOfLE a b hab ≫ t.natTransTruncGEOfLE b c hbc = + t.natTransTruncGEOfLE a c (hab.trans hbc) := + congr_arg (fun x ↦ Functor.whiskerRight x Triangle.π₃) + (t.natTransTriangleLTGEOfLE_trans a b c hab hbc) + +lemma natTransTruncLTOfLE_refl_app (a : ℤ) (X : C) : + (t.natTransTruncLTOfLE a a (by rfl)).app X = 𝟙 _ := + congr_app (t.natTransTruncLTOfLE_refl a) X + +lemma natTransTruncLTOfLE_trans_app (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C) : + (t.natTransTruncLTOfLE a b hab).app X ≫ (t.natTransTruncLTOfLE b c hbc).app X = + (t.natTransTruncLTOfLE a c (hab.trans hbc)).app X := + congr_app (t.natTransTruncLTOfLE_trans a b c hab hbc) X + +lemma natTransTruncGEOfLE_refl_app (a : ℤ) (X : C) : + (t.natTransTruncGEOfLE a a (by rfl)).app X = 𝟙 _ := + congr_app (t.natTransTruncGEOfLE_refl a) X + +lemma natTransTruncGEOfLE_trans_app (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C) : + (t.natTransTruncGEOfLE a b hab).app X ≫ (t.natTransTruncGEOfLE b c hbc).app X = + (t.natTransTruncGEOfLE a c (hab.trans hbc)).app X := + congr_app (t.natTransTruncGEOfLE_trans a b c hab hbc) X + +lemma isLE_of_isZero {X : C} (hX : IsZero X) (n : ℤ) : t.IsLE X n := + t.isLE_of_iso (((t.truncLT (n + 1)).map_isZero hX).isoZero ≪≫ hX.isoZero.symm) n + +lemma isGE_of_isZero {X : C} (hX : IsZero X) (n : ℤ) : t.IsGE X n := + t.isGE_of_iso (((t.truncGE n).map_isZero hX).isoZero ≪≫ hX.isoZero.symm) n + +instance (n : ℤ) : t.IsLE (0 : C) n := t.isLE_of_isZero (isZero_zero C) n + +instance (n : ℤ) : t.IsGE (0 : C) n := t.isGE_of_isZero (isZero_zero C) n + +lemma isLE_iff_isIso_truncLTι_app (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : + t.IsLE X n₀ ↔ IsIso (((t.truncLTι n₁)).app X) := by + subst h + refine ⟨fun _ ↦ ?_, + fun _ ↦ t.isLE_of_iso (asIso (((t.truncLTι (n₀ + 1))).app X)) n₀⟩ + obtain ⟨e, he⟩ := t.triangle_iso_exists + (contractible_distinguished X) (t.triangleLTGE_distinguished (n₀ + 1) X) + (Iso.refl X) n₀ (n₀ + 1) + (by dsimp; infer_instance) (by dsimp; infer_instance) + (by dsimp; infer_instance) (by dsimp; infer_instance) + have he' : e.inv.hom₂ = 𝟙 X := by + rw [← cancel_mono e.hom.hom₂, ← comp_hom₂, e.inv_hom_id, he] + simp + have : (t.truncLTι (n₀ + 1)).app X = e.inv.hom₁ := by + simpa [he'] using e.inv.comm₁ + rw [this] + infer_instance + +lemma isGE_iff_isIso_truncGEπ_app (n : ℤ) (X : C) : + t.IsGE X n ↔ IsIso ((t.truncGEπ n).app X) := by + constructor + · intro h + obtain ⟨e, he⟩ := t.triangle_iso_exists + (inv_rot_of_distTriang _ (contractible_distinguished X)) + (t.triangleLTGE_distinguished n X) (Iso.refl X) (n - 1) n + (t.isLE_of_iso (shiftFunctor C (-1 : ℤ)).mapZeroObject.symm _) + (by dsimp; infer_instance) (by dsimp; infer_instance) (by dsimp; infer_instance) + dsimp at he + have : (truncGEπ t n).app X = e.hom.hom₃ := by + have := e.hom.comm₂ + dsimp at this + rw [← cancel_epi e.hom.hom₂, ← this, he] + rw [this] + infer_instance + · intro + exact t.isGE_of_iso (asIso ((truncGEπ t n).app X)).symm n + +instance (X : C) (n : ℤ) [t.IsGE X n] : IsIso ((t.truncGEπ n).app X) := by + rw [← isGE_iff_isIso_truncGEπ_app] + infer_instance + +lemma isGE_iff_isZero_truncLT_obj (n : ℤ) (X : C) : + t.IsGE X n ↔ IsZero ((t.truncLT n).obj X) := by + rw [t.isGE_iff_isIso_truncGEπ_app n X] + exact (Triangle.isZero₁_iff_isIso₂ _ (t.triangleLTGE_distinguished n X)).symm + +lemma isLE_iff_isZero_truncGE_obj (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : + t.IsLE X n₀ ↔ IsZero ((t.truncGE n₁).obj X) := by + rw [t.isLE_iff_isIso_truncLTι_app n₀ n₁ h X] + exact (Triangle.isZero₃_iff_isIso₁ _ (t.triangleLTGE_distinguished n₁ X)).symm + +lemma isZero_truncLT_obj_of_isGE (n : ℤ) (X : C) [t.IsGE X n] : + IsZero ((t.truncLT n).obj X) := by + rw [← isGE_iff_isZero_truncLT_obj] + infer_instance + +lemma isZero_truncGE_obj_of_isLE (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) [t.IsLE X n₀] : + IsZero ((t.truncGE n₁).obj X) := by + rw [← t.isLE_iff_isZero_truncGE_obj _ _ h X] + infer_instance + +lemma from_truncGE_obj_ext {n : ℤ} {X : C} {Y : C} + {f₁ f₂ : (t.truncGE n).obj X ⟶ Y} (h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂) + [t.IsGE Y n] : + f₁ = f₂ := by + suffices ∀ (f : (t.truncGE n).obj X ⟶ Y), (t.truncGEπ n).app X ≫ f = 0 → f = 0 by + rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)] + intro f hf + obtain ⟨g, hg⟩ := Triangle.yoneda_exact₃ _ + (t.triangleLTGE_distinguished n X) f hf + have hg' := t.zero_of_isLE_of_isGE g (n-2) n (by lia) + (by exact t.isLE_shift _ (n-1) 1 (n-2) (by lia)) inferInstance + rw [hg, hg', comp_zero] + +lemma to_truncLT_obj_ext {n : ℤ} {Y : C} {X : C} + {f₁ f₂ : Y ⟶ (t.truncLT n).obj X} + (h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X) + [t.IsLE Y (n - 1)] : + f₁ = f₂ := by + suffices ∀ (f : Y ⟶ (t.truncLT n).obj X) (_ : f ≫ (t.truncLTι n).app X = 0), f = 0 by + rw [← sub_eq_zero, this (f₁ - f₂) (by cat_disch)] + intro f hf + obtain ⟨g, hg⟩ := Triangle.coyoneda_exact₂ _ (inv_rot_of_distTriang _ + (t.triangleLTGE_distinguished n X)) f hf + have hg' := t.zero_of_isLE_of_isGE g (n - 1) (n + 1) (by lia) inferInstance + (by dsimp; apply (t.isGE_shift _ n (-1) (n + 1) (by lia))) + rw [hg, hg', zero_comp] + +@[reassoc] +lemma truncLT_map_truncLTι_app (n : ℤ) (X : C) : + (t.truncLT n).map ((t.truncLTι n).app X) = (t.truncLTι n).app ((t.truncLT n).obj X) := + t.to_truncLT_obj_ext (by simp) + +@[reassoc] +lemma truncGE_map_truncGEπ_app (n : ℤ) (X : C) : + (t.truncGE n).map ((t.truncGEπ n).app X) = (t.truncGEπ n).app ((t.truncGE n).obj X) := + t.from_truncGE_obj_ext (by simp) + +section + +variable {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsLE X n₀] + +include h in +lemma liftTruncLT_aux : + ∃ (f' : X ⟶ (t.truncLT n₁).obj Y), f = f' ≫ (t.truncLTι n₁).app Y := + Triangle.coyoneda_exact₂ _ (t.triangleLTGE_distinguished n₁ Y) f + (t.zero_of_isLE_of_isGE _ n₀ n₁ (by lia) inferInstance (by dsimp; infer_instance)) + +/-- Constructor for morphisms to `(t.truncLT n₁).obj Y`. -/ +noncomputable def liftTruncLT {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsLE X n₀] : + X ⟶ (t.truncLT n₁).obj Y := + (t.liftTruncLT_aux f n₀ n₁ h).choose + +@[reassoc (attr := simp)] +lemma liftTruncLT_ι {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsLE X n₀] : + t.liftTruncLT f n₀ n₁ h ≫ (t.truncLTι n₁).app Y = f := + (t.liftTruncLT_aux f n₀ n₁ h).choose_spec.symm + +end + end end TStructure From deeebf8fbacff590290f8ccb594a3c3ba6582485 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 15 Feb 2026 17:05:28 +0100 Subject: [PATCH 2/7] remove docstring --- .../CategoryTheory/Triangulated/TStructure/TruncLTGE.lean | 8 -------- 1 file changed, 8 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean b/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean index 81fb6918e516eb..3310661d4e009d 100644 --- a/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean +++ b/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean @@ -19,14 +19,6 @@ part of a distinguished triangle `(t.truncLT n).obj X ⟶ X ⟶ (t.truncGE n).obj X ⟶ ((t.truncLT n).obj X)⟦1⟧` for any `X : C`, with `(t.truncLT n).obj X < n` and `(t.truncGE n).obj X ≥ n`. -We obtain various properties of these truncation functors. -Variants `truncGT` and `truncLE` are introduced in the file -`Mathlib/CategoryTheory/Triangulated/TStucture/TruncLEGT.lean`. -Extensions to indices in `EInt` instead of `ℤ` are introduced in the file -`Mathlib/CategoryTheory/Triangulated/TStucture/ETrunc.lean`. -The spectral object attached to an object `X : C` is constructed in the file -`Mathlib/CategoryTheory/Triangulated/TStucture/SpectralObject.lean`. - -/ universe v u From ddee250f437980a994cf8cbf116d08717ec549d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 15 Feb 2026 17:07:06 +0100 Subject: [PATCH 3/7] trunc-ltge-2 --- .../Triangulated/TStructure/TruncLTGE.lean | 296 ++++++++++++++++++ 1 file changed, 296 insertions(+) diff --git a/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean b/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean index 3310661d4e009d..68fde5fa9735a6 100644 --- a/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean +++ b/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean @@ -6,6 +6,7 @@ Authors: Joël Riou module public import Mathlib.CategoryTheory.Triangulated.TStructure.Basic +public import Mathlib.CategoryTheory.Triangulated.Subcategory /-! # Truncations for a t-structure @@ -19,6 +20,8 @@ part of a distinguished triangle `(t.truncLT n).obj X ⟶ X ⟶ (t.truncGE n).obj X ⟶ ((t.truncLT n).obj X)⟦1⟧` for any `X : C`, with `(t.truncLT n).obj X < n` and `(t.truncGE n).obj X ≥ n`. +We obtain various properties of these truncation functors. + -/ universe v u @@ -550,6 +553,299 @@ lemma liftTruncLT_ι {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n end +section + +variable {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsGE Y n] + +lemma descTruncGE_aux : + ∃ (f' : (t.truncGE n).obj X ⟶ Y), f = (t.truncGEπ n).app X ≫ f' := + Triangle.yoneda_exact₂ _ (t.triangleLTGE_distinguished n X) f + (t.zero_of_isLE_of_isGE _ (n-1) n (by lia) (by dsimp; infer_instance) inferInstance) + +/-- Constructor for morphisms from `(t.truncGE n).obj X`. -/ +noncomputable def descTruncGE : + (t.truncGE n).obj X ⟶ Y := + (t.descTruncGE_aux f n).choose + +@[reassoc (attr := simp)] +lemma π_descTruncGE {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsGE Y n] : + (t.truncGEπ n).app X ≫ t.descTruncGE f n = f := + (t.descTruncGE_aux f n).choose_spec.symm + +end + +lemma isLE_iff_orthogonal (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : + t.IsLE X n₀ ↔ ∀ (Y : C) (f : X ⟶ Y) (_ : t.IsGE Y n₁), f = 0 := by + refine ⟨fun _ Y f _ ↦ t.zero f n₀ n₁ (by lia), fun hX ↦ ?_⟩ + rw [t.isLE_iff_isZero_truncGE_obj n₀ n₁ h, IsZero.iff_id_eq_zero] + exact t.from_truncGE_obj_ext (by simpa using hX _ _ inferInstance) + +lemma isGE_iff_orthogonal (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : + t.IsGE X n₁ ↔ ∀ (Y : C) (f : Y ⟶ X) (_ : t.IsLE Y n₀), f = 0 := by + refine ⟨fun _ Y f _ ↦ t.zero f n₀ n₁ (by lia), fun hX ↦ ?_⟩ + rw [t.isGE_iff_isZero_truncLT_obj n₁ X, IsZero.iff_id_eq_zero] + exact t.to_truncLT_obj_ext (by simpa using hX _ _ (by rw [← h]; infer_instance)) + +lemma isLE₂ (T : Triangle C) (hT : T ∈ distTriang C) (n : ℤ) (h₁ : t.IsLE T.obj₁ n) + (h₃ : t.IsLE T.obj₃ n) : t.IsLE T.obj₂ n := by + rw [t.isLE_iff_orthogonal n (n+1) rfl] + intro Y f hY + obtain ⟨f', hf'⟩ := Triangle.yoneda_exact₂ _ hT f + (t.zero _ n (n + 1) (by lia) ) + rw [hf', t.zero f' n (n + 1) (by lia), comp_zero] + +lemma isGE₂ (T : Triangle C) (hT : T ∈ distTriang C) (n : ℤ) (h₁ : t.IsGE T.obj₁ n) + (h₃ : t.IsGE T.obj₃ n) : t.IsGE T.obj₂ n := by + rw [t.isGE_iff_orthogonal (n-1) n (by lia)] + intro Y f hY + obtain ⟨f', hf'⟩ := Triangle.coyoneda_exact₂ _ hT f (t.zero _ (n-1) n (by lia)) + rw [hf', t.zero f' (n-1) n (by lia), zero_comp] + +instance : t.minus.IsTriangulated where + exists_zero := ⟨0, isZero_zero C, 0, inferInstance⟩ + toIsTriangulatedClosed₂ := .mk' (fun T hT ↦ by + rintro ⟨i₁, hi₁⟩ ⟨i₃, hi₃⟩ + exact ⟨max i₁ i₃, t.isLE₂ T hT _ (t.isLE_of_le _ _ _ (le_max_left i₁ i₃)) + (t.isLE_of_le _ _ _ (le_max_right i₁ i₃))⟩) + +instance : t.plus.IsTriangulated where + exists_zero := ⟨0, isZero_zero C, 0, inferInstance⟩ + toIsTriangulatedClosed₂ := .mk' (fun T hT ↦ by + rintro ⟨i₁, hi₁⟩ ⟨i₃, hi₃⟩ + exact ⟨min i₁ i₃, t.isGE₂ T hT _ (t.isGE_of_ge _ _ _ (min_le_left i₁ i₃)) + (t.isGE_of_ge _ _ _ (min_le_right i₁ i₃))⟩) + +instance : t.bounded.IsTriangulated := by + dsimp [bounded] + infer_instance + +lemma isIso_truncLT_map_iff {X Y : C} (f : X ⟶ Y) (n : ℤ) : + IsIso ((t.truncLT n).map f) ↔ + ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ ((t.truncLT n).obj X)⟦1⟧) + (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distTriang _), t.IsGE Z n := by + refine ⟨fun hf ↦ ?_, fun ⟨Z, g, h, mem, _⟩ ↦ ?_⟩ + · refine ⟨(t.truncGE n).obj Y, (t.truncGEπ n).app Y, + (t.truncGEδLT n).app Y ≫ (inv ((t.truncLT n).map f))⟦1⟧', + isomorphic_distinguished _ (t.triangleLTGE_distinguished n Y) _ ?_, inferInstance⟩ + exact Triangle.isoMk _ _ (asIso ((t.truncLT n).map f)) (Iso.refl _) (Iso.refl _) + · obtain ⟨e, he⟩ := t.triangle_iso_exists + mem (t.triangleLTGE_distinguished n Y) (Iso.refl _) (n - 1) n + (by dsimp; infer_instance) (by dsimp; infer_instance) + (by dsimp; infer_instance) (by dsimp; infer_instance) + suffices ((t.truncLT n).map f) = e.hom.hom₁ by rw [this]; infer_instance + exact t.to_truncLT_obj_ext (Eq.trans (by cat_disch) e.hom.comm₁) + +lemma isIso_truncGE_map_iff {Y Z : C} (g : Y ⟶ Z) (n₀ n₁ : ℤ) (hn : n₀ + 1 = n₁) : + IsIso ((t.truncGE n₁).map g) ↔ + ∃ (X : C) (f : X ⟶ Y) (h : ((t.truncGE n₁).obj Z) ⟶ X⟦(1 : ℤ)⟧) + (_ : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distTriang _), t.IsLE X n₀ := by + refine ⟨fun hf ↦ ?_, fun ⟨X, f, h, mem, _⟩ ↦ ?_⟩ + · refine ⟨_, (t.truncLTι n₁).app Y, inv ((t.truncGE n₁).map g) ≫ (t.truncGEδLT n₁).app Y, + isomorphic_distinguished _ (t.triangleLTGE_distinguished n₁ Y) _ ?_, + by subst hn; infer_instance⟩ + exact Iso.symm (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) + (asIso ((t.truncGE n₁).map g)) (by simp) (by simp) (by simp)) + · obtain ⟨e, he⟩ := + t.triangle_iso_exists (t.triangleLTGE_distinguished n₁ Y) mem (Iso.refl _) n₀ n₁ + (by dsimp; rw [← hn]; infer_instance) (by dsimp; infer_instance) + (by dsimp; infer_instance) (by dsimp; infer_instance) + suffices ((t.truncGE n₁).map g) = e.hom.hom₃ by rw [this]; infer_instance + exact t.from_truncGE_obj_ext (Eq.trans (by cat_disch) e.hom.comm₂.symm) + +instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncLT a).obj X) b := by + by_cases h : a ≤ b + 1 + · exact t.isLE_truncLT_obj .. + · have := (t.isLE_iff_isIso_truncLTι_app (a - 1) a (by lia) X).1 (t.isLE_of_le _ b _ (by lia)) + exact t.isLE_of_iso (show X ≅ _ from (asIso ((t.truncLTι a).app X)).symm) _ + +instance (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncGE b).obj X) a := by + by_cases h : a ≤ b + · exact t.isGE_truncGE_obj .. + · have : t.IsGE X b := t.isGE_of_ge X b a (by lia) + exact t.isGE_of_iso (show X ≅ _ from asIso ((t.truncGEπ b).app X)) _ + +/-- The composition `t.truncLT b ⋙ t.truncGE a`. -/ +noncomputable abbrev truncGELT (a b : ℤ) : C ⥤ C := t.truncLT b ⋙ t.truncGE a + +/-- The composition `t.truncGE b ⋙ t.truncLT a`. -/ +noncomputable abbrev truncLTGE (a b : ℤ) : C ⥤ C := t.truncGE a ⋙ t.truncLT b + +instance (X : C) (a b : ℤ) : t.IsGE ((t.truncGELT a b).obj X) a := by + dsimp; infer_instance + +instance (X : C) (a b : ℤ) : t.IsLE ((t.truncLTGE a b).obj X) (b - 1) := by + dsimp; infer_instance + +section + +variable [IsTriangulated C] + +lemma isIso₁_truncLT_map_of_isGE (T : Triangle C) (hT : T ∈ distTriang C) + (n : ℤ) (h₃ : t.IsGE T.obj₃ n) : + IsIso ((t.truncLT n).map T.mor₁) := by + rw [isIso_truncLT_map_iff] + obtain ⟨Z, g, k, mem⟩ := distinguished_cocone_triangle ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) + refine ⟨_, _, _, mem, ?_⟩ + let H := someOctahedron rfl (t.triangleLTGE_distinguished n T.obj₁) hT mem + exact t.isGE₂ _ H.mem n (by dsimp; infer_instance) (by dsimp; infer_instance) + +lemma isIso₂_truncGE_map_of_isLE (T : Triangle C) (hT : T ∈ distTriang C) + (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (h₁ : t.IsLE T.obj₁ n₀) : + IsIso ((t.truncGE n₁).map T.mor₂) := by + rw [isIso_truncGE_map_iff _ _ _ _ h] + obtain ⟨X, f, k, mem⟩ := distinguished_cocone_triangle₁ (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) + refine ⟨_, _, _, mem, ?_⟩ + subst h + have H := someOctahedron rfl (rot_of_distTriang _ hT) + (rot_of_distTriang _ (t.triangleLTGE_distinguished (n₀ + 1) T.obj₃)) + (rot_of_distTriang _ mem) + have : t.IsLE (X⟦(1 : ℤ)⟧) (n₀ - 1) := + t.isLE₂ _ H.mem (n₀ - 1) (t.isLE_shift T.obj₁ n₀ 1 (n₀ - 1) (by lia)) + (t.isLE_shift ((t.truncLT (n₀ + 1)).obj T.obj₃) n₀ 1 (n₀-1) (by lia)) + exact t.isLE_of_shift X n₀ 1 (n₀ - 1) (by lia) + +instance (X : C) (a b : ℤ) [t.IsGE X a] : + t.IsGE ((t.truncLT b).obj X) a := by + rw [t.isGE_iff_isZero_truncLT_obj] + have := t.isIso₁_truncLT_map_of_isGE _ ((t.triangleLTGE_distinguished b X)) a + (by dsimp; infer_instance) + dsimp at this + refine IsZero.of_iso ?_ (asIso ((t.truncLT a).map ((t.truncLTι b).app X))) + rwa [← isGE_iff_isZero_truncLT_obj] + +instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncGE a).obj X) b := by + rw [t.isLE_iff_isZero_truncGE_obj b (b + 1) rfl] + have := t.isIso₂_truncGE_map_of_isLE _ (t.triangleLTGE_distinguished a X) b _ rfl + (by dsimp; infer_instance) + dsimp at this + refine IsZero.of_iso ?_ (asIso ((t.truncGE (b + 1)).map ((t.truncGEπ a).app X))).symm + rwa [← isLE_iff_isZero_truncGE_obj _ _ _ rfl] + +instance (X : C) (a b : ℤ) : + t.IsLE ((t.truncGELT a b).obj X) (b - 1) := by + dsimp; infer_instance + +instance (X : C) (a b : ℤ) : + t.IsGE ((t.truncLTGE a b).obj X) a := by + dsimp; infer_instance + +lemma isIso_truncGE_map_truncGEπ_app (a b : ℤ) (h : b ≤ a) (X : C) : + IsIso ((t.truncGE a).map ((t.truncGEπ b).app X)) := + t.isIso₂_truncGE_map_of_isLE _ (t.triangleLTGE_distinguished b X) + (a - 1) a (by lia) (t.isLE_truncLT_obj _ _ _ (by simpa)) + +lemma isIso_truncLT_map_truncLTι_app (a b : ℤ) (h : a ≤ b) (X : C) : + IsIso ((t.truncLT a).map ((t.truncLTι b).app X)) := + t.isIso₁_truncLT_map_of_isGE _ (t.triangleLTGE_distinguished b X) a + (t.isGE_of_ge ((t.truncGE b).obj X) a b (by lia)) + +instance (X : C) (n : ℤ) : IsIso ((t.truncLT n).map ((t.truncLTι n).app X)) := + isIso_truncLT_map_truncLTι_app t _ _ (by rfl) X + +instance (X : C) (n : ℤ) : IsIso ((t.truncGE n).map ((t.truncGEπ n).app X)) := + t.isIso_truncGE_map_truncGEπ_app _ _ (by rfl) _ + +instance (a b : ℤ) (X : C) : + IsIso ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) := by + rw [← t.isLE_iff_isIso_truncLTι_app (b - 1) b (by lia)] + infer_instance + +/-- The natural transformation `t.truncGELT a b ⟶ t.truncLTGE a b` +(which is an isomorphism, see `truncGELTIsoLTGE`.) -/ +noncomputable def truncGELTToLTGE (a b : ℤ) : + t.truncGELT a b ⟶ t.truncLTGE a b where + app X := t.liftTruncLT (t.descTruncGE + ((t.truncLTι b).app X ≫ (t.truncGEπ a).app X) a) (b - 1) b (by lia) + naturality _ _ _ := + t.to_truncLT_obj_ext (by dsimp; exact t.from_truncGE_obj_ext (by simp)) + +@[reassoc (attr := simp)] +lemma truncGELTToLTGE_app_pentagon (a b : ℤ) (X : C) : + (t.truncGEπ a).app _ ≫ (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app _ = + (t.truncLTι b).app X ≫ (t.truncGEπ a).app X := by + simp [truncGELTToLTGE] + +lemma truncGELTToLTGE_app_pentagon_uniqueness {a b : ℤ} {X : C} + (φ : (t.truncGELT a b).obj X ⟶ (t.truncLTGE a b).obj X) + (hφ : (t.truncGEπ a).app _ ≫ φ ≫ (t.truncLTι b).app _ = + (t.truncLTι b).app X ≫ (t.truncGEπ a).app X) : + (t.truncGELTToLTGE a b).app X = φ := + t.to_truncLT_obj_ext (by dsimp; exact t.from_truncGE_obj_ext (by cat_disch)) + +@[reassoc] +lemma truncLT_map_truncGE_map_truncLTι_app_fac (a b : ℤ) (X : C) : + (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ + (t.truncGELTToLTGE a b).app X = + (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X)) := by + rw [← cancel_epi (inv ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))), + IsIso.inv_hom_id_assoc] + exact t.truncGELTToLTGE_app_pentagon_uniqueness _ (by simp) + +/-- The connecting homomorphism +`(t.truncGELT a b).obj X ⟶ ((t.truncLT a).obj X)⟦1⟧`, +as a natural transformation. -/ +@[expose, simps!] +noncomputable def truncGELTδLT (a b : ℤ) : + t.truncGELT a b ⟶ t.truncLT a ⋙ shiftFunctor C (1 : ℤ) := + Functor.whiskerLeft (t.truncLT b) (t.truncGEδLT a) ≫ + Functor.whiskerRight (t.truncLTι b) (t.truncLT a ⋙ shiftFunctor C (1 : ℤ)) + +/-- The functorial (distinguished) triangle +`(t.truncLT a).obj X ⟶ (t.truncLT b).obj X ⟶ (t.truncGELT a b).obj X ⟶ ...` +when `a ≤ b`. -/ +@[expose, simps!] +noncomputable def triangleLTLTGELT (a b : ℤ) (h : a ≤ b) : C ⥤ Triangle C := + Triangle.functorMk (t.natTransTruncLTOfLE a b h) + (Functor.whiskerLeft (t.truncLT b) (t.truncGEπ a)) (t.truncGELTδLT a b) + +lemma triangleLTLTGELT_distinguished (a b : ℤ) (h : a ≤ b) (X : C) : + (t.triangleLTLTGELT a b h).obj X ∈ distTriang C := by + have := t.isIso_truncLT_map_truncLTι_app a b h X + refine isomorphic_distinguished _ (t.triangleLTGE_distinguished a ((t.truncLT b).obj X)) _ ?_ + refine Triangle.isoMk _ _ ((asIso ((t.truncLT a).map ((t.truncLTι b).app X))).symm) + (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ + · dsimp + simp only [Category.comp_id, IsIso.eq_inv_comp] + exact t.to_truncLT_obj_ext (by simp) + · simp + · simp + +instance (a b : ℤ) : IsIso (t.truncGELTToLTGE a b) := by + rw [NatTrans.isIso_iff_isIso_app] + intro X + by_cases h : a ≤ b + · let u₁₂ := (t.natTransTruncLTOfLE a b h).app X + let u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X + let u₁₃ : _ ⟶ X := (t.truncLTι a).app X + have eq : u₁₂ ≫ u₂₃ = u₁₃ := by simp [u₁₂, u₂₃, u₁₃] + have H := someOctahedron eq (t.triangleLTLTGELT_distinguished a b h X) + (t.triangleLTGE_distinguished b X) (t.triangleLTGE_distinguished a X) + let m₁ : (t.truncGELT a b).obj X ⟶ _ := H.m₁ + have : IsIso ((t.truncLT b).map H.m₁) := + t.isIso₁_truncLT_map_of_isGE _ H.mem b (by dsimp; infer_instance) + have eq' : t.liftTruncLT m₁ (b - 1) b (by lia) = (t.truncGELTToLTGE a b).app X := + t.to_truncLT_obj_ext + (by dsimp; exact t.from_truncGE_obj_ext (by simpa using H.comm₁)) + rw [← eq'] + have fac : (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ + t.liftTruncLT m₁ (b - 1) b (by lia) = (t.truncLT b).map m₁ := + t.to_truncLT_obj_ext (by simp [truncGELT]) + exact IsIso.of_isIso_fac_left fac + · simp at h + refine ⟨0, ?_, ?_⟩ + all_goals exact IsZero.eq_of_src (t.isZero _ (b-1) a (by lia)) _ _ + +instance (a b : ℤ) (X : C) : + IsIso ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))) := by + rw [← t.truncLT_map_truncGE_map_truncLTι_app_fac a b X] + infer_instance + +/-- The natural transformation `t.truncGELT a b ≅ t.truncLTGE a b`. -/ +noncomputable def truncGELTIsoLTGE (a b : ℤ) : t.truncGELT a b ≅ t.truncLTGE a b := + asIso (t.truncGELTToLTGE a b) + +end + end end TStructure From fe985591420e8f1f2c02eec3f1668cf9c022e48b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 15 Feb 2026 17:14:37 +0100 Subject: [PATCH 4/7] trunc-legt --- Mathlib.lean | 1 + .../Triangulated/TStructure/TruncLEGT.lean | 396 ++++++++++++++++++ 2 files changed, 397 insertions(+) create mode 100644 Mathlib/CategoryTheory/Triangulated/TStructure/TruncLEGT.lean diff --git a/Mathlib.lean b/Mathlib.lean index cd72d6d36a5d31..5e315aa0471081 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3235,6 +3235,7 @@ public import Mathlib.CategoryTheory.Triangulated.Rotate public import Mathlib.CategoryTheory.Triangulated.SpectralObject public import Mathlib.CategoryTheory.Triangulated.Subcategory public import Mathlib.CategoryTheory.Triangulated.TStructure.Basic +public import Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT public import Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE public import Mathlib.CategoryTheory.Triangulated.TriangleShift public import Mathlib.CategoryTheory.Triangulated.Triangulated diff --git a/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLEGT.lean b/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLEGT.lean new file mode 100644 index 00000000000000..bf4482420ce068 --- /dev/null +++ b/Mathlib/CategoryTheory/Triangulated/TStructure/TruncLEGT.lean @@ -0,0 +1,396 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE + +/-! +# Truncations for a t-structure + +Let `t` be a t-structure on a (pre)triangulated category `C`. +In this file, for any `n : ℤ`, we introduce the truncation functors +`t.truncLE n : C ⥤ C` and `t.truncGT n : C ⥤ C`, as variants of the functors +`t.truncLT n : C ⥤ C` and `t.truncGE n : C ⥤ C` introduced in the file +`Mathlib/CategoryTheory/Triangulated/TStucture/TruncLTGE.lean`. + +-/ + +@[expose] public section + +namespace CategoryTheory + +open Limits Pretriangulated + +variable {C : Type*} [Category* C] [Preadditive C] [HasZeroObject C] [HasShift C ℤ] + [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] + +namespace Triangulated + +namespace TStructure + +variable (t : TStructure C) + +/-- Given a t-structure `t` on a pretriangulated category `C` and `n : ℤ`, this +is the `≤ n`-truncation functor. See also the natural transformation `truncLEι`. -/ +noncomputable def truncLE (n : ℤ) : C ⥤ C := t.truncLT (n + 1) + +instance (n : ℤ) : (t.truncLE n).Additive := by + dsimp only [truncLE] + infer_instance + +lemma isLE_truncLE_obj (X : C) (a b : ℤ) (hn : a ≤ b := by lia) : + t.IsLE ((t.truncLE a).obj X) b := + t.isLE_truncLT_obj .. + +instance (n : ℤ) (X : C) : t.IsLE ((t.truncLE n).obj X) n := + t.isLE_truncLE_obj .. + +/-- Given a t-structure `t` on a pretriangulated category `C` and `n : ℤ`, this +is the `> n`-truncation functor. See also the natural transformation `truncGTπ`. -/ +noncomputable def truncGT (n : ℤ) : C ⥤ C := t.truncGE (n + 1) + +instance (n : ℤ) : (t.truncGT n).Additive := by + dsimp only [truncGT] + infer_instance + +lemma isGE_truncGT_obj (X : C) (a b : ℤ) (hn : b ≤ a + 1 := by lia) : + t.IsGE ((t.truncGT a).obj X) b := + t.isGE_truncGE_obj .. + +instance (n : ℤ) (X : C) : t.IsGE ((t.truncGT n).obj X) (n + 1) := + t.isGE_truncGT_obj .. + +instance (n : ℤ) (X : C) : t.IsGE ((t.truncGT (n - 1)).obj X) n := + t.isGE_truncGT_obj .. + +/-- The isomorphism `t.truncLE a ≅ t.truncLT b` when `a + 1 = b`. -/ +noncomputable def truncLEIsoTruncLT (a b : ℤ) (h : a + 1 = b) : + t.truncLE a ≅ t.truncLT b := + eqToIso (by rw [← h]; rfl) + +/-- The isomorphism `t.truncGT a ≅ t.truncGE b` when `a + 1 = b`. -/ +noncomputable def truncGTIsoTruncGE (a b : ℤ) (h : a + 1 = b) : + t.truncGT a ≅ t.truncGE b := + eqToIso (by rw [← h]; rfl) + +/-- The natural transformation `t.truncLE n ⟶ 𝟭 C` when `t` is a t-structure +on a category `C` and `n : ℤ`. -/ +noncomputable def truncLEι (n : ℤ) : t.truncLE n ⟶ 𝟭 C := t.truncLTι (n + 1) + +@[reassoc (attr := simp)] +lemma truncLEIsoTruncLT_hom_ι (a b : ℤ) (h : a + 1 = b) : + (t.truncLEIsoTruncLT a b h).hom ≫ t.truncLTι b = t.truncLEι a := by + subst h + dsimp [truncLEIsoTruncLT, truncLEι] + rw [Category.id_comp] + +@[reassoc (attr := simp)] +lemma truncLEIsoTruncLT_hom_ι_app (a b : ℤ) (h : a + 1 = b) (X : C) : + (t.truncLEIsoTruncLT a b h).hom.app X ≫ (t.truncLTι b).app X = (t.truncLEι a).app X := + congr_app (t.truncLEIsoTruncLT_hom_ι a b h) X + +@[reassoc (attr := simp)] +lemma truncLEIsoTruncLT_inv_ι (a b : ℤ) (h : a + 1 = b) : + (t.truncLEIsoTruncLT a b h).inv ≫ t.truncLEι a = t.truncLTι b := by + subst h + dsimp [truncLEIsoTruncLT, truncLEι, truncLE] + rw [Category.id_comp] + +@[reassoc (attr := simp)] +lemma truncLEIsoTruncLT_inv_ι_app (a b : ℤ) (h : a + 1 = b) (X : C) : + (t.truncLEIsoTruncLT a b h).inv.app X ≫ (t.truncLEι a).app X = (t.truncLTι b).app X := + congr_app (t.truncLEIsoTruncLT_inv_ι a b h) X + +/-- The natural transformation `t.truncLE a ⟶ t.truncLE b` when `a ≤ b`. -/ +noncomputable def natTransTruncLEOfLE (a b : ℤ) (h : a ≤ b) : + t.truncLE a ⟶ t.truncLE b := + t.natTransTruncLTOfLE (a+1) (b+1) (by lia) + +@[reassoc (attr := simp)] +lemma natTransTruncLEOfLE_ι_app (n₀ n₁ : ℤ) (h : n₀ ≤ n₁) (X : C) : + (t.natTransTruncLEOfLE n₀ n₁ h).app X ≫ (t.truncLEι n₁).app X = + (t.truncLEι n₀).app X := + t.natTransTruncLTOfLE_ι_app _ _ _ _ + +@[reassoc (attr := simp)] +lemma natTransTruncLEOfLE_ι (a b : ℤ) (h : a ≤ b) : + t.natTransTruncLEOfLE a b h ≫ t.truncLEι b = t.truncLEι a := by cat_disch + +@[simp] +lemma natTransTruncLEOfLE_refl (a : ℤ) : + t.natTransTruncLEOfLE a a (by rfl) = 𝟙 _ := + t.natTransTruncLTOfLE_refl _ + +@[simp] +lemma natTransTruncLEOfLE_trans (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) : + t.natTransTruncLEOfLE a b hab ≫ t.natTransTruncLEOfLE b c hbc = + t.natTransTruncLEOfLE a c (hab.trans hbc) := + t.natTransTruncLTOfLE_trans _ _ _ _ _ + +lemma natTransTruncLEOfLE_refl_app (a : ℤ) (X : C) : + (t.natTransTruncLEOfLE a a (by rfl)).app X = 𝟙 _ := + congr_app (t.natTransTruncLEOfLE_refl a) X + +@[reassoc (attr := simp)] +lemma natTransTruncLEOfLE_trans_app (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C) : + (t.natTransTruncLEOfLE a b hab).app X ≫ (t.natTransTruncLEOfLE b c hbc).app X = + (t.natTransTruncLEOfLE a c (hab.trans hbc)).app X := + congr_app (t.natTransTruncLEOfLE_trans a b c hab hbc) X + +/-- The natural transformation `𝟭 C ⟶ t.truncGT n` when `t` is a t-structure +on a category `C` and `n : ℤ`. -/ +noncomputable def truncGTπ (n : ℤ) : 𝟭 C ⟶ t.truncGT n := t.truncGEπ (n + 1) + +@[reassoc (attr := simp)] +lemma π_truncGTIsoTruncGE_hom (a b : ℤ) (h : a + 1 = b) : + t.truncGTπ a ≫ (t.truncGTIsoTruncGE a b h).hom = t.truncGEπ b := by + subst h + dsimp [truncGTIsoTruncGE, truncGTπ] + rw [Category.comp_id] + +@[reassoc (attr := simp)] +lemma π_truncGTIsoTruncGE_hom_ι_app (a b : ℤ) (h : a + 1 = b) (X : C) : + (t.truncGTπ a).app X ≫ (t.truncGTIsoTruncGE a b h).hom.app X = (t.truncGEπ b).app X := + congr_app (t.π_truncGTIsoTruncGE_hom a b h) X + +@[reassoc (attr := simp)] +lemma π_truncGTIsoTruncGE_inv (a b : ℤ) (h : a + 1 = b) : + t.truncGEπ b ≫ (t.truncGTIsoTruncGE a b h).inv = t.truncGTπ a := by + subst h + dsimp [truncGTIsoTruncGE, truncGTπ, truncGT] + rw [Category.comp_id] + +@[reassoc (attr := simp)] +lemma π_truncGTIsoTruncGE_inv_ι_app (a b : ℤ) (h : a + 1 = b) (X : C) : + (t.truncGEπ b).app X ≫ (t.truncGTIsoTruncGE a b h).inv.app X = (t.truncGTπ a).app X := + congr_app (t.π_truncGTIsoTruncGE_inv a b h) X + +/-- The connecting homomorphism `(t.truncGE b).obj X ⟶ ((t.truncLE a).obj X)⟦1⟧` +when `a + 1 = b`, as a natural transformation. -/ +noncomputable def truncGEδLE (a b : ℤ) (h : a + 1 = b) : + t.truncGE b ⟶ t.truncLE a ⋙ shiftFunctor C (1 : ℤ) := + t.truncGEδLT b ≫ Functor.whiskerRight (t.truncLEIsoTruncLT a b h).inv (shiftFunctor C (1 : ℤ)) + +/-- The distinguished triangle `(t.truncLE a).obj A ⟶ A ⟶ (t.truncGE b).obj A ⟶ ...` +as a functor `C ⥤ Triangle C` when `t` is a `t`-structure on a pretriangulated +category `C` and `a + 1 = b`. -/ +@[simps!] +noncomputable def triangleLEGE (a b : ℤ) (h : a + 1 = b) : C ⥤ Triangle C := + Triangle.functorMk (t.truncLEι a) (t.truncGEπ b) (t.truncGEδLE a b h) + +/-- The natural isomorphism of triangles `t.triangleLEGE a b h ≅ t.triangleLTGE b` +when `a + 1 = b`. -/ +noncomputable def triangleLEGEIsoTriangleLTGE (a b : ℤ) (h : a + 1 = b) : + t.triangleLEGE a b h ≅ t.triangleLTGE b := by + refine Triangle.functorIsoMk _ _ (t.truncLEIsoTruncLT a b h) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ + · cat_disch + · cat_disch + · ext + dsimp [truncGEδLE] + simp only [Category.assoc, Category.id_comp, ← Functor.map_comp, + Iso.inv_hom_id_app, Functor.map_id, Category.comp_id] + +lemma triangleLEGE_distinguished (a b : ℤ) (h : a + 1 = b) (X : C) : + (t.triangleLEGE a b h).obj X ∈ distTriang C := + isomorphic_distinguished _ (t.triangleLTGE_distinguished b X) _ + ((t.triangleLEGEIsoTriangleLTGE a b h).app X) + +/-- The connecting homomorphism `(t.truncGT n).obj X ⟶ ((t.truncLE n).obj X)⟦1⟧` +for `n : ℤ`, as a natural transformation. -/ +noncomputable def truncGTδLE (n : ℤ) : + t.truncGT n ⟶ t.truncLE n ⋙ shiftFunctor C (1 : ℤ) := + (t.truncGTIsoTruncGE n (n+1) rfl).hom ≫ t.truncGEδLE n (n + 1) (by lia) + +/-- The distinguished triangle `(t.truncLE n).obj A ⟶ A ⟶ (t.truncGT n).obj A ⟶ ...` +as a functor `C ⥤ Triangle C` when `t` is a t-structure on a pretriangulated +category `C` and `n : ℤ`. -/ +@[simps!] +noncomputable def triangleLEGT (n : ℤ) : C ⥤ Triangle C := + Triangle.functorMk (t.truncLEι n) (t.truncGTπ n) (t.truncGTδLE n) + +/-- The natural isomorphism `t.triangleLEGT a ≅ t.triangleLEGE a b h` +when `a + 1 = b`. -/ +noncomputable def triangleLEGTIsoTriangleLEGE (a b : ℤ) (h : a + 1 = b) : + t.triangleLEGT a ≅ t.triangleLEGE a b h := + Triangle.functorIsoMk _ _ (Iso.refl _) (Iso.refl _) (t.truncGTIsoTruncGE a b h) + (by cat_disch) (by cat_disch) (by + ext + dsimp [truncGTδLE] + subst h + simp only [Functor.map_id, Category.comp_id]) + +lemma triangleLEGT_distinguished (n : ℤ) (X : C) : + (t.triangleLEGT n).obj X ∈ distTriang C := + isomorphic_distinguished _ (t.triangleLEGE_distinguished n (n+1) rfl X) _ + ((t.triangleLEGTIsoTriangleLEGE n (n+1) rfl).app X) + +lemma isLE_iff_isIso_truncLEι_app (n : ℤ) (X : C) : + t.IsLE X n ↔ IsIso ((t.truncLEι n).app X) := + t.isLE_iff_isIso_truncLTι_app n (n + 1) rfl X + +lemma isGE_iff_isIso_truncGTπ_app (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) (X : C) : + t.IsGE X n₁ ↔ IsIso ((t.truncGTπ n₀).app X) := by + rw [t.isGE_iff_isIso_truncGEπ_app n₁ X] + exact (MorphismProperty.isomorphisms _).arrow_mk_iso_iff + (Arrow.isoMk (Iso.refl _) ((t.truncGTIsoTruncGE _ _ hn₁).symm.app X)) + +instance (X : C) (n : ℤ) [t.IsLE X n] : IsIso ((t.truncLEι n).app X) := by + rw [← isLE_iff_isIso_truncLEι_app ] + infer_instance + +lemma isLE_iff_isZero_truncGT_obj (n : ℤ) (X : C) : + t.IsLE X n ↔ IsZero ((t.truncGT n).obj X) := by + rw [t.isLE_iff_isIso_truncLEι_app n X] + exact (Triangle.isZero₃_iff_isIso₁ _ (t.triangleLEGT_distinguished n X)).symm + +lemma isGE_iff_isZero_truncLE_obj (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : + t.IsGE X n₁ ↔ IsZero ((t.truncLE n₀).obj X) := by + rw [t.isGE_iff_isIso_truncGEπ_app n₁ X] + exact (Triangle.isZero₁_iff_isIso₂ _ (t.triangleLEGE_distinguished n₀ n₁ h X)).symm + +lemma isZero_truncLE_obj_of_isGE (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) [t.IsGE X n₁] : + IsZero ((t.truncLE n₀).obj X) := by + rw [← t.isGE_iff_isZero_truncLE_obj _ _ h X] + infer_instance + +lemma to_truncLE_obj_ext {n : ℤ} {Y : C} {X : C} + {f₁ f₂ : Y ⟶ (t.truncLE n).obj X} (h : f₁ ≫ (t.truncLEι n).app X = f₂ ≫ (t.truncLEι n).app X) + [t.IsLE Y n] : + f₁ = f₂ := by + have : t.IsLE Y (n + 1 - 1) := by simpa + rw [← cancel_mono ((t.truncLEIsoTruncLT n (n + 1) rfl).hom.app _)] + exact t.to_truncLT_obj_ext (by simpa) + +section + +variable {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsLE X n] + +lemma liftTruncLE_aux : + ∃ (f' : X ⟶ (t.truncLE n).obj Y), f = f' ≫ (t.truncLEι n).app Y := + Triangle.coyoneda_exact₂ _ (t.triangleLEGT_distinguished n Y) f + (t.zero_of_isLE_of_isGE _ n (n + 1) (by lia) inferInstance (by dsimp; infer_instance)) + +/-- Constructor for morphisms to `(t.truncLE n).obj Y`. -/ +noncomputable def liftTruncLE : + X ⟶ (t.truncLE n).obj Y := (t.liftTruncLE_aux f n).choose + +@[reassoc (attr := simp)] +lemma liftTruncLE_ι : + t.liftTruncLE f n ≫ (t.truncLEι n).app Y = f := + (t.liftTruncLE_aux f n).choose_spec.symm + +end + +section + +variable {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsGE Y n₁] + +include h in +lemma descTruncGT_aux : + ∃ (f' : (t.truncGT n₀).obj X ⟶ Y), f = (t.truncGTπ n₀).app X ≫ f' := + Triangle.yoneda_exact₂ _ (t.triangleLEGT_distinguished n₀ X) f + (t.zero_of_isLE_of_isGE _ n₀ n₁ (by lia) (by dsimp; infer_instance) inferInstance) + +/-- Constructor for morphisms from `(t.truncGT n₀).obj Y`. -/ +noncomputable def descTruncGT : + (t.truncGT n₀).obj X ⟶ Y := + (t.descTruncGT_aux f n₀ n₁ h).choose + +@[reassoc (attr := simp)] +lemma π_descTruncGT : + (t.truncGTπ n₀).app X ≫ t.descTruncGT f n₀ n₁ h = f := + (t.descTruncGT_aux f n₀ n₁ h).choose_spec.symm + +end + +lemma isIso_truncLE_map_iff {X Y : C} (f : X ⟶ Y) (a b : ℤ) (h : a + 1 = b) : + IsIso ((t.truncLE a).map f) ↔ + ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ ((t.truncLE a).obj X)⟦1⟧) + (_ : Triangle.mk ((t.truncLEι a).app X ≫ f) g h ∈ distTriang _), t.IsGE Z b := by + subst h + apply isIso_truncLT_map_iff + +lemma isIso_truncGT_map_iff {Y Z : C} (g : Y ⟶ Z) (n : ℤ) : + IsIso ((t.truncGT n).map g) ↔ + ∃ (X : C) (f : X ⟶ Y) (h : ((t.truncGT n).obj Z) ⟶ X⟦(1 : ℤ)⟧) + (_ : Triangle.mk f (g ≫ (t.truncGTπ n).app Z) h ∈ distTriang _), t.IsLE X n := + t.isIso_truncGE_map_iff g n (n + 1) rfl + +instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncLE a).obj X) b := by + dsimp [truncLE] + infer_instance + +instance (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncGT b).obj X) a := by + dsimp [truncGT] + infer_instance + +/-- The composition `t.truncGE a ⋙ t.truncGE b`. -/ +noncomputable abbrev truncLEGE (a b : ℤ) : C ⥤ C := t.truncGE a ⋙ t.truncLE b + +/-- The composition `t.truncLE b ⋙ t.truncGE a`. -/ +noncomputable abbrev truncGELE (a b : ℤ) : C ⥤ C := t.truncLE b ⋙ t.truncGE a + +instance (X : C) (a b : ℤ) : t.IsGE ((t.truncGELE a b).obj X) a := by + dsimp; infer_instance + +/-- The natural isomorphism `t.truncGELE a b ≅ t.truncGELT a b'` when `b + 1 = b'`. -/ +noncomputable def truncGELEIsoTruncGELT (a b b' : ℤ) (hb' : b + 1 = b') : + t.truncGELE a b ≅ t.truncGELT a b' := + Functor.isoWhiskerRight (t.truncLEIsoTruncLT b b' hb') _ + +section + +variable [IsTriangulated C] + +lemma isIso₁_truncLE_map_of_isGE (T : Triangle C) (hT : T ∈ distTriang C) + (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (h₃ : t.IsGE T.obj₃ n₁) : + IsIso ((t.truncLE n₀).map T.mor₁) := by + subst h + exact t.isIso₁_truncLT_map_of_isGE _ hT _ h₃ + +lemma isIso₂_truncGT_map_of_isLE (T : Triangle C) (hT : T ∈ distTriang C) + (n₀ : ℤ) (h₁ : t.IsLE T.obj₁ n₀) : + IsIso ((t.truncGT n₀).map T.mor₂) := + t.isIso₂_truncGE_map_of_isLE _ hT _ _ rfl h₁ + +instance (X : C) (a b : ℤ) [t.IsGE X a] : + t.IsGE ((t.truncLE b).obj X) a := by + dsimp [truncLE]; infer_instance + +instance (X : C) (a b : ℤ) [t.IsLE X b] : + t.IsLE ((t.truncGT a).obj X) b := by + dsimp [truncGT]; infer_instance + +instance (X : C) (a b : ℤ) [t.IsGE X a] : + t.IsGE ((t.truncLE b).obj X) a := by + dsimp [truncLE]; infer_instance + +instance (X : C) (a b : ℤ) : + t.IsLE ((t.truncGELE a b).obj X) b := by + dsimp; infer_instance + +lemma isIso_truncLE_map_truncLEι_app (a b : ℤ) (h : a ≤ b) (X : C) : + IsIso ((t.truncLE a).map ((t.truncLEι b).app X)) := + t.isIso_truncLT_map_truncLTι_app _ _ (by lia) _ + +lemma isIso_truncGT_map_truncGTπ_app (a b : ℤ) (h : b ≤ a) (X : C) : + IsIso ((t.truncGT a).map ((t.truncGTπ b).app X)) := + isIso_truncGE_map_truncGEπ_app _ _ _ (by lia) _ + +instance (X : C) (n : ℤ) : IsIso ((t.truncLE n).map ((t.truncLEι n).app X)) := + t.isIso_truncLE_map_truncLEι_app _ _ (by lia) _ + +/-- The natural isomorphism `t.truncGELE a b ≅ t.truncLEGE a b`. -/ +noncomputable def truncGELEIsoLEGE (a b : ℤ) : t.truncGELE a b ≅ t.truncLEGE a b := + t.truncGELTIsoLTGE a (b + 1) + +end + +end TStructure + +end Triangulated + +end CategoryTheory From 18c7f3cdaff4fc75de8b9165ed9aa1664af88ef6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 15 Feb 2026 17:31:56 +0100 Subject: [PATCH 5/7] etrunc-1 --- Mathlib.lean | 1 + .../Triangulated/TStructure/ETrunc.lean | 541 ++++++++++++++++++ 2 files changed, 542 insertions(+) create mode 100644 Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean diff --git a/Mathlib.lean b/Mathlib.lean index 5e315aa0471081..23214874514099 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3235,6 +3235,7 @@ public import Mathlib.CategoryTheory.Triangulated.Rotate public import Mathlib.CategoryTheory.Triangulated.SpectralObject public import Mathlib.CategoryTheory.Triangulated.Subcategory public import Mathlib.CategoryTheory.Triangulated.TStructure.Basic +public import Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc public import Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT public import Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE public import Mathlib.CategoryTheory.Triangulated.TriangleShift diff --git a/Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean b/Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean new file mode 100644 index 00000000000000..b34c95662a8b64 --- /dev/null +++ b/Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean @@ -0,0 +1,541 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT +public import Mathlib.Order.WithBotTop + +/-! +# Truncations for a t-structure + +Let `t` be a t-structure on a triangulated category `C`. +In this file, we extend the definition of the truncation functors +`truncLT` and `truncGE` for indices in `ℤ` to `EInt`, +as `t.eTruncLT : EInt ⥤ C ⥤ C` and `t.eTruncGE : EInt ⥤ C ⥤ C`. + +-/ + +@[expose] public section + +namespace CategoryTheory + +open Category Limits Pretriangulated ZeroObject Preadditive + +variable {C : Type*} [Category* C] [Preadditive C] [HasZeroObject C] [HasShift C ℤ] + [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] + +namespace Triangulated + +namespace TStructure + +variable (t : TStructure C) + +/-- The functor `EInt ⥤ C ⥤ C` which sends `⊥` to the zero functor, +`n : ℤ` to `t.truncLT n` and `⊤` to `𝟭 C`. -/ +noncomputable def eTruncLT : EInt ⥤ C ⥤ C where + obj n := by + induction n using WithBotTop.rec with + | bot => exact 0 + | coe a => exact t.truncLT a + | top => exact 𝟭 C + map {x y} f := by + induction x using WithBotTop.rec with + | bot => + induction y using WithBotTop.rec with + | bot => exact 𝟙 _ + | coe b => exact 0 + | top => exact 0 + | coe a => + induction y using WithBotTop.rec with + | bot => exact 0 + | coe b => exact t.natTransTruncLTOfLE a b (by simpa using leOfHom f) + | top => exact t.truncLTι a + | top => + induction y using WithBotTop.rec with + | bot => exact 0 + | coe b => exact 0 + | top => exact 𝟙 _ + map_id n := by induction n using WithBotTop.rec <;> simp + map_comp {x y z} f g := by + have f' := leOfHom f + have g' := leOfHom g + induction x using WithBotTop.rec <;> induction y using WithBotTop.rec <;> + induction z using WithBotTop.rec <;> cat_disch + +@[simp] +lemma eTruncLT_obj_top : t.eTruncLT.obj ⊤ = 𝟭 _ := rfl + +@[simp] +lemma eTruncLT_obj_bot : t.eTruncLT.obj ⊥ = 0 := rfl + +@[simp] +lemma eTruncLT_obj_coe (n : ℤ) : t.eTruncLT.obj n = t.truncLT n := rfl + +@[simp] +lemma eTruncLT_map_eq_truncLTι (n : ℤ) : + t.eTruncLT.map (homOfLE (show (n : EInt) ≤ ⊤ by simp)) = t.truncLTι n := rfl + +instance (i : EInt) : (t.eTruncLT.obj i).Additive := by + induction i using WithBotTop.rec <;> constructor <;> cat_disch + +/-- The functor `EInt ⥤ C ⥤ C` which sends `⊥` to `𝟭 C`, +`n : ℤ` to `t.truncGE n` and `⊤` to the zero functor. -/ +noncomputable def eTruncGE : EInt ⥤ C ⥤ C where + obj n := by + induction n using WithBotTop.rec with + | bot => exact 𝟭 C + | coe a => exact t.truncGE a + | top => exact 0 + map {x y} f := by + induction x using WithBotTop.rec with + | bot => + induction y using WithBotTop.rec with + | bot => exact 𝟙 _ + | coe b => exact t.truncGEπ b + | top => exact 0 + | coe a => + induction y using WithBotTop.rec with + | bot => exact 0 + | coe b => exact t.natTransTruncGEOfLE a b (by simpa using leOfHom f) + | top => exact 0 + | top => + induction y using WithBotTop.rec with + | bot => exact 0 + | coe b => exact 0 + | top => exact 𝟙 _ + map_id n := by induction n using WithBotTop.rec <;> simp + map_comp {x y z} f g := by + have f' := leOfHom f + have g' := leOfHom g + induction x using WithBotTop.rec <;> induction y using WithBotTop.rec <;> + induction z using WithBotTop.rec <;> cat_disch + +@[simp] +lemma eTruncGE_obj_bot : + t.eTruncGE.obj ⊥ = 𝟭 _ := rfl + +@[simp] +lemma eTruncGE_obj_top : + t.eTruncGE.obj ⊤ = 0 := rfl + +@[simp] +lemma eTruncGE_obj_coe (n : ℤ) : t.eTruncGE.obj n = t.truncGE n := rfl + +instance (i : EInt) : (t.eTruncGE.obj i).Additive := by + induction i using WithBotTop.rec <;> constructor <;> cat_disch + +/-- The connecting homomorphism from `t.eTruncGE` to the +shift by `1` of `t.eTruncLT`. -/ +noncomputable def eTruncGEδLT : + t.eTruncGE ⟶ t.eTruncLT ⋙ ((Functor.whiskeringRight C C C).obj (shiftFunctor C (1 : ℤ))) where + app a := by + induction a using WithBotTop.rec with + | bot => exact 0 + | coe a => exact t.truncGEδLT a + | top => exact 0 + naturality {a b} hab := by + replace hab := leOfHom hab + induction a using WithBotTop.rec; rotate_right + · apply (isZero_zero _).eq_of_src + all_goals + induction b using WithBotTop.rec <;> simp at hab <;> + dsimp [eTruncGE, eTruncLT] <;> + simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE] + +@[simp] +lemma eTruncGEδLT_coe (n : ℤ) : + t.eTruncGEδLT.app n = t.truncGEδLT n := rfl + +/-- The natural transformation `t.eTruncLT.obj i ⟶ 𝟭 C` for all `i : EInt`. -/ +noncomputable abbrev eTruncLTι (i : EInt) : t.eTruncLT.obj i ⟶ 𝟭 _ := + t.eTruncLT.map (homOfLE (le_top)) + +@[simp] lemma eTruncLT_ι_bot : t.eTruncLTι ⊥ = 0 := rfl +@[simp] lemma eTruncLT_ι_coe (n : ℤ) : t.eTruncLTι n = t.truncLTι n := rfl +@[simp] lemma eTruncLT_ι_top : t.eTruncLTι ⊤ = 𝟙 _ := rfl + +@[reassoc] +lemma eTruncLTι_naturality (i : EInt) {X Y : C} (f : X ⟶ Y) : + (t.eTruncLT.obj i).map f ≫ (t.eTruncLTι i).app Y = (t.eTruncLTι i).app X ≫ f := + (t.eTruncLTι i).naturality f + +instance : IsIso (t.eTruncLTι ⊤) := by + dsimp [eTruncLTι] + infer_instance + +@[reassoc (attr := simp)] +lemma eTruncLT_map_app_eTruncLTι_app {i j : EInt} (f : i ⟶ j) (X : C) : + (t.eTruncLT.map f).app X ≫ (t.eTruncLTι j).app X = (t.eTruncLTι i).app X := by + simp only [← NatTrans.comp_app, ← Functor.map_comp] + rfl + +@[reassoc] +lemma eTruncLT_obj_map_eTruncLTι_app (i : EInt) (X : C) : + (t.eTruncLT.obj i).map ((t.eTruncLTι i).app X) = + (t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X) := by + induction i using WithBotTop.rec with + | bot => simp + | coe n => simp [truncLT_map_truncLTι_app] + | top => simp + +/-- The natural transformation `𝟭 C ⟶ t.eTruncGE.obj i` for all `i : EInt`. -/ +noncomputable abbrev eTruncGEπ (i : EInt) : 𝟭 C ⟶ t.eTruncGE.obj i := + t.eTruncGE.map (homOfLE (bot_le)) + +@[simp] lemma eTruncGEπ_bot : t.eTruncGEπ ⊥ = 𝟙 _ := rfl +@[simp] lemma eTruncGEπ_coe (n : ℤ) : t.eTruncGEπ n = t.truncGEπ n := rfl +@[simp] lemma eTruncGEπ_top : t.eTruncGEπ ⊤ = 0 := rfl + +@[reassoc (attr := simp)] +lemma eTruncGEπ_naturality (i : EInt) {X Y : C} (f : X ⟶ Y) : + (t.eTruncGEπ i).app X ≫ (t.eTruncGE.obj i).map f = f ≫ (t.eTruncGEπ i).app Y := + ((t.eTruncGEπ i).naturality f).symm + +instance : IsIso (t.eTruncGEπ ⊥) := by + dsimp [eTruncGEπ] + infer_instance + +@[reassoc (attr := simp)] +lemma eTruncGEπ_app_eTruncGE_map_app {i j : EInt} (f : i ⟶ j) (X : C) : + (t.eTruncGEπ i).app X ≫ (t.eTruncGE.map f).app X = (t.eTruncGEπ j).app X := by + simp only [← NatTrans.comp_app, ← Functor.map_comp] + rfl + +@[reassoc] +lemma eTruncGE_obj_map_eTruncGEπ_app (i : EInt) (X : C) : + (t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X) = + (t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X) := by + induction i using WithBotTop.rec with + | bot => simp + | coe n => simp [truncGE_map_truncGEπ_app] + | top => simp + +/-- The (distinguished) triangles given by the natural transformations +`t.eTruncLT.obj i ⟶ 𝟭 C ⟶ t.eTruncGE.obj i ⟶ ...` for all `i : EInt`. -/ +@[simps!] +noncomputable def eTriangleLTGE : EInt ⥤ C ⥤ Triangle C where + obj i := Triangle.functorMk (t.eTruncLTι i) (t.eTruncGEπ i) (t.eTruncGEδLT.app i) + map f := Triangle.functorHomMk _ _ (t.eTruncLT.map f) (𝟙 _) (t.eTruncGE.map f) + +lemma eTriangleLTGE_distinguished (i : EInt) (X : C) : + (t.eTriangleLTGE.obj i).obj X ∈ distTriang _ := by + induction i using WithBotTop.rec with + | bot => + rw [Triangle.distinguished_iff_of_isZero₁ _ (Functor.zero_obj X)] + dsimp + infer_instance + | coe n => exact t.triangleLTGE_distinguished n X + | top => + rw [Triangle.distinguished_iff_of_isZero₃ _ (Functor.zero_obj X)] + dsimp + infer_instance + +instance (X : C) (n : ℤ) [t.IsLE X n] (i : EInt) : + t.IsLE ((t.eTruncLT.obj i).obj X) n := by + induction i using WithBotTop.rec with + | bot => exact isLE_of_isZero _ (by simp) _ + | coe _ => dsimp; infer_instance + | top => dsimp; infer_instance + +instance (X : C) (n : ℤ) [t.IsGE X n] (i : EInt) : + t.IsGE ((t.eTruncGE.obj i).obj X) n := by + induction i using WithBotTop.rec with + | bot => dsimp; infer_instance + | coe _ => dsimp; infer_instance + | top => exact isGE_of_isZero _ (by simp) _ + +lemma isGE_eTruncGE_obj_obj (n : ℤ) (i : EInt) (h : n ≤ i) (X : C) : + t.IsGE ((t.eTruncGE.obj i).obj X) n := by + induction i using WithBotTop.rec with + | bot => simp at h + | coe i => + dsimp + exact t.isGE_of_ge _ _ _ (by simpa using h) + | top => exact t.isGE_of_isZero (Functor.zero_obj _) _ + +lemma isLE_eTruncLT_obj_obj (n : ℤ) (i : EInt) (h : i ≤ (n + 1 :)) (X : C) : + t.IsLE (((t.eTruncLT.obj i)).obj X) n := by + induction i using WithBotTop.rec with + | bot => exact t.isLE_of_isZero (by simp) _ + | coe i => + simp only [WithBotTop.coe_le_coe] at h + dsimp + exact t.isLE_of_le _ (i - 1) n (by lia) + | top => simp at h + +lemma isZero_eTruncLT_obj_obj (X : C) (n : ℤ) [t.IsGE X n] (j : EInt) (hj : j ≤ n) : + IsZero ((t.eTruncLT.obj j).obj X) := by + induction j using WithBotTop.rec with + | bot => simp + | coe j => + have := t.isGE_of_ge X j n (by simpa using hj) + exact t.isZero_truncLT_obj_of_isGE _ _ + | top => simp at hj + +lemma isZero_eTruncGE_obj_obj (X : C) (n : ℤ) [t.IsLE X n] (j : EInt) (hj : n < j) : + IsZero ((t.eTruncGE.obj j).obj X) := by + induction j using WithBotTop.rec with + | bot => simp at hj + | coe j => + simp only [WithBotTop.coe_lt_coe] at hj + have := t.isLE_of_le X n (j - 1) (by lia) + exact t.isZero_truncGE_obj_of_isLE (j - 1) j (by lia) _ + | top => simp + +section + +variable [IsTriangulated C] + +lemma isIso_eTruncGE_obj_map_truncGEπ_app (a b : EInt) (h : a ≤ b) (X : C) : + IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) := by + induction b using WithBotTop.rec with + | bot => + obtain rfl : a = ⊥ := by simpa using h + infer_instance + | coe b => + induction a using WithBotTop.rec with + | bot => dsimp; infer_instance + | coe a => exact t.isIso_truncGE_map_truncGEπ_app b a (by simpa using h) X + | top => simp at h + | top => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩ + +lemma isIso_eTruncLT_obj_map_truncLTπ_app (a b : EInt) (h : a ≤ b) (X : C) : + IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι b).app X)) := by + induction a using WithBotTop.rec with + | bot => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩ + | coe a => + induction b using WithBotTop.rec with + | bot => simp at h + | coe b => + exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X + | top => dsimp; infer_instance + | top => + obtain rfl : b = ⊤ := by simpa using h + infer_instance + +instance (a : EInt) (X : C) : IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X)) := + isIso_eTruncLT_obj_map_truncLTπ_app t a a (by rfl) X + +instance (a : EInt) (X : C) : IsIso ((t.eTruncLTι a).app ((t.eTruncLT.obj a).obj X)) := by + rw [← eTruncLT_obj_map_eTruncLTι_app] + infer_instance + +instance (X : C) (n : ℤ) [t.IsGE X n] (i : EInt) : + t.IsGE ((t.eTruncLT.obj i).obj X) n := by + induction i using WithBotTop.rec with + | bot => exact isGE_of_isZero _ (by simp) _ + | coe _ => dsimp; infer_instance + | top => dsimp; infer_instance + +instance (X : C) (n : ℤ) [t.IsLE X n] (i : EInt) : + t.IsLE ((t.eTruncGE.obj i).obj X) n := by + induction i using WithBotTop.rec with + | bot => dsimp; infer_instance + | coe _ => dsimp; infer_instance + | top => exact isLE_of_isZero _ (by simp) _ + +/-- The natural transformation `t.eTruncGE.obj b ⟶ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b` +for all `a` and `b` in `EInt`. -/ +@[simps!] +noncomputable def eTruncGEToGEGE (a b : EInt) : + t.eTruncGE.obj b ⟶ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b := + (Functor.leftUnitor _).inv ≫ Functor.whiskerRight (t.eTruncGEπ a) _ + +lemma isIso_eTruncGEIsoGEGE (a b : EInt) (hab : a ≤ b) : + IsIso (t.eTruncGEToGEGE a b) := by + rw [NatTrans.isIso_iff_isIso_app] + intro X + simp only [Functor.comp_obj, eTruncGEToGEGE_app] + exact t.isIso_eTruncGE_obj_map_truncGEπ_app _ _ hab _ + +section + +variable (a b : EInt) (hab : a ≤ b) + +/-- The natural isomorphism `t.eTruncGE.obj b ≅ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b` +when `a` and `b` in `EInt` satisfy `a ≤ b`. -/ +@[simps! hom] +noncomputable def eTruncGEIsoGEGE : + t.eTruncGE.obj b ≅ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b := + haveI := t.isIso_eTruncGEIsoGEGE a b hab + asIso (t.eTruncGEToGEGE a b) + +@[reassoc (attr := simp)] +lemma eTruncGEIsoGEGE_hom_inv_id_app (X : C) : + (t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X) ≫ (t.eTruncGEIsoGEGE a b hab).inv.app X = + 𝟙 _ := by + simpa using (t.eTruncGEIsoGEGE a b hab).hom_inv_id_app X + +@[reassoc (attr := simp)] +lemma eTruncGEIsoGEGE_inv_hom_id_app (X : C) : + (t.eTruncGEIsoGEGE a b hab).inv.app X ≫ (t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X) = + 𝟙 _ := by + simpa using (t.eTruncGEIsoGEGE a b hab).inv_hom_id_app X + +end + +/-- The natural transformation `t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b` +for all `a` and `b` in `EInt`. -/ +@[simps!] +noncomputable def eTruncLTLTToLT (a b : EInt) : + t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b := + Functor.whiskerRight (t.eTruncLTι a) _ ≫ (Functor.leftUnitor _).hom + +lemma isIso_eTruncLTLTIsoLT (a b : EInt) (hab : b ≤ a) : + IsIso (t.eTruncLTLTToLT a b) := by + rw [NatTrans.isIso_iff_isIso_app] + intro X + simp only [Functor.comp_obj, eTruncLTLTToLT_app] + exact t.isIso_eTruncLT_obj_map_truncLTπ_app _ _ hab _ + +section + +variable (a b : EInt) (hab : b ≤ a) + +/-- The natural isomorphism `t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b` +when `a` and `b` in `EInt` satisfy `b ≤ a`. -/ +@[simps! hom] +noncomputable def eTruncLTLTIsoLT : + t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ≅ t.eTruncLT.obj b := + haveI := t.isIso_eTruncLTLTIsoLT a b hab + asIso (t.eTruncLTLTToLT a b) + +@[reassoc] +lemma eTruncLTLTIsoLT_hom_inv_id_app (X : C) : + (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X) ≫ + (t.eTruncLTLTIsoLT a b hab).inv.app X = 𝟙 _ := by + simpa using (t.eTruncLTLTIsoLT a b hab).hom_inv_id_app X + +@[reassoc (attr := simp)] +lemma eTruncLTLTIsoLT_inv_hom_id_app (X : C) : + (t.eTruncLTLTIsoLT a b hab).inv.app X ≫ + (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X) = 𝟙 _ := by + simpa using (t.eTruncLTLTIsoLT a b hab).inv_hom_id_app X + +@[reassoc (attr := simp)] +lemma eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj (X : C) : + (t.eTruncLTLTIsoLT a b hab).inv.app ((t.eTruncLT.obj a).obj X) ≫ + (t.eTruncLT.obj b).map ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X)) = 𝟙 _ := by + simp [eTruncLT_obj_map_eTruncLTι_app] + +end + + +section + +variable (a b : EInt) + +/-- The natural transformation from +`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b` to +`t.eTruncGE.obj a ⋙ t.eTruncLT.obj b`. (This is an isomorphism.) -/ +@[simps!] +noncomputable def eTruncLTGELTSelfToLTGE : + t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ⟶ + t.eTruncGE.obj a ⋙ t.eTruncLT.obj b := + Functor.whiskerRight (t.eTruncLTι b) _ ≫ (Functor.leftUnitor _).hom + +/-- The natural transformation from +`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b` to +`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a`. (This is an isomorphism.) -/ +@[simps!] +noncomputable def eTruncLTGELTSelfToGELT : + t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ⟶ + t.eTruncLT.obj b ⋙ t.eTruncGE.obj a := + (Functor.associator _ _ _).inv ≫ Functor.whiskerLeft _ (t.eTruncLTι b) ≫ + (Functor.rightUnitor _).hom + +instance : IsIso (t.eTruncLTGELTSelfToLTGE a b) := by + rw [NatTrans.isIso_iff_isIso_app] + intro X + induction b using WithBotTop.rec with + | bot => simp [isIsoZero_iff_source_target_isZero] + | coe b => + induction a using WithBotTop.rec with + | bot => simpa using inferInstanceAs (IsIso ((t.truncLT b).map ((t.truncLTι b).app X))) + | coe a => + simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app, + eTruncLT_map_eq_truncLTι] + infer_instance + | top => + simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app, + eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero] + constructor + all_goals exact Functor.map_isZero _ (Functor.zero_obj _) + | top => simpa using inferInstanceAs (IsIso (𝟙 _)) + +variable (b : EInt) (X : C) + +instance : IsIso (t.eTruncLTGELTSelfToGELT a b) := by + rw [NatTrans.isIso_iff_isIso_app] + intro X + induction a using WithBotTop.rec with + | bot => simpa using inferInstanceAs (IsIso ((t.eTruncLTι b).app ((t.eTruncLT.obj b).obj X))) + | coe a => + induction b using WithBotTop.rec with + | bot => simpa [isIsoZero_iff_source_target_isZero] using + (t.eTruncGE.obj a).map_isZero (Functor.zero_obj _) + | coe b => + simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToGELT_app, + eTruncLT_map_eq_truncLTι] + infer_instance + | top => simpa using inferInstanceAs (IsIso (𝟙 _)) + | top => + exact ⟨0, ((t.eTruncLT.obj b).map_isZero (by simp)).eq_of_src _ _, + IsZero.eq_of_src (by simp) _ _⟩ + +end + +/-- The commutation natural isomorphism +`t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ≅ t.eTruncLT.obj b ⋙ t.eTruncGE.obj a` +for all `a` and `b` in `EInt`. -/ +noncomputable def eTruncLTGEIsoLEGT (a b : EInt) : + t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ≅ t.eTruncLT.obj b ⋙ t.eTruncGE.obj a := + (asIso (t.eTruncLTGELTSelfToLTGE a b)).symm ≪≫ asIso (t.eTruncLTGELTSelfToGELT a b) + +@[reassoc (attr := simp)] +lemma eTruncLTGEIsoLEGT_hom_naturality (a b : EInt) {X Y : C} (f : X ⟶ Y) : + (t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map f) ≫ (t.eTruncLTGEIsoLEGT a b).hom.app Y = + (t.eTruncLTGEIsoLEGT a b).hom.app X ≫ (t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map f) := + (t.eTruncLTGEIsoLEGT a b).hom.naturality f + +@[reassoc] +lemma eTruncLTGEIsoLEGT_hom_app_fac (a b : EInt) (X : C) : + (t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)) ≫ + (t.eTruncLTGEIsoLEGT a b).hom.app X = + (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)):= by + simp [eTruncLTGEIsoLEGT] + +@[reassoc (attr := simp)] +lemma eTruncLTGEIsoLEGT_hom_app_fac' (a b : EInt) (X : C) : + (t.eTruncLTGEIsoLEGT a b).hom.app X ≫ (t.eTruncGE.obj a).map ((t.eTruncLTι b).app X) = + (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj X) := by + simp [eTruncLTGEIsoLEGT] + +open ComposableArrows in +@[reassoc] +lemma eTruncLTGEIsoLEGT_naturality_app (a b : EInt) (hab : a ≤ b) + (a' b' : EInt) (hab' : a' ≤ b') (φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')) (X : C) : + (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj X) ≫ + (t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app X) ≫ + (t.eTruncLTGEIsoLEGT a' b').hom.app X = + (t.eTruncLTGEIsoLEGT a b).hom.app X ≫ (t.eTruncGE.map (φ.app 0)).app _ ≫ + (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X) := by + rw [← cancel_epi ((t.eTruncLTGELTSelfToLTGE a b).app X)] + dsimp + rw [eTruncLTGELTSelfToLTGE_app, eTruncLTGEIsoLEGT_hom_app_fac_assoc, + NatTrans.naturality_assoc, ← Functor.map_comp_assoc, NatTrans.naturality, + Functor.map_comp_assoc, ← t.eTruncLT_map_app_eTruncLTι_app (φ.app 1) X, + Functor.map_comp, Functor.map_comp, Category.assoc, + t.eTruncLTGEIsoLEGT_hom_app_fac] + simp + +end + +end TStructure + +end Triangulated + +end CategoryTheory From 4a878319836d22f942eee2de152ebb1ccf2494e4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 15 Feb 2026 17:38:22 +0100 Subject: [PATCH 6/7] split file --- .../Triangulated/TStructure/ETrunc.lean | 249 ------------------ 1 file changed, 249 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean b/Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean index b34c95662a8b64..7c89764db26a78 100644 --- a/Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean +++ b/Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean @@ -285,255 +285,6 @@ lemma isZero_eTruncGE_obj_obj (X : C) (n : ℤ) [t.IsLE X n] (j : EInt) (hj : n exact t.isZero_truncGE_obj_of_isLE (j - 1) j (by lia) _ | top => simp -section - -variable [IsTriangulated C] - -lemma isIso_eTruncGE_obj_map_truncGEπ_app (a b : EInt) (h : a ≤ b) (X : C) : - IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) := by - induction b using WithBotTop.rec with - | bot => - obtain rfl : a = ⊥ := by simpa using h - infer_instance - | coe b => - induction a using WithBotTop.rec with - | bot => dsimp; infer_instance - | coe a => exact t.isIso_truncGE_map_truncGEπ_app b a (by simpa using h) X - | top => simp at h - | top => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩ - -lemma isIso_eTruncLT_obj_map_truncLTπ_app (a b : EInt) (h : a ≤ b) (X : C) : - IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι b).app X)) := by - induction a using WithBotTop.rec with - | bot => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩ - | coe a => - induction b using WithBotTop.rec with - | bot => simp at h - | coe b => - exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X - | top => dsimp; infer_instance - | top => - obtain rfl : b = ⊤ := by simpa using h - infer_instance - -instance (a : EInt) (X : C) : IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X)) := - isIso_eTruncLT_obj_map_truncLTπ_app t a a (by rfl) X - -instance (a : EInt) (X : C) : IsIso ((t.eTruncLTι a).app ((t.eTruncLT.obj a).obj X)) := by - rw [← eTruncLT_obj_map_eTruncLTι_app] - infer_instance - -instance (X : C) (n : ℤ) [t.IsGE X n] (i : EInt) : - t.IsGE ((t.eTruncLT.obj i).obj X) n := by - induction i using WithBotTop.rec with - | bot => exact isGE_of_isZero _ (by simp) _ - | coe _ => dsimp; infer_instance - | top => dsimp; infer_instance - -instance (X : C) (n : ℤ) [t.IsLE X n] (i : EInt) : - t.IsLE ((t.eTruncGE.obj i).obj X) n := by - induction i using WithBotTop.rec with - | bot => dsimp; infer_instance - | coe _ => dsimp; infer_instance - | top => exact isLE_of_isZero _ (by simp) _ - -/-- The natural transformation `t.eTruncGE.obj b ⟶ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b` -for all `a` and `b` in `EInt`. -/ -@[simps!] -noncomputable def eTruncGEToGEGE (a b : EInt) : - t.eTruncGE.obj b ⟶ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b := - (Functor.leftUnitor _).inv ≫ Functor.whiskerRight (t.eTruncGEπ a) _ - -lemma isIso_eTruncGEIsoGEGE (a b : EInt) (hab : a ≤ b) : - IsIso (t.eTruncGEToGEGE a b) := by - rw [NatTrans.isIso_iff_isIso_app] - intro X - simp only [Functor.comp_obj, eTruncGEToGEGE_app] - exact t.isIso_eTruncGE_obj_map_truncGEπ_app _ _ hab _ - -section - -variable (a b : EInt) (hab : a ≤ b) - -/-- The natural isomorphism `t.eTruncGE.obj b ≅ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b` -when `a` and `b` in `EInt` satisfy `a ≤ b`. -/ -@[simps! hom] -noncomputable def eTruncGEIsoGEGE : - t.eTruncGE.obj b ≅ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b := - haveI := t.isIso_eTruncGEIsoGEGE a b hab - asIso (t.eTruncGEToGEGE a b) - -@[reassoc (attr := simp)] -lemma eTruncGEIsoGEGE_hom_inv_id_app (X : C) : - (t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X) ≫ (t.eTruncGEIsoGEGE a b hab).inv.app X = - 𝟙 _ := by - simpa using (t.eTruncGEIsoGEGE a b hab).hom_inv_id_app X - -@[reassoc (attr := simp)] -lemma eTruncGEIsoGEGE_inv_hom_id_app (X : C) : - (t.eTruncGEIsoGEGE a b hab).inv.app X ≫ (t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X) = - 𝟙 _ := by - simpa using (t.eTruncGEIsoGEGE a b hab).inv_hom_id_app X - -end - -/-- The natural transformation `t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b` -for all `a` and `b` in `EInt`. -/ -@[simps!] -noncomputable def eTruncLTLTToLT (a b : EInt) : - t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b := - Functor.whiskerRight (t.eTruncLTι a) _ ≫ (Functor.leftUnitor _).hom - -lemma isIso_eTruncLTLTIsoLT (a b : EInt) (hab : b ≤ a) : - IsIso (t.eTruncLTLTToLT a b) := by - rw [NatTrans.isIso_iff_isIso_app] - intro X - simp only [Functor.comp_obj, eTruncLTLTToLT_app] - exact t.isIso_eTruncLT_obj_map_truncLTπ_app _ _ hab _ - -section - -variable (a b : EInt) (hab : b ≤ a) - -/-- The natural isomorphism `t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b` -when `a` and `b` in `EInt` satisfy `b ≤ a`. -/ -@[simps! hom] -noncomputable def eTruncLTLTIsoLT : - t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ≅ t.eTruncLT.obj b := - haveI := t.isIso_eTruncLTLTIsoLT a b hab - asIso (t.eTruncLTLTToLT a b) - -@[reassoc] -lemma eTruncLTLTIsoLT_hom_inv_id_app (X : C) : - (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X) ≫ - (t.eTruncLTLTIsoLT a b hab).inv.app X = 𝟙 _ := by - simpa using (t.eTruncLTLTIsoLT a b hab).hom_inv_id_app X - -@[reassoc (attr := simp)] -lemma eTruncLTLTIsoLT_inv_hom_id_app (X : C) : - (t.eTruncLTLTIsoLT a b hab).inv.app X ≫ - (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X) = 𝟙 _ := by - simpa using (t.eTruncLTLTIsoLT a b hab).inv_hom_id_app X - -@[reassoc (attr := simp)] -lemma eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj (X : C) : - (t.eTruncLTLTIsoLT a b hab).inv.app ((t.eTruncLT.obj a).obj X) ≫ - (t.eTruncLT.obj b).map ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X)) = 𝟙 _ := by - simp [eTruncLT_obj_map_eTruncLTι_app] - -end - - -section - -variable (a b : EInt) - -/-- The natural transformation from -`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b` to -`t.eTruncGE.obj a ⋙ t.eTruncLT.obj b`. (This is an isomorphism.) -/ -@[simps!] -noncomputable def eTruncLTGELTSelfToLTGE : - t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ⟶ - t.eTruncGE.obj a ⋙ t.eTruncLT.obj b := - Functor.whiskerRight (t.eTruncLTι b) _ ≫ (Functor.leftUnitor _).hom - -/-- The natural transformation from -`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b` to -`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a`. (This is an isomorphism.) -/ -@[simps!] -noncomputable def eTruncLTGELTSelfToGELT : - t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ⟶ - t.eTruncLT.obj b ⋙ t.eTruncGE.obj a := - (Functor.associator _ _ _).inv ≫ Functor.whiskerLeft _ (t.eTruncLTι b) ≫ - (Functor.rightUnitor _).hom - -instance : IsIso (t.eTruncLTGELTSelfToLTGE a b) := by - rw [NatTrans.isIso_iff_isIso_app] - intro X - induction b using WithBotTop.rec with - | bot => simp [isIsoZero_iff_source_target_isZero] - | coe b => - induction a using WithBotTop.rec with - | bot => simpa using inferInstanceAs (IsIso ((t.truncLT b).map ((t.truncLTι b).app X))) - | coe a => - simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app, - eTruncLT_map_eq_truncLTι] - infer_instance - | top => - simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app, - eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero] - constructor - all_goals exact Functor.map_isZero _ (Functor.zero_obj _) - | top => simpa using inferInstanceAs (IsIso (𝟙 _)) - -variable (b : EInt) (X : C) - -instance : IsIso (t.eTruncLTGELTSelfToGELT a b) := by - rw [NatTrans.isIso_iff_isIso_app] - intro X - induction a using WithBotTop.rec with - | bot => simpa using inferInstanceAs (IsIso ((t.eTruncLTι b).app ((t.eTruncLT.obj b).obj X))) - | coe a => - induction b using WithBotTop.rec with - | bot => simpa [isIsoZero_iff_source_target_isZero] using - (t.eTruncGE.obj a).map_isZero (Functor.zero_obj _) - | coe b => - simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToGELT_app, - eTruncLT_map_eq_truncLTι] - infer_instance - | top => simpa using inferInstanceAs (IsIso (𝟙 _)) - | top => - exact ⟨0, ((t.eTruncLT.obj b).map_isZero (by simp)).eq_of_src _ _, - IsZero.eq_of_src (by simp) _ _⟩ - -end - -/-- The commutation natural isomorphism -`t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ≅ t.eTruncLT.obj b ⋙ t.eTruncGE.obj a` -for all `a` and `b` in `EInt`. -/ -noncomputable def eTruncLTGEIsoLEGT (a b : EInt) : - t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ≅ t.eTruncLT.obj b ⋙ t.eTruncGE.obj a := - (asIso (t.eTruncLTGELTSelfToLTGE a b)).symm ≪≫ asIso (t.eTruncLTGELTSelfToGELT a b) - -@[reassoc (attr := simp)] -lemma eTruncLTGEIsoLEGT_hom_naturality (a b : EInt) {X Y : C} (f : X ⟶ Y) : - (t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map f) ≫ (t.eTruncLTGEIsoLEGT a b).hom.app Y = - (t.eTruncLTGEIsoLEGT a b).hom.app X ≫ (t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map f) := - (t.eTruncLTGEIsoLEGT a b).hom.naturality f - -@[reassoc] -lemma eTruncLTGEIsoLEGT_hom_app_fac (a b : EInt) (X : C) : - (t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)) ≫ - (t.eTruncLTGEIsoLEGT a b).hom.app X = - (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)):= by - simp [eTruncLTGEIsoLEGT] - -@[reassoc (attr := simp)] -lemma eTruncLTGEIsoLEGT_hom_app_fac' (a b : EInt) (X : C) : - (t.eTruncLTGEIsoLEGT a b).hom.app X ≫ (t.eTruncGE.obj a).map ((t.eTruncLTι b).app X) = - (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj X) := by - simp [eTruncLTGEIsoLEGT] - -open ComposableArrows in -@[reassoc] -lemma eTruncLTGEIsoLEGT_naturality_app (a b : EInt) (hab : a ≤ b) - (a' b' : EInt) (hab' : a' ≤ b') (φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')) (X : C) : - (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj X) ≫ - (t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app X) ≫ - (t.eTruncLTGEIsoLEGT a' b').hom.app X = - (t.eTruncLTGEIsoLEGT a b).hom.app X ≫ (t.eTruncGE.map (φ.app 0)).app _ ≫ - (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X) := by - rw [← cancel_epi ((t.eTruncLTGELTSelfToLTGE a b).app X)] - dsimp - rw [eTruncLTGELTSelfToLTGE_app, eTruncLTGEIsoLEGT_hom_app_fac_assoc, - NatTrans.naturality_assoc, ← Functor.map_comp_assoc, NatTrans.naturality, - Functor.map_comp_assoc, ← t.eTruncLT_map_app_eTruncLTι_app (φ.app 1) X, - Functor.map_comp, Functor.map_comp, Category.assoc, - t.eTruncLTGEIsoLEGT_hom_app_fac] - simp - -end - end TStructure end Triangulated From 4ad034fb3936cef74c539813751f6fa265530c50 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 15 Feb 2026 17:40:00 +0100 Subject: [PATCH 7/7] etrunc triangulated --- .../Triangulated/TStructure/ETrunc.lean | 249 ++++++++++++++++++ 1 file changed, 249 insertions(+) diff --git a/Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean b/Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean index 7c89764db26a78..b34c95662a8b64 100644 --- a/Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean +++ b/Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean @@ -285,6 +285,255 @@ lemma isZero_eTruncGE_obj_obj (X : C) (n : ℤ) [t.IsLE X n] (j : EInt) (hj : n exact t.isZero_truncGE_obj_of_isLE (j - 1) j (by lia) _ | top => simp +section + +variable [IsTriangulated C] + +lemma isIso_eTruncGE_obj_map_truncGEπ_app (a b : EInt) (h : a ≤ b) (X : C) : + IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) := by + induction b using WithBotTop.rec with + | bot => + obtain rfl : a = ⊥ := by simpa using h + infer_instance + | coe b => + induction a using WithBotTop.rec with + | bot => dsimp; infer_instance + | coe a => exact t.isIso_truncGE_map_truncGEπ_app b a (by simpa using h) X + | top => simp at h + | top => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩ + +lemma isIso_eTruncLT_obj_map_truncLTπ_app (a b : EInt) (h : a ≤ b) (X : C) : + IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι b).app X)) := by + induction a using WithBotTop.rec with + | bot => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩ + | coe a => + induction b using WithBotTop.rec with + | bot => simp at h + | coe b => + exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X + | top => dsimp; infer_instance + | top => + obtain rfl : b = ⊤ := by simpa using h + infer_instance + +instance (a : EInt) (X : C) : IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X)) := + isIso_eTruncLT_obj_map_truncLTπ_app t a a (by rfl) X + +instance (a : EInt) (X : C) : IsIso ((t.eTruncLTι a).app ((t.eTruncLT.obj a).obj X)) := by + rw [← eTruncLT_obj_map_eTruncLTι_app] + infer_instance + +instance (X : C) (n : ℤ) [t.IsGE X n] (i : EInt) : + t.IsGE ((t.eTruncLT.obj i).obj X) n := by + induction i using WithBotTop.rec with + | bot => exact isGE_of_isZero _ (by simp) _ + | coe _ => dsimp; infer_instance + | top => dsimp; infer_instance + +instance (X : C) (n : ℤ) [t.IsLE X n] (i : EInt) : + t.IsLE ((t.eTruncGE.obj i).obj X) n := by + induction i using WithBotTop.rec with + | bot => dsimp; infer_instance + | coe _ => dsimp; infer_instance + | top => exact isLE_of_isZero _ (by simp) _ + +/-- The natural transformation `t.eTruncGE.obj b ⟶ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b` +for all `a` and `b` in `EInt`. -/ +@[simps!] +noncomputable def eTruncGEToGEGE (a b : EInt) : + t.eTruncGE.obj b ⟶ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b := + (Functor.leftUnitor _).inv ≫ Functor.whiskerRight (t.eTruncGEπ a) _ + +lemma isIso_eTruncGEIsoGEGE (a b : EInt) (hab : a ≤ b) : + IsIso (t.eTruncGEToGEGE a b) := by + rw [NatTrans.isIso_iff_isIso_app] + intro X + simp only [Functor.comp_obj, eTruncGEToGEGE_app] + exact t.isIso_eTruncGE_obj_map_truncGEπ_app _ _ hab _ + +section + +variable (a b : EInt) (hab : a ≤ b) + +/-- The natural isomorphism `t.eTruncGE.obj b ≅ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b` +when `a` and `b` in `EInt` satisfy `a ≤ b`. -/ +@[simps! hom] +noncomputable def eTruncGEIsoGEGE : + t.eTruncGE.obj b ≅ t.eTruncGE.obj a ⋙ t.eTruncGE.obj b := + haveI := t.isIso_eTruncGEIsoGEGE a b hab + asIso (t.eTruncGEToGEGE a b) + +@[reassoc (attr := simp)] +lemma eTruncGEIsoGEGE_hom_inv_id_app (X : C) : + (t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X) ≫ (t.eTruncGEIsoGEGE a b hab).inv.app X = + 𝟙 _ := by + simpa using (t.eTruncGEIsoGEGE a b hab).hom_inv_id_app X + +@[reassoc (attr := simp)] +lemma eTruncGEIsoGEGE_inv_hom_id_app (X : C) : + (t.eTruncGEIsoGEGE a b hab).inv.app X ≫ (t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X) = + 𝟙 _ := by + simpa using (t.eTruncGEIsoGEGE a b hab).inv_hom_id_app X + +end + +/-- The natural transformation `t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b` +for all `a` and `b` in `EInt`. -/ +@[simps!] +noncomputable def eTruncLTLTToLT (a b : EInt) : + t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b := + Functor.whiskerRight (t.eTruncLTι a) _ ≫ (Functor.leftUnitor _).hom + +lemma isIso_eTruncLTLTIsoLT (a b : EInt) (hab : b ≤ a) : + IsIso (t.eTruncLTLTToLT a b) := by + rw [NatTrans.isIso_iff_isIso_app] + intro X + simp only [Functor.comp_obj, eTruncLTLTToLT_app] + exact t.isIso_eTruncLT_obj_map_truncLTπ_app _ _ hab _ + +section + +variable (a b : EInt) (hab : b ≤ a) + +/-- The natural isomorphism `t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ⟶ t.eTruncLT.obj b` +when `a` and `b` in `EInt` satisfy `b ≤ a`. -/ +@[simps! hom] +noncomputable def eTruncLTLTIsoLT : + t.eTruncLT.obj a ⋙ t.eTruncLT.obj b ≅ t.eTruncLT.obj b := + haveI := t.isIso_eTruncLTLTIsoLT a b hab + asIso (t.eTruncLTLTToLT a b) + +@[reassoc] +lemma eTruncLTLTIsoLT_hom_inv_id_app (X : C) : + (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X) ≫ + (t.eTruncLTLTIsoLT a b hab).inv.app X = 𝟙 _ := by + simpa using (t.eTruncLTLTIsoLT a b hab).hom_inv_id_app X + +@[reassoc (attr := simp)] +lemma eTruncLTLTIsoLT_inv_hom_id_app (X : C) : + (t.eTruncLTLTIsoLT a b hab).inv.app X ≫ + (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X) = 𝟙 _ := by + simpa using (t.eTruncLTLTIsoLT a b hab).inv_hom_id_app X + +@[reassoc (attr := simp)] +lemma eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj (X : C) : + (t.eTruncLTLTIsoLT a b hab).inv.app ((t.eTruncLT.obj a).obj X) ≫ + (t.eTruncLT.obj b).map ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X)) = 𝟙 _ := by + simp [eTruncLT_obj_map_eTruncLTι_app] + +end + + +section + +variable (a b : EInt) + +/-- The natural transformation from +`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b` to +`t.eTruncGE.obj a ⋙ t.eTruncLT.obj b`. (This is an isomorphism.) -/ +@[simps!] +noncomputable def eTruncLTGELTSelfToLTGE : + t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ⟶ + t.eTruncGE.obj a ⋙ t.eTruncLT.obj b := + Functor.whiskerRight (t.eTruncLTι b) _ ≫ (Functor.leftUnitor _).hom + +/-- The natural transformation from +`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b` to +`t.eTruncLT.obj b ⋙ t.eTruncGE.obj a`. (This is an isomorphism.) -/ +@[simps!] +noncomputable def eTruncLTGELTSelfToGELT : + t.eTruncLT.obj b ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ⟶ + t.eTruncLT.obj b ⋙ t.eTruncGE.obj a := + (Functor.associator _ _ _).inv ≫ Functor.whiskerLeft _ (t.eTruncLTι b) ≫ + (Functor.rightUnitor _).hom + +instance : IsIso (t.eTruncLTGELTSelfToLTGE a b) := by + rw [NatTrans.isIso_iff_isIso_app] + intro X + induction b using WithBotTop.rec with + | bot => simp [isIsoZero_iff_source_target_isZero] + | coe b => + induction a using WithBotTop.rec with + | bot => simpa using inferInstanceAs (IsIso ((t.truncLT b).map ((t.truncLTι b).app X))) + | coe a => + simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app, + eTruncLT_map_eq_truncLTι] + infer_instance + | top => + simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app, + eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero] + constructor + all_goals exact Functor.map_isZero _ (Functor.zero_obj _) + | top => simpa using inferInstanceAs (IsIso (𝟙 _)) + +variable (b : EInt) (X : C) + +instance : IsIso (t.eTruncLTGELTSelfToGELT a b) := by + rw [NatTrans.isIso_iff_isIso_app] + intro X + induction a using WithBotTop.rec with + | bot => simpa using inferInstanceAs (IsIso ((t.eTruncLTι b).app ((t.eTruncLT.obj b).obj X))) + | coe a => + induction b using WithBotTop.rec with + | bot => simpa [isIsoZero_iff_source_target_isZero] using + (t.eTruncGE.obj a).map_isZero (Functor.zero_obj _) + | coe b => + simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToGELT_app, + eTruncLT_map_eq_truncLTι] + infer_instance + | top => simpa using inferInstanceAs (IsIso (𝟙 _)) + | top => + exact ⟨0, ((t.eTruncLT.obj b).map_isZero (by simp)).eq_of_src _ _, + IsZero.eq_of_src (by simp) _ _⟩ + +end + +/-- The commutation natural isomorphism +`t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ≅ t.eTruncLT.obj b ⋙ t.eTruncGE.obj a` +for all `a` and `b` in `EInt`. -/ +noncomputable def eTruncLTGEIsoLEGT (a b : EInt) : + t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ≅ t.eTruncLT.obj b ⋙ t.eTruncGE.obj a := + (asIso (t.eTruncLTGELTSelfToLTGE a b)).symm ≪≫ asIso (t.eTruncLTGELTSelfToGELT a b) + +@[reassoc (attr := simp)] +lemma eTruncLTGEIsoLEGT_hom_naturality (a b : EInt) {X Y : C} (f : X ⟶ Y) : + (t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map f) ≫ (t.eTruncLTGEIsoLEGT a b).hom.app Y = + (t.eTruncLTGEIsoLEGT a b).hom.app X ≫ (t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map f) := + (t.eTruncLTGEIsoLEGT a b).hom.naturality f + +@[reassoc] +lemma eTruncLTGEIsoLEGT_hom_app_fac (a b : EInt) (X : C) : + (t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)) ≫ + (t.eTruncLTGEIsoLEGT a b).hom.app X = + (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X)):= by + simp [eTruncLTGEIsoLEGT] + +@[reassoc (attr := simp)] +lemma eTruncLTGEIsoLEGT_hom_app_fac' (a b : EInt) (X : C) : + (t.eTruncLTGEIsoLEGT a b).hom.app X ≫ (t.eTruncGE.obj a).map ((t.eTruncLTι b).app X) = + (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj X) := by + simp [eTruncLTGEIsoLEGT] + +open ComposableArrows in +@[reassoc] +lemma eTruncLTGEIsoLEGT_naturality_app (a b : EInt) (hab : a ≤ b) + (a' b' : EInt) (hab' : a' ≤ b') (φ : mk₁ (homOfLE hab) ⟶ mk₁ (homOfLE hab')) (X : C) : + (t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj X) ≫ + (t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app X) ≫ + (t.eTruncLTGEIsoLEGT a' b').hom.app X = + (t.eTruncLTGEIsoLEGT a b).hom.app X ≫ (t.eTruncGE.map (φ.app 0)).app _ ≫ + (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X) := by + rw [← cancel_epi ((t.eTruncLTGELTSelfToLTGE a b).app X)] + dsimp + rw [eTruncLTGELTSelfToLTGE_app, eTruncLTGEIsoLEGT_hom_app_fac_assoc, + NatTrans.naturality_assoc, ← Functor.map_comp_assoc, NatTrans.naturality, + Functor.map_comp_assoc, ← t.eTruncLT_map_app_eTruncLTι_app (φ.app 1) X, + Functor.map_comp, Functor.map_comp, Category.assoc, + t.eTruncLTGEIsoLEGT_hom_app_fac] + simp + +end + end TStructure end Triangulated