Documentation

Hironaka.Scheme.IdealSheaf.StalkIdeal

The stalk of an ideal sheaf #

For an ideal sheaf J on a scheme X and a point x, the stalk ideal J.stalkIdeal x โŠ† ๐’ช_{X,x} is the ideal generated by the germs at x of the sections of J over the affine opens containing x (Hironaka's J_x [Hir64, Ch. 0, ยง5, p. 142]). Every such open gives the same ideal (stalkIdeal_eq_map_germ), so the supremum over all of them is a choice-free definition. It is the stalk used in the statements of the main theorems.

The stalk of an inverse image ideal sheaf: stalkIdeal_comap says that the stalk of I.comap f at y is the image of the stalk of I at f y under f.stalkMap y (the affine computation map_germ_ideal_comap, read through the stalks; compare the proof of [TSPA, Tag 0805]). stalkIdeal_eq_span_iff_of_isOpenImmersion is the corresponding statement for generators along an open immersion. These are the forms in which the universal property of the affine blow-up handles stalks.

The stalk of an invertible ideal sheaf is generated by a nonzerodivisor (IsInvertible.exists_mem_nonZeroDivisors_stalkIdeal_eq_span); on a locally Noetherian scheme this stalkwise condition is equivalent to invertibility (Hironaka/Scheme/IdealSheaf/Invertible.lean).

source
theorem AlgebraicGeometry.Scheme.IdealSheafData.map_germ_le_stalkIdeal {X : Scheme} (J : X.IdealSheafData) (U : โ†‘X.affineOpens) {x : โ†ฅX} (hx : x โˆˆ โ†‘U) :
Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (โ†‘U) x hx)) (J.ideal U) โ‰ค J.stalkIdeal x
source
theorem AlgebraicGeometry.Scheme.IdealSheafData.map_germ_eq_of_le {X : Scheme} (J : X.IdealSheafData) {V W : โ†‘X.affineOpens} (h : W โ‰ค V) {x : โ†ฅX} (hx : x โˆˆ โ†‘W) :
Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (โ†‘W) x hx)) (J.ideal W) = Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (โ†‘V) x โ‹ฏ)) (J.ideal V)

Germs of sections over a smaller affine open give the same ideal: J(W) = J(V) ฮ“(W) for affine W โ‰ค V (Mathlib's map_ideal) and germ โˆ˜ res = germ.

source
theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_eq_map_germ {X : Scheme} (J : X.IdealSheafData) (U : โ†‘X.affineOpens) {x : โ†ฅX} (hx : x โˆˆ โ†‘U) :
J.stalkIdeal x = Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (โ†‘U) x hx)) (J.ideal U)

Every affine open U โˆ‹ x computes the stalk ideal: J_x is the image of J(U) under the germ map.

source
theorem AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_comap {X Y : Scheme} (I : X.IdealSheafData) (f : Y โŸถ X) (y : โ†ฅY) :
(I.comap f).stalkIdeal y = Ideal.map (CommRingCat.Hom.hom (Hom.stalkMap f y)) (I.stalkIdeal (f y))

The stalk of the inverse image I.comap f at y is generated by the image under f.stalkMap y of the stalk of I at f y (compare the proof of [TSPA, Tag 0805]).

source
theorem AlgebraicGeometry.Scheme.Hom.germ_appLE_apply {X Y : Scheme} (f : Y โŸถ X) (U : X.Opens) (V : Y.Opens) (e : V โ‰ค (TopologicalSpace.Opens.map f.base).obj U) {z : โ†ฅY} (hz : z โˆˆ V) (hfz : f z โˆˆ U) (s : โ†‘(X.presheaf.obj (Opposite.op U))) :
(CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ V z hz)) ((CategoryTheory.ConcreteCategory.hom (appLE f U V e)) s) = (CategoryTheory.ConcreteCategory.hom (stalkMap f z)) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U (f z) hfz)) s)

The germ of fโ™ฏs (s a section over U โŠ† X, restricted along f to V โŠ† fโปยนU) at z โˆˆ V is the stalk map applied to the germ of s at f z.

source
theorem AlgebraicGeometry.Scheme.IdealSheafData.germ_mem_nonZeroDivisors {X : Scheme} (V : โ†‘X.affineOpens) {x : โ†ฅX} (hx : x โˆˆ โ†‘V) {s : โ†‘(X.presheaf.obj (Opposite.op โ†‘V))} (hs : s โˆˆ nonZeroDivisors โ†‘(X.presheaf.obj (Opposite.op โ†‘V))) :
(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (โ†‘V) x hx)) s โˆˆ nonZeroDivisors โ†‘(X.presheaf.stalk x)

A nonzerodivisor of ฮ“(X, V), V affine, has a nonzerodivisor germ at every point of V: the stalk is a localization of ฮ“(X, V) (Mathlib's IsAffineOpen.isLocalization_stalk).

source
theorem AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.exists_mem_nonZeroDivisors_stalkIdeal_eq_span {X : Scheme} {J : X.IdealSheafData} (hJ : J.IsInvertible) (x : โ†ฅX) :
โˆƒ h โˆˆ nonZeroDivisors โ†‘(X.presheaf.stalk x), J.stalkIdeal x = Ideal.span {h}

The stalk of an invertible ideal sheaf at any point is generated by a nonzerodivisor.

source
theorem AlgebraicGeometry.stalkIdeal_vanishingIdeal_congr {X : Scheme} {Z Z' : TopologicalSpace.Closeds โ†ฅX} (U : โ†‘X.affineOpens) {x : โ†ฅX} (hx : x โˆˆ โ†‘U) (h : โˆ€ y โˆˆ โ†‘U, y โˆˆ Z โ†” y โˆˆ Z') :
(Scheme.IdealSheafData.vanishingIdeal Z).stalkIdeal x = (Scheme.IdealSheafData.vanishingIdeal Z').stalkIdeal x

The stalk of the vanishing ideal of a closed set depends only on the trace of the set on an affine neighbourhood of the point.