Documentation

TauCeti.AlgebraicGeometry.LineBundle.GlobalGeneration

Global generation of line bundles #

A line bundle is globally generated if every point has a global section which generates its stalk. Equivalently, the nonvanishing loci of its global sections cover the scheme. A morphism to the residue skyscraper detects a generating section whenever its image is nonzero. This criterion turns surjectivity of restriction to a point into generation of the line bundle there. Global generation is equivalent to the existence of Mathlib's SheafOfModules.GeneratingSections, including the epimorphism from a free sheaf onto the line bundle.

References #

source
theorem TauCeti.AlgebraicGeometry.exists_skyscraperResidueFieldHom_ne_zero {X : AlgebraicGeometry.Scheme} {M : X.Modules} [SheafOfModules.isInvertible X M] (x : ↥X) :
∃ (φ : M ⟶ AlgebraicGeometry.Scheme.skyscraperResidueField x), φ ≠ 0

An invertible sheaf has a nonzero morphism to the residue skyscraper at every point.

source
theorem TauCeti.AlgebraicGeometry.mem_nonvanishingLocus_of_app_ne_zero {X : AlgebraicGeometry.Scheme} {M : X.Modules} [SheafOfModules.isInvertible X M] {U : X.Opens} {x : ↥X} (hx : x ∈ U) (φ : M ⟶ AlgebraicGeometry.Scheme.skyscraperResidueField x) (s : ↑(M.presheaf.obj (Opposite.op U))) (hs : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app φ U)) s ≠ 0) :
x ∈ M.nonvanishingLocus s

A section of an invertible sheaf generates at x if some morphism to the residue skyscraper at x sends it to a nonzero element.

source
def TauCeti.AlgebraicGeometry.InvertibleSheaf.IsGloballyGenerated {X : AlgebraicGeometry.Scheme} (L : InvertibleSheaf X) :
Prop

A line bundle is globally generated if, at each point, some global section generates the stalk.

Instances For
    source
    theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.isGloballyGenerated_iff {X : AlgebraicGeometry.Scheme} {L : InvertibleSheaf X} :
    L.IsGloballyGenerated ↔ ∀ (x : ↥X), ∃ (s : ↑(L.obj.presheaf.obj (Opposite.op ⊤))), x ∈ L.obj.nonvanishingLocus s

    Global generation means that a generating global section exists at each point.

    source
    theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.isGloballyGenerated_iff_iSup_nonvanishingLocus_eq_top {X : AlgebraicGeometry.Scheme} {L : InvertibleSheaf X} :
    L.IsGloballyGenerated ↔ ⨆ (s : ↑(L.obj.presheaf.obj (Opposite.op ⊤))), L.obj.nonvanishingLocus s = ⊤

    Global generation is equivalent to the nonvanishing loci of global sections covering X.

    source
    theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.isGloballyGenerated_iff_of_iso {X : AlgebraicGeometry.Scheme} {L N : InvertibleSheaf X} (e : L.obj ≅ N.obj) :
    L.IsGloballyGenerated ↔ N.IsGloballyGenerated

    Global generation is invariant under isomorphism of line bundles.

    source
    theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.isGloballyGenerated_iff_forall_isClosed {X : AlgebraicGeometry.Scheme} [JacobsonSpace ↥X] {L : InvertibleSheaf X} :
    L.IsGloballyGenerated ↔ ∀ (x : ↥X), IsClosed {x} → ∃ (s : ↑(L.obj.presheaf.obj (Opposite.op ⊤))), x ∈ L.obj.nonvanishingLocus s

    On a Jacobson scheme, global generation can be checked at closed points.

    source
    theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.IsGloballyGenerated.hom_ext {X : AlgebraicGeometry.Scheme} {L : InvertibleSheaf X} (hL : L.IsGloballyGenerated) {N : X.Modules} (f g : L.obj ⟶ N) (htop : ∀ (s : ↑(L.obj.presheaf.obj (Opposite.op ⊤))), (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app f ⊤)) s = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app g ⊤)) s) :
    f = g

    Morphisms out of a globally generated line bundle are determined by global sections.

    source
    theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.IsGloballyGenerated.nonempty_generatingSections {X : AlgebraicGeometry.Scheme} {L : InvertibleSheaf X} (hL : L.IsGloballyGenerated) :
    Nonempty (SheafOfModules.GeneratingSections L.obj)

    A globally generated line bundle admits Mathlib's generating-section data. The associated morphism from the free sheaf is an epimorphism.

    source
    theorem TauCeti.AlgebraicGeometry.InvertibleSheaf.isGloballyGenerated_iff_nonempty_generatingSections {X : AlgebraicGeometry.Scheme} {L : InvertibleSheaf X} :
    L.IsGloballyGenerated ↔ Nonempty (SheafOfModules.GeneratingSections L.obj)

    Global generation of a line bundle is equivalent to the existence of Mathlib's family of generating global sections.