Locally free sheaves under pullback

Pullback of module sheaves along any morphism of schemes preserves local freeness, with the same index type on each chart. On a chart U of Y the generating sections of M.over U are transported by Mathlib's GeneratingSections.map along pullback on slices, pullbackOverFunctor, which preserves coproducts, being a left adjoint, and sends the structure sheaf to the structure sheaf (pullbackOverUnitIso); the restriction square pullbackOverIso then moves them onto (f⁺ M).over (f ⁻¹ᵁ U). This is the site-level LocalGeneratorsData.transport applied chart by chart, and a free basis stays a free basis because GeneratingSections.map sends an isomorphism π to an isomorphism. No flatness enters, exactly as for invertible sheaves in Pullback/Invertible.lean, and the transport is the one Coherent/Pullback.lean runs on presentations.

Main definitions

• Scheme.Modules.pullbackLocalGeneratorsData: local generator data pulls back, on the preimage cover with the same index types.

Main results

• Scheme.Modules.isLocallyFreeData_pullbackLocalGeneratorsData: locally free data pulls back to locally free data;
• Scheme.Modules.isLocallyFree_pullback: pullback preserves local freeness.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackLocalGeneratorsData {X Y : Scheme} (f : X ⟶ Y) {E : Y.Modules} (q : (have this := E; this).LocalGeneratorsData) : (have this := (pullback f).obj E; this).LocalGeneratorsData

Local generator data pulls back along any morphism of schemes: on the preimage of each chart the generators are GeneratingSections.map along pullback on slices, moved onto (f⁺ E).over (f ⁻¹ᵁ U) by the restriction square, with the same index types (LocalGeneratorsData.transport).

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullbackLocalGeneratorsData_generators_I {X Y : Scheme} (f : X ⟶ Y) {E : Y.Modules} (q : (have this := E; this).LocalGeneratorsData) (i : q.I) : ((pullbackLocalGeneratorsData f q).generators i).I = (q.generators i).I

The pulled-back generators on the preimage of a chart have the original index type: this is what lets a fixed-rank atlas pull back with its rank.

instance AlgebraicGeometry.Scheme.Modules.isLocallyFreeData_pullbackLocalGeneratorsData {X Y : Scheme} (f : X ⟶ Y) {E : Y.Modules} (q : (have this := E; this).LocalGeneratorsData) [q.IsLocallyFreeData] : (pullbackLocalGeneratorsData f q).IsLocallyFreeData

Locally free data pulls back to locally free data (LocalGeneratorsData.isLocallyFreeData_transport).

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

Pullback preserves local freeness with no flatness hypothesis: chart generators are transported by pullbackOverFunctor, a left adjoint fixing the structure sheaf, exactly as in isInvertible_pullback. The data is pullbackLocalGeneratorsData; this lemma forgets it to the Prop through LocalGeneratorsData.isLocallyFree. It is registered as an instance, keyed at the show SheafOfModules _ from _ spelling, so it fires on goals written at that spelling.