Restriction of semiorthogonal sequences

A zero-preserving faithful functor reflects the vanishing that defines a semiorthogonal sequence. Consequently a sequence on the target restricts to the inverse-image components on the source. The intended consumer is a fully faithful inclusion of a bounded or coherent full subcategory.

The second half restricts a chosen right projection along the inclusion of an object property, provided the ambient projection preserves that property. This is the precise categorical obligation needed when passing a strong semiorthogonal decomposition to a bounded subcategory.

Preserves is stated for one property at a time and is closed under conjunction, so a restriction whose defining property is a conjunction -- a bounded and coherent locus, say -- splits into one obligation per conjunct.

def CategoryTheory.Triangulated.SemiorthogonalSequence.inverseImage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] {ι : Type w} [Preorder ι] (T : SemiorthogonalSequence D ι) (F : Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] : SemiorthogonalSequence C ι

Restrict a semiorthogonal sequence along a faithful functor that preserves zero morphisms. Each component is pulled back as an object property.

Equations

• T.inverseImage F = { component := fun (i : ι) => (T.component i).inverseImage F, semiorthogonal := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.inverseImage_component {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] {ι : Type w} [Preorder ι] (T : SemiorthogonalSequence D ι) (F : Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] (i : ι) : (T.inverseImage F).component i = (T.component i).inverseImage F

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.inverseImage_compatible {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] {ι : Type w} [Preorder ι] (T : SemiorthogonalSequence D ι) (F : Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] : (T.inverseImage F).CompatibleWith F T

The restricting functor is tautologically compatible with the restricted and ambient sequences.

def CategoryTheory.ObjectProperty.RightProjectionData.inverseImageInclusion {C : Type u₁} [Category.{v₁, u₁} C] {P Q : ObjectProperty C} : Functor (Q.inverseImage P.ι).FullSubcategory Q.FullSubcategory

Forget that an object of P lies in the inverse image of Q, retaining its Q-membership in the ambient category.

Equations

• CategoryTheory.ObjectProperty.RightProjectionData.inverseImageInclusion = Q.lift ((Q.inverseImage P.ι).ι.comp P.ι) ⋯

def CategoryTheory.ObjectProperty.RightProjectionData.inverseImageInclusionFullyFaithful {C : Type u₁} [Category.{v₁, u₁} C] {P Q : ObjectProperty C} : inverseImageInclusion.FullyFaithful

The inverse-image inclusion is fully faithful.

Equations

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

def CategoryTheory.ObjectProperty.RightProjectionData.restrictedProjection {C : Type u₁} [Category.{v₁, u₁} C] {P Q : ObjectProperty C} (R : Q.RightProjectionData) (hP : P ≤ P.inverseImage R.ambientProjection) : Functor P.FullSubcategory (Q.inverseImage P.ι).FullSubcategory

The right projection restricted to P, landing in the inverse-image component inside P.FullSubcategory. The preservation hypothesis says that the projected ambient object still lies in P.

Equations

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

noncomputable def CategoryTheory.ObjectProperty.RightProjectionData.restrict {C : Type u₁} [Category.{v₁, u₁} C] {P Q : ObjectProperty C} (R : Q.RightProjectionData) (hP : P ≤ P.inverseImage R.ambientProjection) : (Q.inverseImage P.ι).RightProjectionData

A chosen right projection restricts along a full-subcategory inclusion when its ambient endofunctor preserves the defining object property.

Equations

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

def CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.Preserves {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {ι : Type w} [Preorder ι] {S : SemiorthogonalSequence C ι} (Q : S.RightProjectionData) (P : ObjectProperty C) : Prop

All component projections preserve an object property P.

Equations

• Q.Preserves P = ∀ (i : ι), P ≤ P.inverseImage (Q.ambientProjection i)

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.Preserves.of_iff {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {ι : Type w} [Preorder ι] {S : SemiorthogonalSequence C ι} {Q : S.RightProjectionData} {P₁ P₂ : ObjectProperty C} (h : ∀ (X : C), P₁ X ↔ P₂ X) (hP : Q.Preserves P₁) : Q.Preserves P₂

Preservation only depends on the objects a property holds of.

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.Preserves.inf {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] {ι : Type w} [Preorder ι] {S : SemiorthogonalSequence C ι} {Q : S.RightProjectionData} {P₁ P₂ : ObjectProperty C} (hP₁ : Q.Preserves P₁) (hP₂ : Q.Preserves P₂) : Q.Preserves (P₁ ⊓ P₂)

Two preserved properties are preserved together.

noncomputable def CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.restrict {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] {S : SemiorthogonalSequence C ι} (Q : S.RightProjectionData) (P : ObjectProperty C) [P.IsTriangulated] (hP : Q.Preserves P) : (S.inverseImage P.ι).RightProjectionData

Restrict all chosen component projections to a full subcategory.

Equations

• Q.restrict P hP = { componentProjection := fun (i : ι) => (Q.componentProjection i).restrict ⋯ }

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.inverseImage_isStrong {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {ι : Type w} [Preorder ι] {S : SemiorthogonalSequence C ι} (Q : S.RightProjectionData) (P : ObjectProperty C) [P.IsTriangulated] (hS : S.HasTriangulatedComponents) (hIso : ∀ (i : ι), (S.component i).IsClosedUnderIsomorphisms) (hP : Q.Preserves P) : (S.inverseImage P.ι).IsStrong

Restricting chosen projections proves that the inverse-image sequence is strong in the paper's sense. Repleteness of the ambient components is needed to transport their triangulated closure through the inclusion.