Mass--Hom bounds on bounded coherent derived categories

This file only identifies the geometric test class. It does not manufacture Hom-finiteness: a consumer must supply the appropriate geometric finiteness input before forming a mass--Hom bound.

def AlgebraicGeometry.DerivedCategory.boundedSchemePerfect (X : Scheme) [IsLocallyNoetherian X] : CategoryTheory.ObjectProperty (SchemeBoundedCoherentDerivedCategory X)

Perfect objects viewed inside Dᵇ(Coh X). The property is the inverse image of schemePerfect X along the fully faithful bounded inclusion.

Equations

• AlgebraicGeometry.DerivedCategory.boundedSchemePerfect X = (AlgebraicGeometry.DerivedCategory.schemePerfect X).inverseImage DerivedCategory.Bounded.ι

@[simp]

theorem AlgebraicGeometry.DerivedCategory.boundedSchemePerfect_iff (X : Scheme) [IsLocallyNoetherian X] (E : SchemeBoundedCoherentDerivedCategory X) : boundedSchemePerfect X E ↔ schemePerfect X (DerivedCategory.Bounded.ι.obj E)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.HasPerfectMassHomBound {k : Type w} [Field k] (X : Scheme) [IsLocallyNoetherian X] [CategoryTheory.Linear k (SchemeBoundedCoherentDerivedCategory X)] [CategoryTheory.SerreFunctor.HomFinite k (SchemeBoundedCoherentDerivedCategory X)] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ (SchemeBoundedCoherentDerivedCategory X) →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap (SchemeBoundedCoherentDerivedCategory X) v) : Prop

The mass--Hom predicate specialized to perfect test objects in Dᵇ(Coh X). Hom-finiteness and k-linearity stay explicit inputs.

Equations

• AlgebraicGeometry.DerivedCategory.HasPerfectMassHomBound X σ = σ.HasMassHomBound (AlgebraicGeometry.DerivedCategory.boundedSchemePerfect X)

theorem AlgebraicGeometry.DerivedCategory.hasPerfectMassHomBound_of_stable_generators {k : Type w} [Field k] (X : Scheme) [IsLocallyNoetherian X] [CategoryTheory.Linear k (SchemeBoundedCoherentDerivedCategory X)] [∀ (n : ℤ), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor (SchemeBoundedCoherentDerivedCategory X) n)] [CategoryTheory.SerreFunctor.HomFinite k (SchemeBoundedCoherentDerivedCategory X)] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ (SchemeBoundedCoherentDerivedCategory X) →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap (SchemeBoundedCoherentDerivedCategory X) v) (G : CategoryTheory.ObjectProperty (SchemeBoundedCoherentDerivedCategory X)) (hG : G.triangEnvelope = boundedSchemePerfect X) (hJH : σ.slicing.HasJordanHolderFiltrations) (hstable : σ.HasStableMassHomBound G) : HasPerfectMassHomBound X σ

Remark 7.2: stable-target bounds on a classically generating collection give the perfect mass--Hom bound. Classical generation is kept as the explicit equality G.triangEnvelope = boundedSchemePerfect X; this abstract adapter does not manufacture a geometric generating theorem.

Finite pullback transfer

theorem AlgebraicGeometry.DerivedCategory.hasPerfectMassHomBound_finitePullback {S : Scheme} {T U : Families.SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [IsFinite (CategoryTheory.Over.Hom.left f)] {k : Type w} [Field k] [CategoryTheory.Linear k T.BoundedCoherentDerivedFiber] [CategoryTheory.Linear k U.BoundedCoherentDerivedFiber] [∀ (n : ℤ), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor T.BoundedCoherentDerivedFiber n)] [CategoryTheory.SerreFunctor.HomFinite k T.BoundedCoherentDerivedFiber] [CategoryTheory.SerreFunctor.HomFinite k U.BoundedCoherentDerivedFiber] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ U.BoundedCoherentDerivedFiber →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap U.BoundedCoherentDerivedFiber v) (hσ : HasPerfectMassHomBound (CategoryTheory.Over.left U) σ) (hpre : Families.SchemeBaseChange.BoundedCoherentPushforwardPreimageData f σ.slicing) (pull : CategoryTheory.Functor U.BoundedCoherentDerivedFiber T.BoundedCoherentDerivedFiber) [pull.Additive] [CategoryTheory.Functor.Linear k pull] (adj : pull ⊣ Families.SchemeBaseChange.boundedCoherentDerivedPushforward f) (hgen : boundedSchemePerfect (CategoryTheory.Over.left T) ≤ ((boundedSchemePerfect (CategoryTheory.Over.left U)).map pull).triangEnvelope) : HasPerfectMassHomBound (CategoryTheory.Over.left T) (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.boundedCoherentPullback f σ hpre)

