Finite local freeness is local on the scheme

An 𝒪_X-module M on a scheme X is finite locally free exactly when it is trivialized by an open cover of X: for some open cover fᵢ : Uᵢ ⟶ X, each pullback fᵢ^* M is isomorphic to the free 𝒪_{Uᵢ}-module on a finite type (AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree_iff_exists_openCover). Consequently finite local freeness can be checked on any open cover (AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree_iff_forall_pullback): M is finite locally free if and only if every fᵢ^* M is.

Finite local freeness of 𝒪_X-modules is defined on the site of opens of X, through finite local bases over the slices at a cover of X by opens (SheafOfModules.isFiniteLocallyFree_iff_exists_isLocallyFreeData_isFiniteType). The characterization by open covers states it instead through the modules on the open subschemes Uᵢ. The slice at an open U and the open subscheme U carry equivalent categories of modules (AlgebraicGeometry.Scheme.Modules.overEquiv), restriction along U.ι corresponds to restriction to the slice (AlgebraicGeometry.Scheme.Modules.overFunctorEquiv), and these identifications, as well as pullback along an isomorphism of schemes, preserve free modules. An arbitrary open immersion f is identified with the inclusion of its open image f.opensRange through the isomorphism f.isoOpensRange.

Checking on an open cover is how statements about modules on affine schemes, where they are modules over a ring, extend to modules on arbitrary schemes, along an affine open cover.

Main declarations

• AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree_iff_exists_openCover: a module is finite locally free if and only if some open cover trivializes it with finite free modules;
• AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree_iff_forall_pullback: a module is finite locally free if and only if its pullback to each member of a given open cover is.

References

• The Stacks Project, Tag 01C6

theorem AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree_iff_exists_openCover {X : Scheme} (M : X.Modules) : isFiniteLocallyFree X M ↔ ∃ (𝒰 : X.OpenCover), ∀ (i : 𝒰.I₀), ∃ (I : Type u), Finite I ∧ Nonempty ((pullback (𝒰.f i)).obj M ≅ SheafOfModules.free I)

An 𝒪_X-module is finite locally free if and only if it is trivialized by an open cover: for some open cover fᵢ : Uᵢ ⟶ X, each pullback fᵢ^* M is isomorphic to the free 𝒪_{Uᵢ}-module on a finite type.

theorem AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree_iff_forall_pullback {X : Scheme} (𝒰 : X.OpenCover) (M : X.Modules) : isFiniteLocallyFree X M ↔ ∀ (i : 𝒰.I₀), isFiniteLocallyFree (𝒰.X i) ((pullback (𝒰.f i)).obj M)

Finite local freeness of 𝒪_X-modules can be checked on an open cover: an 𝒪_X-module M is finite locally free if and only if its pullback fᵢ^* M to each member fᵢ : Uᵢ ⟶ X of an open cover is.