Base-change categories from K-flat derived tensor

This file specializes the generic external-product construction in BaseChangeCategory.lean to the actual derived tensor obtained from a K-flat resolution of complexes of module sheaves on the fibre product. Its parameters are geometric evidence about that construction—preservation of quasicoherent cohomology and compact objects—rather than an arbitrary bifunctor on Dqc.

The resulting aliases are the K-flat forms of the paper's (Dqc)_T and D_T. Constructing the resolution and proving quasicoherence and compactness for its resolved complex-level tensors remains explicit in their signatures; the corresponding facts for arbitrary derived objects are then theorems.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatBaseChangeExternalProduct {S : Scheme} (X T : SchemeBaseChange S) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pullX : DqcLeftDerivedPullback (X.baseChangeFst T)) (pullT : DqcLeftDerivedPullback (X.baseChangeSnd T)) (R : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) : CategoryTheory.Functor (X.SourcePerfectPartCategory P) (CategoryTheory.Functor T.CompactDqcFiber (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))))

The base-change external product formed with the derived tensor constructed from a K-flat resolution of complexes of module sheaves on X_T.

Equations

• X.kFlatBaseChangeExternalProduct T P pullX pullT R hR = X.baseChangeExternalProduct T P pullX pullT (R.derivedTensorToDqc ⋯)

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatBaseChangeExternalProduct_obj_obj_obj {S : Scheme} (X T : SchemeBaseChange S) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pullX : DqcLeftDerivedPullback (X.baseChangeFst T)) (pullT : DqcLeftDerivedPullback (X.baseChangeSnd T)) (R : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) (F : X.SourcePerfectPartCategory P) (G : T.CompactDqcFiber) : (((X.kFlatBaseChangeExternalProduct T P pullX pullT R hR).obj F).obj G).obj = (R.derivedTensor.obj (pullX.functor.obj F.obj).obj).obj (pullT.functor.obj G.obj).obj

After forgetting quasicoherence witnesses, the K-flat external product is the ambient K-flat derived tensor of the two derived pullbacks.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatBaseChangeExternalProduct_obj_isCompact {S : Scheme} (X T : SchemeBaseChange S) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pullX : DqcLeftDerivedPullback (X.baseChangeFst T)) (pullT : DqcLeftDerivedPullback (X.baseChangeSnd T)) (R : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) (hpullX : pullX.PreservesCompactObjects) (hpullT : pullT.PreservesCompactObjects) (htensor : R.ResolvedTensorPreservesCompactObjects hR) (F : X.SourcePerfectPartCategory P) (G : T.CompactDqcFiber) : CategoryTheory.IsCompactObject (((X.kFlatBaseChangeExternalProduct T P pullX pullT R hR).obj F).obj G)

K-flat external products of compact factors are compact when the two pullbacks and the restricted K-flat tensor preserve compact objects.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatPerfectBaseChangeGenerators {S : Scheme} (X T : SchemeBaseChange S) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pullX : DqcLeftDerivedPullback (X.baseChangeFst T)) (pullT : DqcLeftDerivedPullback (X.baseChangeSnd T)) (R : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T)))

The external-product generators obtained from K-flat derived tensor.

Equations

• X.kFlatPerfectBaseChangeGenerators T P pullX pullT R hR = X.perfectBaseChangeGenerators T P (X.kFlatBaseChangeExternalProduct T P pullX pullT R hR)

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatPerfectBaseChangeEnvelope {S : Scheme} (X T : SchemeBaseChange S) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pullX : DqcLeftDerivedPullback (X.baseChangeFst T)) (pullT : DqcLeftDerivedPullback (X.baseChangeSnd T)) (R : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T)))

The perfect base-change envelope generated using K-flat derived tensor.

Equations

• X.kFlatPerfectBaseChangeEnvelope T P pullX pullT R hR = X.perfectBaseChangeEnvelope T P (X.kFlatBaseChangeExternalProduct T P pullX pullT R hR)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatPerfectBaseChangeEnvelopeCategory {S : Scheme} (X T : SchemeBaseChange S) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pullX : DqcLeftDerivedPullback (X.baseChangeFst T)) (pullT : DqcLeftDerivedPullback (X.baseChangeSnd T)) (R : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) : Type (u + 1)

The full perfect base-change envelope constructed from K-flat derived tensor.

Equations

