Semiorthogonal sequences

This file defines the generic root for semiorthogonal decompositions. The root is a sequence of object properties with the expected ordered Hom-vanishing. Generation, strong generation, and closure of the components under the triangulated operations are deliberately separate predicates: none of them is smuggled into the carrier.

The components are object properties rather than new full subcategory structures. This lets the root reuse Mathlib's orthogonals and triangulated envelope, and lets geometric realizations add their own closure and base-change theorems without creating a sibling hierarchy.

instance CategoryTheory.ObjectProperty.rightOrthogonal_isStableUnderRetracts {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : P.rightOrthogonal.IsStableUnderRetracts

The right orthogonal of any property is stable under retracts: a map from a P-object into a retract extends to the ambient object, where it vanishes.

instance CategoryTheory.ObjectProperty.leftOrthogonal_isStableUnderRetracts {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : P.leftOrthogonal.IsStableUnderRetracts

The left orthogonal of any property is stable under retracts.

structure CategoryTheory.Triangulated.SemiorthogonalSequence (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] (ι : Type w) [Preorder ι] : Type (max u w)

An ordered family of object properties in which maps from an earlier component to a later component vanish. Fullness and triangulated closure are independent refinements below.

• component : ι → ObjectProperty C

  The component at an index.

• semiorthogonal ⦃i j : ι⦄ : i < j → self.component j ≤ (self.component i).rightOrthogonal

  Maps from an earlier component to a later component vanish.

def CategoryTheory.Triangulated.SemiorthogonalSequence.total {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) : ObjectProperty C

The property of lying in one of the components. This is the common generator property used by both classical and strong fullness.

Equations

• S.total = ⨆ (i : ι), S.component i

def CategoryTheory.Triangulated.SemiorthogonalSequence.residual {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) : ObjectProperty C

The residual object property of a semiorthogonal sequence: the right orthogonal to the union of its components. This definition does not assert that the sequence is full or that its components are admissible.

Equations

• S.residual = S.total.rightOrthogonal

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.component_le_total {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) (i : ι) : S.component i ≤ S.total

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.hom_eq_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) ⦃i j : ι⦄ (hij : i < j) ⦃X Y : C⦄ (hX : S.component i X) (hY : S.component j Y) (f : X ⟶ Y) : f = 0

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.component_hom_residual_eq_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) (i : ι) ⦃X Y : C⦄ (hX : S.component i X) (hY : S.residual Y) (f : X ⟶ Y) : f = 0

Maps from any component of the sequence to a residual object vanish.

def CategoryTheory.Triangulated.SemiorthogonalSequence.HasTriangulatedComponents {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Prop

Each component is a triangulated object property. This is independent of fullness.

Equations

• S.HasTriangulatedComponents = ∀ (i : ι), (S.component i).IsTriangulated

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.HasTriangulatedComponents.totalIsStableUnderShift {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (hS : S.HasTriangulatedComponents) : S.total.IsStableUnderShift ℤ

The union of triangulated components is stable under shifts. The union need not itself be extension-closed, which is why this conclusion is stated only at the strength needed by orthogonal closure.

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.HasTriangulatedComponents.residual_isTriangulated {D : Type u_1} [Category.{u_3, u_1} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {κ : Type u_2} [Preorder κ] {T : SemiorthogonalSequence D κ} (hT : T.HasTriangulatedComponents) : T.residual.IsTriangulated

The residual of a sequence with triangulated components is triangulated. No fullness or admissibility hypothesis is required for this closure fact.

def CategoryTheory.Triangulated.SemiorthogonalSequence.IsFull {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Prop

Classical fullness: the union of the components generates under shifts, binary products, retracts, and arbitrarily many extensions.

Equations

• S.IsFull = S.total.IsClassicalTriangulatedGenerator

def CategoryTheory.Triangulated.SemiorthogonalSequence.IsStronglyFull {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Prop

Strong fullness: the union of the components generates after a uniformly bounded number of extensions. This is stronger than IsFull, not a field of the sequence.

Equations

• S.IsStronglyFull = S.total.IsStrongTriangulatedGenerator

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.IsStronglyFull.isFull {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (hS : S.IsStronglyFull) : S.IsFull

def CategoryTheory.Triangulated.SemiorthogonalSequence.map {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) {D : Type u_1} [Category.{v_1, u_1} D] [Limits.HasZeroMorphisms D] (F : Functor C D) (h : ∀ ⦃i j : ι⦄, i < j → (S.component j).map F ≤ ((S.component i).map F).rightOrthogonal) : SemiorthogonalSequence D ι

Transport the components along a functor once orthogonality of their essential images has been proved in the target. In particular, a geometric pullback theorem supplies h; pullback is not a field of the semiorthogonal sequence.

Equations

• S.map F h = { component := fun (i : ι) => (S.component i).map F, semiorthogonal := h }

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.map_component {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) {D : Type u_1} [Category.{v_1, u_1} D] [Limits.HasZeroMorphisms D] (F : Functor C D) (h : ∀ ⦃i j : ι⦄, i < j → (S.component j).map F ≤ ((S.component i).map F).rightOrthogonal) (i : ι) : (S.map F h).component i = (S.component i).map F

def CategoryTheory.Triangulated.SemiorthogonalSequence.reindex {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) {κ : Type u_1} [Preorder κ] (f : κ → ι) (hf : ∀ ⦃i j : κ⦄, i < j → f i < f j) : SemiorthogonalSequence C κ

Restrict a semiorthogonal sequence along a strictly monotone map of index types.

Equations

• S.reindex f hf = { component := fun (i : κ) => S.component (f i), semiorthogonal := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.reindex_component {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) {κ : Type u_1} [Preorder κ] (f : κ → ι) (hf : ∀ ⦃i j : κ⦄, i < j → f i < f j) (i : κ) : (S.reindex f hf).component i = S.component (f i)