Pullback of invertible module sheaves

An arbitrary scheme morphism pulls locally free rank-one module sheaves back to locally free rank-one module sheaves. The proof pulls a chosen rank-one trivializing cover back along the underlying continuous map and transports each trivialization through pullbackOverIso.

No preservation certificate is stored as data: the result is a theorem about Mathlib's existing scheme-module pullback functor and the repository's intrinsic SheafOfModules.IsInvertible root.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackTrivializationOver {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) (U : Y.Opens) (e : SheafOfModules.unit (CategoryTheory.Sheaf.over Y.ringCatSheaf U) ≅ SheafOfModules.over M U) : SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf ((TopologicalSpace.Opens.map f.base).obj U)) ≅ SheafOfModules.over ((pullback f).obj M) ((TopologicalSpace.Opens.map f.base).obj U)

A trivialization of M on U pulls back to a trivialization of f⁺ M on f⁻¹ U: the structure-sheaf identification pullbackOverUnitIso, the trivialization transported by pullbackOverFunctor, and the restriction square pullbackOverIso.

Equations

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

instance AlgebraicGeometry.Scheme.Modules.isInvertible_pullback {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) [(have this := M; this).IsInvertible] : (have this := (pullback f).obj M; this).IsInvertible

Pullback along an arbitrary scheme morphism preserves intrinsic invertibility.