The pretriangulated axioms, with rotation only forward

Pretriangulated states TR2 as an ↔: a triangle is distinguished exactly when its rotation is. Only the forward half is ever proved by a construction. The reverse half is a theorem about the other four axioms, and this file proves it, so a category that supplies the forward half supplies the class.

The redundancy

Axioms bundles the five things a construction actually establishes: isomorphism-closure, the contractible triangles, a cone on every morphism, the forward rotation, and the completion of a square. Axioms.mem_of_rotate_mem derives the reverse rotation from them, and Axioms.pretriangulated assembles the class.

The proof is the classical one. Given T.rotate distinguished, take a cone triangle S on T.mor₁; the completion axiom against mor₂ -- itself the completion axiom applied to rotations -- produces φ : T.obj₃ ⟶ S.obj₃ commuting with both remaining maps. Hom(U, -) is exact at the second vertex of a distinguished triangle (Axioms.coyoneda_exact₂), and applying that to the rotations of T.rotate and of S makes post-composition with φ injective and surjective on every Hom(U, -). So φ is an isomorphism, T ≅ S, and T is distinguished.

Nothing here is circular: every exactness fact used is read off a triangle already known to be distinguished -- T.rotate and its further rotations, or S and its rotations -- never off T itself.

Placement

Generic triangulated vocabulary. This file imports Mathlib alone, mentions no dg category and no stability condition, and lives in Mathlib's CategoryTheory.Pretriangulated namespace because everything it says is about Mathlib's Triangle and Pretriangulated.

The backward options

Mathlib sets both of these on the same lemmas (comp_distTriang_mor_zero₁₂, complete_distinguished_triangle_morphism₁, the coyoneda_exact family). The projections (contractibleTriangle X).obj₂ and T.rotate.mor₂ are definitional but not reducible, so a hypothesis stated through them will not unify with the same statement written directly without them. They are set for the file rather than per declaration because every proof below is of that kind.

theorem CategoryTheory.Pretriangulated.exists_lift_of_iso {D : Type u} [Category.{v, u} D] [HasShift D ℤ] {T₁ T₂ S₁ S₂ : Triangle D} (e₁ : T₁ ≅ S₁) (e₂ : T₂ ≅ S₂) (H : ∀ (a' : S₁.obj₁ ⟶ S₂.obj₁) (b' : S₁.obj₂ ⟶ S₂.obj₂), CategoryStruct.comp S₁.mor₁ b' = CategoryStruct.comp a' S₂.mor₁ → ∃ (c' : S₁.obj₃ ⟶ S₂.obj₃), CategoryStruct.comp S₁.mor₂ c' = CategoryStruct.comp b' S₂.mor₂ ∧ CategoryStruct.comp S₁.mor₃ ((shiftFunctor D 1).map a') = CategoryStruct.comp c' S₂.mor₃) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (comm : CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁) : ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), CategoryStruct.comp T₁.mor₂ c = CategoryStruct.comp b T₂.mor₂ ∧ CategoryStruct.comp T₁.mor₃ ((shiftFunctor D 1).map a) = CategoryStruct.comp c T₂.mor₃

The lifting axiom transports along isomorphisms of triangles.

A class of distinguished triangles is an isomorphism-closure, so the completion axiom only ever has to be proved for the triangles that generate the class. This is what moves it to the closure: a and b are conjugated into the generators, the lift is conjugated back, and each of the two squares is the corresponding square of the generators with four Iso.hom_inv_id cancellations around it.

It asks for no more than a shift, so a construction can use it before it knows its class satisfies Axioms.

structure CategoryTheory.Pretriangulated.Axioms {D : Type u} [Category.{v, u} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] (triangles : Set (Triangle D)) : Prop

The Pretriangulated axioms, with the rotation axiom weakened to its forward direction only.

• isomorphic (T₁ : Triangle D) : T₁ ∈ triangles → ∀ (T₂ : Triangle D) (a✝ : T₂ ≅ T₁), T₂ ∈ triangles

  a triangle isomorphic to a distinguished one is distinguished

• contractible (X : D) : contractibleTriangle X ∈ triangles

  the contractible triangles are distinguished

• cocone {X Y : D} (f : X ⟶ Y) : ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ (shiftFunctor D 1).obj X), Triangle.mk f g h ∈ triangles

  every morphism fits into a distinguished triangle

• rotate (T : Triangle D) : T ∈ triangles → T.rotate ∈ triangles

  the rotation of a distinguished triangle is distinguished

• complete (T₁ T₂ : Triangle D) : T₁ ∈ triangles → T₂ ∈ triangles → ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂), CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁ → ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), CategoryStruct.comp T₁.mor₂ c = CategoryStruct.comp b T₂.mor₂ ∧ CategoryStruct.comp T₁.mor₃ ((shiftFunctor D 1).map a) = CategoryStruct.comp c T₂.mor₃

  a commuting square between the first two vertices extends to the third

theorem CategoryTheory.Pretriangulated.Axioms.comp_eq_zero₁₂ {D : Type u} [Category.{v, u} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] {triangles : Set (Triangle D)} (h : Axioms triangles) (T : Triangle D) (hT : T ∈ triangles) : CategoryStruct.comp T.mor₁ T.mor₂ = 0

Consecutive morphisms of a distinguished triangle compose to zero.

theorem CategoryTheory.Pretriangulated.Axioms.exists_lift₁ {D : Type u} [Category.{v, u} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] {triangles : Set (Triangle D)} (h : Axioms triangles) (T₁ T₂ : Triangle D) (hT₁ : T₁ ∈ triangles) (hT₂ : T₂ ∈ triangles) (b : T₁.obj₂ ⟶ T₂.obj₂) (c : T₁.obj₃ ⟶ T₂.obj₃) (comm : CategoryStruct.comp T₁.mor₂ c = CategoryStruct.comp b T₂.mor₂) : ∃ (a : T₁.obj₁ ⟶ T₂.obj₁), CategoryStruct.comp T₁.mor₁ b = CategoryStruct.comp a T₂.mor₁ ∧ CategoryStruct.comp T₁.mor₃ ((shiftFunctor D 1).map a) = CategoryStruct.comp c T₂.mor₃

The completion axiom against mor₂: a square between the second and third vertices extends backwards to the first.

theorem CategoryTheory.Pretriangulated.Axioms.coyoneda_exact₂ {D : Type u} [Category.{v, u} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] {triangles : Set (Triangle D)} (h : Axioms triangles) (T : Triangle D) (hT : T ∈ triangles) {U : D} (u : U ⟶ T.obj₂) (hu : CategoryStruct.comp u T.mor₂ = 0) : ∃ (v : U ⟶ T.obj₁), u = CategoryStruct.comp v T.mor₁

Hom(U, -) is exact at the second vertex of a distinguished triangle.

theorem CategoryTheory.Pretriangulated.Axioms.mem_of_rotate_mem {D : Type u} [Category.{v, u} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] {triangles : Set (Triangle D)} (h : Axioms triangles) (T : Triangle D) (hT : T.rotate ∈ triangles) : T ∈ triangles

The reverse direction of the rotation axiom is redundant.

@[reducible]

def CategoryTheory.Pretriangulated.Axioms.pretriangulated {D : Type u} [Category.{v, u} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] {triangles : Set (Triangle D)} (h : Axioms triangles) : Pretriangulated D

The Pretriangulated structure carried by a class of triangles satisfying Axioms. The rotation axiom's reverse direction is supplied by mem_of_rotate_mem, so nothing beyond the forward one has to be proved.

Equations

• One or more equations did not get rendered due to their size.