• X.KFlatPerfectBaseChangeEnvelopeCategory T P pullX pullT R hR = (X.kFlatPerfectBaseChangeEnvelope T P pullX pullT R hR).FullSubcategory

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatQuasicoherentBaseChangeComponent {S : Scheme} (X T : SchemeBaseChange S) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pullX : DqcLeftDerivedPullback (X.baseChangeFst T)) (pullT : DqcLeftDerivedPullback (X.baseChangeSnd T)) (R : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T)))

The quasicoherent base-change component (Dqc)_T constructed from K-flat derived tensor.

Equations

• X.kFlatQuasicoherentBaseChangeComponent T P pullX pullT R hR = X.quasicoherentBaseChangeComponent T P (X.kFlatBaseChangeExternalProduct T P pullX pullT R hR)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatQuasicoherentBaseChangeCategory {S : Scheme} (X T : SchemeBaseChange S) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pullX : DqcLeftDerivedPullback (X.baseChangeFst T)) (pullT : DqcLeftDerivedPullback (X.baseChangeSnd T)) (R : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) : Type (u + 1)

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

Equations

• X.KFlatQuasicoherentBaseChangeCategory T P pullX pullT R hR = (X.kFlatQuasicoherentBaseChangeComponent T P pullX pullT R hR).FullSubcategory

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatBoundedBaseChangeComponent {S : Scheme} (X T : SchemeBaseChange S) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pullX : DqcLeftDerivedPullback (X.baseChangeFst T)) (pullT : DqcLeftDerivedPullback (X.baseChangeSnd T)) (R : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) : CategoryTheory.ObjectProperty (Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ T)))

The bounded base-change component D_T constructed from K-flat derived tensor.

Equations

• X.kFlatBoundedBaseChangeComponent T P pullX pullT R hR = X.boundedBaseChangeComponent T P (X.kFlatBaseChangeExternalProduct T P pullX pullT R hR)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBoundedBaseChangeCategory {S : Scheme} (X T : SchemeBaseChange S) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pullX : DqcLeftDerivedPullback (X.baseChangeFst T)) (pullT : DqcLeftDerivedPullback (X.baseChangeSnd T)) (R : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) : Type (u + 1)

The full K-flat bounded base-change category D_T.

Equations

• X.KFlatBoundedBaseChangeCategory T P pullX pullT R hR = (X.kFlatBoundedBaseChangeComponent T P pullX pullT R hR).FullSubcategory

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatPerfectBaseChangeEnvelope_le_compact {S : Scheme} (X T : SchemeBaseChange S) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pullX : DqcLeftDerivedPullback (X.baseChangeFst T)) (pullT : DqcLeftDerivedPullback (X.baseChangeSnd T)) (R : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))) (hR : R.ResolvedTensorPreservesQuasicoherentCohomology) (hpullX : pullX.PreservesCompactObjects) (hpullT : pullT.PreservesCompactObjects) (htensor : R.ResolvedTensorPreservesCompactObjects hR) : X.kFlatPerfectBaseChangeEnvelope T P pullX pullT R hR ≤ CategoryTheory.ObjectProperty.compactObjects

The whole perfect envelope built from K-flat tensor lies in the compact objects when the geometric operations preserve compactness.

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

The K-flat resolutions and resolved representative-level facts needed to construct all three operations in the base-change external product. In particular, the two derived pullbacks are not supplied as independent functors: they are constructed from fstResolution and sndResolution.

• fstResolution : SchemeKFlatResolution (CategoryTheory.Over.left X)

  A K-flat replacement on X, used to derive pullback along X_T ⟶ X.

• fstAcyclic : KFlatPullbackAcyclic self.fstResolution (X.baseChangeFst T)

  Pullback along X_T ⟶ X is acyclic on the chosen replacements.

• fstQuasicoherent : KFlatResolvedPullbackPreservesQuasicoherentCohomology self.fstResolution (X.baseChangeFst T)

  Resolved pullback along X_T ⟶ X preserves quasicoherent cohomology.

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

  A K-flat replacement on T, used to derive pullback along X_T ⟶ T.

• sndAcyclic : KFlatPullbackAcyclic self.sndResolution (X.baseChangeSnd T)

  Pullback along X_T ⟶ T is acyclic on the chosen replacements.

• sndQuasicoherent : KFlatResolvedPullbackPreservesQuasicoherentCohomology self.sndResolution (X.baseChangeSnd T)

  Resolved pullback along X_T ⟶ T preserves quasicoherent cohomology.

