Admissible triangulated object properties

An object property is right (respectively left) admissible when the inclusion of its full subcategory has a right (respectively left) adjoint. Completing the counit (respectively unit) of that adjunction gives the two orthogonal decomposition triangles.

For a right-admissible P, the third vertex of the counit triangle is the object usually called the left mutation of X through P. This file deliberately records the triangle and not a mutation object or functor. Cones are not functorial in a bare triangulated category, so a mutation functor needs an enhancement (the dg-enhancement lane, issues #853--#855). The familiar formula for mutation through an exceptional object additionally needs finite-dimensional Hom spaces, which are outside the present coherent-sheaf linearity interface (issue #332).

No theorem here claims that an arbitrary triangulated object property is admissible, or that an operation on object properties preserves admissibility. Admissibility remains an explicit hypothesis in every decomposition theorem.

The two-block construction feeds the classically ordered family ⟨P.rightOrthogonal, P⟩ to SemiorthogonalSequence.ofReverseFin. Thus its root-facing components are P followed by P.rightOrthogonal: the root vanishes Hom from earlier to later, while the literature reads a semiorthogonal decomposition in the reverse direction. Orientation.lean is the single source of truth for that convention.

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.zeroObjects {C : Type u} [Category.{v, u} C] : ObjectProperty C

The object property of being a zero object.

Equations

• CategoryTheory.ObjectProperty.zeroObjects X = CategoryTheory.Limits.IsZero X

instance CategoryTheory.ObjectProperty.topIsTriangulated {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : ⊤.IsTriangulated

The top object property is triangulated.

instance CategoryTheory.ObjectProperty.zeroObjectsIsClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] : zeroObjects.IsClosedUnderIsomorphisms

Being a zero object is invariant under isomorphism.

instance CategoryTheory.ObjectProperty.zeroObjectsIsTriangulated {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : zeroObjects.IsTriangulated

Zero objects form a triangulated object property.

def CategoryTheory.ObjectProperty.IsRightAdmissible {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : Prop

An object property is right admissible when it is triangulated and its inclusion has a right adjoint.

Equations

• P.IsRightAdmissible = (P.IsTriangulated ∧ ∃ (G : CategoryTheory.Functor C P.FullSubcategory), Nonempty (P.ι ⊣ G))

def CategoryTheory.ObjectProperty.IsLeftAdmissible {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : Prop

An object property is left admissible when it is triangulated and its inclusion has a left adjoint.

Equations

• P.IsLeftAdmissible = (P.IsTriangulated ∧ ∃ (L : CategoryTheory.Functor C P.FullSubcategory), Nonempty (L ⊣ P.ι))

def CategoryTheory.ObjectProperty.IsAdmissible {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : Prop

A triangulated object property is admissible when it is both left and right admissible.

Equations

• P.IsAdmissible = (P.IsLeftAdmissible ∧ P.IsRightAdmissible)

theorem CategoryTheory.ObjectProperty.top_isRightAdmissible {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : ⊤.IsRightAdmissible

The top object property is right admissible, through its canonical equivalence with C.

theorem CategoryTheory.ObjectProperty.top_isLeftAdmissible {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : ⊤.IsLeftAdmissible

The top object property is left admissible, through its canonical equivalence with C.

theorem CategoryTheory.ObjectProperty.zeroObjects_isRightAdmissible {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : zeroObjects.IsRightAdmissible

Zero objects are right admissible: the right adjoint is the constant zero functor.

theorem CategoryTheory.ObjectProperty.zeroObjects_isLeftAdmissible {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : zeroObjects.IsLeftAdmissible

Zero objects are left admissible: the left adjoint is the constant zero functor.

theorem CategoryTheory.ObjectProperty.IsRightAdmissible.exists_distTriang_mem_rightOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} (hP : P.IsRightAdmissible) (X : C) : P.extensionProduct P.rightOrthogonal X

The counit triangle of a right-admissible property has its third vertex in the right orthogonal. The right adjoint is triangulated because it is adjoint to the triangulated inclusion; after applying it, full faithfulness makes the mapped counit an isomorphism, hence its cone a zero object.

theorem CategoryTheory.ObjectProperty.IsLeftAdmissible.exists_distTriang_mem_leftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} (hP : P.IsLeftAdmissible) (X : C) : P.leftOrthogonal.extensionProduct P X

The unit triangle of a left-admissible property has its first vertex in the left orthogonal.

theorem CategoryTheory.ObjectProperty.IsRightAdmissible.extensionProduct_rightOrthogonal_eq_top {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} (hP : P.IsRightAdmissible) : P.extensionProduct P.rightOrthogonal = ⊤

Right admissibility is equivalently consumed as the equality saying that every object is an extension of an object of P by an object of P.rightOrthogonal.

theorem CategoryTheory.ObjectProperty.IsLeftAdmissible.leftOrthogonal_extensionProduct_eq_top {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P : ObjectProperty C} (hP : P.IsLeftAdmissible) : P.leftOrthogonal.extensionProduct P = ⊤

The dual extension-product form of left admissibility.

@[simp]

theorem CategoryTheory.ObjectProperty.top_rightOrthogonal {C : Type u} [Category.{v, u} C] [Preadditive C] : ⊤.rightOrthogonal = zeroObjects

The right orthogonal of all objects is precisely the zero-object property.

@[simp]

theorem CategoryTheory.ObjectProperty.zeroObjects_rightOrthogonal {C : Type u} [Category.{v, u} C] [Preadditive C] : zeroObjects.rightOrthogonal = ⊤

Every object is right orthogonal to the zero objects.

def CategoryTheory.Triangulated.SemiorthogonalSequence.twoBlock {C : Type u} [Category.{v, u} C] [Preadditive C] (P : ObjectProperty C) : SemiorthogonalSequence C (Fin 2)

The root-facing two-block sequence attached to P and its right orthogonal.

It is constructed by passing the classically ordered family ![P.rightOrthogonal, P] to ofReverseFin; consequently component 0 is P and component 1 is P.rightOrthogonal. See Orientation.lean for the convention reversal.

Equations

• CategoryTheory.Triangulated.SemiorthogonalSequence.twoBlock P = CategoryTheory.Triangulated.SemiorthogonalSequence.ofReverseFin 2 ![P.rightOrthogonal, P] ⋯

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.twoBlock_component_zero {C : Type u} [Category.{v, u} C] [Preadditive C] (P : ObjectProperty C) : (twoBlock P).component 0 = P

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.twoBlock_component_one {C : Type u} [Category.{v, u} C] [Preadditive C] (P : ObjectProperty C) : (twoBlock P).component 1 = P.rightOrthogonal

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.twoBlock_hasTriangulatedComponents {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (hP : P.IsRightAdmissible) : (twoBlock P).HasTriangulatedComponents

The two blocks are triangulated object properties.

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.twoBlock_isStronglyFull {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (hP : P.IsRightAdmissible) : (twoBlock P).IsStronglyFull

A right-admissible two-block sequence is strongly full with the explicit bound 1. triangEnvelopeIter 0 already closes under shifts, binary products and retracts; the counit triangle contributes the single extension counted by triangEnvelopeIter_succ.

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.twoBlock_top_component {C : Type u} [Category.{v, u} C] [Preadditive C] (i : Fin 2) : (twoBlock ⊤).component i = if i = 0 then ⊤ else ObjectProperty.zeroObjects

For P = ⊤, the two blocks are all objects followed by the zero objects.

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.twoBlock_zeroObjects_component {C : Type u} [Category.{v, u} C] [Preadditive C] (i : Fin 2) : (twoBlock ObjectProperty.zeroObjects).component i = if i = 0 then ObjectProperty.zeroObjects else ⊤

For the zero-object property, the two blocks are zero objects followed by all objects.