K-flat base-scheme action for base-change semiorthogonality

This file removes the last abstract pullback from the S-linearity route to perfect-component semiorthogonality. A KFlatBasePullbackData X constructs the derived pullback Dqc(S) ⥤ Dqc(X) from a K-flat resolution on S, its pullback-acyclicity along X → S, and resolved quasicoherence preservation.

The resulting aliases and end-to-end theorems state both compact and quasicoherent base-coefficient/S-linearity inputs entirely in terms of this constructed pullback.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBasePullbackData {S : Scheme} (X : SchemeBaseChange S) : Type (u + 1)

K-flat geometric data constructing derived pullback along the structure morphism X → S.

The resolution lives on S, the source category of the contravariant pullback. The two remaining fields are exactly the operational hypotheses required by kFlatDqcLeftDerivedPullback.

• resolution : SchemeKFlatResolution S

  A K-flat replacement on the base scheme.

• acyclic : KFlatPullbackAcyclic self.resolution X.toIdentityBaseChange

  Pullback along X → S is acyclic on the chosen replacements.

• quasicoherent : KFlatResolvedPullbackPreservesQuasicoherentCohomology self.resolution X.toIdentityBaseChange

  Resolved pullback along X → S preserves quasicoherent cohomology.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBasePullbackData.pullback {S : Scheme} {X : SchemeBaseChange S} (B : X.KFlatBasePullbackData) : DqcLeftDerivedPullback X.toIdentityBaseChange

The genuine Dqc pullback along X → S constructed from the bundled K-flat base resolution.

Equations

• B.pullback = AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatDqcLeftDerivedPullback B.resolution X.toIdentityBaseChange ⋯ ⋯

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.KFlatSLinearComponents {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] (Q : D.SourceTensorData) (B : X.KFlatBasePullbackData) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) : Prop

S-linearity using the base action constructed from K-flat pullback data, rather than a separately supplied derived pullback.

Equations

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

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.KFlatDqcSLinearComponents {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] (Q : D.SourceTensorData) (B : X.KFlatBasePullbackData) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) : Prop

Dqc(S)-linearity using the base action constructed from K-flat pullback data.

Equations

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

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.KFlatBaseCoefficientData {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {H : D.toDerivedBaseChangeData.CompactFiberTensorDuality} {Q : D.SourceTensorData} {pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)} (P : D.CompactFiberProjectionFormula H Q pushFst) (B : X.KFlatBasePullbackData) : Type (u + 1)

Projection coefficients represented by compact base objects through the K-flat-constructed pullback Dqc(S) ⥤ Dqc(X).

Equations

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

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.KFlatDqcBaseCoefficientData {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {H : D.toDerivedBaseChangeData.CompactFiberTensorDuality} {Q : D.SourceTensorData} {pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)} (P : D.CompactFiberProjectionFormula H Q pushFst) (B : X.KFlatBasePullbackData) : Type (u + 1)

Quasicoherent base coefficients represented through the K-flat-constructed pullback Dqc(S) ⥤ Dqc(X).

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.perfectComponentsSemiorthogonal_of_kFlatProjectionFormula_of_sLinear {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : A.HasTriangulatedComponents) (hIso : ∀ (j : ι), (A.component j).IsClosedUnderIsomorphisms) (H : D.toDerivedBaseChangeData.CompactFiberTensorDuality) (Q : D.SourceTensorData) (B : X.KFlatBasePullbackData) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] (P : D.CompactFiberProjectionFormula H Q pushFst) (C : CompactFiberProjectionFormula.KFlatBaseCoefficientData D P B) (hS : SourceTensorData.KFlatSLinearComponents D Q B A) : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

Compact-fibre duality, a first-projection formula with compact base coefficients, and S-linearity prove perfect-component semiorthogonality, with the base pullback constructed from K-flat resolution data.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.perfectComponentsSemiorthogonal_of_kFlatProjectionFormula_of_dqcSLinear {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : A.HasTriangulatedComponents) (hIso : ∀ (j : ι), (A.component j).IsClosedUnderIsomorphisms) (H : D.toDerivedBaseChangeData.CompactFiberTensorDuality) (Q : D.SourceTensorData) (B : X.KFlatBasePullbackData) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] (P : D.CompactFiberProjectionFormula H Q pushFst) (C : CompactFiberProjectionFormula.KFlatDqcBaseCoefficientData D P B) (hS : SourceTensorData.KFlatDqcSLinearComponents D Q B A) : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

The fully K-flat route from quasicoherent base coefficients and Dqc(S)-linearity to perfect-component semiorthogonality.