Derived base-change data, independent of how it is constructed

BaseChangeCategory.lean builds the base-change categories of §3 of arXiv:1902.08184 from three supplied operations: a derived pullback along each projection off the fibre product, and a derived tensor on it. Every construction there -- the external product, the perfect generators and their envelope, the quasicoherent component (Dqc)_T, the bounded component D_T -- takes those three as separate arguments.

This file bundles them. DerivedBaseChangeData is that bundle and nothing more: two DqcLeftDerivedPullbacks and an operation-level tensor bifunctor. It says how base change is consumed, not how it was produced. In particular, derivedTensor is deliberately not presented as a universal-property construction of the unbounded derived tensor on Dqc; exactness, monoidal coherence, and geometric existence must be supplied by a producer or by the theorem using the operation. A field of this type is therefore an interface, not a proof of the corresponding geometric fact.

Why the bundle is the root and not the K-flat one. K-flat resolutions are a model: one way to produce these three operations, and the one KFlatBaseChange.lean uses. They are not what base change is. Stating the downstream API on the model means a second construction -- pullback along an open immersion, which OpenImmersionPullback.lean already proves exact and so needs no resolution at all; a flat base; an eventual ∞-categorical tensor -- cannot reuse any of it. abstraction-tree.md names that failure directly: a leaf must not copy the carrier or fields of its root, and until this file there was no root for a leaf to reach.

So KFlatBaseChangeData keeps its resolutions and becomes a producer of this structure rather than a rival carrier, through KFlatBaseChangeData.toDerivedBaseChangeData.

Nothing here is inhabited, and nothing here is new mathematics: every declaration is the corresponding one from KFlatBaseChange.lean with the model projected away.

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

The derived operations base change is built from: a derived pullback along each projection off the fibre product, and a derived tensor on it.

This is the model-free root. KFlatBaseChangeData produces one of these from K-flat resolutions; any other construction of the same three operations produces one too, and reaches the whole API below by doing so.

• pullFst : DqcLeftDerivedPullback (X.baseChangeFst T)

  Derived pullback along X_T ⟶ X.

• pullSnd : DqcLeftDerivedPullback (X.baseChangeSnd T)

  Derived pullback along X_T ⟶ T.

• derivedTensor : CategoryTheory.Functor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) (CategoryTheory.Functor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))))

  A derived tensor on the fibre product. It stays explicit because the repository does not yet construct the unbounded derived tensor on Dqc.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.ofExactPullbacks {S : Scheme} {X T : SchemeBaseChange S} [IsExactPullback (X.baseChangeFst T)] [IsExactPullback (X.baseChangeSnd T)] (tensor : CategoryTheory.Functor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) (CategoryTheory.Functor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))))) (hFst : ∀ (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X)), Dqc.schemeQuasicoherentCohomology (CategoryTheory.Over.left (X ⨯ T)) ((derivedPullback (X.baseChangeFst T)).obj E.obj)) (hSnd : ∀ (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left T)), Dqc.schemeQuasicoherentCohomology (CategoryTheory.Over.left (X ⨯ T)) ((derivedPullback (X.baseChangeSnd T)).obj E.obj)) : X.DerivedBaseChangeData T

Assemble the model-free root from exact geometric pullbacks.

This is a second producer for DerivedBaseChangeData: exact or flat/open base-change morphisms can use the canonical derived pullback without choosing K-flat resolutions. The tensor and the two Dqc preservation statements remain explicit because this file does not claim a general unbounded tensor or a general-scheme quasi-coherence theorem.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.externalProduct {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : CategoryTheory.Functor (X.SourcePerfectPartCategory P) (CategoryTheory.Functor T.CompactDqcFiber (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))))

The base-change external product of the bundled operations.

Equations

• D.externalProduct P = X.baseChangeExternalProduct T P D.pullFst D.pullSnd D.derivedTensor

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectGenerators {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T)))

The external-product generators of the bundled operations.

Equations

• D.perfectGenerators P = X.perfectBaseChangeGenerators T P (D.externalProduct P)

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.externalProduct_mem_perfectGenerators {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (F : X.SourcePerfectPartCategory P) (G : T.CompactDqcFiber) : D.perfectGenerators P (((D.externalProduct P).obj F).obj G)

Every concrete external product belongs to the generator property.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.shiftedPerfectGenerators {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T)))

The external-product generators with all their shifts and isomorphic copies.

Equations

• D.shiftedPerfectGenerators P = (D.perfectGenerators P).shiftClosure ℤ

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.externalProduct_shift_mem_shiftedPerfectGenerators {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (F : X.SourcePerfectPartCategory P) (G : T.CompactDqcFiber) (n : ℤ) : D.shiftedPerfectGenerators P ((CategoryTheory.shiftFunctor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) n).obj (((D.externalProduct P).obj F).obj G))

Every shift of a concrete external product belongs to the shifted generator property.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.shiftedPerfectGenerators_isStableUnderShift {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : (D.shiftedPerfectGenerators P).IsStableUnderShift ℤ

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectEnvelope {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T)))

The perfect base-change envelope of the bundled operations.

Equations

• D.perfectEnvelope P = X.perfectBaseChangeEnvelope T P (D.externalProduct P)

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentComponent {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T)))

The quasicoherent base-change component (Dqc)_T.

Equations

• D.quasicoherentComponent P = X.quasicoherentBaseChangeComponent T P (D.externalProduct P)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.QuasicoherentCategory {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : Type (u + 1)

The full quasicoherent base-change category (Dqc)_T.

Equations

• D.QuasicoherentCategory P = (D.quasicoherentComponent P).FullSubcategory

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedComponent {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : CategoryTheory.ObjectProperty (Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ T)))

The bounded base-change component D_T.

Equations

• D.boundedComponent P = X.boundedBaseChangeComponent T P (D.externalProduct P)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.BoundedCategory {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : Type (u + 1)

The full bounded base-change category D_T.

Equations

• D.BoundedCategory P = (D.boundedComponent P).FullSubcategory

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectEnvelope_isClosedUnderIsomorphisms {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : (D.perfectEnvelope P).IsClosedUnderIsomorphisms

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectEnvelope_isTriangulated {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) [P.ContainsZero] : (D.perfectEnvelope P).IsTriangulated

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentComponent_isTriangulated {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) [P.ContainsZero] : (D.quasicoherentComponent P).IsTriangulated

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentComponent_isClosedUnderIsomorphisms {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : (D.quasicoherentComponent P).IsClosedUnderIsomorphisms

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedComponent_isClosedUnderIsomorphisms {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) : (D.boundedComponent P).IsClosedUnderIsomorphisms

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PreservesCompactObjects {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) : Prop

The compactness obligations on the three bundled operations, stated on the operations rather than on whatever produced them.

• fst : D.pullFst.PreservesCompactObjects

  Pullback along X_T ⟶ X preserves compact objects.

• snd : D.pullSnd.PreservesCompactObjects

  Pullback along X_T ⟶ T preserves compact objects.

• tensor : X.TensorPreservesCompactObjects T D.derivedTensor

  The derived tensor preserves compact objects.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.externalProduct_obj_isCompact {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (hD : D.PreservesCompactObjects) (F : X.SourcePerfectPartCategory P) (G : T.CompactDqcFiber) : CategoryTheory.IsCompactObject (((D.externalProduct P).obj F).obj G)

Under those obligations every external-product generator is compact.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectEnvelope_le_compact {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (hD : D.PreservesCompactObjects) : D.perfectEnvelope P ≤ CategoryTheory.ObjectProperty.compactObjects

Under those obligations the whole perfect envelope consists of compact objects.