Exact pullback on scheme-derived fibers

Mathlib constructs an additive pullback functor on sheaves of modules for every scheme morphism, together with coherent identity and composition isomorphisms. This file exposes that functor for morphisms between scheme base changes and lifts it to the concrete derived categories from Families.SchemeDerived when the pullback functor is exact.

Exactness is an explicit hypothesis. In particular, this file does not assert that pullback along an arbitrary scheme morphism is exact, prove the hypothesis from flatness, construct a left-derived functor for a nonexact pullback, or supply pseudofunctor coherence after passage to derived categories. It also asserts no geometric slicing, relative HN, openness, boundedness, moduli, or Theorem 22.2 conclusion.

@[reducible, inline]

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

Pullback of sheaves of modules along a morphism of scheme base changes.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePullback f = AlgebraicGeometry.Scheme.Modules.pullback (CategoryTheory.Over.Hom.left f)

@[reducible, inline]

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

Pushforward of sheaves of modules along a morphism of scheme base changes, the right adjoint of modulePullback through Scheme.Modules.pullbackPushforwardAdjunction. Its coherent restriction and derived direct image live in Families/CoherentPushforward.lean.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePushforward f = AlgebraicGeometry.Scheme.Modules.pushforward (CategoryTheory.Over.Hom.left f)

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePullbackId {S : Scheme} (T : SchemeBaseChange S) : modulePullback (CategoryTheory.CategoryStruct.id T) ≅ CategoryTheory.Functor.id (CategoryTheory.Over.left T).Modules

Module pullback along the identity is naturally isomorphic to the identity functor.

Equations

• T.modulePullbackId = AlgebraicGeometry.Scheme.Modules.pullbackId (CategoryTheory.Over.left T)

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePullbackComp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) : (modulePullback g).comp (modulePullback f) ≅ modulePullback (CategoryTheory.CategoryStruct.comp f g)

Module pullback along a composite is the composite of the pullbacks.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePullbackComp f g = AlgebraicGeometry.Scheme.Modules.pullbackComp (CategoryTheory.Over.Hom.left f) (CategoryTheory.Over.Hom.left g)

@[reducible, inline]

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

Degreewise pullback of cochain complexes of module sheaves.

Equations

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

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

The explicit exactness requirement under which ordinary module pullback descends to the derived categories by mapping complexes degreewise.

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

  Pullback preserves finite limits.

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

  Pullback preserves finite colimits.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePullback_preservesFiniteColimits {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) : CategoryTheory.Limits.PreservesFiniteColimits (modulePullback f)

Module-sheaf pullback preserves finite colimits for every scheme morphism, because it is left adjoint to module-sheaf pushforward.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.IsExactPullback.of_preservesFiniteLimits {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [CategoryTheory.Limits.PreservesFiniteLimits (modulePullback f)] : IsExactPullback f

Construct exact module-sheaf pullback from the only nonautomatic obligation: preservation of finite limits.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isExactPullback_iff_preservesFiniteLimits {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) : IsExactPullback f ↔ CategoryTheory.Limits.PreservesFiniteLimits (modulePullback f)

Exactness of module-sheaf pullback is equivalent to preservation of finite limits; finite-colimit preservation is automatic.

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

The triangulated pullback functor between concrete scheme-derived fibers, defined when module pullback is exact.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback f = (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePullback f).mapDerivedCategory

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullbackFactors {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] : (SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).comp (derivedPullback f) ≅ (complexPullback f).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left T))

The derived pullback is induced by degreewise pullback of cochain complexes and the two localization functors.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullbackFactors f = (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.modulePullback f).mapDerivedCategoryFactors

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instCommShiftDerivedFiberDerivedPullbackInt {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] : (derivedPullback f).CommShift ℤ

Equations

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

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.instIsTriangulatedDerivedFiberDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] : (derivedPullback f).IsTriangulated

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullK₀ {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] : CategoryTheory.Triangulated.K₀ U.DerivedFiber →+ CategoryTheory.Triangulated.K₀ T.DerivedFiber

Pullback on the triangulated Grothendieck groups of the concrete derived fibers.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullK₀ f = CategoryTheory.Triangulated.K₀.map (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback f)

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullK₀_of {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] (E : U.DerivedFiber) : (derivedPullK₀ f) (CategoryTheory.Triangulated.K₀.of U.DerivedFiber E) = CategoryTheory.Triangulated.K₀.of T.DerivedFiber ((derivedPullback f).obj E)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullToResidue {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) [IsExactPullback (T.residueTo x)] : CategoryTheory.Functor T.DerivedFiber (T.ResidueDerivedFiber x)

Exact pullback from a scheme base change to its residue-field derived fiber. Exactness of this particular module pullback remains explicit.

Equations

• T.derivedPullToResidue x = AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback (T.residueTo x)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullK₀ToResidue {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) [IsExactPullback (T.residueTo x)] : CategoryTheory.Triangulated.K₀ T.DerivedFiber →+ CategoryTheory.Triangulated.K₀ (T.ResidueDerivedFiber x)

Exact pullback on Grothendieck groups from a scheme base change to its residue-field derived fiber.

Equations

• T.derivedPullK₀ToResidue x = AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullK₀ (T.residueTo x)

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullK₀ToResidue_of {S : Scheme} (T : SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) [IsExactPullback (T.residueTo x)] (E : T.DerivedFiber) : (T.derivedPullK₀ToResidue x) (CategoryTheory.Triangulated.K₀.of T.DerivedFiber E) = CategoryTheory.Triangulated.K₀.of (T.ResidueDerivedFiber x) ((T.derivedPullToResidue x).obj E)