Loogle!

Result

Found 55 declarations mentioning CategoryTheory.Triangulated.TStructure.truncLE.

• CategoryTheory.Triangulated.TStructure.truncLE 📋 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 : ℤ) : CategoryTheory.Functor C C
• CategoryTheory.Triangulated.TStructure.instAdditiveTruncLE 📋 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 : ℤ) : (t.truncLE n).Additive
• CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLE 📋 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.IsLE ((t.truncLE n).obj X) n
• CategoryTheory.Triangulated.TStructure.isLE_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) (X : C) (a b : ℤ) (hn : a ≤ b := by lia) : t.IsLE ((t.truncLE a).obj X) b
• CategoryTheory.Triangulated.TStructure.truncLEι 📋 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 : ℤ) : t.truncLE n ⟶ CategoryTheory.Functor.id C
• CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLE_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) (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncLE a).obj X) b
• CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_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 : ℤ) (j : C) : ((t.triangleLEGT n).obj j).obj₁ = (t.truncLE n).obj j
• CategoryTheory.Triangulated.TStructure.liftTruncLE 📋 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 : ℤ) [t.IsLE X n] : X ⟶ (t.truncLE n).obj Y
• 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.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.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.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.natTransTruncLEOfLE 📋 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 ≤ b) : t.truncLE a ⟶ t.truncLE b
• CategoryTheory.Triangulated.TStructure.truncGTδLE 📋 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 : ℤ) : t.truncGT n ⟶ (t.truncLE n).comp (CategoryTheory.shiftFunctor C 1)
• CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_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) (a b : ℤ) (h : a + 1 = b) (j : C) : ((t.triangleLEGE a b h).obj j).obj₁ = (t.truncLE a).obj j
• CategoryTheory.Triangulated.TStructure.instIsIsoAppTruncLEιOfIsLE 📋 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) (n : ℤ) [t.IsLE X n] : CategoryTheory.IsIso ((t.truncLEι n).app X)
• CategoryTheory.Triangulated.TStructure.isLE_iff_isIso_truncLEι_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 : ℤ) (X : C) : t.IsLE X n ↔ CategoryTheory.IsIso ((t.truncLEι n).app X)
• CategoryTheory.Triangulated.TStructure.truncGEδLE 📋 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.truncGE b ⟶ (t.truncLE a).comp (CategoryTheory.shiftFunctor C 1)
• CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_refl 📋 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 : ℤ) : t.natTransTruncLEOfLE a a ⋯ = CategoryTheory.CategoryStruct.id (t.truncLE a)
• CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_mor₁ 📋 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 : ℤ) (j : C) : ((t.triangleLEGT n).obj j).mor₁ = (t.truncLEι n).app j
• CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_refl_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 : ℤ) (X : C) : (t.natTransTruncLEOfLE a a ⋯).app X = CategoryTheory.CategoryStruct.id ((t.truncLE a).obj X)
• CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_mor₁ 📋 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) (j : C) : ((t.triangleLEGE a b h).obj j).mor₁ = (t.truncLEι a).app j
• CategoryTheory.Triangulated.TStructure.liftTruncLE_ι 📋 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 : ℤ) [t.IsLE X n] : CategoryTheory.CategoryStruct.comp (t.liftTruncLE f n) ((t.truncLEι n).app Y) = f
• CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι 📋 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 ≤ b) : CategoryTheory.CategoryStruct.comp (t.natTransTruncLEOfLE a b h) (t.truncLEι b) = t.truncLEι a
• CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncLEAppTruncLEι 📋 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) (n : ℤ) : CategoryTheory.IsIso ((t.truncLE n).map ((t.truncLEι n).app X))
• CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_mor₃ 📋 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 : ℤ) (j : C) : ((t.triangleLEGT n).obj j).mor₃ = (t.truncGTδLE n).app j
• 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.isIso_truncLE_map_truncLEι_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) [CategoryTheory.IsTriangulated C] (a b : ℤ) (h : a ≤ b) (X : C) : CategoryTheory.IsIso ((t.truncLE a).map ((t.truncLEι b).app X))
• CategoryTheory.Triangulated.TStructure.liftTruncLE_ι_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 : ℤ) [t.IsLE X n] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.liftTruncLE f n) (CategoryTheory.CategoryStruct.comp ((t.truncLEι n).app Y) h) = CategoryTheory.CategoryStruct.comp f h
• CategoryTheory.Triangulated.TStructure.liftTruncLE_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 : ℤ) [t.IsLE X n] : ∃ f', f = CategoryTheory.CategoryStruct.comp f' ((t.truncLEι n).app Y)
• CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_trans 📋 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 c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) : CategoryTheory.CategoryStruct.comp (t.natTransTruncLEOfLE a b hab) (t.natTransTruncLEOfLE b c hbc) = t.natTransTruncLEOfLE a c ⋯
• 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.triangleLEGE_obj_mor₃ 📋 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) (j : C) : ((t.triangleLEGE a b h).obj j).mor₃ = (t.truncGEδLE a b h).app j
• CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι_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₁ : ℤ) (h : n₀ ≤ n₁) (X : C) : CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE n₀ n₁ h).app X) ((t.truncLEι n₁).app X) = (t.truncLEι n₀).app X
• CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι_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 ≤ b) {Z : CategoryTheory.Functor C C} (h✝ : CategoryTheory.Functor.id C ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.natTransTruncLEOfLE a b h) (CategoryTheory.CategoryStruct.comp (t.truncLEι b) h✝) = CategoryTheory.CategoryStruct.comp (t.truncLEι a) h✝
• CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι_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) (n₀ n₁ : ℤ) (h : n₀ ≤ n₁) (X : C) {Z : C} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE n₀ n₁ h).app X) (CategoryTheory.CategoryStruct.comp ((t.truncLEι n₁).app X) h✝) = CategoryTheory.CategoryStruct.comp ((t.truncLEι n₀).app X) h✝
• 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.natTransTruncLEOfLE_trans_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 c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C) : CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE a b hab).app X) ((t.natTransTruncLEOfLE b c hbc).app X) = (t.natTransTruncLEOfLE a c ⋯).app X
• CategoryTheory.Triangulated.TStructure.to_truncLE_obj_ext 📋 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 : ℤ} {Y X : C} {f₁ f₂ : Y ⟶ (t.truncLE n).obj X} (h : CategoryTheory.CategoryStruct.comp f₁ ((t.truncLEι n).app X) = CategoryTheory.CategoryStruct.comp f₂ ((t.truncLEι n).app X)) [t.IsLE Y n] : f₁ = f₂
• 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.natTransTruncLEOfLE_trans_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 c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C) {Z : C} (h : (t.truncLE c).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE a b hab).app X) (CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE b c hbc).app X) h) = CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE a c ⋯).app X) h
• CategoryTheory.Triangulated.TStructure.triangleLEGT_map_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) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGT n).map φ).hom₂ = φ
• CategoryTheory.Triangulated.TStructure.triangleLEGE_map_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) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGE a b h).map φ).hom₂ = φ
• CategoryTheory.Triangulated.TStructure.triangleLEGT_map_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) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGT n).map φ).hom₁ = (t.truncLE n).map φ
• CategoryTheory.Triangulated.TStructure.triangleLEGT_map_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) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGT n).map φ).hom₃ = (t.truncGT n).map φ
• 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.Triangulated.TStructure.triangleLEGE_map_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) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGE a b h).map φ).hom₁ = (t.truncLE a).map φ
• CategoryTheory.Triangulated.TStructure.triangleLEGE_map_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) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGE a b h).map φ).hom₃ = (t.truncGE b).map φ
• 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} [P.IsTriangulated] {t : CategoryTheory.Triangulated.TStructure C} (h : ∀ (X : C), P X → ∀ (n : ℤ), P ((t.truncLE n).obj X) ∧ P ((t.truncGE n).obj X)) : P.HasInducedTStructure t

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