Documentation

Hironaka.AnalyticSpace.VanishingIdeal

The vanishing ideal of a set of points #

For a locally ringed space X and a set C โŠ† |X|, the vanishing ideal of C at y is the ideal ๐“˜_C(y) โŠ† ๐’ช_{X,y} of the germs of sections g (over some open V โˆ‹ y) that vanish at every point of C โˆฉ V โ€” "vanish at y'" meaning that the germ of g at y' lies in the maximal ideal of ๐’ช_{X,y'}. This is the stalk at y of the sheaf of ideals of the closed set C, the ideal sheaf ๐“˜(A) of an analytic set A in [GR84, Ch. 4, ยง1]. The closed subspace of an irreducible component C of an analytic space is the one cut out by this ideal, once Cartan's theorem (hasLocalGenerators_radical_of_cartan, Hironaka/AnalyticSpace/ModelTransport.lean) provides local generators (IdealSheaf.ofStalks); see Hironaka/AnalyticSpace/Nullstellensatz.lean.

source
theorem AnalyticSpace.map_mem_maximalIdeal_iff {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R โ†’+* S) [IsLocalHom f] (a : R) :
f a โˆˆ IsLocalRing.maximalIdeal S โ†” a โˆˆ IsLocalRing.maximalIdeal R

A local ring homomorphism pulls the maximal ideal back to the maximal ideal.

source
def AnalyticSpace.vanishingStalkIdeal (X : AlgebraicGeometry.LocallyRingedSpace) (C : Set โ†‘X.toTopCat) (y : โ†‘X.toTopCat) :
Ideal โ†‘(X.presheaf.stalk y)

