Fixed-rank locally free atlases under pullback #
FiniteLocallyFreeData E n pulls back along any morphism of schemes to
FiniteLocallyFreeData (f⁺ E) n: the atlas is pullbackLocalGeneratorsData, whose index
types are those of the original atlas, so the rank equivalences carry over unchanged. This is
the rank-n input behind coherent pullback preserving perfect complexes
(DerivedCategory/Families/PerfectPullback.lean).
Main definitions #
Scheme.Modules.FiniteLocallyFreeData.pullback: the pulled-back atlas, of the same rank.
noncomputable def
AlgebraicGeometry.Scheme.Modules.FiniteLocallyFreeData.pullback
{X Y : Scheme}
(f : X ⟶ Y)
{E : Y.Modules}
{n : ℕ}
(D : E.FiniteLocallyFreeData n)
:
((Modules.pullback f).obj E).FiniteLocallyFreeData n
A fixed-rank locally free atlas pulls back along any morphism of schemes, with the same rank: the pulled-back generator data has the original index types.
Equations
- One or more equations did not get rendered due to their size.