Loogle!

Result

Found 75 declarations mentioning CategoryTheory.Triangulated.TStructure.eTruncLT.

CategoryTheory.Triangulated.TStructure.eTruncLT 📋 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.instAdditiveObjEIntFunctorETruncLT 📋 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.eTruncLT.obj i).Additive
CategoryTheory.Triangulated.TStructure.eTruncLT_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.eTruncLT.obj ⊤ = CategoryTheory.Functor.id C
CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe 📋 Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : t.eTruncLT.obj (WithBotTop.coe n) = t.truncLT n
CategoryTheory.Triangulated.TStructure.eTruncLTι 📋 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.eTruncLT.obj i ⟶ CategoryTheory.Functor.id C
CategoryTheory.Triangulated.TStructure.instIsLEObjEIntFunctorETruncLT 📋 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] (i : EInt) : t.IsLE ((t.eTruncLT.obj i).obj X) n
CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTιTopEInt 📋 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.eTruncLTι ⊤)
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.eTruncLT_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.eTruncLT.obj ⊥ = 0
CategoryTheory.Triangulated.TStructure.isLE_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) (n : ℤ) (i : EInt) (h : i ≤ WithBotTop.coe (n + 1)) (X : C) : t.IsLE ((t.eTruncLT.obj i).obj X) n
CategoryTheory.Triangulated.TStructure.eTruncLT_ι_coe 📋 Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : t.eTruncLTι (WithBotTop.coe n) = t.truncLTι n
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.eTruncLT.obj i).obj j
CategoryTheory.Triangulated.TStructure.eTruncLTLTToLT 📋 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 a).comp (t.eTruncLT.obj b) ⟶ t.eTruncLT.obj b
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT 📋 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 : b ≤ a) : (t.eTruncLT.obj a).comp (t.eTruncLT.obj b) ≅ t.eTruncLT.obj b
CategoryTheory.Triangulated.TStructure.eTruncLT_ι_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.eTruncLTι ⊤ = CategoryTheory.CategoryStruct.id (t.eTruncLT.obj ⊤)
CategoryTheory.Triangulated.TStructure.isIso_eTruncLTLTIsoLT 📋 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 : b ≤ a) : CategoryTheory.IsIso (t.eTruncLTLTToLT 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.eTruncLTι i).app j
CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι 📋 Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : t.eTruncLT.map (CategoryTheory.homOfLE ⋯) = t.truncLTι n
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.instIsIsoAppETruncLTιObjEIntFunctorETruncLT 📋 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 : EInt) (X : C) : CategoryTheory.IsIso ((t.eTruncLTι a).app ((t.eTruncLT.obj a).obj X))
CategoryTheory.Triangulated.TStructure.eTruncLT_ι_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.eTruncLTι ⊥ = 0
CategoryTheory.Triangulated.TStructure.instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι 📋 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 : EInt) (X : C) : CategoryTheory.IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))
CategoryTheory.Triangulated.TStructure.isIso_eTruncLT_obj_map_truncLTπ_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.eTruncLT.obj a).map ((t.eTruncLTι b).app X))
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_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 : b ≤ a) : (t.eTruncLTLTIsoLT a b hab).hom = t.eTruncLTLTToLT a b
CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_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.eTruncLT.obj i).map ((t.eTruncLTι i).app X) = (t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)
CategoryTheory.Triangulated.TStructure.eTruncLTι_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.eTruncLT.obj i).map f) ((t.eTruncLTι i).app Y) = CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).app X) f
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.eTruncLT_map_app_eTruncLTι_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.eTruncLT.map f).app X) ((t.eTruncLTι j).app X) = (t.eTruncLTι i).app X
CategoryTheory.Triangulated.TStructure.eTruncLTLTToLT_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.eTruncLTLTToLT a b).app X = (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)
CategoryTheory.Triangulated.TStructure.eTruncLTι_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 : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj i).map f) (CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).app Y) h) = CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).app X) (CategoryTheory.CategoryStruct.comp f 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.eTruncLT_map_app_eTruncLTι_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 : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.map f).app X) (CategoryTheory.CategoryStruct.comp ((t.eTruncLTι j).app X) h) = CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).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.eTruncLT_obj_map_eTruncLTι_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.eTruncLT.obj i).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj i).map ((t.eTruncLTι i).app X)) h = CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)) h
CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_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.eTruncLT.obj i).map ((t.eTruncLTι j).app X)) ((t.eTruncLT.map f).app X) = (t.eTruncLTι i).app ((t.eTruncLT.obj j).obj X)
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.eTruncLTLTIsoLT_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 : b ≤ a) (X : C) : CategoryTheory.CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app X) ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)) = CategoryTheory.CategoryStruct.id ((t.eTruncLT.obj b).obj X)
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_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 : b ≤ a) (X : C) {Z : C} (h : (t.eTruncLT.obj b).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app X) (CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)) h) = h
CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_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.eTruncLT.obj j).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj i).map ((t.eTruncLTι j).app X)) (CategoryTheory.CategoryStruct.comp ((t.eTruncLT.map f).app X) h) = CategoryTheory.CategoryStruct.comp ((t.eTruncLTι i).app ((t.eTruncLT.obj j).obj X)) h
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_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 : b ≤ a) (X : C) {Z : C} (h : (t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)) (CategoryTheory.CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app X) h) = h
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_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 : b ≤ a) (X : C) : CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)) ((t.eTruncLTLTIsoLT a b hab).inv.app X) = CategoryTheory.CategoryStruct.id ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).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.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_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) [CategoryTheory.IsTriangulated C] (a b : EInt) (hab : b ≤ a) (X : C) : CategoryTheory.CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app ((t.eTruncLT.obj a).obj X)) ((t.eTruncLT.obj b).map ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))) = CategoryTheory.CategoryStruct.id ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X))
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj_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 : b ≤ a) (X : C) {Z : C} (h : (t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app ((t.eTruncLT.obj a).obj X)) (CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))) h) = h
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