K-flat fibre coefficients for base-change semiorthogonality

This file makes the fibre object in the faithful-base-change argument concrete. A K-flat resolution on T supplies the derived tensor on Dqc(T), and compact duality chooses G⁺ right-adjoint to tensoring by each compact fibre object G. The coefficient attached to Gi[a] and Gj[b] is then

(Gj ⊗ Gi⁺)[b - a].

The remaining comparison with the coefficient produced by the first projection formula is kept explicit. It is precisely the associativity, pullback/tensor, and duality coherence still missing from the current K-flat monoidal layer.

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

A K-flat construction of the derived tensor on Dqc(T).

• resolution : SchemeKFlatResolution (CategoryTheory.Over.left T)

  A K-flat replacement on the fibre scheme.

• tensorQuasicoherent : self.resolution.ResolvedTensorPreservesQuasicoherentCohomology

  Resolved tensor preserves quasicoherent cohomology.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatFiberTensorData.derivedTensor {S : Scheme} {T : SchemeBaseChange S} (K : T.KFlatFiberTensorData) : CategoryTheory.Functor (BaseDqc (CategoryTheory.Over.left T)) (CategoryTheory.Functor (BaseDqc (CategoryTheory.Over.left T)) (BaseDqc (CategoryTheory.Over.left T)))

The derived tensor on Dqc(T) selected by the K-flat fibre data.

Equations

• K.derivedTensor = K.resolution.derivedTensorToDqc ⋯

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatFiberTensorData.derivedTensor_obj_obj_obj {S : Scheme} {T : SchemeBaseChange S} (K : T.KFlatFiberTensorData) (E F : BaseDqc (CategoryTheory.Over.left T)) : ((K.derivedTensor.obj E).obj F).obj = (K.resolution.derivedTensor.obj E.obj).obj F.obj

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatCompactFiberDualityData {S : Scheme} {T : SchemeBaseChange S} (K : T.KFlatFiberTensorData) : Type (u + 1)

Chosen compact duals for the actual K-flat tensor on Dqc(T).

The adjunction records that tensoring on the right by G⁺ is right adjoint to tensoring on the right by G.

• dual : T.CompactDqcFiber → T.CompactDqcFiber

  The chosen compact dual of a compact fibre object.

• adjunction (G : T.CompactDqcFiber) : K.derivedTensor.flip.obj G.obj ⊣ K.derivedTensor.flip.obj (self.dual G).obj

  Tensor-duality adjunction for the chosen compact dual.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatCompactFiberDualityData.coefficient {S : Scheme} {T : SchemeBaseChange S} {K : T.KFlatFiberTensorData} (V : KFlatCompactFiberDualityData K) (Gi Gj : T.CompactDqcFiber) (a b : ℤ) : BaseDqc (CategoryTheory.Over.left T)

The explicit fibre coefficient left by dualizing Gi[a] against Gj[b]: tensor Gj by the chosen dual of Gi, then shift by b - a.

Equations

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

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatCompactFiberDualityData.coefficient_obj {S : Scheme} {T : SchemeBaseChange S} {K : T.KFlatFiberTensorData} (V : KFlatCompactFiberDualityData K) (Gi Gj : T.CompactDqcFiber) (a b : ℤ) : (V.coefficient Gi Gj a b).obj = ((CategoryTheory.shiftFunctor (BaseDqc (CategoryTheory.Over.left T)) (b - a)).obj ((K.derivedTensor.obj Gj.obj).obj (V.dual Gi).obj)).obj

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.pulledBackTensorCoefficient {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (K : T.KFlatFiberTensorData) (V : KFlatCompactFiberDualityData K) (Gi Gj : T.CompactDqcFiber) (a b : ℤ) : X.TargetDqc T

The target-side tensor coefficient obtained by pulling back the two compact fibre factors separately, tensoring them with the target K-flat tensor, and applying the shift left by compact duality.

This is the intermediate object at which the projection-formula comparison and the monoidality of fibre pullback meet.

Equations

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

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.KFlatTensorCoefficientComparison {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) (K : T.KFlatFiberTensorData) (V : KFlatCompactFiberDualityData K) : Type (u + 1)

Atomic comparisons underlying the explicit K-flat fibre coefficient.

The first isomorphism is the projection-formula/duality calculation on X_T. The second isomorphism is the tensor compatibility of pullback from T. Keeping them separate prevents either geometric theorem from being hidden in the final coefficient comparison.

• projectionIso (Gi Gj : T.CompactDqcFiber) (a b : ℤ) : P.coefficient Gi Gj a b ≅ pushFst.functor.obj (D.pulledBackTensorCoefficient K V Gi Gj a b)

  Projection formula and compact duality identify the source coefficient with the pushforward of the separately pulled-back tensor coefficient.

• pullbackTensorIso (Gi Gj : T.CompactDqcFiber) (a b : ℤ) : D.pulledBackTensorCoefficient K V Gi Gj a b ≅ D.pullSnd.functor.obj (V.coefficient Gi Gj a b)

  Pullback from the fibre commutes with its K-flat tensor coefficient.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.KFlatTensorCoefficientData {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) (K : T.KFlatFiberTensorData) (V : KFlatCompactFiberDualityData K) : Type (u + 1)

The first-projection coefficient is represented by the explicit K-flat fibre tensor of the later factor with the dual of the earlier factor.

• coefficientIso (Gi Gj : T.CompactDqcFiber) (a b : ℤ) : P.coefficient Gi Gj a b ≅ pushFst.functor.obj (D.pullSnd.functor.obj (V.coefficient Gi Gj a b))

  Comparison between the abstract projection coefficient and the pushforward of the explicit pulled-back fibre tensor coefficient.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.KFlatTensorCoefficientData.toFiberCoefficientData {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} {K : T.KFlatFiberTensorData} {V : KFlatCompactFiberDualityData K} (C : KFlatTensorCoefficientData D P K V) : FiberCoefficientData D P

Forget the explicit tensor formula while retaining its fibre coefficient and comparison.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.KFlatTensorCoefficientComparison.toKFlatTensorCoefficientData {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} {K : T.KFlatFiberTensorData} {V : KFlatCompactFiberDualityData K} (C : KFlatTensorCoefficientComparison D P K V) : KFlatTensorCoefficientData D P K V

Compose the projection/duality comparison with monoidality of fibre pullback to obtain the coefficient comparison used by faithful base change.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.KFlatTensorCoefficientComparison.toFiberCoefficientData {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} {K : T.KFlatFiberTensorData} {V : KFlatCompactFiberDualityData K} (C : KFlatTensorCoefficientComparison D P K V) : FiberCoefficientData D P

The atomic K-flat comparisons also supply the fibre-coefficient datum consumed by the faithful-base-change argument.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.perfectComponentsSemiorthogonal_of_kFlatTensorCoefficients {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) (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.KFlatTensorCoefficientData D P K V) (hS : SourceTensorData.KFlatDqcSLinearComponents D Q B A) : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

The end-to-end semiorthogonality theorem with all three tensor operations and the base pullback pinned to K-flat constructions, and with faithful base change applied to the explicit dual fibre coefficient.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.perfectComponentsSemiorthogonal_of_kFlatTensorCoefficientComparison {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) (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.KFlatDqcSLinearComponents D Q B A) : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

The end-to-end semiorthogonality theorem stated using the two atomic coherence comparisons rather than a bundled coefficient isomorphism.