The vanishing ideal of C at y [GR84, Ch. 4, ยง1]: the germs at y of the sections vanishing at every point of C near y โ€” a germ vanishes at a point when it lies in the maximal ideal of the stalk there.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AnalyticSpace.mem_vanishingStalkIdeal_iff (X : AlgebraicGeometry.LocallyRingedSpace) (C : Set โ†‘X.toTopCat) {y : โ†‘X.toTopCat} {s : โ†‘(X.presheaf.stalk y)} :
    s โˆˆ vanishingStalkIdeal X C y โ†” โˆƒ (V : TopologicalSpace.Opens โ†‘X.toTopCat) (hy : y โˆˆ V) (g : โ†‘(X.presheaf.obj (Opposite.op V))), (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V y hy)) g = s โˆง โˆ€ (y' : โ†‘X.toTopCat) (hy' : y' โˆˆ V), y' โˆˆ C โ†’ (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V y' hy')) g โˆˆ IsLocalRing.maximalIdeal โ†‘(X.presheaf.stalk y')
    source
    theorem AnalyticSpace.germ_mem_vanishingStalkIdeal (X : AlgebraicGeometry.LocallyRingedSpace) (C : Set โ†‘X.toTopCat) {V : TopologicalSpace.Opens โ†‘X.toTopCat} {y : โ†‘X.toTopCat} (hy : y โˆˆ V) (g : โ†‘(X.presheaf.obj (Opposite.op V))) (hg : โˆ€ (y' : โ†‘X.toTopCat) (hy' : y' โˆˆ V), y' โˆˆ C โ†’ (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V y' hy')) g โˆˆ IsLocalRing.maximalIdeal โ†‘(X.presheaf.stalk y')) :
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V y hy)) g โˆˆ vanishingStalkIdeal X C y

    The germ of a section vanishing on C near y lies in the vanishing ideal.

    source
    theorem AnalyticSpace.vanishingStalkIdeal_eq_top_of_not_mem_closure (X : AlgebraicGeometry.LocallyRingedSpace) (C : Set โ†‘X.toTopCat) {y : โ†‘X.toTopCat} (hy : y โˆ‰ closure C) :
    vanishingStalkIdeal X C y = โŠค

    Off the closure of C the vanishing ideal is everything.

    source
    theorem AnalyticSpace.vanishingStalkIdeal_ne_top_of_mem (X : AlgebraicGeometry.LocallyRingedSpace) (C : Set โ†‘X.toTopCat) {y : โ†‘X.toTopCat} (hy : y โˆˆ C) :
    vanishingStalkIdeal X C y โ‰  โŠค

    At a point of C the vanishing ideal is proper.

    source
    theorem AnalyticSpace.isRadical_vanishingStalkIdeal (X : AlgebraicGeometry.LocallyRingedSpace) (C : Set โ†‘X.toTopCat) (y : โ†‘X.toTopCat) :
    (vanishingStalkIdeal X C y).IsRadical

    The vanishing ideal is radical.

    source
    theorem AnalyticSpace.vanishingStalkIdeal_anti {X : AlgebraicGeometry.LocallyRingedSpace} {C D : Set โ†‘X.toTopCat} (h : C โŠ† D) (y : โ†‘X.toTopCat) :
    vanishingStalkIdeal X D y โ‰ค vanishingStalkIdeal X C y

    Vanishing on a larger set is the stronger condition.

    source
    theorem AnalyticSpace.vanishingStalkIdeal_inter_of_mem_nhds {X : AlgebraicGeometry.LocallyRingedSpace} (C : Set โ†‘X.toTopCat) {t : Set โ†‘X.toTopCat} {y : โ†‘X.toTopCat} (ht : t โˆˆ nhds y) :
    vanishingStalkIdeal X (C โˆฉ t) y = vanishingStalkIdeal X C y

    Only the germ of C at y matters: cutting C down to a neighbourhood of y changes nothing.

    source
    theorem AnalyticSpace.vanishingStalkIdeal_union {X : AlgebraicGeometry.LocallyRingedSpace} (A B : Set โ†‘X.toTopCat) (y : โ†‘X.toTopCat) :
    vanishingStalkIdeal X (A โˆช B) y = vanishingStalkIdeal X A y โŠ“ vanishingStalkIdeal X B y

    Vanishing on a union is vanishing on both sets.

    source
    theorem AnalyticSpace.map_stalkMap_vanishingStalkIdeal_le {A B : AlgebraicGeometry.LocallyRingedSpace} (ฯ† : A โŸถ B) (D : Set โ†‘B.toTopCat) (a : โ†‘A.toTopCat) :
    Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap ฯ† a)) (vanishingStalkIdeal B D ((CategoryTheory.ConcreteCategory.hom ฯ†.base) a)) โ‰ค vanishingStalkIdeal A (โ‡‘(CategoryTheory.ConcreteCategory.hom ฯ†.base) โปยน' D) a

    The stalk map of a morphism carries the vanishing ideal of D into the vanishing ideal of the preimage of D (sections pull back; the stalk maps are local).

    source
    theorem AnalyticSpace.vanishingStalkIdeal_preimage_eq_map {A B : AlgebraicGeometry.LocallyRingedSpace} (ฯ† : A โŸถ B) (hind : Topology.IsInducing โ‡‘(CategoryTheory.ConcreteCategory.hom ฯ†.base)) (hsurj : โˆ€ (a : โ†‘A.toTopCat), Function.Surjective โ‡‘(CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap ฯ† a))) {D : Set โ†‘B.toTopCat} (hD : D โŠ† Set.range โ‡‘(CategoryTheory.ConcreteCategory.hom ฯ†.base)) (a : โ†‘A.toTopCat) :
    vanishingStalkIdeal A (โ‡‘(CategoryTheory.ConcreteCategory.hom ฯ†.base) โปยน' D) a = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap ฯ† a)) (vanishingStalkIdeal B D ((CategoryTheory.ConcreteCategory.hom ฯ†.base) a))

    Transport of the vanishing ideal along a morphism ฯ† whose base map is inducing and whose stalk maps are surjective (an open immersion, a K-isomorphism, the closed immersion of a quotient): for D inside the image of ฯ†, the vanishing ideal of ฯ†โปยนD at a is the image of the vanishing ideal of D at ฯ† a.

    source
    theorem AnalyticSpace.hasLocalGenerators_vanishingStalkIdeal_of_forall_mem_closure (X : AlgebraicGeometry.LocallyRingedSpace) (C : Set โ†‘X.toTopCat) (h : โˆ€ y โˆˆ closure C, โˆƒ (U : TopologicalSpace.Opens โ†‘X.toTopCat) (_ : y โˆˆ U) (ฮน : Type) (x : Fintype ฮน) (f : ฮน โ†’ โ†‘(X.presheaf.obj (Opposite.op U))), โˆ€ (b : โ†‘X.toTopCat) (hb : b โˆˆ U), vanishingStalkIdeal X C b = Ideal.span (Set.range fun (i : ฮน) => (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U b hb)) (f i))) :
    Manifold.IdealSheaf.HasLocalGenerators (vanishingStalkIdeal X C)

    Local generators of the vanishing ideal, given them at the points of the closure of C (off the closure the ideal is everything, generated by 1).

    source
    noncomputable def AnalyticSpace.vanishingIdealSheaf (X : AlgebraicGeometry.LocallyRingedSpace) (C : Set โ†‘X.toTopCat) (hgen : Manifold.IdealSheaf.HasLocalGenerators (vanishingStalkIdeal X C)) :
    Manifold.IdealSheaf X.๐’ช

    The vanishing ideal sheaf of C, once its stalks have local generators.

    Equations
    Instances For
      source
      theorem AnalyticSpace.stalkIdeal_vanishingIdealSheaf (X : AlgebraicGeometry.LocallyRingedSpace) (C : Set โ†‘X.toTopCat) (hgen : Manifold.IdealSheaf.HasLocalGenerators (vanishingStalkIdeal X C)) (y : โ†‘X.toTopCat) :
      (vanishingIdealSheaf X C hgen).stalkIdeal y = vanishingStalkIdeal X C y
      source
      theorem AnalyticSpace.cosupport_vanishingIdealSheaf (X : AlgebraicGeometry.LocallyRingedSpace) (C : Set โ†‘X.toTopCat) (hC : IsClosed C) (hgen : Manifold.IdealSheaf.HasLocalGenerators (vanishingStalkIdeal X C)) :
      (vanishingIdealSheaf X C hgen).support = C

      The support of the vanishing ideal sheaf of a closed set C is C.