The k-algebra structure on a stalk of a scheme over Spec k #
For f : X ⟶ Spec k and a point x, the stalk 𝒪_{X,x} is a k-algebra through
k ≅ Γ(Spec k, ⊤) → Γ(X, f⁻¹ ⊤) → 𝒪_{X,x} (Scheme.Hom.stalkAlgebra), and for every open
U ∋ x this structure is the composite of the k-algebra structure on Γ(X, U) induced by f
(Scheme.Hom.sectionsAlgebra) with the germ map Γ(X, U) → 𝒪_{X,x}
(germ_comp_algebraMap_sectionsAlgebra; the scalar tower k → Γ(X, U) → 𝒪_{X,x}). This is the
structure in which the residue field κ(x) of the stalk is a k-algebra, so that its
transcendence degree over k enters the dimension formula of RegularSmooth/SchemeForms.lean.
Like sectionsAlgebra, it is a definition bound with letI, not an instance: it depends on f.
The k-algebra structure on the stalk 𝒪_{X,x} induced by f : X ⟶ Spec k, through
k ≅ Γ(Spec k, ⊤) → Γ(X, f⁻¹ ⊤) → 𝒪_{X,x}. Not an instance: it depends on f.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Through any open U ∋ x, the k-algebra structure of Γ(X, U) followed by the germ map is
the k-algebra structure of the stalk.
The scalar tower k → Γ(X, U) → 𝒪_{X,x} for the structures induced by f.