Strong semiorthogonal decompositions and compatible functors

This file records the vocabulary of Definitions 3.3, 3.5, and 3.7 of arXiv:1902.08184 without adding any geometric existence claim.

Here strong has the paper's meaning: every component is right admissible. It is deliberately distinct from SemiorthogonalSequence.IsStronglyFull, which says that the components generate after uniformly many extensions.

A compatible functor carries each source component into the component with the same index. Chosen component projections are kept as data, separately from proposition-valued admissibility, and their underlying ambient endofunctors can be assigned a cohomological amplitude relative to a t-structure.

def CategoryTheory.Functor.HasCohomologicalAmplitude {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (F : Functor C D) (t : Triangulated.TStructure C) (t' : Triangulated.TStructure D) (a b : ℤ) : Prop

A functor has cohomological amplitude [a, b] if it sends every t-cohomological window [p, q] into the target window [p + a, q + b]. This is Definition 3.7 of arXiv:1902.08184.

Equations

• F.HasCohomologicalAmplitude t t' a b = ∀ (p q : ℤ) (X : C), t.IsGE X p → t.IsLE X q → t'.IsGE (F.obj X) (p + a) ∧ t'.IsLE (F.obj X) (q + b)

theorem CategoryTheory.Functor.hasCohomologicalAmplitude_zero {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (F : Functor C D) (t : Triangulated.TStructure C) (t' : Triangulated.TStructure D) [F.IsTExact t t'] : F.HasCohomologicalAmplitude t t' 0 0

A t-exact functor has cohomological amplitude [0, 0].

theorem CategoryTheory.Functor.HasCohomologicalAmplitude.weaken {C : Type u₁} [Category.{v₁, u₁} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Preadditive D] [Limits.HasZeroObject D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {F : Functor C D} {t : Triangulated.TStructure C} {t' : Triangulated.TStructure D} {a b a' b' : ℤ} (hF : F.HasCohomologicalAmplitude t t' a b) (ha : a' ≤ a) (hb : b ≤ b') : F.HasCohomologicalAmplitude t t' a' b'

An amplitude interval can be enlarged on either side.

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

A functor is compatible with two semiorthogonal sequences when it maps the component at every index into the component with the same index. This is Definition 3.3 of arXiv:1902.08184.

Equations

• S.CompatibleWith F T = ∀ (i : ι), S.component i ≤ (T.component i).inverseImage F

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.compatibleWith_id {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) : S.CompatibleWith (Functor.id C) S

The identity functor is compatible with a sequence.

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.CompatibleWith.comp {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] {ι : Type w} [Preorder ι] (S : SemiorthogonalSequence C ι) {E : Type u_1} [Category.{u_2, u_1} E] [Limits.HasZeroMorphisms E] {T : SemiorthogonalSequence D ι} {U : SemiorthogonalSequence E ι} {F : Functor C D} {G : Functor D E} (hF : S.CompatibleWith F T) (hG : T.CompatibleWith G U) : S.CompatibleWith (F.comp G) U

Compatibility is closed under composition.

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

A strong semiorthogonal sequence in the sense of Definition 3.5 of arXiv:1902.08184: every component is right admissible.

Equations

• S.IsStrong = ∀ (i : ι), (S.component i).IsRightAdmissible

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

Strongness supplies triangulated closure of every component.

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

A simultaneous choice of right-adjoint projections for all components of a semiorthogonal sequence.

• componentProjection (i : ι) : (S.component i).RightProjectionData

  The chosen right projection onto the component at i.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.ambientProjection {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] {S : SemiorthogonalSequence C ι} (Q : S.RightProjectionData) (i : ι) : Functor C C

The ambient endofunctor projecting onto component i.

Equations

• Q.ambientProjection i = (Q.componentProjection i).ambientProjection

def CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.HasCohomologicalAmplitude {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] {ι : Type w} [Preorder ι] {S : SemiorthogonalSequence C ι} [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Q : S.RightProjectionData) (t : TStructure C) (a b : ℤ) : Prop

All component projections have the specified cohomological amplitude.

Equations

• Q.HasCohomologicalAmplitude t a b = ∀ (i : ι), (Q.ambientProjection i).HasCohomologicalAmplitude t t a b

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

Choose projection data for every component of a strong sequence.

Equations

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