Stalks of a Scheme #
Main definitions and results #
AlgebraicGeometry.Scheme.fromSpecStalk
: The canonical morphismSpec 𝒪_{X, x} ⟶ X
.AlgebraicGeometry.Scheme.range_fromSpecStalk
: The range of the mapSpec 𝒪_{X, x} ⟶ X
is exactly they
s that specialize tox
.AlgebraicGeometry.SpecToEquivOfLocalRing
: Given a local ringR
and schemeX
, morphismsSpec R ⟶ X
corresponds to pairs(x, f)
wherex : X
andf : 𝒪_{X, x} ⟶ R
is a local ring homomorphism.
A morphism from Spec(O_x)
to X
, which is defined with the help of an affine open
neighborhood U
of x
.
Equations
- hU.fromSpecStalk hxU = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.germ U x hxU)) hU.fromSpec
Instances For
The morphism from Spec(O_x)
to X
given by IsAffineOpen.fromSpec
does not depend on the affine
open neighborhood of x
we choose.
If x
is a point of X
, this is the canonical morphism from Spec(O_x)
to X
.
Equations
- X.fromSpecStalk x = ⋯.fromSpecStalk ⋯
Instances For
Equations
- AlgebraicGeometry.instOverSpecStalkCommRingCatPresheaf X x = { hom := X.fromSpecStalk x }
Equations
- AlgebraicGeometry.instCanonicallyOver X x = CategoryTheory.CanonicallyOverClass.mk
A variant of Spec_fromSpecStalk
that breaks abstraction boundaries.
The canonical map Spec 𝒪_{X, x} ⟶ U
given x ∈ U ⊆ X
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
For a local ring (R, 𝔪)
,
this is the isomorphism between the stalk of Spec R
at 𝔪
and R
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a local ring (R, 𝔪)
and a morphism f : Spec R ⟶ X
,
they induce a (local) ring homomorphism φ : 𝒪_{X, f 𝔪} ⟶ R
.
This is inverse to φ ↦ Spec.map φ ≫ X.fromSpecStalk (f 𝔪)
. See SpecToEquivOfLocalRing
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Copy of isLocalHom_stalkClosedPointTo
which unbundles the comm ring.
Useful for use in combination with CommRingCat.of K
for a field K
.
useful lemma for applications of SpecToEquivOfLocalRing
Given a local ring R
and scheme X
, morphisms Spec R ⟶ X
corresponds to pairs
(x, f)
where x : X
and f : 𝒪_{X, x} ⟶ R
is a local ring homomorphism.
Equations
- One or more equations did not get rendered due to their size.