Left-derived pullback along arbitrary scheme morphisms

Ordinary pullback of module sheaves is right exact, so applying it degreewise does not define a functor on unbounded derived categories for an arbitrary scheme morphism. This file records the correct construction boundary.

A LeftDerivedPullback contains an actual functor between the scheme-derived categories, a comparison from localization followed by that functor to degreewise module pullback followed by localization, and Mathlib's left-derived universal property for this comparison. Thus an inhabitant cannot be supplied by choosing an unrelated functor.

Exact pullback gives a genuine inhabitant. The later K-flat construction can provide inhabitants for nonexact morphisms through the same interface.

Main definitions

• SchemeBaseChange.LeftDerivedPullback: arbitrary left-derived pullback data with its universal property.
• SchemeBaseChange.LeftDerivedPullback.ofExact: the existing exact derived pullback as an instance of the general interface.
• SchemeBaseChange.LeftDerivedPullback.exactComparison: uniqueness of the general and exact constructions when ordinary pullback is exact.

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

An actual left-derived pullback along an arbitrary scheme base-change morphism.

The isLeftDerived field is the universal property of the displayed comparison. It is deliberately stronger than storing only a functor with the correct source and target.

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

  The functor on the unbounded derived categories of module sheaves.

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

  Comparison from applying the functor after localization to applying ordinary pullback degreewise before localization.

• isLeftDerived : self.functor.IsLeftDerivedFunctor self.counit (HomologicalComplex.quasiIso (CategoryTheory.Over.left U).Modules (ComplexShape.up ℤ))

  The comparison exhibits functor as the left-derived functor of degreewise module pullback.

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

Exact derived pullback satisfies the arbitrary left-derived pullback interface.

Equations

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

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

The left-derived pullback along the identity morphism.

Equations

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

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

Any arbitrary left-derived pullback agrees canonically with the existing exact construction when ordinary pullback is exact.

Equations

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

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

Transport arbitrary derived-pullback data along equality of the underlying scheme base-change morphisms.

Equations

• P.congr h = h ▸ P