Transport of module-sheaf presentations by scheme pullback

The presentation transport is independent of finite generation or quasi-coherence. Both quasi-coherent and coherent pullback consume it.

Main definitions

• AlgebraicGeometry.Scheme.Modules.pullbackPresentationOver transports a presentation on an open through pullback on slice sites.

Main results

The transported presentation has no finiteness requirement and can be used by both the quasi-coherent and coherent module-sheaf owners.

Implementation notes

SheafOfModules.Presentation.map uses the left-adjoint pullback on slice sites and its unit comparison; SheafOfModules.Presentation.ofIsIso transports across the restriction square.

References

The construction uses pinned Mathlib's SheafOfModules.Presentation.map and the repository's AlgebraicGeometry.Scheme.Modules.pullbackOverIso.

Tags

scheme modules, pullback, presentations

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackPresentationOver {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) (U : Y.Opens) (P : (SheafOfModules.over M U).Presentation) : (SheafOfModules.over ((pullback f).obj M) ((TopologicalSpace.Opens.map f.base).obj U)).Presentation

A presentation of M on U pulls back to a presentation of f⁺ M on f⁻¹ U: transport along pullback on slices, then across the restriction square AlgebraicGeometry.Scheme.Modules.pullbackOverIso. No finiteness premise is needed.

Equations

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