Pushforward between constructed base-change categories

This file lifts a genuine RightDerivedPushforward to Dqc, restricts it to intrinsic bounded-coherent complexes, and then restricts both functors to the derived base-change components. The ambient right-derived universal property remains part of the data throughout.

For a morphism f : T ⟶ U, the induced morphism of fibre products is X ×_S T ⟶ X ×_S U; pushforward therefore runs from the component over T to the component over U.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) : Type (u + 1)

A genuine right-derived pushforward which preserves quasicoherent cohomology.

• ambient : RightDerivedPushforward f

  The right-derived pushforward on ambient derived categories.

• mapsQuasicoherent (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left T)) : Dqc.schemeQuasicoherentCohomology (CategoryTheory.Over.left U) (self.ambient.functor.obj E.obj)

  Ambient right-derived pushforward preserves quasicoherent cohomology.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward.functor {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : DqcRightDerivedPushforward f) : CategoryTheory.Functor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left T)) (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left U))

Lift a genuine right-derived pushforward to the Dqc loci.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward.functorCompInclusion {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : DqcRightDerivedPushforward f) : P.functor.comp (Dqc.SchemeQuasicoherentDerivedCategory.ι (CategoryTheory.Over.left U)) ≅ (Dqc.SchemeQuasicoherentDerivedCategory.ι (CategoryTheory.Over.left T)).comp P.ambient.functor

Forgetting quasicoherence witnesses recovers the ambient right-derived pushforward.

Equations

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

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward.functor_obj_obj {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : DqcRightDerivedPushforward f) (E : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left T)) : (P.functor.obj E).obj = P.ambient.functor.obj E.obj

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward.functor_full {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : DqcRightDerivedPushforward f) [P.ambient.functor.Full] : P.functor.Full

Fullness of ambient right-derived pushforward descends to its Dqc restriction.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward.functor_faithful {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : DqcRightDerivedPushforward f) [P.ambient.functor.Faithful] : P.functor.Faithful

Faithfulness of ambient right-derived pushforward descends to its Dqc restriction.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward.PreservesBoundedCoherent {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : DqcRightDerivedPushforward f) : Prop

A Dqc right-derived pushforward preserves intrinsic bounded-coherent complexes.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward.boundedFunctor {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : DqcRightDerivedPushforward f) (h : P.PreservesBoundedCoherent) : CategoryTheory.Functor (Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left T)) (Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left U))

Restrict right-derived pushforward to intrinsic bounded-coherent complexes.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward.boundedFunctorCompInclusion {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : DqcRightDerivedPushforward f) (h : P.PreservesBoundedCoherent) : (P.boundedFunctor h).comp (Dqc.SchemeBoundedCoherentDqcCategory.ι (CategoryTheory.Over.left U)) ≅ (Dqc.SchemeBoundedCoherentDqcCategory.ι (CategoryTheory.Over.left T)).comp P.functor

Forgetting bounded-coherent witnesses recovers right-derived pushforward on Dqc.

Equations

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

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward.boundedFunctor_obj_obj {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : DqcRightDerivedPushforward f) (h : P.PreservesBoundedCoherent) (E : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left T)) : ((P.boundedFunctor h).obj E).obj = P.functor.obj E.obj

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward.boundedFunctor_full {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : DqcRightDerivedPushforward f) (h : P.PreservesBoundedCoherent) [P.functor.Full] : (P.boundedFunctor h).Full

Fullness of right-derived pushforward on Dqc descends to its intrinsic bounded-coherent restriction.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DqcRightDerivedPushforward.boundedFunctor_faithful {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : DqcRightDerivedPushforward f) (h : P.PreservesBoundedCoherent) [P.functor.Faithful] : (P.boundedFunctor h).Faithful

Faithfulness of right-derived pushforward on Dqc descends to its intrinsic bounded-coherent restriction.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PushforwardPreservesQuasicoherentComponent {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) : Prop

The component-level condition that right-derived pushforward preserves (Dqc).

Equations

• DT.PushforwardPreservesQuasicoherentComponent DU P push = (DT.quasicoherentComponent P ≤ (DU.quasicoherentComponent P).inverseImage push.functor)

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PushforwardMapsPerfectEnvelope {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) : Prop

The smaller generator-level condition that pushforward sends the source perfect envelope into the target quasicoherent component.

Equations

