Coherent pullback along a morphism of schemes

Pullback of module sheaves along any morphism of schemes preserves finite presentation, hence coherence. This file proves it and packages the result as the functor Coh.pullback f : Coh Y ⥤ Coh X. When Y is locally Noetherian, this functor is right exact; it is also left exact when module-sheaf pullback is, which flatness supplies.

Main definitions

• AlgebraicGeometry.Coh.pullback: the functor f^* : Coh Y ⥤ Coh X, with AlgebraicGeometry.Coh.pullbackCompι, its comparison with module-sheaf pullback.
• AlgebraicGeometry.Coh.pullbackComp, AlgebraicGeometry.Coh.pullbackId, and AlgebraicGeometry.Coh.pullbackEquivalence: coherent pullback respects composition and identities, and a scheme isomorphism induces an equivalence.

Main results

• AlgebraicGeometry.Scheme.Modules.isFinitePresentation_pullback and AlgebraicGeometry.Scheme.Modules.isCoherent_pullback: pullback preserves finite presentation and coherence, along every morphism; AlgebraicGeometry.Scheme.Modules.isFinite_pullbackPresentationOver is the chart-level statement.
• AlgebraicGeometry.Coh.pullback_preservesFiniteColimits: finite colimits are preserved when Y is locally Noetherian.
• AlgebraicGeometry.Coh.pullback_preservesFiniteLimits: finite limits are preserved when Y is locally Noetherian and module-sheaf pullback preserves finite limits.
• AlgebraicGeometry.Coh.pullback_additive: additivity holds for every scheme morphism.

The argument

A finitely presented sheaf is locally the cokernel of a map of finite free sheaves; pullback is right exact and sends free sheaves to free sheaves, so the cokernel presentation pulls back to a presentation on the preimage open. Mathlib's SheafOfModules.Presentation.map transports it for a colimit-preserving functor that fixes the structure sheaf; here the functor is pullback on slices, AlgebraicGeometry.Scheme.Modules.pullbackOverFunctor, with colimit preservation from AlgebraicGeometry.Scheme.Modules.pullbackOverFunctor_preservesColimits and the structure-sheaf identification AlgebraicGeometry.Scheme.Modules.pullbackOverUnitIso. The restriction square AlgebraicGeometry.Scheme.Modules.pullbackOverIso then moves the presentation onto (f⁺ M).over (f ⁻¹ᵁ U), and the preimages of a cover of Y cover X (AlgebraicGeometry.Scheme.Hom.coversTop_preimage).

Implementation notes

Two things about the proof are deliberate. Finiteness of the transported presentation is proved from the index types, which SheafOfModules.Presentation.map and SheafOfModules.Presentation.ofIsIso leave unchanged. The designated route, SheafOfModules.Presentation.isFinite_map supplied by haveI and the ofIsIso instance asked for by inferInstanceAs, fails to synthesize here, for the reason Algebra/Category/ModuleCat/Sheaf/Presentation/Finite.lean records: the universe parameters of these classes are not pinned by the goal and default to 0. And the quasi-coherent data of the pullback is a local definition inside the one proof that consumes it, with the universes of its finiteness written out and the class built field by field rather than by an anonymous constructor: naming the data globally and restating the finiteness of its projections makes Lean re-check instance arguments of the presentation type at whnf and does not terminate in the default heartbeat budget, and an anonymous constructor for either finiteness class elaborates it at universe 0 whatever the expected type says.

References

• Hartshorne, Algebraic Geometry, Proposition II.5.8(b) (pullback of a coherent sheaf; Hartshorne assumes X and Y noetherian, which finite presentation does not need) and Proposition II.5.2(e), f^*(M~) ≅ (M ⊗_A B)~, with II.5.2(a) and (c) for right exactness and direct sums, for the local model.

Tags

scheme modules, coherent sheaves, pullback

theorem AlgebraicGeometry.Scheme.Modules.isFinite_pullbackPresentationOver {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) (U : Y.Opens) (P : (SheafOfModules.over M U).Presentation) [hP : P.IsFinite] : (pullbackPresentationOver f M U P).IsFinite

The pulled-back presentation of a finite presentation is finite: neither SheafOfModules.Presentation.map nor SheafOfModules.Presentation.ofIsIso changes the index types of generators and relations.

theorem AlgebraicGeometry.Scheme.Modules.isFinitePresentation_pullback {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) (hM : SheafOfModules.IsFinitePresentation M) : SheafOfModules.IsFinitePresentation ((pullback f).obj M)