The finite-morphism pullback half of Lemma 7.4, with its two unfinished geometric inputs explicit.

For a finite morphism, boundedCoherentDerivedPushforward f is the actual exact direct image used to construct f^♯σ. Any linear left adjoint pull transfers the mass--Hom bound provided its perfect images classically generate the source perfect test class.

The repository does not yet construct the required bounded coherent derived pullback for an arbitrary finite morphism: perfectDerivedPullback is defined only under the exact coherent-pullback contract and has domain Perf, whereas the adjunction here is against all of Dᵇ(Coh). Accordingly pull, adj, and the generation containment are parameters rather than manufactured instances. The future geometric discharges are tracked by #1033 and #723.

Flat pushforward transfer

theorem AlgebraicGeometry.DerivedCategory.hasPerfectMassHomBound_flatPushforward {S : Scheme} {T U : Families.SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [Flat (CategoryTheory.Over.Hom.left f)] {k : Type w} [Field k] [CategoryTheory.Linear k T.BoundedCoherentDerivedFiber] [CategoryTheory.Linear k U.BoundedCoherentDerivedFiber] [∀ (n : ℤ), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor U.BoundedCoherentDerivedFiber n)] [CategoryTheory.SerreFunctor.HomFinite k T.BoundedCoherentDerivedFiber] [CategoryTheory.SerreFunctor.HomFinite k U.BoundedCoherentDerivedFiber] {Λ : Type u'} [AddCommGroup Λ] {v : CategoryTheory.Triangulated.K₀ T.BoundedCoherentDerivedFiber →+ Λ} (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap T.BoundedCoherentDerivedFiber v) (hσ : HasPerfectMassHomBound (CategoryTheory.Over.left T) σ) (hpre : Families.SchemeBaseChange.BoundedCoherentPullbackPreimageData f σ.slicing) (lowerShriek : CategoryTheory.Functor T.BoundedCoherentDerivedFiber U.BoundedCoherentDerivedFiber) [lowerShriek.Additive] [CategoryTheory.Functor.Linear k lowerShriek] (adj : lowerShriek ⊣ Families.SchemeBaseChange.boundedCoherentDerivedPullback f) (hgen : boundedSchemePerfect (CategoryTheory.Over.left U) ≤ ((boundedSchemePerfect (CategoryTheory.Over.left T)).map lowerShriek).triangEnvelope) : HasPerfectMassHomBound (CategoryTheory.Over.left U) (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.boundedCoherentPushforward f σ hpre)

The transfer core of the faithfully-flat half of Lemma 7.4, with the lower shriek and its generation input explicit.

Flatness is the hypothesis this statement uses: it supplies the exact bounded coherent pullback f^* that detects f_♯σ, through isExactPullbackOfFlat and hasCoherentPullbackOfIsExactPullback. Given a linear left adjoint lowerShriek ⊣ f^*, the abstract preimage theorem transfers a perfect mass--Hom bound once the lowerShriek images of perfect tests generate the target perfect class.

Why surjectivity is not a hypothesis here. Lemma 7.4(2) assumes f faithfully flat with relative dualizing complex ω_f^• in D_perf, and those two extra assumptions do exactly two jobs. The dualizing complex builds f_! = f_*(- ⊗ ω_f^•) together with its adjunction against f^*; surjectivity makes f^* conservative on Dqc, which is what the Neeman--Ravenel criterion turns into the statement that f_! carries a classical generator of Perf T to one of Perf U. Both jobs are discharged into explicit parameters here -- lowerShriek and adj for the first, hgen for the second -- because the repository owns neither construction. A Surjective f.left binder would therefore be inert: it is the hypothesis of results this statement assumes rather than proves, and carrying it would claim a geometric input the proof never consumes. Those two constructions are the precise remaining #1033 and #723 interfaces; discharging them is what earns back the faithfully flat hypothesis, and the name, on a downstream theorem.