Loogle!

Result

Found 66 declarations mentioning CategoryTheory.Triangulated.TStructure.IsGE.

• CategoryTheory.Triangulated.TStructure.IsGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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) (X : C) (n : ℤ) : Prop
• CategoryTheory.Triangulated.TStructure.ge_of_isGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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) (X : C) (n : ℤ) [t.IsGE X n] : t.ge n X
• CategoryTheory.Triangulated.TStructure.IsGE.ge 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.HasShift C ℤ} {inst✝⁴ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst✝⁵ : CategoryTheory.Pretriangulated C} {t : CategoryTheory.Triangulated.TStructure C} {X : C} {n : ℤ} [self : t.IsGE X n] : t.ge n X
• CategoryTheory.Triangulated.TStructure.IsGE.mk 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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} {X : C} {n : ℤ} (ge : t.ge n X) : t.IsGE X n
• CategoryTheory.Triangulated.TStructure.ge_iff_isGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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) (X : C) (n : ℤ) : t.ge n X ↔ t.IsGE X n
• CategoryTheory.Triangulated.TStructure.isGE_of_iso 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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) {X Y : C} (e : X ≅ Y) (n : ℤ) [t.IsGE X n] : t.IsGE Y n
• CategoryTheory.Triangulated.TStructure.isGE_of_ge 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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) (X : C) (p q : ℤ) (hpq : p ≤ q := by lia) [t.IsGE X q] : t.IsGE X p
• CategoryTheory.Triangulated.TStructure.isZero 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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) (X : C) (n₀ n₁ : ℤ) (h : n₀ < n₁ := by lia) [t.IsLE X n₀] [t.IsGE X n₁] : CategoryTheory.Limits.IsZero X
• CategoryTheory.Triangulated.TStructure.isGE_of_shift 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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) (X : C) (n a n' : ℤ) (hn' : a + n' = n := by lia) [t.IsGE ((CategoryTheory.shiftFunctor C a).obj X) n'] : t.IsGE X n
• CategoryTheory.Triangulated.TStructure.isGE_shift 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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) (X : C) (n a n' : ℤ) (hn' : a + n' = n := by lia) [t.IsGE X n] : t.IsGE ((CategoryTheory.shiftFunctor C a).obj X) n'
• CategoryTheory.Triangulated.TStructure.isGE_shift_iff 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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) (X : C) (n a n' : ℤ) (hn' : a + n' = n := by lia) : t.IsGE ((CategoryTheory.shiftFunctor C a).obj X) n' ↔ t.IsGE X n
• CategoryTheory.Triangulated.TStructure.zero_of_isLE_of_isGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ < n₁) : t.IsLE X n₀ → t.IsGE Y n₁ → f = 0
• CategoryTheory.Triangulated.TStructure.zero 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Basic
  {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) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ < n₁ := by lia) [t.IsLE X n₀] [t.IsGE Y n₁] : f = 0
