Documentation

Mathlib.AlgebraicGeometry.Stalk

Stalks of a Scheme #

Main definitions and results #

noncomputable def AlgebraicGeometry.IsAffineOpen.fromSpecStalk {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {x : X.toPresheafedSpace} (hxU : x U) :
AlgebraicGeometry.Spec (X.presheaf.stalk x) X

A morphism from Spec(O_x) to X, which is defined with the help of an affine open neighborhood U of x.

Equations
Instances For
    theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (hV : AlgebraicGeometry.IsAffineOpen V) (x : X.toPresheafedSpace) (hxU : x U) (hxV : x V) :
    hU.fromSpecStalk hxU = hV.fromSpecStalk hxV

    The morphism from Spec(O_x) to X given by IsAffineOpen.fromSpec does not depend on the affine open neighborhood of x we choose.

    noncomputable def AlgebraicGeometry.Scheme.fromSpecStalk (X : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) :
    AlgebraicGeometry.Spec (X.presheaf.stalk x) X

    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
      noncomputable instance AlgebraicGeometry.instOverSpecStalkCommRingCatPresheaf (X : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) :
      (AlgebraicGeometry.Spec (X.presheaf.stalk x)).Over X
      Equations
      @[simp]
      theorem AlgebraicGeometry.instOverSpecStalkCommRingCatPresheaf_over (X : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) :
      AlgebraicGeometry.Spec (X.presheaf.stalk x) X = X.fromSpecStalk x
      Equations
      @[simp]
      theorem AlgebraicGeometry.instCanonicallyOver_over (X : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) :
      AlgebraicGeometry.Spec (X.presheaf.stalk x) X = X.fromSpecStalk x
      @[simp]
      theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {x : X.toPresheafedSpace} (hxU : x U) :
      hU.fromSpecStalk hxU = X.fromSpecStalk x
      instance AlgebraicGeometry.IsAffineOpen.fromSpecStalk_isPreimmersion {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : X.toPresheafedSpace) (hx : x U) :
      AlgebraicGeometry.IsPreimmersion (hU.fromSpecStalk hx)
      theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) {x : X.toPresheafedSpace} (hxU : x U) :
      (hU.fromSpecStalk hxU).base (IsLocalRing.closedPoint (X.presheaf.stalk x)) = x
      @[simp]
      theorem AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint {X : AlgebraicGeometry.Scheme} {x : X.toPresheafedSpace} :
      (X.fromSpecStalk x).base (IsLocalRing.closedPoint (X.presheaf.stalk x)) = x
      theorem AlgebraicGeometry.Scheme.fromSpecStalk_app {X : AlgebraicGeometry.Scheme} {U : X.Opens} {x : X.toPresheafedSpace} (hxU : x U) :
      AlgebraicGeometry.Scheme.Hom.app (X.fromSpecStalk x) U = CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x hxU) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.stalk x)).inv ((AlgebraicGeometry.Spec (X.presheaf.stalk x)).presheaf.map (CategoryTheory.homOfLE ).op))
      @[simp]
      theorem AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk {X : AlgebraicGeometry.Scheme} {x y : X.toPresheafedSpace} (h : x y) :
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) (X.fromSpecStalk y) = X.fromSpecStalk x
      @[simp]
      theorem AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk_assoc {X : AlgebraicGeometry.Scheme} {x y : X.toPresheafedSpace} (h : x y) {Z : AlgebraicGeometry.Scheme} (h✝ : X Z) :
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) (CategoryTheory.CategoryStruct.comp (X.fromSpecStalk y) h✝) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) h✝

      A variant of Spec_fromSpecStalk that breaks abstraction boundaries.

      theorem AlgebraicGeometry.Scheme.range_fromSpecStalk {X : AlgebraicGeometry.Scheme} {x : X.toPresheafedSpace} :
      Set.range (X.fromSpecStalk x).base = {y : X.toPresheafedSpace | y x}

      Stacks Tag 01J7

      noncomputable def AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) :
      AlgebraicGeometry.Spec (X.presheaf.stalk x) U

      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
        @[simp]
        theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) :
        CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) U = X.fromSpecStalk x
        @[simp]
        theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι_assoc {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) {Z : AlgebraicGeometry.Scheme} (h : X Z) :
        instance AlgebraicGeometry.Scheme.instIsOverFromSpecStalkOfMem {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) :
        AlgebraicGeometry.Scheme.Hom.IsOver (U.fromSpecStalkOfMem x hxU) X
        theorem AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ (X : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) :
        CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) X.toSpecΓ = AlgebraicGeometry.Spec.map (X.presheaf.germ x trivial)
        @[simp]
        theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) :
        CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) U.toSpecΓ = AlgebraicGeometry.Spec.map (X.presheaf.germ U x hxU)
        @[simp]
        theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U)) Z) :

        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
            theorem AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk {X : AlgebraicGeometry.Scheme} (x : X.toPresheafedSpace) :
            AlgebraicGeometry.Scheme.stalkClosedPointTo (X.fromSpecStalk x) = (X.presheaf.stalkCongr ).hom
            theorem AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff {X : AlgebraicGeometry.Scheme} {R : CommRingCat} {f₁ f₂ : (x : X.toPresheafedSpace) × { f : X.presheaf.stalk x R // IsLocalHom f.hom }} :
            f₁ = f₂ ∃ (h₁ : f₁.fst = f₂.fst), f₁.snd = CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ).hom f₂.snd

            useful lemma for applications of SpecToEquivOfLocalRing

            noncomputable def AlgebraicGeometry.SpecToEquivOfLocalRing (X : AlgebraicGeometry.Scheme) (R : CommRingCat) [IsLocalRing R] :
            (AlgebraicGeometry.Spec R X) (x : X.toPresheafedSpace) × { f : X.presheaf.stalk x R // IsLocalHom f.hom }

            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.
            Instances For
              @[simp]
              theorem AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply (X : AlgebraicGeometry.Scheme) (R : CommRingCat) [IsLocalRing R] (xf : (x : X.toPresheafedSpace) × { f : X.presheaf.stalk x R // IsLocalHom f.hom }) :