Stalks of invertible sheaves

The stalk of an invertible sheaf M on a scheme X at a point x is free of rank one over the local ring 𝒪_{X,x}: the germ of the basis section of a rank-one trivialization near x is a basis. This is the pointwise form of local freeness used to read off local generators of a line bundle, for instance of the sheaf of differentials of a smooth curve.

Main results

• AlgebraicGeometry.Scheme.Modules.nonempty_linearEquiv_stalk_of_isInvertible: the stalk of an invertible sheaf is isomorphic to the local ring as a module over it;
• AlgebraicGeometry.Scheme.Modules.free_stalk_of_isInvertible and AlgebraicGeometry.Scheme.Modules.finrank_stalk_of_isInvertible: the stalk is free of rank one.
• AlgebraicGeometry.Scheme.Modules.span_germ_trivializationGenerator: the germ of the basis section of a rank-one trivialization generates the stalk.
• AlgebraicGeometry.Scheme.Modules.bijective_toSpanSingleton_of_span_eq_top: every generator of the stalk of an invertible sheaf is a basis of it, and AlgebraicGeometry.Scheme.Modules.span_smul_eq_top_iff: a multiple a • g generates the stalk exactly when a is a unit and g generates.

theorem AlgebraicGeometry.Scheme.Modules.span_germ_trivializationGenerator {X : Scheme} (M : X.Modules) (x : ↥X) {V : X.Opens} (t : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over M V) (hxV : x ∈ V) : ↑(X.presheaf.stalk x) ∙ (CategoryTheory.ConcreteCategory.hom (M.presheaf.germ V x hxV)) (M.trivializationGenerator t) = ⊤

The germ of the basis section of a rank-one trivialization generates the stalk: every germ of a section of M is a germ of a regular function times it.

theorem AlgebraicGeometry.Scheme.Modules.nonempty_linearEquiv_stalk_of_isInvertible {X : Scheme} (M : X.Modules) [TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X M] (x : ↥X) : Nonempty (↑(X.presheaf.stalk x) ≃ₗ[↑(X.presheaf.stalk x)] ↑(M.presheaf.stalk x))

The stalk of an invertible sheaf is free of rank one. The stalk M_x of an invertible sheaf is isomorphic to the local ring 𝒪_{X,x} as a module over it.

instance AlgebraicGeometry.Scheme.Modules.free_stalk_of_isInvertible {X : Scheme} (M : X.Modules) [TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X M] (x : ↥X) : Module.Free ↑(X.presheaf.stalk x) ↑(M.presheaf.stalk x)

The stalk of an invertible sheaf is a free module over the local ring.

theorem AlgebraicGeometry.Scheme.Modules.finrank_stalk_of_isInvertible {X : Scheme} (M : X.Modules) [TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X M] (x : ↥X) : Module.finrank ↑(X.presheaf.stalk x) ↑(M.presheaf.stalk x) = 1

The stalk of an invertible sheaf has rank one over the local ring.

theorem AlgebraicGeometry.Scheme.Modules.bijective_toSpanSingleton_of_span_eq_top {X : Scheme} (M : X.Modules) [TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X M] (x : ↥X) {g : ↑(M.presheaf.stalk x)} (hg : ↑(X.presheaf.stalk x) ∙ g = ⊤) : Function.Bijective ⇑(LinearMap.toSpanSingleton (↑(X.presheaf.stalk x)) (↑(M.presheaf.stalk x)) g)

A generator of the stalk of an invertible sheaf is a basis. If the germ g generates the stalk M_x, then a ↦ a • g is a bijection from the local ring 𝒪_{X,x} onto M_x: since M_x is isomorphic to 𝒪_{X,x}, a surjective endomorphism of it is injective.

theorem AlgebraicGeometry.Scheme.Modules.span_smul_eq_top_iff {X : Scheme} (M : X.Modules) [TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X M] (x : ↥X) {a : ↑(X.presheaf.stalk x)} {g : ↑(M.presheaf.stalk x)} : ↑(X.presheaf.stalk x) ∙ a • g = ⊤ ↔ IsUnit a ∧ ↑(X.presheaf.stalk x) ∙ g = ⊤

A multiple a • g generates the stalk of an invertible sheaf exactly when a is a unit of the local ring and g generates the stalk.