Proposition 3.15 assembly for scheme base change

This file assembles the formal core of Proposition 3.15 of arXiv:1902.08184 from the independent geometric inputs isolated by the base-change API.

The first package combines presentable S-linearity with the explicit K-flat fibre-coefficient comparison and faithful derived base change. The second adds external-product generation and propagation from perfect objects to Dqc. Thus it produces semiorthogonality and fullness for both the perfect and quasicoherent sequences.

The projection layer constructs the Dqc projectors from componentwise compact-generator approximations and obtains the perfect projectors by restriction to compact objects. Proposition315ProjectionConstructionData records the remaining geometric inputs: cocontinuity of the corresponding truncations, preservation of compact objects, and the compact-intersection identification. It produces Proposition315ProjectionData, which in turn converts the core package to DecompositionData.

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

The semiorthogonality part of Proposition 3.15, with the source triangulatedness and the presentably extended base-linearity retained for later construction steps.

• sourceComponentsTriangulated : A.HasTriangulatedComponents

  The original source components are triangulated.

• sourceComponentsDqcSLinear : SourceTensorData.KFlatDqcSLinearComponents D Q B A

  The Perf(S)-linear source action has been extended to Dqc(S).

• perfectSemiorthogonal : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

  The perfect external-product envelopes are semiorthogonal.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.Proposition315SemiorthogonalityData.ofKFlatTensorCoefficientComparison {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) (hCoprod : ∀ (j : ι) (κ : Type u), (A.component j).IsClosedUnderColimitsOfShape (CategoryTheory.Discrete κ)) (H : D.toDerivedBaseChangeData.CompactFiberTensorDuality) (Q : D.SourceTensorData) (B : X.KFlatBasePullbackData) (presentable : SourceTensorData.PresentableBaseActionData D Q B.pullback) (K : T.KFlatFiberTensorData) (V : KFlatCompactFiberDualityData K) (pushBase : DqcRightDerivedPushforward T.toIdentityBaseChange) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] (P : D.CompactFiberProjectionFormula H Q pushFst) (faithful : D.DqcFaithfulBaseChange B.pullback pushBase pushFst) (C : CompactFiberProjectionFormula.KFlatTensorCoefficientComparison D P K V) (hS : SourceTensorData.KFlatSLinearComponents D Q B A) : D.Proposition315SemiorthogonalityData A Q B

Assemble semiorthogonality from the atomic K-flat tensor comparisons.

The source only has to be Perf(S)-linear at input. Presentability extends that action to Dqc(S), after which the explicit coefficient comparison and faithful base change prove the required external-product Hom vanishing.

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

The formal core of Proposition 3.15: the perfect and quasicoherent base-change sequences are semiorthogonal and full, and the source linearity used in the construction is available at the Dqc(S) level.

• semiorthogonality : D.Proposition315SemiorthogonalityData A Q B

  Semiorthogonality and presentable source linearity.

• perfectFull : (D.toDerivedBaseChangeData.perfectCategorySequence A ⋯).IsFull

  External products generate the perfect base-change category.

• quasicoherentFull : (D.toDerivedBaseChangeData.quasicoherentSequence A ⋯ ⋯).IsFull

  The corresponding quasicoherent components generate Dqc(X_T).

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.Proposition315SemiorthogonalityData.toCoreData {S : Scheme} {X T : SchemeBaseChange S} {ι : Type w} [Preorder ι] {D : X.KFlatBaseChangeData T} {A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι} {Q : D.SourceTensorData} {B : X.KFlatBasePullbackData} (C : D.Proposition315SemiorthogonalityData A Q B) (hcompact : D.PreservesCompactObjects) (hgen : (D.toDerivedBaseChangeData.perfectCategoryExternalProductGenerators A).IsClassicalTriangulatedGenerator) (G : D.toDerivedBaseChangeData.QuasicoherentFullnessPropagationData A ⋯ ⋯) : D.Proposition315CoreData A Q B hcompact

Add the two generation inputs to the semiorthogonality package.