• tensorResolution : SchemeKFlatResolution (CategoryTheory.Over.left (X ⨯ T))

  A K-flat replacement on the fibre product, used to derive tensor there.

• tensorQuasicoherent : self.tensorResolution.ResolvedTensorPreservesQuasicoherentCohomology

  Resolved tensor on the fibre product preserves quasicoherent cohomology.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.pullFst {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) : DqcLeftDerivedPullback (X.baseChangeFst T)

The Dqc pullback along X_T ⟶ X constructed from the first K-flat resolution.

Equations

• D.pullFst = AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatDqcLeftDerivedPullback D.fstResolution (X.baseChangeFst T) ⋯ ⋯

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.pullSnd {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) : DqcLeftDerivedPullback (X.baseChangeSnd T)

The Dqc pullback along X_T ⟶ T constructed from the second K-flat resolution.

Equations

• D.pullSnd = AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatDqcLeftDerivedPullback D.sndResolution (X.baseChangeSnd T) ⋯ ⋯

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.derivedTensor {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) : 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))))

The K-flat derived tensor on the fibre product underlying a base-change datum.

Moved here from BaseChangeLinearity.lean: it is a projection of KFlatBaseChangeData, so it belongs at the structure's definition site.

Equations

• D.derivedTensor = D.tensorResolution.derivedTensorToDqc ⋯

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.derivedTensor_obj_obj_obj {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (E F : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) : ((D.derivedTensor.obj E).obj F).obj = (D.tensorResolution.derivedTensor.obj E.obj).obj F.obj

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.toDerivedBaseChangeData {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) : X.DerivedBaseChangeData T

The K-flat resolutions produce model-free base-change data.

This is the one-way adapter from the model to the root: everything below is stated on DerivedBaseChangeData and reaches KFlatBaseChangeData through here, so a second construction of the same three operations inherits the whole API without copying it.

Equations

• D.toDerivedBaseChangeData = { pullFst := D.pullFst, pullSnd := D.pullSnd, derivedTensor := D.derivedTensor }

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.externalProduct {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData 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 with both pullbacks and tensor constructed from the bundled K-flat resolutions.

Equations

• D.externalProduct P = D.toDerivedBaseChangeData.externalProduct P

@[reducible, inline]

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

The external-product generators associated to the bundled K-flat construction.

Equations

• D.perfectGenerators P = D.toDerivedBaseChangeData.perfectGenerators P

@[reducible, inline]

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

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

Equations

• D.shiftedPerfectGenerators P = D.toDerivedBaseChangeData.shiftedPerfectGenerators P

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.externalProduct_shift_mem_shiftedPerfectGenerators {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData 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 K-flat external product belongs to the shifted generator property.

@[reducible, inline]

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

The perfect base-change envelope obtained entirely from the bundled K-flat resolutions.

Equations

• D.perfectEnvelope P = D.toDerivedBaseChangeData.perfectEnvelope P

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.quasicoherentComponent {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData 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 obtained entirely from the bundled K-flat resolutions.

Equations

• D.quasicoherentComponent P = D.toDerivedBaseChangeData.quasicoherentComponent P

@[reducible, inline]

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

The full quasicoherent base-change category (Dqc)_T constructed from the bundled K-flat resolutions.

Equations

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

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.boundedComponent {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData 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 obtained entirely from the bundled K-flat resolutions.

Equations

• D.boundedComponent P = D.toDerivedBaseChangeData.boundedComponent P

@[reducible, inline]

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

The full bounded base-change category D_T constructed from the bundled K-flat resolutions.

Equations

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

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

Representative-level compactness conditions for the three K-flat operations bundled in KFlatBaseChangeData.

• fst : KFlatResolvedPullbackPreservesCompactObjects D.fstResolution (X.baseChangeFst T) ⋯
• snd : KFlatResolvedPullbackPreservesCompactObjects D.sndResolution (X.baseChangeSnd T) ⋯
• tensor : D.tensorResolution.ResolvedTensorPreservesCompactObjects ⋯

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.toDerivedPreservesCompactObjects {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (hD : D.PreservesCompactObjects) : D.toDerivedBaseChangeData.PreservesCompactObjects

Model-level compactness produces the model-free obligations. Both consequences below now route through the root rather than reproving on the resolutions.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.externalProduct_obj_isCompact {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData 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 representative-level compactness for the three resolutions, every external-product generator produced by the fully K-flat construction is compact.

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

Under representative-level compactness for the three resolutions, the whole fully K-flat perfect envelope consists of compact objects.