Faithful base change for external-product coefficients

This file names the derived base-change isomorphism expressing that T → S is faithful with respect to X → S:

L(X → S)⁎ R(T → S)⁎ ≅ R(X_T → X)⁎ L(X_T → T)⁎.

A coefficient object on T can therefore be pushed to S and pulled back to X, where it agrees with the push-pull coefficient produced by the first-projection formula. This constructs the quasicoherent base-coefficient data used by Dqc(S)-linearity without imposing compactness on pushforward.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.DqcFaithfulBaseChange {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (pushBase : DqcRightDerivedPushforward T.toIdentityBaseChange) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) : Type (u + 1)

The derived base-change isomorphism saying that T → S is faithful with respect to X → S.

Both pullbacks in the square are genuine derived pullbacks: the right-hand one is the K-flat pullback bundled in D, while the left-hand one is supplied explicitly (and can be constructed by KFlatBasePullbackData).

• iso : pushBase.functor.comp pullBase.functor ≅ D.pullSnd.functor.comp pushFst.functor

  Pulling a fibre pushforward back to X agrees with pushing its pullback from X_T forward to X.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.DqcFlatBaseChangeTheorem {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (pushBase : DqcRightDerivedPushforward T.toIdentityBaseChange) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) : Type (u + 1)

The missing geometric flat-base-change theorem, stated once with the two flatness alternatives used in Proposition 3.15.

This is deliberately stronger than accepting an unrelated isomorphism at each call site: an implementation must produce faithful base change uniformly from flatness of either the source morphism X → S or the base-change morphism T → S.

• ofSourceFlat [Flat (CategoryTheory.Over.hom X)] : D.DqcFaithfulBaseChange pullBase pushBase pushFst

  Flatness of X → S gives derived base change.

• ofBaseFlat [Flat (CategoryTheory.Over.hom T)] : D.DqcFaithfulBaseChange pullBase pushBase pushFst

  Flatness of T → S gives derived base change.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.baseChangeProjections_isPullback {S : Scheme} {X T : SchemeBaseChange S} : CategoryTheory.IsPullback (X.baseChangeSnd T) (X.baseChangeFst T) T.toIdentityBaseChange X.toIdentityBaseChange

The two projections from X ×_S T form the defining pullback square over the identity object of Over S.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.DqcFlatBaseChangeTheorem.baseChangeSnd_flat {S : Scheme} {X T : SchemeBaseChange S} [Flat (CategoryTheory.Over.hom X)] : Flat (CategoryTheory.Over.Hom.left (X.baseChangeSnd T))

Under flatness of X → S, its pullback projection X_T → T is flat.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.DqcFlatBaseChangeTheorem.baseChangeFst_flat {S : Scheme} {X T : SchemeBaseChange S} [Flat (CategoryTheory.Over.hom T)] : Flat (CategoryTheory.Over.Hom.left (X.baseChangeFst T))

Under flatness of T → S, its pullback projection X_T → X is flat.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.DqcFlatBaseChangeTheorem.faithfulOfSourceFlat {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange} {pushBase : DqcRightDerivedPushforward T.toIdentityBaseChange} {pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)} (H : D.DqcFlatBaseChangeTheorem pullBase pushBase pushFst) [Flat (CategoryTheory.Over.hom X)] : D.DqcFaithfulBaseChange pullBase pushBase pushFst

Specialize the flat-base-change theorem using flatness of X → S.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.DqcFlatBaseChangeTheorem.faithfulOfSourceFlat D H = H.ofSourceFlat

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.DqcFlatBaseChangeTheorem.faithfulOfBaseFlat {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange} {pushBase : DqcRightDerivedPushforward T.toIdentityBaseChange} {pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)} (H : D.DqcFlatBaseChangeTheorem pullBase pushBase pushFst) [Flat (CategoryTheory.Over.hom T)] : D.DqcFaithfulBaseChange pullBase pushBase pushFst

Specialize the flat-base-change theorem using flatness of T → S.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.DqcFlatBaseChangeTheorem.faithfulOfBaseFlat D H = H.ofBaseFlat

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.FiberCoefficientData {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) : Type (u + 1)

A first-projection coefficient represented by a quasicoherent object on T, before applying faithful base change.

In the geometric application this object is the tensor of the dual of the earlier compact fibre factor with the later one, including the two shifts.

• fiberCoefficient : T.CompactDqcFiber → T.CompactDqcFiber → ℤ → ℤ → BaseDqc (CategoryTheory.Over.left T)

  The quasicoherent coefficient on T.

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

  The coefficient on X is pushforward of the pullback of the fibre coefficient.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.FiberCoefficientData.toDqcBaseCoefficientData {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} {pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange} (pushBase : DqcRightDerivedPushforward T.toIdentityBaseChange) (faithful : D.DqcFaithfulBaseChange pullBase pushBase pushFst) (C : FiberCoefficientData D P) : DqcBaseCoefficientData D P pullBase

Faithful base change pushes a fibre coefficient to S and identifies its pullback to X with the projection-formula coefficient.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.perfectComponentsSemiorthogonal_of_projectionFormula_of_faithfulBaseChange {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) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (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 pullBase pushBase pushFst) (C : CompactFiberProjectionFormula.FiberCoefficientData D P) (hS : SourceTensorData.DqcSLinearComponents D Q pullBase A) : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

Faithful base change converts fibre coefficients into base coefficients; Dqc(S)-linearity then proves perfect-component semiorthogonality.

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

The faithful-base-change route with L(X → S)⁎ constructed from a K-flat resolution on the base.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.perfectComponentsSemiorthogonal_of_kFlatProjectionFormula_of_sourceFlat {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) (pushBase : DqcRightDerivedPushforward T.toIdentityBaseChange) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] [Flat (CategoryTheory.Over.hom X)] (P : D.CompactFiberProjectionFormula H Q pushFst) (flatBaseChange : D.DqcFlatBaseChangeTheorem B.pullback pushBase pushFst) (C : CompactFiberProjectionFormula.FiberCoefficientData D P) (hS : SourceTensorData.KFlatDqcSLinearComponents D Q B A) : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

The K-flat coefficient route under the paper's first flatness alternative, flatness of X → S.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.perfectComponentsSemiorthogonal_of_kFlatProjectionFormula_of_baseFlat {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) (pushBase : DqcRightDerivedPushforward T.toIdentityBaseChange) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] [Flat (CategoryTheory.Over.hom T)] (P : D.CompactFiberProjectionFormula H Q pushFst) (flatBaseChange : D.DqcFlatBaseChangeTheorem B.pullback pushBase pushFst) (C : CompactFiberProjectionFormula.FiberCoefficientData D P) (hS : SourceTensorData.KFlatDqcSLinearComponents D Q B A) : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

The K-flat coefficient route under the paper's second flatness alternative, flatness of T → S.