Loogle!

Result

Found 68 declarations mentioning CategoryTheory.Triangulated.TStructure.eTruncGE.

CategoryTheory.Triangulated.TStructure.eTruncGE 📋 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.Functor EInt (CategoryTheory.Functor C C)
CategoryTheory.Triangulated.TStructure.instAdditiveObjEIntFunctorETruncGE 📋 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) (i : EInt) : (t.eTruncGE.obj i).Additive
CategoryTheory.Triangulated.TStructure.eTruncGE_obj_bot 📋 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) : t.eTruncGE.obj ⊥ = CategoryTheory.Functor.id C
CategoryTheory.Triangulated.TStructure.eTruncGE_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.eTruncGE.obj (WithBotTop.coe n) = t.truncGE n
CategoryTheory.Triangulated.TStructure.eTruncGEπ 📋 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) (i : EInt) : CategoryTheory.Functor.id C ⟶ t.eTruncGE.obj i
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.instIsIsoFunctorETruncGEπBotEInt 📋 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.IsIso (t.eTruncGEπ ⊥)
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.instIsLEObjEIntFunctorETruncGE 📋 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.IsLE X n] (i : EInt) : t.IsLE ((t.eTruncGE.obj i).obj X) n
CategoryTheory.Triangulated.TStructure.isZero_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) (X : C) (n : ℤ) [t.IsLE X n] (j : EInt) (hj : WithBotTop.coe n < j) : CategoryTheory.Limits.IsZero ((t.eTruncGE.obj j).obj X)
CategoryTheory.Triangulated.TStructure.eTruncGE_obj_top 📋 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) : t.eTruncGE.obj ⊤ = 0
CategoryTheory.Triangulated.TStructure.eTruncGEπ_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.eTruncGEπ (WithBotTop.coe n) = t.truncGEπ n
CategoryTheory.Triangulated.TStructure.eTruncGEπ_bot 📋 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) : t.eTruncGEπ ⊥ = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.id C)
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_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) (i : EInt) (j : C) : ((t.eTriangleLTGE.obj i).obj j).obj₃ = (t.eTruncGE.obj i).obj j
CategoryTheory.Triangulated.TStructure.eTruncGEToGEGE 📋 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) (a b : EInt) : t.eTruncGE.obj b ⟶ (t.eTruncGE.obj a).comp (t.eTruncGE.obj b)
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE 📋 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] (a b : EInt) (hab : a ≤ b) : t.eTruncGE.obj b ≅ (t.eTruncGE.obj a).comp (t.eTruncGE.obj b)
CategoryTheory.Triangulated.TStructure.isIso_eTruncGEIsoGEGE 📋 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] (a b : EInt) (hab : a ≤ b) : CategoryTheory.IsIso (t.eTruncGEToGEGE a b)
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT 📋 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] (a b : EInt) : (t.eTruncGE.obj a).comp (t.eTruncLT.obj b) ≅ (t.eTruncLT.obj b).comp (t.eTruncGE.obj a)
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₂ 📋 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) (i : EInt) (j : C) : ((t.eTriangleLTGE.obj i).obj j).mor₂ = (t.eTruncGEπ i).app j
CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT 📋 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) (a b : EInt) : (t.eTruncLT.obj b).comp ((t.eTruncGE.obj a).comp (t.eTruncLT.obj b)) ⟶ (t.eTruncLT.obj b).comp (t.eTruncGE.obj a)
CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE 📋 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) (a b : EInt) : (t.eTruncLT.obj b).comp ((t.eTruncGE.obj a).comp (t.eTruncLT.obj b)) ⟶ (t.eTruncGE.obj a).comp (t.eTruncLT.obj b)
CategoryTheory.Triangulated.TStructure.eTruncGEδLT 📋 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) : t.eTruncGE ⟶ t.eTruncLT.comp ((CategoryTheory.Functor.whiskeringRight C C C).obj (CategoryTheory.shiftFunctor C 1))
CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToGELT 📋 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] (a b : EInt) : CategoryTheory.IsIso (t.eTruncLTGELTSelfToGELT a b)
CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToLTGE 📋 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] (a b : EInt) : CategoryTheory.IsIso (t.eTruncLTGELTSelfToLTGE a b)
CategoryTheory.Triangulated.TStructure.eTruncGEπ_top 📋 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) : t.eTruncGEπ ⊤ = 0
CategoryTheory.Triangulated.TStructure.isIso_eTruncGE_obj_map_truncGEπ_app 📋 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] (a b : EInt) (h : a ≤ b) (X : C) : CategoryTheory.IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom 📋 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] (a b : EInt) (hab : a ≤ b) : (t.eTruncGEIsoGEGE a b hab).hom = t.eTruncGEToGEGE a b
CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality 📋 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) (i : EInt) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app X) ((t.eTruncGE.obj i).map f) = CategoryTheory.CategoryStruct.comp f ((t.eTruncGEπ i).app Y)
CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_app 📋 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) (i : EInt) (X : C) : (t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X) = (t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)
CategoryTheory.Triangulated.TStructure.eTruncGEδLT_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.eTruncGEδLT.app (WithBotTop.coe n) = t.truncGEδLT n
CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_app 📋 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) {i j : EInt} (f : i ⟶ j) (X : C) : CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app X) ((t.eTruncGE.map f).app X) = (t.eTruncGEπ j).app X
CategoryTheory.Triangulated.TStructure.eTruncGEToGEGE_app 📋 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) (a b : EInt) (X : C) : (t.eTruncGEToGEGE a b).app X = (t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)
CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality_assoc 📋 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) (i : EInt) {X Y : C} (f : X ⟶ Y) {Z : C} (h : (t.eTruncGE.obj i).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app X) (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj i).map f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app Y) h)
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₃ 📋 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) (i : EInt) (j : C) : ((t.eTriangleLTGE.obj i).obj j).mor₃ = (t.eTruncGEδLT.app i).app j
CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_app_assoc 📋 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) {i j : EInt} (f : i ⟶ j) (X : C) {Z : C} (h : (t.eTruncGE.obj j).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app X) (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.map f).app X) h) = CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ j).app X) h
CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT_app 📋 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) (a b : EInt) (X : C) : (t.eTruncLTGELTSelfToGELT a b).app X = (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X))
CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_app_assoc 📋 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) (i : EInt) (X : C) {Z : C} (h : (t.eTruncGE.obj i).obj ((t.eTruncGE.obj i).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X)) h = CategoryTheory.CategoryStruct.comp ((t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)) h
CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE_app 📋 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) (a b : EInt) (X : C) : (t.eTruncLTGELTSelfToLTGE a b).app X = (t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X))
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_app 📋 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] (a b : EInt) (hab : a ≤ b) (X : C) : CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) ((t.eTruncGEIsoGEGE a b hab).inv.app X) = CategoryTheory.CategoryStruct.id ((t.eTruncGE.obj b).obj ((CategoryTheory.Functor.id C).obj X))
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_app_assoc 📋 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] (a b : EInt) (hab : a ≤ b) (X : C) {Z : C} (h : (t.eTruncGE.obj b).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) (CategoryTheory.CategoryStruct.comp ((t.eTruncGEIsoGEGE a b hab).inv.app X) h) = h
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_app_assoc 📋 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] (a b : EInt) (hab : a ≤ b) (X : C) {Z : C} (h : (t.eTruncGE.obj b).obj ((t.eTruncGE.obj a).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncGEIsoGEGE a b hab).inv.app X) (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) h) = h
CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_app 📋 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] (a b : EInt) (hab : a ≤ b) (X : C) : CategoryTheory.CategoryStruct.comp ((t.eTruncGEIsoGEGE a b hab).inv.app X) ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)) = CategoryTheory.CategoryStruct.id (((t.eTruncGE.obj a).comp (t.eTruncGE.obj b)).obj X)
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac' 📋 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] (a b : EInt) (X : C) : CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)) = (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj X)
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₂ 📋 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) (i : EInt) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.eTriangleLTGE.obj i).map φ).hom₂ = φ
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac'_assoc 📋 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] (a b : EInt) (X : C) {Z : C} (h : (t.eTruncGE.obj a).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)) h) = CategoryTheory.CategoryStruct.comp ((t.eTruncLTι b).app ((t.eTruncGE.obj a).obj X)) h
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₁ 📋 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) (i : EInt) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.eTriangleLTGE.obj i).map φ).hom₁ = (t.eTruncLT.obj i).map φ
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₃ 📋 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) (i : EInt) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.eTriangleLTGE.obj i).map φ).hom₃ = (t.eTruncGE.obj i).map φ
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac 📋 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] (a b : EInt) (X : C) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X))) ((t.eTruncLTGEIsoGELT a b).hom.app X) = (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X))
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac_assoc 📋 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] (a b : EInt) (X : C) {Z : C} (h : (t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X))) (CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) h) = CategoryTheory.CategoryStruct.comp ((t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X))) h
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality 📋 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] (a b : EInt) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map f)) ((t.eTruncLTGEIsoGELT a b).hom.app Y) = CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map f))
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₂ 📋 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✝ Y✝ : EInt} (f : X✝ ⟶ Y✝) (j : C) : ((t.eTriangleLTGE.map f).app j).hom₂ = CategoryTheory.CategoryStruct.id j
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality_assoc 📋 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] (a b : EInt) {X Y : C} (f : X ⟶ Y) {Z : C} (h : (t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map f)) (CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app Y) h) = CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map f)) h)
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₁ 📋 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✝ Y✝ : EInt} (f : X✝ ⟶ Y✝) (j : C) : ((t.eTriangleLTGE.map f).app j).hom₁ = (t.eTruncLT.map f).app j
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₃ 📋 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✝ Y✝ : EInt} (f : X✝ ⟶ Y✝) (j : C) : ((t.eTriangleLTGE.map f).app j).hom₃ = (t.eTruncGE.map f).app j
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app 📋 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] (a b : EInt) (hab : a ≤ b) (a' b' : EInt) (hab' : a' ≤ b') (φ : CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hab) ⟶ CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hab')) (X : C) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj X)) (CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app X)) ((t.eTruncLTGEIsoGELT a' b').hom.app X)) = CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X)) ((t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)))
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app_assoc 📋 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] (a b : EInt) (hab : a ≤ b) (a' b' : EInt) (hab' : a' ≤ b') (φ : CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hab) ⟶ CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hab')) (X : C) {Z : C} (h : (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.map (φ.app 1)).app ((t.eTruncGE.obj a).obj X)) (CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b').map ((t.eTruncGE.map (φ.app 0)).app X)) (CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a' b').hom.app X) h)) = CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X) (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj X)) (CategoryTheory.CategoryStruct.comp ((t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app X)) h))
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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 c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) : ((t.triangleω₁δ a b c hab hbc).obj j).obj₁ = (t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj j)
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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 c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) : ((t.triangleω₁δ a b c hab hbc).obj j).obj₂ = (t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj j)
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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 c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) : ((t.triangleω₁δ a b c hab hbc).obj j).obj₃ = (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj j)
CategoryTheory.Triangulated.TStructure.ω₁_obj 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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) (D : CategoryTheory.ComposableArrows EInt 1) : t.ω₁.obj D = (t.eTruncLT.obj (D.obj 1)).comp (t.eTruncGE.obj (D.obj 0))
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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 c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) : ((t.triangleω₁δ a b c hab hbc).obj j).mor₂ = (t.eTruncGE.map (CategoryTheory.homOfLE hab)).app ((t.eTruncLT.obj c).obj j)
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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 c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) : ((t.triangleω₁δ a b c hab hbc).obj j).mor₁ = (t.eTruncGE.obj a).map ((t.eTruncLT.map (CategoryTheory.homOfLE hbc)).app j)
CategoryTheory.Triangulated.TStructure.ω₁_map 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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✝ : CategoryTheory.ComposableArrows EInt 1} (φ : X✝ ⟶ Y✝) : t.ω₁.map φ = t.eTruncLT.map (φ.app 1) ◫ t.eTruncGE.map (φ.app 0)
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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 c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (j : C) : ((t.triangleω₁δ a b c hab hbc).obj j).mor₃ = CategoryTheory.CategoryStruct.comp ((t.eTruncGEδLT.app b).app ((t.eTruncLT.obj c).obj j)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map ((t.eTruncLT.obj b).map ((t.eTruncGEπ a).app ((t.eTruncLT.obj c).obj j)))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map ((t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj j))) ((CategoryTheory.shiftFunctor C 1).map ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map ((t.eTruncLTι c).app j))))))
CategoryTheory.Triangulated.TStructure.ω₁δ_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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 c : EInt) (hab : a ≤ b) (hbc : b ≤ c) (X : C) : (t.ω₁δ a b c hab hbc).app X = CategoryTheory.CategoryStruct.comp ((t.eTruncGEδLT.app b).app ((t.eTruncLT.obj c).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map ((t.eTruncLT.obj b).map ((t.eTruncGEπ a).app ((t.eTruncLT.obj c).obj X)))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map ((t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X))) ((CategoryTheory.shiftFunctor C 1).map ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map ((t.eTruncLTι c).app X))))))
CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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 c : EInt) (hab : a ≤ b) (hbc : b ≤ c) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleω₁δ a b c hab hbc).map φ).hom₁ = (t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map φ)
CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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 c : EInt) (hab : a ≤ b) (hbc : b ≤ c) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleω₁δ a b c hab hbc).map φ).hom₃ = (t.eTruncGE.obj b).map ((t.eTruncLT.obj c).map φ)
CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
{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 c : EInt) (hab : a ≤ b) (hbc : b ≤ c) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleω₁δ a b c hab hbc).map φ).hom₂ = (t.eTruncGE.obj a).map ((t.eTruncLT.obj c).map φ)

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
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