Loogle!

Result

Found 66 declarations mentioning CategoryTheory.Functor.IsTriangulated.

CategoryTheory.Functor.IsTriangulated.instId 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] : (CategoryTheory.Functor.id C).IsTriangulated
CategoryTheory.Functor.IsTriangulated 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] : Prop
CategoryTheory.Functor.IsTriangulated.instAdditive 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] : F.Additive
CategoryTheory.Functor.IsTriangulated.instPreservesLimitsOfShapeDiscreteWalkingPair 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F
CategoryTheory.Functor.IsTriangulated.instPreservesZeroMorphisms 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] : F.PreservesZeroMorphisms
CategoryTheory.IsTriangulated.of_fully_faithful_triangulated_functor 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] [F.Full] [F.Faithful] [CategoryTheory.IsTriangulated D] : CategoryTheory.IsTriangulated C
CategoryTheory.Functor.isTriangulated_of_iso 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] [F₁.IsTriangulated] : F₂.IsTriangulated
CategoryTheory.Functor.isTriangulated_iff_of_iso 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] : F₁.IsTriangulated ↔ F₂.IsTriangulated
CategoryTheory.Functor.map_distinguished 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
CategoryTheory.Functor.IsTriangulated.map_distinguished 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Category.{v_2, u_2} D} {inst✝² : CategoryTheory.HasShift C ℤ} {inst✝³ : CategoryTheory.HasShift D ℤ} {F : CategoryTheory.Functor C D} {inst✝⁴ : F.CommShift ℤ} {inst✝⁵ : CategoryTheory.Limits.HasZeroObject C} {inst✝⁶ : CategoryTheory.Limits.HasZeroObject D} {inst✝⁷ : CategoryTheory.Preadditive C} {inst✝⁸ : CategoryTheory.Preadditive D} {inst✝⁹ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst✝¹⁰ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive} {inst✝¹¹ : CategoryTheory.Pretriangulated C} {inst✝¹² : CategoryTheory.Pretriangulated D} [self : F.IsTriangulated] (T : CategoryTheory.Pretriangulated.Triangle C) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
CategoryTheory.Functor.IsTriangulated.mk 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] {F : CategoryTheory.Functor C D} [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (map_distinguished : ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : F.IsTriangulated
CategoryTheory.Functor.map_distinguished_iff 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] [F.Full] [F.Faithful] (T : CategoryTheory.Pretriangulated.Triangle C) : F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
CategoryTheory.Functor.IsTriangulated.instComp 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (G : CategoryTheory.Functor D E) [G.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroObject E] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Preadditive E] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [CategoryTheory.Pretriangulated E] [F.IsTriangulated] [G.IsTriangulated] : (F.comp G).IsTriangulated
CategoryTheory.Functor.isTriangulated_of_precomp 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (G : CategoryTheory.Functor D E) [G.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroObject E] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Preadditive E] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [CategoryTheory.Pretriangulated E] [(F.comp G).IsTriangulated] [F.IsTriangulated] [F.mapArrow.EssSurj] : G.IsTriangulated
CategoryTheory.Functor.mem_mapTriangle_essImage_of_distinguished 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] [F.mapArrow.EssSurj] (T : CategoryTheory.Pretriangulated.Triangle D) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : ∃ T', ∃ (_ : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)
CategoryTheory.Functor.isTriangulated_iff_comp_right 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroObject E] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Preadditive E] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [CategoryTheory.Pretriangulated E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} (e : F.comp G ≅ H) [F.CommShift ℤ] [G.CommShift ℤ] [H.CommShift ℤ] [CategoryTheory.NatTrans.CommShift e.hom ℤ] [G.IsTriangulated] [G.Full] [G.Faithful] : F.IsTriangulated ↔ H.IsTriangulated
CategoryTheory.isTriangulated_of_essSurj_mapComposableArrows_two 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] [(F.mapComposableArrows 2).EssSurj] [CategoryTheory.IsTriangulated C] : CategoryTheory.IsTriangulated D
CategoryTheory.Functor.isTriangulated_of_precomp_iso 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} {E : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift E ℤ] {F : CategoryTheory.Functor C D} [F.CommShift ℤ] {G : CategoryTheory.Functor D E} [G.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroObject E] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Preadditive E] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [CategoryTheory.Pretriangulated E] {H : CategoryTheory.Functor C E} (e : F.comp G ≅ H) [H.CommShift ℤ] [H.IsTriangulated] [F.IsTriangulated] [F.mapArrow.EssSurj] [CategoryTheory.NatTrans.CommShift e.hom ℤ] : G.IsTriangulated
CategoryTheory.Triangulated.Octahedron.map 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : CategoryTheory.Triangulated.Octahedron ⋯ ⋯ ⋯ ⋯
CategoryTheory.Triangulated.Octahedron.map_m₁ 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : (h.map F).m₁ = F.map h.m₁
CategoryTheory.Triangulated.Octahedron.map_m₃ 📋 Mathlib.CategoryTheory.Triangulated.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles} {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles} {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles} (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃) (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : (h.map F).m₃ = F.map h.m₃
HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory 📋 Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] (G : CategoryTheory.Functor C D) [G.Additive] : (G.mapHomotopyCategory (ComplexShape.up ℤ)).IsTriangulated
CategoryTheory.Triangulated.Localization.isTriangulated 📋 Mathlib.CategoryTheory.Localization.Triangulated
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [L.IsTriangulated] [CategoryTheory.IsTriangulated C] : CategoryTheory.IsTriangulated D
CategoryTheory.Triangulated.Localization.isTriangulated_functor 📋 Mathlib.CategoryTheory.Localization.Triangulated
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] [W.IsCompatibleWithTriangulation] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [L.Additive] : L.IsTriangulated
CategoryTheory.Functor.distTriang_iff 📋 Mathlib.CategoryTheory.Localization.Triangulated
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.HasShift D ℤ] [L.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [L.mapArrow.EssSurj] [L.IsTriangulated] (T : CategoryTheory.Pretriangulated.Triangle D) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ T ∈ L.essImageDistTriang
CategoryTheory.ObjectProperty.instIsTriangulatedEssImageOfIsTriangulatedOfFull 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
{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_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] [F.Full] : F.essImage.IsTriangulated
CategoryTheory.ObjectProperty.instIsTriangulatedInverseImage 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
{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_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor D C) [F.CommShift ℤ] [F.IsTriangulated] [P.IsClosedUnderIsomorphisms] [P.IsTriangulated] : (P.inverseImage F).IsTriangulated
CategoryTheory.ObjectProperty.instIsTriangulatedMapOfIsTriangulatedOfFull 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
{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] (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] {D : Type u_4} [CategoryTheory.Category.{u_5, u_4} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] [F.Full] : (P.map F).IsTriangulated
CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategoryι 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
{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] (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] : P.ι.IsTriangulated
CategoryTheory.ObjectProperty.inverseImage_trW_isInverted 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
{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_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor D C) [F.CommShift ℤ] [F.IsTriangulated] [P.IsClosedUnderIsomorphisms] {E : Type u_4} [CategoryTheory.Category.{u_5, u_4} E] (L : CategoryTheory.Functor C E) [L.IsLocalization P.trW] : (P.inverseImage F).trW.IsInvertedBy (F.comp L)
CategoryTheory.ObjectProperty.inverseImage_trW_iff 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
{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_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor D C) [F.CommShift ℤ] [F.IsTriangulated] [P.IsClosedUnderIsomorphisms] {X Y : D} (s : X ⟶ Y) : (P.inverseImage F).trW s ↔ P.trW (F.map s)
CategoryTheory.ObjectProperty.isTriangulated_lift 📋 Mathlib.CategoryTheory.Triangulated.Subcategory
{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] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.HasShift E ℤ] (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] (F : CategoryTheory.Functor E C) (hF : ∀ (X : E), P (F.obj X)) [CategoryTheory.Preadditive E] [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject E] [∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [CategoryTheory.Pretriangulated E] [F.IsTriangulated] : (P.lift F hF).IsTriangulated
CategoryTheory.Functor.instIsHomologicalCompOfIsTriangulated 📋 Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
{C : Type u_1} {D : Type u_2} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Abelian A] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor D A) [L.CommShift ℤ] [L.IsTriangulated] [F.IsHomological] : (L.comp F).IsHomological
CategoryTheory.Functor.isHomological_of_localization 📋 Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
{C : Type u_1} {D : Type u_2} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.Category.{v_3, u_3} A] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Abelian A] (L : CategoryTheory.Functor C D) [L.CommShift ℤ] [L.IsTriangulated] [L.mapArrow.EssSurj] (F : CategoryTheory.Functor D A) (G : CategoryTheory.Functor C A) (e : L.comp F ≅ G) [G.IsHomological] : F.IsHomological
DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh 📋 Mathlib.Algebra.Homology.DerivedCategory.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Qh.IsTriangulated
CategoryTheory.Functor.instIsTriangulatedPlusMapHomotopyCategoryPlus 📋 Mathlib.Algebra.Homology.HomotopyCategory.Plus
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] : F.mapHomotopyCategoryPlus.IsTriangulated
CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategoryFunctorTrWInverseImageιTriangulatedLocalizerMorphism 📋 Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [A.IsTriangulated] : (A.triangulatedLocalizerMorphism B).functor.IsTriangulated
DerivedCategory.Plus.instIsTriangulatedPlusQh 📋 Mathlib.Algebra.Homology.DerivedCategory.Plus
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : DerivedCategory.Plus.Qh.IsTriangulated
CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
{C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : F.mapDerivedCategory.IsTriangulated
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.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.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.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.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.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.Functor.isTriangulated_of_rightExtension 📋 Mathlib.CategoryTheory.Functor.Derived.LeftDerivedTriangulated
{C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} H] (F' : CategoryTheory.Functor H D) {F : CategoryTheory.Functor C D} {L : CategoryTheory.Functor C H} [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift H ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroObject H] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Preadditive H] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor H n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [CategoryTheory.Pretriangulated H] [F.CommShift ℤ] [L.CommShift ℤ] [F'.CommShift ℤ] [F.IsTriangulated] [L.IsTriangulated] (α : L.comp F' ⟶ F) [CategoryTheory.NatTrans.CommShift α ℤ] (h : ∀ ⦃X Y : H⦄ (f : X ⟶ Y), ∃ T, ∃ (_ : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (_ : CategoryTheory.IsIso (α.app T.obj₁)) (_ : CategoryTheory.IsIso (α.app T.obj₂)) (_ : CategoryTheory.IsIso (α.app T.obj₃)), Nonempty (CategoryTheory.Arrow.mk (L.map T.mor₁) ≅ CategoryTheory.Arrow.mk f)) : F'.IsTriangulated
CategoryTheory.Functor.isTriangulated_of_leftExtension 📋 Mathlib.CategoryTheory.Functor.Derived.RightDerivedTriangulated
{C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Category.{v_3, u_3} H] (F' : CategoryTheory.Functor H D) {F : CategoryTheory.Functor C D} {L : CategoryTheory.Functor C H} [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [CategoryTheory.HasShift H ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroObject H] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Preadditive H] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor H n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] [CategoryTheory.Pretriangulated H] [F.CommShift ℤ] [L.CommShift ℤ] [F'.CommShift ℤ] [F.IsTriangulated] [L.IsTriangulated] (α : F ⟶ L.comp F') [CategoryTheory.NatTrans.CommShift α ℤ] (h : ∀ ⦃X Y : H⦄ (f : X ⟶ Y), ∃ T, ∃ (_ : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (_ : CategoryTheory.IsIso (α.app T.obj₁)) (_ : CategoryTheory.IsIso (α.app T.obj₂)) (_ : CategoryTheory.IsIso (α.app T.obj₃)), Nonempty (CategoryTheory.Arrow.mk (L.map T.mor₁) ≅ CategoryTheory.Arrow.mk f)) : F'.IsTriangulated
CategoryTheory.Functor.isTriangulated_of_op 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [F.op.IsTriangulated] : F.IsTriangulated
CategoryTheory.Pretriangulated.Opposite.functor_isTriangulated_op 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [F.IsTriangulated] : F.op.IsTriangulated
CategoryTheory.Functor.op_isTriangulated_iff 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Functor
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] : F.op.IsTriangulated ↔ F.IsTriangulated
CategoryTheory.Adjunction.IsTriangulated.leftAdjoint_isTriangulated 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Category.{v_2, u_2} D} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.Limits.HasZeroObject D} {inst✝⁴ : CategoryTheory.Preadditive C} {inst✝⁵ : CategoryTheory.Preadditive D} {inst✝⁶ : CategoryTheory.HasShift C ℤ} {inst✝⁷ : CategoryTheory.HasShift D ℤ} {inst✝⁸ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst✝⁹ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive} {inst✝¹⁰ : CategoryTheory.Pretriangulated C} {inst✝¹¹ : CategoryTheory.Pretriangulated D} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {inst✝¹² : F.CommShift ℤ} {inst✝¹³ : G.CommShift ℤ} [self : adj.IsTriangulated] : F.IsTriangulated
CategoryTheory.Adjunction.IsTriangulated.rightAdjoint_isTriangulated 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Category.{v_2, u_2} D} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.Limits.HasZeroObject D} {inst✝⁴ : CategoryTheory.Preadditive C} {inst✝⁵ : CategoryTheory.Preadditive D} {inst✝⁶ : CategoryTheory.HasShift C ℤ} {inst✝⁷ : CategoryTheory.HasShift D ℤ} {inst✝⁸ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst✝⁹ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive} {inst✝¹⁰ : CategoryTheory.Pretriangulated C} {inst✝¹¹ : CategoryTheory.Pretriangulated D} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {inst✝¹² : F.CommShift ℤ} {inst✝¹³ : G.CommShift ℤ} [self : adj.IsTriangulated] : G.IsTriangulated
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctor 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] [E.IsTriangulated] : E.functor.IsTriangulated
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverse 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] [E.IsTriangulated] : E.inverse.IsTriangulated
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctorSymmOfInverse 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.inverse.CommShift ℤ] [h : E.inverse.IsTriangulated] : E.symm.functor.IsTriangulated
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverseSymmOfFunctor 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [h : E.functor.IsTriangulated] : E.symm.inverse.IsTriangulated
CategoryTheory.Adjunction.isTriangulated_leftAdjoint 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommShift ℤ] [adj.CommShift ℤ] [G.IsTriangulated] : F.IsTriangulated
CategoryTheory.Adjunction.isTriangulated_rightAdjoint 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommShift ℤ] [adj.CommShift ℤ] [F.IsTriangulated] : G.IsTriangulated
CategoryTheory.Equivalence.IsTriangulated.mk' 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] [E.CommShift ℤ] (h : E.functor.IsTriangulated) : E.IsTriangulated
CategoryTheory.Equivalence.IsTriangulated.mk'' 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] [E.CommShift ℤ] (h : E.inverse.IsTriangulated) : E.IsTriangulated
CategoryTheory.Adjunction.IsTriangulated.mk' 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommShift ℤ] [adj.CommShift ℤ] [F.IsTriangulated] : adj.IsTriangulated
CategoryTheory.Adjunction.IsTriangulated.mk'' 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommShift ℤ] [adj.CommShift ℤ] [G.IsTriangulated] : adj.IsTriangulated
CategoryTheory.Adjunction.IsTriangulated.mk 📋 Mathlib.CategoryTheory.Triangulated.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} [F.CommShift ℤ] [G.CommShift ℤ] (commShift : adj.CommShift ℤ := by infer_instance) (leftAdjoint_isTriangulated : F.IsTriangulated := by infer_instance) (rightAdjoint_isTriangulated : G.IsTriangulated := by infer_instance) : adj.IsTriangulated
CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOp 📋 Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] : (CategoryTheory.opOp C).IsTriangulated
CategoryTheory.Pretriangulated.instIsTriangulatedOppositeUnopUnop 📋 Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] : (CategoryTheory.unopUnop C).IsTriangulated

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