Loogle!

Result

Found 82 declarations mentioning CategoryTheory.Triangulated.TStructure.truncLT.

• CategoryTheory.Triangulated.TStructure.truncLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : CategoryTheory.Functor C C
• CategoryTheory.Triangulated.TStructure.instAdditiveTruncLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : (t.truncLT n).Additive
• CategoryTheory.Triangulated.TStructure.isZero_truncLT_obj_of_isGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) [t.IsGE X n] : CategoryTheory.Limits.IsZero ((t.truncLT n).obj X)
• CategoryTheory.Triangulated.TStructure.isGE_iff_isZero_truncLT_obj 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) : t.IsGE X n ↔ CategoryTheory.Limits.IsZero ((t.truncLT n).obj X)
• CategoryTheory.Triangulated.TStructure.truncLTι 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : t.truncLT n ⟶ CategoryTheory.Functor.id C
• CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncLT a).obj X) b
• CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLTHAddIntOfNat 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ) : t.IsLE ((t.truncLT (n + 1)).obj X) n
• CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLTHSubIntOfNat 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ) : t.IsLE ((t.truncLT n).obj X) (n - 1)
• CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).obj₁ = (t.truncLT n).obj j
• CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncLT b).obj X) a
• CategoryTheory.Triangulated.TStructure.isLE_truncLT_obj 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (X : C) (a b : ℤ) (hn : a ≤ b + 1 := by lia) : t.IsLE ((t.truncLT a).obj X) b
• CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) : t.truncLT a ⟶ t.truncLT b
• CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).obj₁ = (t.truncLT a).obj j
• CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).obj₂ = (t.truncLT b).obj j
• CategoryTheory.Triangulated.TStructure.truncGEδLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : t.truncGE n ⟶ (t.truncLT n).comp (CategoryTheory.shiftFunctor C 1)
• CategoryTheory.Triangulated.TStructure.liftTruncLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsLE X n₀] : X ⟶ (t.truncLT n₁).obj Y
• CategoryTheory.Triangulated.TStructure.truncGELTδLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) : t.truncGELT a b ⟶ (t.truncLT a).comp (CategoryTheory.shiftFunctor C 1)
• CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).obj₃ = (t.truncGE a).obj ((t.truncLT b).obj j)
• CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_refl 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a : ℤ) : t.natTransTruncLTOfLE a a ⋯ = CategoryTheory.CategoryStruct.id (t.truncLT a)
• CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLTι_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : t.IsLE X n₀ ↔ CategoryTheory.IsIso ((t.truncLTι n₁).app X)
• CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).mor₁ = (t.truncLTι n).app j
• CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_refl_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a : ℤ) (X : C) : (t.natTransTruncLTOfLE a a ⋯).app X = CategoryTheory.CategoryStruct.id ((t.truncLT a).obj X)
• CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).mor₁ = (t.natTransTruncLTOfLE a b h).app j
• CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) : CategoryTheory.CategoryStruct.comp (t.natTransTruncLTOfLE a b h) (t.truncLTι b) = t.truncLTι a
• CategoryTheory.Triangulated.TStructure.isIso₁_truncLT_map_of_isGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n : ℤ) (h₃ : t.IsGE T.obj₃ n) : CategoryTheory.IsIso ((t.truncLT n).map T.mor₁)
• CategoryTheory.Triangulated.TStructure.liftTruncLT_ι 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsLE X n₀] : CategoryTheory.CategoryStruct.comp (t.liftTruncLT f n₀ n₁ h) ((t.truncLTι n₁).app Y) = f
• CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncLTAppTruncLTι 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (n : ℤ) : CategoryTheory.IsIso ((t.truncLT n).map ((t.truncLTι n).app X))
• CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).mor₂ = (t.truncGEπ a).app ((t.truncLT b).obj j)
• CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).mor₃ = (t.truncGEδLT n).app j
• CategoryTheory.Triangulated.TStructure.isIso_truncLT_map_truncLTι_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (h : a ≤ b) (X : C) : CategoryTheory.IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
• CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_trans 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) : CategoryTheory.CategoryStruct.comp (t.natTransTruncLTOfLE a b hab) (t.natTransTruncLTOfLE b c hbc) = t.natTransTruncLTOfLE a c ⋯
• CategoryTheory.Triangulated.TStructure.instIsIsoAppTruncLTιObjTruncGETruncLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) : CategoryTheory.IsIso ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))
• CategoryTheory.Triangulated.TStructure.liftTruncLT_aux 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsLE X n₀] : ∃ f', f = CategoryTheory.CategoryStruct.comp f' ((t.truncLTι n₁).app Y)
• CategoryTheory.Triangulated.TStructure.liftTruncLT_ι_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsLE X n₀] {Z : C} (h✝ : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.liftTruncLT f n₀ n₁ h) (CategoryTheory.CategoryStruct.comp ((t.truncLTι n₁).app Y) h✝) = CategoryTheory.CategoryStruct.comp f h✝
• CategoryTheory.Triangulated.TStructure.truncLT_map_truncLTι_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) : (t.truncLT n).map ((t.truncLTι n).app X) = (t.truncLTι n).app ((t.truncLT n).obj X)
• CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) : CategoryTheory.CategoryStruct.comp ((t.natTransTruncLTOfLE a b h).app X) ((t.truncLTι b).app X) = (t.truncLTι a).app X
• CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {Z : CategoryTheory.Functor C C} (h✝ : CategoryTheory.Functor.id C ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.natTransTruncLTOfLE a b h) (CategoryTheory.CategoryStruct.comp (t.truncLTι b) h✝) = CategoryTheory.CategoryStruct.comp (t.truncLTι a) h✝
• CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : CategoryTheory.CategoryStruct.comp (t.truncLTι n) (t.truncGEπ n) = 0
• CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) {Z : C} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.natTransTruncLTOfLE a b h).app X) (CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) h✝) = CategoryTheory.CategoryStruct.comp ((t.truncLTι a).app X) h✝
• CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_trans_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C) : CategoryTheory.CategoryStruct.comp ((t.natTransTruncLTOfLE a b hab).app X) ((t.natTransTruncLTOfLE b c hbc).app X) = (t.natTransTruncLTOfLE a c ⋯).app X
• CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncLTTruncGEAppTruncLTι 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) : CategoryTheory.IsIso ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X)))
• CategoryTheory.Triangulated.TStructure.to_truncLT_obj_ext 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {n : ℤ} {Y X : C} {f₁ f₂ : Y ⟶ (t.truncLT n).obj X} (h : CategoryTheory.CategoryStruct.comp f₁ ((t.truncLTι n).app X) = CategoryTheory.CategoryStruct.comp f₂ ((t.truncLTι n).app X)) [t.IsLE Y (n - 1)] : f₁ = f₂
• CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncLTι n).app X) ((t.truncGEπ n).app X) = 0
• CategoryTheory.Triangulated.TStructure.truncLT_map_truncLTι_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) {Z : C} (h : (t.truncLT n).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncLT n).map ((t.truncLTι n).app X)) h = CategoryTheory.CategoryStruct.comp ((t.truncLTι n).app ((t.truncLT n).obj X)) h
• CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : CategoryTheory.CategoryStruct.comp (t.truncGEπ n) (t.truncGEδLT n) = 0
• CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) : CategoryTheory.CategoryStruct.comp (t.truncGEδLT a) (CategoryTheory.Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (CategoryTheory.shiftFunctor C 1)) = CategoryTheory.CategoryStruct.comp (t.natTransTruncGEOfLE a b h) (t.truncGEδLT b)
• CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {Z : CategoryTheory.Functor C C} (h : t.truncGE n ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncLTι n) (CategoryTheory.CategoryStruct.comp (t.truncGEπ n) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) {Z : C} (h : (t.truncGE n).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncLTι n).app X) (CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : CategoryTheory.CategoryStruct.comp (t.truncGEδLT n) (CategoryTheory.Functor.whiskerRight (t.truncLTι n) (CategoryTheory.shiftFunctor C 1)) = 0
• CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) ((t.truncGEδLT n).app X) = 0
• CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTGE n).map φ).hom₂ = φ
• CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {Z : CategoryTheory.Functor C C} (h : (t.truncLT n).comp (CategoryTheory.shiftFunctor C 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncGEπ n) (CategoryTheory.CategoryStruct.comp (t.truncGEδLT n) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Triangulated.TStructure.isIso_truncLT_map_iff 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) : CategoryTheory.IsIso ((t.truncLT n).map f) ↔ ∃ Z g h, ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk (CategoryTheory.CategoryStruct.comp ((t.truncLTι n).app X) f) g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), t.IsGE Z n
• CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncGEδLT n).app X) ((CategoryTheory.shiftFunctor C 1).map ((t.truncLTι n).app X)) = 0
• CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {Z : CategoryTheory.Functor C C} (h✝ : (t.truncLT b).comp (CategoryTheory.shiftFunctor C 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncGEδLT a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (CategoryTheory.shiftFunctor C 1)) h✝) = CategoryTheory.CategoryStruct.comp (t.natTransTruncGEOfLE a b h) (CategoryTheory.CategoryStruct.comp (t.truncGEδLT b) h✝)
• CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj ((t.truncLT n).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) (CategoryTheory.CategoryStruct.comp ((t.truncGEδLT n).app X) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTGE n).map φ).hom₁ = (t.truncLT n).map φ
• CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTGE n).map φ).hom₃ = (t.truncGE n).map φ
• CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).mor₃ = CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app ((t.truncLT b).obj j)) ((CategoryTheory.shiftFunctor C 1).map ((t.truncLT a).map ((t.truncLTι b).app j)))
• CategoryTheory.Triangulated.TStructure.truncGELTδLT_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (X : C) : (t.truncGELTδLT a b).app X = CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app ((t.truncLT b).obj X)) ((CategoryTheory.shiftFunctor C 1).map ((t.truncLT a).map ((t.truncLTι b).app X)))
• CategoryTheory.Triangulated.TStructure.truncLT_map_truncGE_map_truncLTι_app_fac 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) : CategoryTheory.CategoryStruct.comp ((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))
• CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app X) ((CategoryTheory.shiftFunctor C 1).map ((t.natTransTruncLTOfLE a b h).app X)) = CategoryTheory.CategoryStruct.comp ((t.natTransTruncGEOfLE a b h).app X) ((t.truncGEδLT b).app X)
• CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {Z : CategoryTheory.Functor C C} (h : (CategoryTheory.Functor.id C).comp (CategoryTheory.shiftFunctor C 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncGEδLT n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (t.truncLTι n) (CategoryTheory.shiftFunctor C 1)) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X)) (CategoryTheory.CategoryStruct.comp ((t.truncGELTToLTGE a b).app X) ((t.truncLTι b).app ((t.truncGE a).obj X))) = CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) ((t.truncGEπ a).app X)
• CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEδLT n).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map ((t.truncLTι n).app X)) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) {Z : C} (h : (t.truncGE a).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X)) (CategoryTheory.CategoryStruct.comp ((t.truncGELTToLTGE a b).app X) (CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app ((t.truncGE a).obj X)) h)) = CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) (CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app X) h)
• CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) {Z : C} (h✝ : (CategoryTheory.shiftFunctor C 1).obj ((t.truncLT b).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map ((t.natTransTruncLTOfLE a b h).app X)) h✝) = CategoryTheory.CategoryStruct.comp ((t.natTransTruncGEOfLE a b h).app X) (CategoryTheory.CategoryStruct.comp ((t.truncGEδLT b).app X) h✝)
• CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon_uniqueness 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] {a b : ℤ} {X : C} (φ : (t.truncGELT a b).obj X ⟶ (t.truncLTGE a b).obj X) (hφ : CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X)) (CategoryTheory.CategoryStruct.comp φ ((t.truncLTι b).app ((t.truncGE a).obj X))) = CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) ((t.truncGEπ a).app X)) : (t.truncGELTToLTGE a b).app X = φ
• CategoryTheory.Triangulated.TStructure.truncLT_map_truncGE_map_truncLTι_app_fac_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) {Z : C} (h : (t.truncLT b).obj ((t.truncGE a).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) (CategoryTheory.CategoryStruct.comp ((t.truncGELTToLTGE a b).app X) h) = CategoryTheory.CategoryStruct.comp ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))) h
• CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTLTGELT a b h).map φ).hom₁ = (t.truncLT a).map φ
• CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTLTGELT a b h).map φ).hom₂ = (t.truncLT b).map φ
• CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTLTGELT a b h).map φ).hom₃ = (t.truncGE a).map ((t.truncLT b).map φ)
• CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) : t.truncLE a ≅ t.truncLT b
• CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) : CategoryTheory.CategoryStruct.comp (t.truncLEIsoTruncLT a b h).hom (t.truncLTι b) = t.truncLEι a
• CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) : CategoryTheory.CategoryStruct.comp (t.truncLEIsoTruncLT a b h).inv (t.truncLEι a) = t.truncLTι b
• CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).hom.app X) ((t.truncLTι b).app X) = (t.truncLEι a).app X
• CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).inv.app X) ((t.truncLEι a).app X) = (t.truncLTι b).app X
• CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {Z : CategoryTheory.Functor C C} (h✝ : CategoryTheory.Functor.id C ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncLEIsoTruncLT a b h).hom (CategoryTheory.CategoryStruct.comp (t.truncLTι b) h✝) = CategoryTheory.CategoryStruct.comp (t.truncLEι a) h✝
• CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {Z : CategoryTheory.Functor C C} (h✝ : CategoryTheory.Functor.id C ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncLEIsoTruncLT a b h).inv (CategoryTheory.CategoryStruct.comp (t.truncLEι a) h✝) = CategoryTheory.CategoryStruct.comp (t.truncLTι b) h✝
• CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).hom.app X) (CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) h✝) = CategoryTheory.CategoryStruct.comp ((t.truncLEι a).app X) h✝
• CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_inv_ι_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).inv.app X) (CategoryTheory.CategoryStruct.comp ((t.truncLEι a).app X) h✝) = CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) h✝
• CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe 📋 Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : t.eTruncLT.obj (WithBotTop.coe n) = t.truncLT n

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59