The rank of a finite locally free sheaf

A finite locally free sheaf E on a scheme X is free on a finite basis over an open neighbourhood of every point. Its rank at x is the number of elements of such a basis around x. This does not depend on the neighbourhood or on the basis: two bases around x restrict to bases of E over their common neighbourhood W, and since Γ(X, W) is a nonzero commutative ring, isomorphic finite free sheaves over W have bases of the same cardinality. As the same basis computes the rank at every point of its neighbourhood, the rank is a locally constant function X → ℕ. It need not be constant: on a disconnected scheme the rank may differ between components.

Main declarations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank: the rank of a finite locally free sheaf, as a locally constant function on X, computed on any local basis by FiniteLocallyFreeSheaf.rank_apply_eq_natCard;
• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rankLocus: the clopen locus where the rank takes a given value;
• FiniteLocallyFreeSheaf.rank_eq_of_iso, FiniteLocallyFreeSheaf.rank_free_apply and FiniteLocallyFreeSheaf.rank_pullback_apply: the rank is invariant under isomorphism, is |I| for the free sheaf on I, and is preserved by pullback;
• FiniteLocallyFreeSheaf.rank_biprod_apply and FiniteLocallyFreeSheaf.rank_tensor_apply: rank is additive under direct sums and multiplicative under tensor products;
• FiniteLocallyFreeSheaf.isInvertible_iff_forall_rank_eq_one: the invertible sheaves are exactly the finite locally free sheaves of rank one at every point, so that the fully faithful inclusion InvertibleSheaf.toFiniteLocallyFree identifies InvertibleSheaf X with the rank-one objects (InvertibleSheaf.rank_toFiniteLocallyFree_apply).

References

• The Stacks Project, Tag 01C9
• [R. Hartshorne, Algebraic Geometry][hartshorne1977], Chapter II, Section 5

theorem TauCeti.AlgebraicGeometry.natCard_generatingSections_eq_of_mem {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U V : X.Opens} {x : ↥X} (hU : x ∈ U) (hV : x ∈ V) (σ : (SheafOfModules.over M U).GeneratingSections) (τ : (SheafOfModules.over M V).GeneratingSections) [CategoryTheory.IsIso σ.π] [CategoryTheory.IsIso τ.π] [Finite σ.I] [Finite τ.I] : Nat.card σ.I = Nat.card τ.I

Two finite bases of an 𝒪_X-module over open neighbourhoods of a common point have the same number of elements.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.exists_generatingSections {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) (x : ↥X) : ∃ (U : X.Opens) (_ : x ∈ U) (σ : (SheafOfModules.over E.obj U).GeneratingSections), CategoryTheory.IsIso σ.π ∧ Finite σ.I

A finite locally free sheaf is free on a finite basis over some open neighbourhood of each point.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : LocallyConstant ↥X ℕ

The rank of a finite locally free sheaf E on X, as a locally constant function on X. Its value at x is the number of elements of a basis of E over any open neighbourhood of x on which E is free (rank_apply_eq_natCard).

Equations

• E.rank = { toFun := TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rankAt✝ E, isLocallyConstant := ⋯ }

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_apply_eq_natCard {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) {U : X.Opens} {x : ↥X} (hx : x ∈ U) (σ : (SheafOfModules.over E.obj U).GeneratingSections) [CategoryTheory.IsIso σ.π] [Finite σ.I] : E.rank x = Nat.card σ.I

The rank of E at x is the number of elements of any basis of E over an open neighbourhood of x.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_eq_of_iso {X : AlgebraicGeometry.Scheme} {E F : FiniteLocallyFreeSheaf X} (e : E.obj ≅ F.obj) : E.rank = F.rank

Isomorphic finite locally free sheaves have the same rank.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_free_apply {X : AlgebraicGeometry.Scheme} (I : Type u) [Finite I] (x : ↥X) : (free X I).rank x = Nat.card I

The free sheaf on a finite type I has rank |I| at every point.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_pullback_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (E : FiniteLocallyFreeSheaf Y) (x : ↥X) : ((pullback f).obj E).rank x = E.rank (f x)

The rank of the pullback of a finite locally free sheaf E along f : X ⟶ Y at x is the rank of E at f x.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_biprod_apply {X : AlgebraicGeometry.Scheme} (E F : FiniteLocallyFreeSheaf X) (x : ↥X) : (E ⊞ F).rank x = E.rank x + F.rank x

The rank of a direct sum is the sum of the ranks of its summands.

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_tensor_apply {X : AlgebraicGeometry.Scheme} (E F : FiniteLocallyFreeSheaf X) (x : ↥X) : (CategoryTheory.MonoidalCategoryStruct.tensorObj E F).rank x = E.rank x * F.rank x

The rank of a tensor product is the product of the ranks of its factors.

def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rankLocus {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) (n : ℕ) : TopologicalSpace.Clopens ↥X

The rank locus of E in rank n: the clopen set of points at which E has rank n.

Equations

• E.rankLocus n = { carrier := ⇑E.rank ⁻¹' {n}, isClopen' := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.mem_rankLocus {X : AlgebraicGeometry.Scheme} {E : FiniteLocallyFreeSheaf X} {n : ℕ} {x : ↥X} : x ∈ E.rankLocus n ↔ E.rank x = n

A point lies in the rank locus of E in rank n exactly when E has rank n there.

@[simp]

theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.rank_toFiniteLocallyFree_apply {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) (x : ↥X) : ((toFiniteLocallyFree X).obj L).rank x = 1

An invertible sheaf has rank one at every point.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.isInvertible_iff_forall_rank_eq_one {X : AlgebraicGeometry.Scheme} (E : FiniteLocallyFreeSheaf X) : SheafOfModules.isInvertible X E.obj ↔ ∀ (x : ↥X), E.rank x = 1

A finite locally free sheaf is invertible if and only if it has rank one at every point.