Basic semiorthogonal sequences

Two inhabitants keep the generic root honest before any geometry is introduced:

• the one-block sequence, which is strongly full;
• the two-block sequence on a product category, whose blocks are the two factors.

Mathlib does not currently put zero morphisms on product categories, so this file supplies the componentwise instance. No preadditive or pretriangulated product instance is asserted.

@[implicit_reducible]

instance CategoryTheory.Limits.productHasZeroMorphisms (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] : HasZeroMorphisms (C × D)

Product categories inherit zero morphisms componentwise.

Equations

• CategoryTheory.Limits.productHasZeroMorphisms C D = { zero := fun (X Y : C × D) => { zero := (0, 0) }, comp_zero := ⋯, zero_comp := ⋯ }

def CategoryTheory.Triangulated.SemiorthogonalSequence.single {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] : SemiorthogonalSequence C (Fin 1)

The one-block semiorthogonal sequence.

Equations

• CategoryTheory.Triangulated.SemiorthogonalSequence.single = { component := fun (x : Fin 1) => ⊤, semiorthogonal := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.single_component {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] (i : Fin 1) : single.component i = ⊤

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.single_total {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] : single.total = ⊤

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.single_isStronglyFull {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : single.IsStronglyFull

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.single_isFull {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : single.IsFull

def CategoryTheory.Triangulated.SemiorthogonalSequence.productComponent {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (i : Fin 2) : ObjectProperty (C × D)

The two factor properties on C × D. The first block consists of objects whose second component is zero; the second block consists of objects whose first component is zero.

Equations

• CategoryTheory.Triangulated.SemiorthogonalSequence.productComponent i = if i = 0 then fun (X : C × D) => CategoryTheory.Limits.IsZero X.2 else fun (X : C × D) => CategoryTheory.Limits.IsZero X.1

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.productComponent_zero {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] : productComponent 0 = fun (X : C × D) => Limits.IsZero X.2

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.productComponent_one {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] : productComponent 1 = fun (X : C × D) => Limits.IsZero X.1

def CategoryTheory.Triangulated.SemiorthogonalSequence.product {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] : SemiorthogonalSequence (C × D) (Fin 2)

The factors of a product category form a two-block semiorthogonal sequence.

Equations

• CategoryTheory.Triangulated.SemiorthogonalSequence.product = { component := CategoryTheory.Triangulated.SemiorthogonalSequence.productComponent, semiorthogonal := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.product_component {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (i : Fin 2) : product.component i = productComponent i