• CategoryTheory.Triangulated.TStructure.isGE_of_isZero 📋 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} (hX : CategoryTheory.Limits.IsZero X) (n : ℤ) : t.IsGE X n
• CategoryTheory.Triangulated.TStructure.instIsGEOfNat 📋 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.IsGE 0 n
• CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGE 📋 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.IsGE ((t.truncGE n).obj X) n
• CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGELT 📋 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.IsGE ((t.truncGELT a b).obj X) a
• 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.isGE_truncGE_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 : b ≤ a := by lia) : t.IsGE ((t.truncGE a).obj X) b
• CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLTGE 📋 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 ((t.truncLTGE a b).obj X) a
• CategoryTheory.Triangulated.TStructure.instIsGEObj₃ObjTriangleTriangleLTGE 📋 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.IsGE ((t.triangleLTGE n).obj X).obj₃ n
• CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGE_1 📋 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.IsGE X a] : t.IsGE ((t.truncGE b).obj X) a
• CategoryTheory.Triangulated.TStructure.descTruncGE 📋 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 : ℤ) [t.IsGE Y n] : (t.truncGE n).obj X ⟶ Y
• 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.instIsIsoAppTruncGEπOfIsGE 📋 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.IsGE X n] : CategoryTheory.IsIso ((t.truncGEπ n).app X)
• CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_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) : t.IsGE X n ↔ CategoryTheory.IsIso ((t.truncGEπ n).app X)
• CategoryTheory.Triangulated.TStructure.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) (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n : ℤ) (h₁ : t.IsGE T.obj₁ n) (h₃ : t.IsGE T.obj₃ n) : t.IsGE T.obj₂ n
• CategoryTheory.Triangulated.TStructure.isGE_iff_orthogonal 📋 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.IsGE X n₁ ↔ ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
• CategoryTheory.Triangulated.TStructure.isLE_iff_orthogonal 📋 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₀ ↔ ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0
• CategoryTheory.Triangulated.TStructure.π_descTruncGE 📋 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 : ℤ) [t.IsGE Y n] : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) (t.descTruncGE f n) = f
• 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.π_descTruncGE_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 : ℤ) [t.IsGE Y n] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) (CategoryTheory.CategoryStruct.comp (t.descTruncGE f n) h) = CategoryTheory.CategoryStruct.comp f h
• CategoryTheory.Triangulated.TStructure.descTruncGE_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 : ℤ) [t.IsGE Y n] : ∃ f', f = CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) f'
• CategoryTheory.Triangulated.TStructure.triangle_map_exists 📋 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) {T T' : CategoryTheory.Pretriangulated.Triangle C} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (φ : T.obj₂ ⟶ T'.obj₂) (a b : ℤ) (h₀ : t.IsLE T.obj₁ a) (h₁' : t.IsGE T'.obj₃ b) (h : a < b := by lia) : ∃ f, f.hom₂ = φ
• CategoryTheory.Triangulated.TStructure.triangle_map_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) {T T' : CategoryTheory.Pretriangulated.Triangle C} {f₁ f₂ : T ⟶ T'} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (a b : ℤ) (h₀ : t.IsLE T.obj₁ a) (h₁ : t.IsGE T'.obj₃ b) (H : f₁.hom₂ = f₂.hom₂ := by cat_disch) (hab : a ≤ b := by lia) : f₁ = f₂
• CategoryTheory.Triangulated.TStructure.triangle_iso_exists 📋 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) {T T' : CategoryTheory.Pretriangulated.Triangle C} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (hT' : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (e : T.obj₂ ≅ T'.obj₂) (a b : ℤ) (h₀ : t.IsLE T.obj₁ a) (h₁ : t.IsGE T.obj₃ b) (h₀' : t.IsLE T'.obj₁ a) (h₁' : t.IsGE T'.obj₃ b) (h : a < b := by lia) : ∃ e', e'.hom.hom₂ = e.hom
• CategoryTheory.Triangulated.TStructure.from_truncGE_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 : ℤ} {X Y : C} {f₁ f₂ : (t.truncGE n).obj X ⟶ Y} (h : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) f₁ = CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) f₂) [t.IsGE Y n] : f₁ = f₂
• 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.instIsGEObjTruncGELE 📋 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) (X : C) (a b : ℤ) : t.IsGE ((t.truncGELE a b).obj X) a
• CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGT 📋 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) (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncGT b).obj X) a
• CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGTHAddIntOfNat 📋 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) (n : ℤ) (X : C) : t.IsGE ((t.truncGT n).obj X) (n + 1)
• CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGTHSubIntOfNat 📋 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) (n : ℤ) (X : C) : t.IsGE ((t.truncGT (n - 1)).obj X) n
• CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLE 📋 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) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncLE b).obj X) a
• CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLE_1 📋 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) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncLE b).obj X) a
• CategoryTheory.Triangulated.TStructure.isGE_truncGT_obj 📋 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) (X : C) (a b : ℤ) (hn : b ≤ a + 1 := by lia) : t.IsGE ((t.truncGT a).obj X) b
• CategoryTheory.Triangulated.TStructure.isZero_truncLE_obj_of_isGE 📋 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) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) [t.IsGE X n₁] : CategoryTheory.Limits.IsZero ((t.truncLE n₀).obj X)
• CategoryTheory.Triangulated.TStructure.isGE_iff_isZero_truncLE_obj 📋 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) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : t.IsGE X n₁ ↔ CategoryTheory.Limits.IsZero ((t.truncLE n₀).obj X)
• CategoryTheory.Triangulated.TStructure.descTruncGT 📋 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) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsGE Y n₁] : (t.truncGT n₀).obj X ⟶ Y
• CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_truncGTπ_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) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) (X : C) : t.IsGE X n₁ ↔ CategoryTheory.IsIso ((t.truncGTπ n₀).app X)
• CategoryTheory.Triangulated.TStructure.π_descTruncGT 📋 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) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsGE Y n₁] : CategoryTheory.CategoryStruct.comp ((t.truncGTπ n₀).app X) (t.descTruncGT f n₀ n₁ h) = f
• CategoryTheory.Triangulated.TStructure.isIso₁_truncLE_map_of_isGE 📋 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) [CategoryTheory.IsTriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (h₃ : t.IsGE T.obj₃ n₁) : CategoryTheory.IsIso ((t.truncLE n₀).map T.mor₁)
• CategoryTheory.Triangulated.TStructure.descTruncGT_aux 📋 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) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsGE Y n₁] : ∃ f', f = CategoryTheory.CategoryStruct.comp ((t.truncGTπ n₀).app X) f'
• CategoryTheory.Triangulated.TStructure.π_descTruncGT_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) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) [t.IsGE Y n₁] {Z : C} (h✝ : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGTπ n₀).app X) (CategoryTheory.CategoryStruct.comp (t.descTruncGT f n₀ n₁ h) h✝) = CategoryTheory.CategoryStruct.comp f h✝
• CategoryTheory.Triangulated.TStructure.isIso_truncLE_map_iff 📋 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) {X Y : C} (f : X ⟶ Y) (a b : ℤ) (h : a + 1 = b) : CategoryTheory.IsIso ((t.truncLE a).map f) ↔ ∃ Z g h, ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk (CategoryTheory.CategoryStruct.comp ((t.truncLEι a).app X) f) g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), t.IsGE Z b
• CategoryTheory.ObjectProperty.mem_of_hasInductedTStructure 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Induced
  {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] (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] (t : CategoryTheory.Triangulated.TStructure C) [P.IsClosedUnderIsomorphisms] [P.HasInducedTStructure t] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (h₁ : t.IsLE T.obj₁ n₀) (h₂ : P T.obj₂) (h₃ : t.IsGE T.obj₃ n₁) : P T.obj₁ ∧ P T.obj₃
