Triangles in full triangulated subcategories

An ambient triangle whose three objects satisfy a triangulated object property has a canonical lift to the corresponding full subcategory. This file owns that construction, its comparison with the ambient triangle, and the lift of triangle morphisms.

Concrete bounded-derived-category adapters should provide only the three objectwise membership proofs. They do not need to repeat the fully faithful preimage construction or manipulate the inclusion's shift comparison.

structure CategoryTheory.ObjectProperty.OnTriangle {C : Type u} [Category.{v, u} C] [HasShift C ℤ] (P : ObjectProperty C) (T : Pretriangulated.Triangle C) : Prop

The assertion that an object property holds on all three objects of a triangle.

• obj₁ : P T.obj₁
• obj₂ : P T.obj₂
• obj₃ : P T.obj₃

noncomputable def CategoryTheory.ObjectProperty.liftTriangle {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] (T : Pretriangulated.Triangle C) (hT : P.OnTriangle T) : Pretriangulated.Triangle P.FullSubcategory

Lift an ambient triangle objectwise to a full triangulated subcategory.

The third morphism is transported through the inverse of the inclusion's shift comparison before fullness is used.

Equations

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

noncomputable def CategoryTheory.ObjectProperty.liftTriangleIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] (T : Pretriangulated.Triangle C) (hT : P.OnTriangle T) : P.ι.mapTriangle.obj (P.liftTriangle T hT) ≅ T

The canonical comparison from the image of a lifted triangle to its ambient triangle.

Equations

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

theorem CategoryTheory.ObjectProperty.liftTriangle_distinguished {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] (T : Pretriangulated.Triangle C) (hT : P.OnTriangle T) (h : T ∈ Pretriangulated.distinguishedTriangles) : P.liftTriangle T hT ∈ Pretriangulated.distinguishedTriangles

A distinguished ambient triangle with objects in P lifts to a distinguished triangle in the full subcategory.

noncomputable def CategoryTheory.ObjectProperty.liftTriangleMap {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] {T₁ T₂ : Pretriangulated.Triangle C} (hT₁ : P.OnTriangle T₁) (hT₂ : P.OnTriangle T₂) (f : T₁ ⟶ T₂) : P.liftTriangle T₁ hT₁ ⟶ P.liftTriangle T₂ hT₂

Lift a morphism of ambient triangles to the corresponding objectwise lifts in a full triangulated subcategory.

Equations

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

@[simp]

theorem CategoryTheory.ObjectProperty.map_liftTriangleMap {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] {T₁ T₂ : Pretriangulated.Triangle C} (hT₁ : P.OnTriangle T₁) (hT₂ : P.OnTriangle T₂) (f : T₁ ⟶ T₂) : P.ι.mapTriangle.map (P.liftTriangleMap hT₁ hT₂ f) = CategoryStruct.comp (P.liftTriangleIso T₁ hT₁).hom (CategoryStruct.comp f (P.liftTriangleIso T₂ hT₂).inv)

The image of a lifted triangle map is the ambient map conjugated by the canonical comparison isomorphisms.

theorem CategoryTheory.ObjectProperty.liftTriangleMap_ambient {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] {T₁ T₂ : Pretriangulated.Triangle C} (hT₁ : P.OnTriangle T₁) (hT₂ : P.OnTriangle T₂) (f : T₁ ⟶ T₂) : CategoryStruct.comp (P.liftTriangleIso T₁ hT₁).inv (CategoryStruct.comp (P.ι.mapTriangle.map (P.liftTriangleMap hT₁ hT₂ f)) (P.liftTriangleIso T₂ hT₂).hom) = f

After identifying both images with their ambient triangles, a lifted map is exactly the original triangle map.

theorem CategoryTheory.ObjectProperty.liftTriangleMap_id {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] (T : Pretriangulated.Triangle C) (hT : P.OnTriangle T) : P.liftTriangleMap hT hT (CategoryStruct.id T) = CategoryStruct.id (P.liftTriangle T hT)

Lifting preserves identity triangle maps.

theorem CategoryTheory.ObjectProperty.liftTriangleMap_comp {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [P.IsTriangulated] {T₁ T₂ T₃ : Pretriangulated.Triangle C} (hT₁ : P.OnTriangle T₁) (hT₂ : P.OnTriangle T₂) (hT₃ : P.OnTriangle T₃) (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) : P.liftTriangleMap hT₁ hT₃ (CategoryStruct.comp f g) = CategoryStruct.comp (P.liftTriangleMap hT₁ hT₂ f) (P.liftTriangleMap hT₂ hT₃ g)

Lifting preserves composition of triangle maps.