Pullback preserves finite presentation, along every morphism of schemes: the cover chosen for M pulls back to a cover of X, and each chart's presentation to AlgebraicGeometry.Scheme.Modules.pullbackPresentationOver, which is finite.

theorem AlgebraicGeometry.Scheme.Modules.isCoherent_pullback {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) (hM : IsCoherent Y M) : IsCoherent X ((pullback f).obj M)

Coherence is preserved by pullback along every morphism of schemes; no Noetherian or flatness hypothesis enters, because coherence in this repository is finite presentation.

noncomputable def AlgebraicGeometry.Coh.pullback {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.Functor (Coh Y) (Coh X)

Pullback of coherent sheaves along a morphism of schemes, f^* : Coh Y ⥤ Coh X: module-sheaf pullback restricted to coherent sheaves, which lands in coherent sheaves by AlgebraicGeometry.Scheme.Modules.isCoherent_pullback. Defined for every morphism; exactness is where a hypothesis on f enters.

Equations

• AlgebraicGeometry.Coh.pullback f = X.coherent.lift ((AlgebraicGeometry.Coh.ι Y).comp (AlgebraicGeometry.Scheme.Modules.pullback f)) ⋯

noncomputable def AlgebraicGeometry.Coh.pullbackCompι {X Y : Scheme} (f : X ⟶ Y) : (pullback f).comp (ι X) ≅ (ι Y).comp (Scheme.Modules.pullback f)

Forgetting coherence after coherent pullback is module-sheaf pullback after forgetting coherence. Definitional, since CategoryTheory.ObjectProperty.liftCompιIso is CategoryTheory.Iso.refl; recorded because the contract AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback asks for the comparison as data.

Equations

• AlgebraicGeometry.Coh.pullbackCompι f = X.coherent.liftCompιIso ((AlgebraicGeometry.Coh.ι Y).comp (AlgebraicGeometry.Scheme.Modules.pullback f)) ⋯

noncomputable def AlgebraicGeometry.Coh.pullbackComp {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) : (pullback g).comp (pullback f) ≅ pullback (CategoryTheory.CategoryStruct.comp f g)

Coherent pullback along a composite is the composite of coherent pullbacks. This is the module-sheaf comparison transported through the fully faithful inclusion.

Equations

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

noncomputable def AlgebraicGeometry.Coh.pullbackId (X : Scheme) : pullback (CategoryTheory.CategoryStruct.id X) ≅ CategoryTheory.Functor.id (Coh X)

Pullback along the identity morphism is naturally isomorphic to the identity on coherent sheaves.

Equations

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

noncomputable def AlgebraicGeometry.Coh.pullbackEquivalence {Y Z : Scheme} (e : Y ≅ Z) : Coh Z ≌ Coh Y

Pullback along a scheme isomorphism is an equivalence of coherent-sheaf categories. The inverse is ordinary coherent pullback along the inverse scheme morphism.

Equations

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

instance AlgebraicGeometry.Coh.pullback_preservesFiniteColimits {X Y : Scheme} (f : X ⟶ Y) [IsLocallyNoetherian Y] : CategoryTheory.Limits.PreservesFiniteColimits (pullback f)

When Y is locally Noetherian, coherent pullback preserves finite colimits for every morphism f: module-sheaf pullback is a left adjoint, Coh.ι Y is right exact, and the fully faithful Coh.ι X reflects. The composite instance is CategoryTheory.Limits.comp_preservesFiniteColimits, a lemma rather than an instance, hence supplied by name.

instance AlgebraicGeometry.Coh.pullback_preservesFiniteLimits {X Y : Scheme} (f : X ⟶ Y) [IsLocallyNoetherian Y] [CategoryTheory.Limits.PreservesFiniteLimits (Scheme.Modules.pullback f)] : CategoryTheory.Limits.PreservesFiniteLimits (pullback f)

Coherent pullback preserves finite limits when module-sheaf pullback does, which is the case for a flat morphism (proved in the families layer, Families/FlatPullback.lean, from flatness of the stalk maps); Coh.ι Y is left exact on a locally Noetherian scheme and the fully faithful Coh.ι X reflects.

instance AlgebraicGeometry.Coh.pullback_additive {X Y : Scheme} (f : X ⟶ Y) : (pullback f).Additive

Coherent pullback is additive, reflected through the faithful additive inclusion Coh.ι X. Needed by CategoryTheory.Functor.mapDerivedCategory, which asks for additivity separately from exactness.