Classical generation by explicit external products proves perfect fullness; compact generation and filtration/coproduct compatibility then propagate it to quasicoherent fullness.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.Proposition315ProjectionData {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] {A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι} {Q : D.SourceTensorData} {B : X.KFlatBasePullbackData} {hcompact : D.PreservesCompactObjects} (C : D.Proposition315CoreData A Q B hcompact) : Type (max (u + 1) w)

The exact remaining projection boundary after the Proposition 3.15 core has been assembled. No existence or cocontinuity theorem for these projectors is inferred from semiorthogonality or generation.

• perfectProjections : (D.toDerivedBaseChangeData.perfectCategorySequence A ⋯).RightProjectionData

  Chosen right projections onto the perfect components.

• quasicoherentProjections : (D.toDerivedBaseChangeData.quasicoherentSequence A ⋯ ⋯).RightProjectionData

  Chosen right projections onto the quasicoherent components.

• quasicoherentProjectionCocontinuous (i : ι) : (self.quasicoherentProjections.ambientProjection i).PreservesSmallCoproducts

  The ambient quasicoherent projection functors preserve coproducts.

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

Geometric inputs from which all chosen projections in Proposition 3.15 are constructed.

• approximation : D.toDerivedBaseChangeData.QuasicoherentProjectionApproximationData A

  Compact-generator approximations for the perfect envelopes.

• truncationCocontinuous (i : ι) : (⋯.tStructure.truncLE 0).PreservesSmallCoproducts

  The zero truncation attached to each approximation preserves coproducts in the scheme universe.

• compactRestriction : D.toDerivedBaseChangeData.PerfectProjectionRestrictionData A ⋯ ⋯ (⋯.quasicoherentProjections ⋯ ⋯)

  The quasicoherent projectors preserve compact objects, and compact intersection identifies their restrictions with the perfect components.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.Proposition315ProjectionConstructionData.toProjectionData {S : Scheme} {X T : SchemeBaseChange S} {ι : Type w} [Preorder ι] {D : X.KFlatBaseChangeData T} {A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι} {Q : D.SourceTensorData} {B : X.KFlatBasePullbackData} {hcompact : D.PreservesCompactObjects} {C : D.Proposition315CoreData A Q B hcompact} (P : D.Proposition315ProjectionConstructionData C) : D.Proposition315ProjectionData C

Construct all perfect and quasicoherent projection data required by the Proposition 3.15 core.

Equations

• P.toProjectionData = { perfectProjections := ⋯.perfectProjections, quasicoherentProjections := ⋯.quasicoherentProjections ⋯ ⋯, quasicoherentProjectionCocontinuous := ⋯ }

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.Proposition315CoreData.toDecompositionData {S : Scheme} {X T : SchemeBaseChange S} {ι : Type w} [Preorder ι] {D : X.KFlatBaseChangeData T} {A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι} {Q : D.SourceTensorData} {B : X.KFlatBasePullbackData} {hcompact : D.PreservesCompactObjects} (C : D.Proposition315CoreData A Q B hcompact) (P : D.Proposition315ProjectionData C) : D.toDerivedBaseChangeData.DecompositionData A ⋯ ⋯

Supply the remaining projection data to obtain the existing paper-strength decomposition package.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.Proposition315CoreData.toDecompositionDataOfProjectionConstruction {S : Scheme} {X T : SchemeBaseChange S} {ι : Type w} [Preorder ι] {D : X.KFlatBaseChangeData T} {A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι} {Q : D.SourceTensorData} {B : X.KFlatBasePullbackData} {hcompact : D.PreservesCompactObjects} (C : D.Proposition315CoreData A Q B hcompact) (P : D.Proposition315ProjectionConstructionData C) : D.toDerivedBaseChangeData.DecompositionData A ⋯ ⋯

Construct the projectors from compact-generator approximations and pass directly to the paper-strength decomposition package.

Equations

• C.toDecompositionDataOfProjectionConstruction P = C.toDecompositionData P.toProjectionData