Loogle!

Result

Found 67 declarations mentioning CategoryTheory.Triangulated.SpectralObject.

• CategoryTheory.Triangulated.SpectralObject 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  (C : Type u_1) (ι : Type u_2) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] : Type (max (max (max u_1 u_2) v_1) v_2)
• CategoryTheory.Triangulated.SpectralObject.instCategory 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] : CategoryTheory.Category.{max (max u_2 v_1) v_2, max (max (max u_2 v_2) u_1) v_1} (CategoryTheory.Triangulated.SpectralObject C ι)
• CategoryTheory.Triangulated.SpectralObject.Hom 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X Y : CategoryTheory.Triangulated.SpectralObject C ι) : Type (max (max u_2 v_1) v_2)
• CategoryTheory.Triangulated.SpectralObject.precomp 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {ι' : Type u_4} [CategoryTheory.Category.{u_5, u_4} ι'] (F : CategoryTheory.Functor ι' ι) : CategoryTheory.Triangulated.SpectralObject C ι'
• CategoryTheory.Triangulated.SpectralObject.triangle 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : CategoryTheory.Pretriangulated.Triangle C
• CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {A : Type u_4} [CategoryTheory.Category.{v_4, u_4} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] : CategoryTheory.Abelian.SpectralObject A ι
• CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctorFunctor 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {A : Type u_4} [CategoryTheory.Category.{v_4, u_4} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (ι : Type u_5) [CategoryTheory.Category.{v_5, u_5} ι] : CategoryTheory.Functor (CategoryTheory.Triangulated.SpectralObject C ι) (CategoryTheory.Abelian.SpectralObject A ι)
• CategoryTheory.Triangulated.SpectralObject.triangle_distinguished 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : X.triangle f g ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
• CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u_3} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (X : CategoryTheory.Triangulated.SpectralObject C ι) (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : CategoryTheory.Triangulated.SpectralObject D ι
• CategoryTheory.Triangulated.SpectralObject.ω₁ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (self : CategoryTheory.Triangulated.SpectralObject C ι) : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C
• CategoryTheory.Triangulated.SpectralObject.ω₂ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 2) (CategoryTheory.Pretriangulated.Triangle C)
• CategoryTheory.Functor.mapTriangulatedSpectralObject 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u_3} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (ι : Type u_4) [CategoryTheory.Category.{v_4, u_4} ι] : CategoryTheory.Functor (CategoryTheory.Triangulated.SpectralObject C ι) (CategoryTheory.Triangulated.SpectralObject D ι)
• CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctorFunctor_obj 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {A : Type u_4} [CategoryTheory.Category.{v_4, u_4} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (ι : Type u_5) [CategoryTheory.Category.{v_5, u_5} ι] (X : CategoryTheory.Triangulated.SpectralObject C ι) : (CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctorFunctor F ι).obj X = X.mapHomologicalFunctor F
• CategoryTheory.Triangulated.SpectralObject.triangleMap 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : X.triangle f g ⟶ Y.triangle f g
• CategoryTheory.Triangulated.SpectralObject.ω₂_obj_distinguished 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) (D : CategoryTheory.ComposableArrows ι 2) : X.ω₂.obj D ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
• CategoryTheory.Triangulated.SpectralObject.triangle_obj₁ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).obj₁ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Triangulated.SpectralObject.triangle_obj₃ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).obj₃ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ g)
• CategoryTheory.Triangulated.SpectralObject.triangle_obj₂ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).obj₂ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.CategoryStruct.comp f g))
• CategoryTheory.Functor.mapTriangulatedSpectralObject_obj 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u_3} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (ι : Type u_4) [CategoryTheory.Category.{v_4, u_4} ι] (X : CategoryTheory.Triangulated.SpectralObject C ι) : (F.mapTriangulatedSpectralObject ι).obj X = X.mapTriangulatedFunctor F
• CategoryTheory.Triangulated.SpectralObject.mapTriangle 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} {f : i ⟶ j} {g : j ⟶ k} {i' j' k' : ι} {f' : i' ⟶ j'} {g' : j' ⟶ k'} (φ : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') : X.triangle f g ⟶ X.triangle f' g'
• CategoryTheory.Triangulated.SpectralObject.δ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ (CategoryTheory.shiftFunctor C 1).obj (X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ f))
• CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor_H 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {A : Type u_4} [CategoryTheory.Category.{v_4, u_4} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (n : ℤ) : (X.mapHomologicalFunctor F).H n = X.ω₁.comp (F.shift n)
• CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_ω₁ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u_3} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (X : CategoryTheory.Triangulated.SpectralObject C ι) (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : (X.mapTriangulatedFunctor F).ω₁ = X.ω₁.comp F
• CategoryTheory.Triangulated.SpectralObject.triangle_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).mor₃ = X.δ f g
• CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctor_δ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {A : Type u_4} [CategoryTheory.Category.{v_4, u_4} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁ := by lia) : (X.mapHomologicalFunctor F).δ f g n₀ n₁ h = F.homologySequenceδ (X.triangle f g) n₀ n₁ h
• CategoryTheory.Triangulated.SpectralObject.Hom.hom 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (self : X.Hom Y) : X.ω₁ ⟶ Y.ω₁
• CategoryTheory.Triangulated.SpectralObject.triangle_mor₁ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).mor₁ = X.ω₁.map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g (CategoryTheory.CategoryStruct.comp f g) ⋯)
• CategoryTheory.Triangulated.SpectralObject.triangle_mor₂ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.triangle f g).mor₂ = X.ω₁.map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g (CategoryTheory.CategoryStruct.comp f g) ⋯)
• CategoryTheory.Triangulated.SpectralObject.Hom.ext 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Category.{v_2, u_2} ι} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.HasShift C ℤ} {inst✝⁴ : CategoryTheory.Preadditive C} {inst✝⁵ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst✝⁶ : CategoryTheory.Pretriangulated C} {X Y : CategoryTheory.Triangulated.SpectralObject C ι} {x y : X.Hom Y} (hom : x.hom = y.hom) : x = y
• CategoryTheory.Triangulated.SpectralObject.Hom.ext_iff 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Category.{v_2, u_2} ι} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.HasShift C ℤ} {inst✝⁴ : CategoryTheory.Preadditive C} {inst✝⁵ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst✝⁶ : CategoryTheory.Pretriangulated C} {X Y : CategoryTheory.Triangulated.SpectralObject C ι} {x y : X.Hom Y} : x = y ↔ x.hom = y.hom
• CategoryTheory.Triangulated.SpectralObject.triangleMap_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (CategoryTheory.Triangulated.SpectralObject.triangleMap φ f g).hom₁ = φ.hom.app (CategoryTheory.ComposableArrows.mk₁ f)
• CategoryTheory.Triangulated.SpectralObject.triangleMap_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (CategoryTheory.Triangulated.SpectralObject.triangleMap φ f g).hom₃ = φ.hom.app (CategoryTheory.ComposableArrows.mk₁ g)
• CategoryTheory.Triangulated.SpectralObject.triangleMap_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (φ : X ⟶ Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (CategoryTheory.Triangulated.SpectralObject.triangleMap φ f g).hom₂ = φ.hom.app (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.CategoryStruct.comp f g))
• CategoryTheory.Triangulated.SpectralObject.hom_ext 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X Y : CategoryTheory.Triangulated.SpectralObject C ι} {α β : X ⟶ Y} (h : α.hom = β.hom) : α = β
• CategoryTheory.Triangulated.SpectralObject.hom_ext_iff 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X Y : CategoryTheory.Triangulated.SpectralObject C ι} {α β : X ⟶ Y} : α = β ↔ α.hom = β.hom
• CategoryTheory.Triangulated.SpectralObject.id_hom 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) : (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.ω₁
• CategoryTheory.Triangulated.SpectralObject.mapTriangle_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} {f : i ⟶ j} {g : j ⟶ k} {i' j' k' : ι} {f' : i' ⟶ j'} {g' : j' ⟶ k'} (φ : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') : (X.mapTriangle φ).hom₁ = X.ω₁.map ((CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Triangulated.SpectralObject._proof_6 CategoryTheory.Triangulated.SpectralObject._proof_2).map φ)
• CategoryTheory.Triangulated.SpectralObject.mapTriangle_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} {f : i ⟶ j} {g : j ⟶ k} {i' j' k' : ι} {f' : i' ⟶ j'} {g' : j' ⟶ k'} (φ : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') : (X.mapTriangle φ).hom₃ = X.ω₁.map ((CategoryTheory.ComposableArrows.functorArrows ι 1 2 2 CategoryTheory.Triangulated.SpectralObject._proof_2 CategoryTheory.Triangulated.SpectralObject._proof_4).map φ)
• CategoryTheory.Triangulated.SpectralObject.mapTriangle_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} {f : i ⟶ j} {g : j ⟶ k} {i' j' k' : ι} {f' : i' ⟶ j'} {g' : j' ⟶ k'} (φ : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') : (X.mapTriangle φ).hom₂ = X.ω₁.map ((CategoryTheory.ComposableArrows.functorArrows ι 0 2 2 CategoryTheory.Triangulated.SpectralObject._proof_8 CategoryTheory.Triangulated.SpectralObject._proof_4).map φ)
• CategoryTheory.Triangulated.SpectralObject.comp_hom 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X✝ Y✝ Z✝ : CategoryTheory.Triangulated.SpectralObject C ι} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
• CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₂ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2) : (X.ω₂.obj j).obj₂ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (j.map (CategoryTheory.homOfLE ⋯)))
• CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₃ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2) : (X.ω₂.obj j).obj₃ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (j.map (CategoryTheory.homOfLE ⋯)))
• CategoryTheory.Triangulated.SpectralObject.δ' 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (self : CategoryTheory.Triangulated.SpectralObject C ι) : (CategoryTheory.ComposableArrows.functorArrows ι 1 2 2 CategoryTheory.Triangulated.SpectralObject._proof_2 CategoryTheory.Triangulated.SpectralObject._proof_4).comp self.ω₁ ⟶ (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Triangulated.SpectralObject._proof_6 CategoryTheory.Triangulated.SpectralObject._proof_2).comp (self.ω₁.comp (CategoryTheory.shiftFunctor C 1))
• CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₁ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2) : (X.ω₂.obj j).obj₁ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (j.map (CategoryTheory.homOfLE ⋯)))
• CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctorFunctor_map_hom 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {A : Type u_4} [CategoryTheory.Category.{v_4, u_4} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (ι : Type u_5) [CategoryTheory.Category.{v_5, u_5} ι] {X✝ Y✝ : CategoryTheory.Triangulated.SpectralObject C ι} (φ : X✝ ⟶ Y✝) (n : ℤ) : ((CategoryTheory.Triangulated.SpectralObject.mapHomologicalFunctorFunctor F ι).map φ).hom n = CategoryTheory.Functor.whiskerRight φ.hom (F.shift n)
• CategoryTheory.Functor.mapTriangulatedSpectralObject_map_hom 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u_3} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (ι : Type u_4) [CategoryTheory.Category.{v_4, u_4} ι] {X✝ Y✝ : CategoryTheory.Triangulated.SpectralObject C ι} (α : X✝ ⟶ Y✝) : ((F.mapTriangulatedSpectralObject ι).map α).hom = CategoryTheory.Functor.whiskerRight α.hom F
• CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u_3} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (X : CategoryTheory.Triangulated.SpectralObject C ι) (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : (X.mapTriangulatedFunctor F).δ f g = CategoryTheory.CategoryStruct.comp (F.map (X.δ f g)) ((CategoryTheory.Functor.commShiftIso F 1).hom.app (X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ f)))
• CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2) : (X.ω₂.obj j).mor₃ = X.δ'.app j
• CategoryTheory.Triangulated.SpectralObject.Hom.comm 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (self : X.Hom Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) : CategoryTheory.CategoryStruct.comp (X.δ f g) ((CategoryTheory.shiftFunctor C 1).map (self.hom.app (CategoryTheory.ComposableArrows.mk₁ f))) = CategoryTheory.CategoryStruct.comp (self.hom.app (CategoryTheory.ComposableArrows.mk₁ g)) (Y.δ f g)
• CategoryTheory.Triangulated.SpectralObject.Hom.comm_assoc 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (self : X.Hom Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj (Y.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ f)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.δ f g) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map (self.hom.app (CategoryTheory.ComposableArrows.mk₁ f))) h) = CategoryTheory.CategoryStruct.comp (self.hom.app (CategoryTheory.ComposableArrows.mk₁ g)) (CategoryTheory.CategoryStruct.comp (Y.δ f g) h)
• CategoryTheory.Triangulated.SpectralObject.comp_hom_assoc 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X✝ Y✝ Z✝ : CategoryTheory.Triangulated.SpectralObject C ι} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {Z : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C} (h : Z✝.ω₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
• CategoryTheory.Triangulated.SpectralObject.Hom.mk 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (hom : X.ω₁ ⟶ Y.ω₁) (comm : ∀ {i j k : ι} (f : i ⟶ j) (g : j ⟶ k), CategoryTheory.CategoryStruct.comp (X.δ f g) ((CategoryTheory.shiftFunctor C 1).map (hom.app (CategoryTheory.ComposableArrows.mk₁ f))) = CategoryTheory.CategoryStruct.comp (hom.app (CategoryTheory.ComposableArrows.mk₁ g)) (Y.δ f g) := by cat_disch) : X.Hom Y
• CategoryTheory.Triangulated.SpectralObject.δ_naturality 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f') (β : CategoryTheory.ComposableArrows.mk₁ g ⟶ CategoryTheory.ComposableArrows.mk₁ g') (hαβ : α.app 1 = β.app 0) : CategoryTheory.CategoryStruct.comp (X.ω₁.map β) (X.δ f' g') = CategoryTheory.CategoryStruct.comp (X.δ f g) ((CategoryTheory.shiftFunctor C 1).map (X.ω₁.map α))
• CategoryTheory.Triangulated.SpectralObject.δ_naturality_assoc 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j') (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f') (β : CategoryTheory.ComposableArrows.mk₁ g ⟶ CategoryTheory.ComposableArrows.mk₁ g') (hαβ : α.app 1 = β.app 0) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj (X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ f')) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.ω₁.map β) (CategoryTheory.CategoryStruct.comp (X.δ f' g') h) = CategoryTheory.CategoryStruct.comp (X.δ f g) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map (X.ω₁.map α)) h)
• CategoryTheory.Triangulated.SpectralObject.distinguished' 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (self : CategoryTheory.Triangulated.SpectralObject C ι) (D : CategoryTheory.ComposableArrows ι 2) : CategoryTheory.Pretriangulated.Triangle.mk (self.ω₁.map ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2 CategoryTheory.Triangulated.SpectralObject._proof_6 CategoryTheory.Triangulated.SpectralObject._proof_8 CategoryTheory.Triangulated.SpectralObject._proof_10 CategoryTheory.Triangulated.SpectralObject._proof_2 CategoryTheory.Triangulated.SpectralObject._proof_4).app D)) (self.ω₁.map ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2 CategoryTheory.Triangulated.SpectralObject._proof_8 CategoryTheory.Triangulated.SpectralObject._proof_2 CategoryTheory.Triangulated.SpectralObject._proof_6 CategoryTheory.Triangulated.SpectralObject._proof_4 CategoryTheory.Triangulated.SpectralObject._proof_4).app D)) (self.δ'.app D) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
• CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ' 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {D : Type u_3} [CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (X : CategoryTheory.Triangulated.SpectralObject C ι) (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : (X.mapTriangulatedFunctor F).δ' = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight X.δ' F) (((CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Triangulated.SpectralObject._proof_6 CategoryTheory.Triangulated.SpectralObject._proof_2).comp X.ω₁).whiskerLeft (CategoryTheory.Functor.commShiftIso F 1).hom)
• CategoryTheory.Triangulated.SpectralObject.mk 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (ω₁ : CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C) (δ' : (CategoryTheory.ComposableArrows.functorArrows ι 1 2 2 CategoryTheory.Triangulated.SpectralObject._proof_2 CategoryTheory.Triangulated.SpectralObject._proof_4).comp ω₁ ⟶ (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Triangulated.SpectralObject._proof_6 CategoryTheory.Triangulated.SpectralObject._proof_2).comp (ω₁.comp (CategoryTheory.shiftFunctor C 1))) (distinguished' : ∀ (D : CategoryTheory.ComposableArrows ι 2), CategoryTheory.Pretriangulated.Triangle.mk (ω₁.map ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2 CategoryTheory.Triangulated.SpectralObject._proof_6 CategoryTheory.Triangulated.SpectralObject._proof_8 CategoryTheory.Triangulated.SpectralObject._proof_10 CategoryTheory.Triangulated.SpectralObject._proof_2 CategoryTheory.Triangulated.SpectralObject._proof_4).app D)) (ω₁.map ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 2 1 2 2 CategoryTheory.Triangulated.SpectralObject._proof_8 CategoryTheory.Triangulated.SpectralObject._proof_2 CategoryTheory.Triangulated.SpectralObject._proof_6 CategoryTheory.Triangulated.SpectralObject._proof_4 CategoryTheory.Triangulated.SpectralObject._proof_4).app D)) (δ'.app D) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : CategoryTheory.Triangulated.SpectralObject C ι
• CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {X✝ Y✝ : CategoryTheory.ComposableArrows ι 2} (φ : X✝ ⟶ Y✝) : (X.ω₂.map φ).hom₂ = X.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (φ.app 0) (φ.app ⟨2, ⋯⟩) ⋯)
• CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {X✝ Y✝ : CategoryTheory.ComposableArrows ι 2} (φ : X✝ ⟶ Y✝) : (X.ω₂.map φ).hom₃ = X.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (φ.app 1) (φ.app ⟨2, ⋯⟩) ⋯)
• CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) {X✝ Y✝ : CategoryTheory.ComposableArrows ι 2} (φ : X✝ ⟶ Y✝) : (X.ω₂.map φ).hom₁ = X.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (φ.app 0) (φ.app 1) ⋯)
• CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2) : (X.ω₂.obj j).mor₂ = X.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (j.map (CategoryTheory.homOfLE ⋯)) (CategoryTheory.CategoryStruct.id (j.obj ⟨2, ⋯⟩)) ⋯)
• CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁ 📋 Mathlib.CategoryTheory.Triangulated.SpectralObject
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} ι] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2) : (X.ω₂.obj j).mor₁ = X.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (CategoryTheory.CategoryStruct.id (j.obj 0)) (j.map (CategoryTheory.homOfLE ⋯)) ⋯)
• HomotopyCategory.spectralObjectMappingCone 📋 Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Triangulated.SpectralObject (HomotopyCategory C (ComplexShape.up ℤ)) (CochainComplex C ℤ)
• CategoryTheory.Triangulated.TStructure.spectralObject 📋 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] (X : C) : CategoryTheory.Triangulated.SpectralObject C EInt
• CategoryTheory.Triangulated.TStructure.spectralObjectFunctor 📋 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] : CategoryTheory.Functor C (CategoryTheory.Triangulated.SpectralObject C EInt)
• CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_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] (X : C) : t.spectralObjectFunctor.obj X = t.spectralObject X
• CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_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] {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : (t.spectralObjectFunctor.map φ).hom = t.ω₁.whiskerLeft ((CategoryTheory.evaluation C 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:

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

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

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

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

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

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

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

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

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

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

Source code

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

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c