Theorem 7.5: mass--Hom bounds on the distinguished component

This file assembles the already formalized algebraic base case, pushforward and pullback transfers, and connected-component invariance into the statement layer of Theorem 7.5 of arXiv:2607.28411v1.

The absolute projective-family construction (PF3) has not yet produced the distinguished stability condition on every projective scheme. Its exact current output is therefore isolated as DistinguishedComponentInhabitant: one stability condition with a perfect mass--Hom bound, together with membership of the target in its connected component. Theorem 7.5 is then formal, and ofAlgebraicTransferChain below constructs this inhabitant from the algebraic seed and the two transfers once their geometric data are provided.

No projectivity, ampleness, adjunction, or generation assertion is manufactured here. In particular, the lower-shriek and finite-pullback functors remain the explicit PF3 inputs already documented by Lemma 7.4.

structure AlgebraicGeometry.DerivedCategory.DistinguishedComponentInhabitant (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) : Type (max (u + 1) u')

The exact PF3 inhabitant needed by Theorem 7.5 before the absolute projective-family construction is available: a bounded point in the distinguished connected component.

• base : CategoryTheory.Triangulated.StabilityCondition.WithClassMap (SchemeBoundedCoherentDerivedCategory X) v

  The constructed base point of the distinguished component.

• base_hasPerfectMassHomBound : HasPerfectMassHomBound X self.base

  The base point has the bound supplied by the algebraic seed and the two transfer steps.

• target_mem_connectedComponent : σ ∈ connectedComponent self.base

  The target lies in the connected component selected by that base point.

noncomputable def AlgebraicGeometry.DerivedCategory.DistinguishedComponentInhabitant.ofAlgebraicTransferChain {S : Scheme} {T U X : Families.SchemeBaseChange S} (f : T ⟶ U) (i : X ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [IsLocallyNoetherian (CategoryTheory.Over.left X)] [Flat (CategoryTheory.Over.Hom.left f)] [IsFinite (CategoryTheory.Over.Hom.left i)] {k : Type w} [Field k] [CategoryTheory.Linear k T.BoundedCoherentDerivedFiber] [CategoryTheory.Linear k U.BoundedCoherentDerivedFiber] [CategoryTheory.Linear k X.BoundedCoherentDerivedFiber] [∀ (n : ℤ), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor U.BoundedCoherentDerivedFiber n)] [∀ (n : ℤ), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor X.BoundedCoherentDerivedFiber n)] [CategoryTheory.SerreFunctor.HomFinite k T.BoundedCoherentDerivedFiber] [CategoryTheory.SerreFunctor.HomFinite k U.BoundedCoherentDerivedFiber] [CategoryTheory.SerreFunctor.HomFinite k X.BoundedCoherentDerivedFiber] [CategoryTheory.Triangulated.HomFiniteBounded k T.BoundedCoherentDerivedFiber] {Λ : Type u'} [AddCommGroup Λ] {vT : CategoryTheory.Triangulated.K₀ T.BoundedCoherentDerivedFiber →+ Λ} (σT : CategoryTheory.Triangulated.StabilityCondition.WithClassMap T.BoundedCoherentDerivedFiber vT) (hσT : σT.IsAlgebraic) (hpush : Families.SchemeBaseChange.BoundedCoherentPullbackPreimageData f σT.slicing) (lowerShriek : CategoryTheory.Functor T.BoundedCoherentDerivedFiber U.BoundedCoherentDerivedFiber) [lowerShriek.Additive] [CategoryTheory.Functor.Linear k lowerShriek] (lowerShriekAdjunction : lowerShriek ⊣ Families.SchemeBaseChange.boundedCoherentDerivedPullback f) (hpushGenerates : boundedSchemePerfect (CategoryTheory.Over.left U) ≤ ((boundedSchemePerfect (CategoryTheory.Over.left T)).map lowerShriek).triangEnvelope) (hpull : Families.SchemeBaseChange.BoundedCoherentPushforwardPreimageData i (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.boundedCoherentPushforward f σT hpush).slicing) (pull : CategoryTheory.Functor U.BoundedCoherentDerivedFiber X.BoundedCoherentDerivedFiber) [pull.Additive] [CategoryTheory.Functor.Linear k pull] (pullAdjunction : pull ⊣ Families.SchemeBaseChange.boundedCoherentDerivedPushforward i) (hpullGenerates : boundedSchemePerfect (CategoryTheory.Over.left X) ≤ ((boundedSchemePerfect (CategoryTheory.Over.left U)).map pull).triangEnvelope) (σX : CategoryTheory.Triangulated.StabilityCondition.WithClassMap X.BoundedCoherentDerivedFiber ((vT.comp (CategoryTheory.Triangulated.K₀.map (Families.SchemeBaseChange.boundedCoherentDerivedPullback f))).comp (CategoryTheory.Triangulated.K₀.map (Families.SchemeBaseChange.boundedCoherentDerivedPushforward i)))) (hcomponent : σX ∈ connectedComponent (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.boundedCoherentPullback i (CategoryTheory.Triangulated.StabilityCondition.WithClassMap.boundedCoherentPushforward f σT hpush) hpull)) : DistinguishedComponentInhabitant k (CategoryTheory.Over.left X) σX

Assemble the PF3 inhabitant from the proof chain of Theorem 7.5: an algebraic seed, the flat pushforward step, the finite pullback step, and membership in the resulting connected component.

The functors, adjunctions, preimage data, and generation containments are exactly the open geometric inputs of the two Lemma 7.4 adapters.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.theorem75 {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) (h : DistinguishedComponentInhabitant k X σ) : HasPerfectMassHomBound X σ

Theorem 7.5, conditional only on the named PF3 inhabitant until the absolute projective-family construction lands.

theorem AlgebraicGeometry.DerivedCategory.remark14_autoequivalence_iff {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) (a : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPair v) [CategoryTheory.Functor.Linear k a.Φ.e.functor] [CategoryTheory.Functor.Linear k a.Φ.e.inverse] (hperfect : boundedSchemePerfect X = (boundedSchemePerfect X).inverseImage a.Φ.e.inverse) : HasPerfectMassHomBound X (a.act σ) ↔ HasPerfectMassHomBound X σ

Remark 1.4: the perfect mass--Hom bound is invariant under a compatible derived autoequivalence which preserves the perfect test class.