Module

GeometricPointLocalization.lean

Nyll.SchemeTheory.Affine.GeometricPointLocalization

3 declarations indexed from sourceView source ↗

Module documentation

Geometric points of localized étale charts

A prescribed point of a localized stalk in an étale chart admits a geometric point over any chosen algebraically closed residue-field extension downstairs. The construction uses the actual residue map of the chart and the isomorphisms on stalks of localization morphisms, so the resulting triangle commutes as scheme morphisms.

Imports4

Nyll.SchemeTheory.Affine.StalkLocalization
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Mathlib.FieldTheory.IsAlgClosed.Basic

Imported by2

theorem

exists_geometricPoint_of_isIso_stalkMap

L31 ↗

AlgebraicGeometry.exists_geometricPoint_of_isIso_stalkMap

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem exists_geometricPoint_of_isIso_stalkMap
    {X U V : Scheme.{u}} (f : U ⟶ X) [Etale f] (h : V ⟶ U) (v : V)
    [IsIso (h.stalkMap v)] (η : X) (hv : f (h v) = η)
    (Ω : Type u) [Field Ω] [IsAlgClosed Ω]
    (a : X.residueField η ⟶ CommRingCat.of Ω) :
    ∃ t : Spec (CommRingCat.of Ω) ⟶ V,
      t (closedPoint Ω) = v ∧
      t ≫ h ≫ f = Spec.map a ≫ X.fromSpecResidueField η

theorem

exists_geometricPoint_localized_stalk

L75 ↗

AlgebraicGeometry.exists_geometricPoint_localized_stalk

Documentation

A point of any localization of a chart stalk lifts the prescribed geometric point downstairs, with its underlying point unchanged.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem exists_geometricPoint_localized_stalk
    {X U : Scheme.{u}} (f : U ⟶ X) [Etale f] (u : U)
    (M : Submonoid (U.presheaf.stalk u)) (S : Type u) [CommRing S]
    [Algebra (U.presheaf.stalk u) S] [IsLocalization M S]
    (q : Spec (CommRingCat.of S)) (η : X)
    (hq : f (U.fromSpecStalk u
      ((Spec.map (CommRingCat.ofHom (algebraMap (U.presheaf.stalk u) S))) q)) = η)
    (Ω : Type u) [Field Ω] [IsAlgClosed Ω]
    (a : X.residueField η ⟶ CommRingCat.of Ω) :
    ∃ t : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of S),
      t (closedPoint Ω) = q ∧
      t ≫ Spec.map (CommRingCat.ofHom (algebraMap (U.presheaf.stalk u) S)) ≫
        U.fromSpecStalk u ≫ f = Spec.map a ≫ X.fromSpecResidueField η

theorem

exists_geometricPoint_localized_chart_branch

L106 ↗

AlgebraicGeometry.exists_geometricPoint_localized_chart_branch

Documentation

The extension of a chosen chart branch to a prime localization carries a geometric point over the fixed geometric point downstairs. The prime itself and its inverse image are supplied by localization of the given inclusion.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem exists_geometricPoint_localized_chart_branch
    {X U : Scheme.{u}} (f : U ⟶ X) [Etale f] (u : U)
    (q : Spec (U.presheaf.stalk u)) (P : Ideal (U.presheaf.stalk u)) [P.IsPrime]
    (hqP : q.asIdeal ≤ P) (η : X) (hqη : f (U.fromSpecStalk u q) = η)
    (Ω : Type u) [Field Ω] [IsAlgClosed Ω]
    (a : X.residueField η ⟶ CommRingCat.of Ω) :
    ∃ t : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of (Localization.AtPrime P)),
      (t (closedPoint Ω)).asIdeal =
        q.asIdeal.map (algebraMap (U.presheaf.stalk u) (Localization.AtPrime P)) ∧
      t ≫ Spec.map (CommRingCat.ofHom
          (algebraMap (U.presheaf.stalk u) (Localization.AtPrime P))) ≫
        U.fromSpecStalk u ≫ f = Spec.map a ≫ X.fromSpecResidueField η

Module documentation

Geometric points of localized étale charts

Declarations

exists_geometricPoint_of_isIso_stalkMap

exists_geometricPoint_localized_stalk

exists_geometricPoint_localized_chart_branch