Right-derived pushforward along scheme morphisms

Ordinary pushforward of module sheaves is left exact, so applying it degreewise does not in general define a functor on derived categories. RightDerivedPushforward records an actual functor, its comparison with degreewise pushforward, and Mathlib's right-derived universal property. Thus later base-change constructions can accept the genuinely derived operation without postulating an unrelated functor.

When module-sheaf pushforward is exact, its degreewise derived functor inhabits the interface. Closed immersions provide a concrete geometric instance of this normalization.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPushforward {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left T).Modules ℤ) (CochainComplex (CategoryTheory.Over.left U).Modules ℤ)

Degreewise pushforward of cochain complexes of module sheaves.

Equations

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

class AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.IsExactPushforward {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) : Prop

The exactness condition under which module-sheaf pushforward derives degreewise.

• preservesFiniteLimits : CategoryTheory.Limits.PreservesFiniteLimits (modulePushforward f)

  Pushforward preserves finite limits.

• preservesFiniteColimits : CategoryTheory.Limits.PreservesFiniteColimits (modulePushforward f)

  Pushforward preserves finite colimits.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePushforward_preservesFiniteLimits {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) : CategoryTheory.Limits.PreservesFiniteLimits (modulePushforward f)

Module-sheaf pushforward preserves finite limits for every scheme morphism because it is a right adjoint.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.IsExactPushforward.of_preservesFiniteColimits {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [CategoryTheory.Limits.PreservesFiniteColimits (modulePushforward f)] : IsExactPushforward f

Construct exact pushforward from its only nonautomatic obligation.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isExactPushforward_of_isClosedImmersion {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsClosedImmersion (CategoryTheory.Over.Hom.left f)] : IsExactPushforward f

Pushforward along a closed immersion is exact.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPushforward {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPushforward f] : CategoryTheory.Functor T.DerivedFiber U.DerivedFiber

Degreewise derived pushforward when module-sheaf pushforward is exact.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPushforward f = (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePushforward f).mapDerivedCategory

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPushforwardFactors {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPushforward f] : (SchemeDerivedCategory.Q (CategoryTheory.Over.left T)).comp (derivedPushforward f) ≅ (complexPushforward f).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left U))

Exact derived pushforward is induced by degreewise pushforward before localization.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPushforwardFactors f = (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePushforward f).mapDerivedCategoryFactors

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instCommShiftDerivedFiberDerivedPushforwardInt {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPushforward f] : (derivedPushforward f).CommShift ℤ

Equations

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

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instIsTriangulatedDerivedFiberDerivedPushforward {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPushforward f] : (derivedPushforward f).IsTriangulated

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

An actual right-derived pushforward along an arbitrary scheme base-change morphism.

• functor : CategoryTheory.Functor T.DerivedFiber U.DerivedFiber

  The functor on unbounded derived categories of module sheaves.

• unit : (complexPushforward f).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)) ⟶ (SchemeDerivedCategory.Q (CategoryTheory.Over.left T)).comp self.functor

  Comparison from degreewise pushforward to the derived functor after localization.

• isRightDerived : self.functor.IsRightDerivedFunctor self.unit (HomologicalComplex.quasiIso (CategoryTheory.Over.left T).Modules (ComplexShape.up ℤ))

  The comparison exhibits functor as the right-derived pushforward.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.RightDerivedPushforward.ofExact {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPushforward f] : RightDerivedPushforward f

Exact derived pushforward satisfies the arbitrary right-derived interface.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.RightDerivedPushforward.identity {S : Scheme} (T : SchemeBaseChange S) : RightDerivedPushforward (CategoryTheory.CategoryStruct.id T)

Right-derived pushforward along the identity.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.RightDerivedPushforward.exactComparison {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : RightDerivedPushforward f) [IsExactPushforward f] : P.functor ≅ derivedPushforward f

Every right-derived pushforward agrees canonically with degreewise derived pushforward when ordinary pushforward is exact.

Equations

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

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.RightDerivedPushforward.congr {S : Scheme} {T U : SchemeBaseChange S} {f g : T ⟶ U} (P : RightDerivedPushforward f) (h : f = g) : RightDerivedPushforward g

Transport right-derived pushforward data along equality of the underlying morphisms.

Equations

• P.congr h = h ▸ P