• DT.PushforwardMapsPerfectEnvelope DU P push = ((DT.perfectEnvelope P).map push.functor ≤ DU.quasicoherentComponent P)

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.pushforward_preservesQuasicoherentComponent_of_perfectEnvelope {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) [push.functor.CommShift ℤ] [push.functor.IsTriangulated] (hCoproducts : push.functor.PreservesSmallCoproducts) (hEnvelope : DT.PushforwardMapsPerfectEnvelope DU P push) : DT.PushforwardPreservesQuasicoherentComponent DU P push

A coproduct-preserving triangulated pushforward preserves the whole quasicoherent component once it maps the perfect envelope into the target component.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPushforward {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (h : DT.PushforwardPreservesQuasicoherentComponent DU P push) : CategoryTheory.Functor (DT.QuasicoherentCategory P) (DU.QuasicoherentCategory P)

Right-derived pushforward between the constructed quasicoherent base-change categories.

Equations

• DT.quasicoherentPushforward DU P push h = CategoryTheory.ObjectProperty.liftOfLE push.functor h

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPushforwardOfPerfectEnvelope {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) [push.functor.CommShift ℤ] [push.functor.IsTriangulated] (hCoproducts : push.functor.PreservesSmallCoproducts) (hEnvelope : DT.PushforwardMapsPerfectEnvelope DU P push) : CategoryTheory.Functor (DT.QuasicoherentCategory P) (DU.QuasicoherentCategory P)

Pushforward between quasicoherent base-change components, constructed from the smaller perfect-envelope preservation condition.

Equations

• DT.quasicoherentPushforwardOfPerfectEnvelope DU P push hCoproducts hEnvelope = DT.quasicoherentPushforward DU P push ⋯

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPushforwardCompInclusion {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (h : DT.PushforwardPreservesQuasicoherentComponent DU P push) : (DT.quasicoherentPushforward DU P push h).comp (DU.quasicoherentComponent P).ι ≅ (DT.quasicoherentComponent P).ι.comp push.functor

Forgetting component witnesses recovers right-derived pushforward on Dqc.

Equations

• DT.quasicoherentPushforwardCompInclusion DU P push h = (DU.quasicoherentComponent P).liftCompιIso ((DT.quasicoherentComponent P).ι.comp push.functor) ⋯

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.pushforward_preservesBoundedComponent {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (hDqc : DT.PushforwardPreservesQuasicoherentComponent DU P push) (hBounded : push.PreservesBoundedCoherent) : DT.boundedComponent P ≤ (DU.boundedComponent P).inverseImage (push.boundedFunctor hBounded)

Preservation of the bounded base-change component follows formally from preservation of its quasicoherent companion and of intrinsic bounded-coherent complexes.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPushforward {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (hDqc : DT.PushforwardPreservesQuasicoherentComponent DU P push) (hBounded : push.PreservesBoundedCoherent) : CategoryTheory.Functor (DT.BoundedCategory P) (DU.BoundedCategory P)

Right-derived pushforward between the constructed bounded base-change categories.

Equations

• DT.boundedPushforward DU P push hDqc hBounded = CategoryTheory.ObjectProperty.liftOfLE (push.boundedFunctor hBounded) ⋯

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPushforwardOfPerfectEnvelope {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) [push.functor.CommShift ℤ] [push.functor.IsTriangulated] (hCoproducts : push.functor.PreservesSmallCoproducts) (hEnvelope : DT.PushforwardMapsPerfectEnvelope DU P push) (hBounded : push.PreservesBoundedCoherent) : CategoryTheory.Functor (DT.BoundedCategory P) (DU.BoundedCategory P)

Bounded pushforward constructed from perfect-envelope preservation and preservation of intrinsic bounded-coherent objects.

Equations

• DT.boundedPushforwardOfPerfectEnvelope DU P push hCoproducts hEnvelope hBounded = DT.boundedPushforward DU P push ⋯ hBounded

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPushforwardCompInclusion {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (hDqc : DT.PushforwardPreservesQuasicoherentComponent DU P push) (hBounded : push.PreservesBoundedCoherent) : (DT.boundedPushforward DU P push hDqc hBounded).comp (DU.boundedComponent P).ι ≅ (DT.boundedComponent P).ι.comp (push.boundedFunctor hBounded)

Forgetting component witnesses recovers pushforward on intrinsic bounded-coherent loci.

Equations

• DT.boundedPushforwardCompInclusion DU P push hDqc hBounded = (DU.boundedComponent P).liftCompιIso ((DT.boundedComponent P).ι.comp (push.boundedFunctor hBounded)) ⋯