Finite cohomological amplitude and the bounded restriction

SemiorthogonalDecomposition/Strong.lean records Definition 3.7 of arXiv:1902.08184 -- a functor has cohomological amplitude [a, b] when it carries the t-cohomological window [p, q] into [p + a, q + b] -- and the amplitude of a chosen family of component projections. This file draws the consequence that a bounded restriction needs: a functor of finite amplitude carries t-bounded objects to t'-bounded objects, so chosen projections of finite amplitude preserve the bounded object property and therefore restrict along its inclusion, and the restricted sequence is again strong.

Finiteness is recorded twice. Functor.HasFiniteCohomologicalAmplitude existentially quantifies the interval, and the projection-data version quantifies it separately at each index. The interval is deliberately not uniform over the index: preserving boundedness never needs one interval to work for every component at once, and a uniform demand would exclude an infinite sequence whose component amplitudes grow.

Nothing here asserts that any projection has finite amplitude. That is a geometric input. What is formal is only the passage from amplitude to preservation, to restriction, and to strongness of the restricted sequence.

theorem CategoryTheory.Functor.HasCohomologicalAmplitude.isGE {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 : ℤ} (hF : F.HasCohomologicalAmplitude t t' a b) (p q : ℤ) (X : C) (hGE : t.IsGE X p) (hLE : t.IsLE X q) : t'.IsGE (F.obj X) (p + a)

The bounded-below half of an amplitude bound.

theorem CategoryTheory.Functor.HasCohomologicalAmplitude.isLE {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 : ℤ} (hF : F.HasCohomologicalAmplitude t t' a b) (p q : ℤ) (X : C) (hGE : t.IsGE X p) (hLE : t.IsLE X q) : t'.IsLE (F.obj X) (q + b)

The bounded-above half of an amplitude bound.

theorem CategoryTheory.Functor.HasCohomologicalAmplitude.comp {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] {E : Type u₃} [Category.{v₃, u₃} E] [Preadditive E] [Limits.HasZeroObject E] [HasShift E ℤ] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated E] {F : Functor C D} {G : Functor D E} {t : Triangulated.TStructure C} {t' : Triangulated.TStructure D} {t'' : Triangulated.TStructure E} {a b a' b' : ℤ} (hF : F.HasCohomologicalAmplitude t t' a b) (hG : G.HasCohomologicalAmplitude t' t'' a' b') : (F.comp G).HasCohomologicalAmplitude t t'' (a + a') (b + b')

Amplitudes add along a composite.

theorem CategoryTheory.Functor.HasCohomologicalAmplitude.bounded_le {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 : ℤ} (hF : F.HasCohomologicalAmplitude t t' a b) : t.bounded ≤ t'.bounded.inverseImage F

A functor with an amplitude bound carries t-bounded objects to t'-bounded objects. The witnessing integers move, so the conclusion is membership in the bounded locus and not a bound on a fixed window.

def CategoryTheory.Functor.HasFiniteCohomologicalAmplitude {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) : Prop

A functor has finite cohomological amplitude when some interval bounds it. The interval is not retained: every consequence drawn here is insensitive to which one works.

Equations

• F.HasFiniteCohomologicalAmplitude t t' = ∃ (a : ℤ) (b : ℤ), F.HasCohomologicalAmplitude t t' a b

theorem CategoryTheory.Functor.HasCohomologicalAmplitude.hasFinite {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 : ℤ} (hF : F.HasCohomologicalAmplitude t t' a b) : F.HasFiniteCohomologicalAmplitude t t'

A named amplitude interval is in particular a finite one.

theorem CategoryTheory.Functor.hasFiniteCohomologicalAmplitude_of_isTExact {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.HasFiniteCohomologicalAmplitude t t'

A t-exact functor has finite cohomological amplitude.

theorem CategoryTheory.Functor.HasFiniteCohomologicalAmplitude.bounded_le {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} (hF : F.HasFiniteCohomologicalAmplitude t t') : t.bounded ≤ t'.bounded.inverseImage F

Finite amplitude is enough to carry bounded objects to bounded objects.

theorem CategoryTheory.Functor.HasFiniteCohomologicalAmplitude.comp {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] {E : Type u₃} [Category.{v₃, u₃} E] [Preadditive E] [Limits.HasZeroObject E] [HasShift E ℤ] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated E] {F : Functor C D} {G : Functor D E} {t : Triangulated.TStructure C} {t' : Triangulated.TStructure D} {t'' : Triangulated.TStructure E} (hF : F.HasFiniteCohomologicalAmplitude t t') (hG : G.HasFiniteCohomologicalAmplitude t' t'') : (F.comp G).HasFiniteCohomologicalAmplitude t t''

Finite amplitude is closed under composition.

def CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.HasFiniteCohomologicalAmplitude {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) (t : TStructure C) : Prop

Every chosen component projection has finite cohomological amplitude, by an interval that may depend on the index.

Equations

• Q.HasFiniteCohomologicalAmplitude t = ∀ (i : ι), (Q.ambientProjection i).HasFiniteCohomologicalAmplitude t t

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.HasCohomologicalAmplitude.hasFinite {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} {t : TStructure C} {a b : ℤ} (h : Q.HasCohomologicalAmplitude t a b) : Q.HasFiniteCohomologicalAmplitude t

A uniform amplitude interval is in particular a finite one at each index.

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.HasFiniteCohomologicalAmplitude.preserves_bounded {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} {t : TStructure C} (h : Q.HasFiniteCohomologicalAmplitude t) : Q.Preserves t.bounded

Projections of finite amplitude preserve the bounded object property. This is the whole formal content of the bounded restriction: the obligation Preserves records is discharged by an amplitude bound and by nothing else about the projection.

noncomputable def CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.HasFiniteCohomologicalAmplitude.boundedProjections {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} {t : TStructure C} (h : Q.HasFiniteCohomologicalAmplitude t) : (S.inverseImage t.bounded.ι).RightProjectionData

The chosen projections restricted to the t-bounded locus.

Equations

• h.boundedProjections = Q.restrict t.bounded ⋯

theorem CategoryTheory.Triangulated.SemiorthogonalSequence.RightProjectionData.HasFiniteCohomologicalAmplitude.inverseImage_bounded_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} {t : TStructure C} (hS : S.HasTriangulatedComponents) (hIso : ∀ (i : ι), (S.component i).IsClosedUnderIsomorphisms) (h : Q.HasFiniteCohomologicalAmplitude t) : (S.inverseImage t.bounded.ι).IsStrong

The bounded restriction of a sequence whose chosen projections have finite amplitude is again strong in the sense of Definition 3.5.