• CategoryTheory.ObjectProperty.tStructure_isGE_iff 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Induced
  {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] (P : CategoryTheory.ObjectProperty C) (t : CategoryTheory.Triangulated.TStructure C) [P.IsTriangulated] [h : P.HasInducedTStructure t] (X : P.FullSubcategory) (n : ℤ) : (P.tStructure t).IsGE X n ↔ t.IsGE X.obj n
• CategoryTheory.ObjectProperty.HasInducedTStructure.exists_triangle_zero_one 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Induced
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.HasShift C ℤ} {inst✝⁴ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst✝⁵ : CategoryTheory.Pretriangulated C} {P : CategoryTheory.ObjectProperty C} {t : CategoryTheory.Triangulated.TStructure C} {inst✝⁶ : P.IsTriangulated} [self : P.HasInducedTStructure t] (A : C) (hA : P A) : ∃ X Y, ∃ (_ : t.IsLE X 0) (_ : t.IsGE Y 1), ∃ f g h, ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), P.isoClosure X ∧ P.isoClosure Y
• CategoryTheory.ObjectProperty.HasInducedTStructure.mk 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Induced
  {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] {P : CategoryTheory.ObjectProperty C} {t : CategoryTheory.Triangulated.TStructure C} [P.IsTriangulated] (exists_triangle_zero_one : ∀ (A : C), P A → ∃ X Y, ∃ (_ : t.IsLE X 0) (_ : t.IsGE Y 1), ∃ f g h, ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), P.isoClosure X ∧ P.isoClosure Y) : P.HasInducedTStructure t
• CategoryTheory.ObjectProperty.hasInducedTStructure_iff 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Induced
  {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] (P : CategoryTheory.ObjectProperty C) (t : CategoryTheory.Triangulated.TStructure C) [P.IsTriangulated] : P.HasInducedTStructure t ↔ ∀ (A : C), P A → ∃ X Y, ∃ (_ : t.IsLE X 0) (_ : t.IsGE Y 1), ∃ f g h, ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), P.isoClosure X ∧ P.isoClosure Y
• CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncGE 📋 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) (X : C) (n : ℤ) [t.IsGE X n] (i : EInt) : t.IsGE ((t.eTruncGE.obj i).obj X) n
• CategoryTheory.Triangulated.TStructure.isGE_eTruncGE_obj_obj 📋 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 : ℤ) (i : EInt) (h : WithBotTop.coe n ≤ i) (X : C) : t.IsGE ((t.eTruncGE.obj i).obj X) n
• CategoryTheory.Triangulated.TStructure.isZero_eTruncLT_obj_obj 📋 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) (X : C) (n : ℤ) [t.IsGE X n] (j : EInt) (hj : j ≤ WithBotTop.coe n) : CategoryTheory.Limits.IsZero ((t.eTruncLT.obj j).obj X)
• CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncLT 📋 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) [CategoryTheory.IsTriangulated C] (X : C) (n : ℤ) [t.IsGE X n] (i : EInt) : t.IsGE ((t.eTruncLT.obj i).obj X) n
• CategoryTheory.Triangulated.TStructure.mem_heart_iff 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Heart
  {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) : t.heart X ↔ t.IsLE X 0 ∧ t.IsGE X 0
• CategoryTheory.Triangulated.TStructure.instIsGEObjιHeartOfNatInt 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Heart
  {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) (H : Type u') [CategoryTheory.Category.{v', u'} H] [CategoryTheory.Preadditive H] [t.Heart H] (X : H) : t.IsGE (t.ιHeart.obj X) 0

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 ce5dd8c