NYLL
Module

GeometricStalkPuncture.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkPuncture
5 declarations indexed from sourceView source ↗

Module documentation

The closed fiber and puncture of the actual geometric stalk

The maximal ideal of an arbitrary local base ring generates the maximal ideal of its geometric étale stalk. A nonunit germ is represented on an affine pointed étale neighborhood; after localization at the selected prime, the unramified local algebra theorem expresses it in the extended base ideal. Essential finite type is used only for this localized neighborhood ring.

Consequently the inverse image of the base closed point is exactly the stalk closed point, and the actual punctured stalk spectrum is the base change of the punctured base spectrum. No finiteness, reducedness, normality, dimension, or separability assumption on the chosen geometric overfield is needed.

Imports11
Imported by3

Declarations

theorem

geometricStalkStructureMap_map_maximalIdeal

L47 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkStructureMap_map_maximalIdeal
Documentation

The maximal ideal of the local base generates the maximal ideal of the actual geometric étale stalk.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsLocalRing R] [Field Ω]
  (φ : R →+* Ω) [IsLocalHom φ]
Lean source · statement
theorem geometricStalkStructureMap_map_maximalIdeal :
    (IsLocalRing.maximalIdeal R).map (geometricStalkStructureMap φ) =
      IsLocalRing.maximalIdeal (geometricStalk (Spec.map (CommRingCat.ofHom φ)))
theorem

geometricStalkStructureMap_comap_eq_closedPoint_iff

L109 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkStructureMap_comap_eq_closedPoint_iff
Documentation

The closed fiber of the actual geometric stalk spectrum has exactly its closed point as its underlying set.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsLocalRing R] [Field Ω]
  (φ : R →+* Ω) [IsLocalHom φ]
Lean source · statement
theorem geometricStalkStructureMap_comap_eq_closedPoint_iff
    (x : PrimeSpectrum (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) :
    PrimeSpectrum.comap (geometricStalkStructureMap φ) x = IsLocalRing.closedPoint R ↔
      x = IsLocalRing.closedPoint (geometricStalk (Spec.map (CommRingCat.ofHom φ)))
theorem

geometricStalkStructureMap_preimage_puncturedSpectrumOpen

L125 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkStructureMap_preimage_puncturedSpectrumOpen
Documentation

The inverse image of the punctured local spectrum is the actual punctured geometric stalk spectrum, for an arbitrary local base ring.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsLocalRing R] [Field Ω]
  (φ : R →+* Ω) [IsLocalHom φ]
Lean source · statement
theorem geometricStalkStructureMap_preimage_puncturedSpectrumOpen :
    Spec.map (CommRingCat.ofHom (geometricStalkStructureMap φ)) ⁻¹ᵁ
        Scheme.puncturedSpectrumOpen R =
      Scheme.puncturedSpectrumOpen (geometricStalk (Spec.map (CommRingCat.ofHom φ)))
def

geometricStalkPuncturedSpectrumPullbackIso

L136 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkPuncturedSpectrumPullbackIso
Documentation

The actual punctured geometric stalk spectrum is the pullback of the punctured base spectrum along the actual stalk structure map.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsLocalRing R] [Field Ω]
  (φ : R →+* Ω) [IsLocalHom φ]
Lean source · statement
def geometricStalkPuncturedSpectrumPullbackIso :
    pullback (Spec.map (CommRingCat.ofHom (geometricStalkStructureMap φ)))
        (Scheme.puncturedSpectrumInclusion R) ≅
      Scheme.puncturedSpectrum (geometricStalk (Spec.map (CommRingCat.ofHom φ)))
theorem

geometricStalkPuncturedSpectrumPullbackIso_hom_inclusion

L149 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkPuncturedSpectrumPullbackIso_hom_inclusion
Documentation

The puncture comparison respects the canonical map to the full stalk spectrum.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsLocalRing R] [Field Ω]
  (φ : R →+* Ω) [IsLocalHom φ]
Lean source · statement
theorem geometricStalkPuncturedSpectrumPullbackIso_hom_inclusion :
    (geometricStalkPuncturedSpectrumPullbackIso φ).hom ≫
        Scheme.puncturedSpectrumInclusion
          (geometricStalk (Spec.map (CommRingCat.ofHom φ))) =
      pullback.fst (Spec.map (CommRingCat.ofHom (geometricStalkStructureMap φ)))
        (Scheme.puncturedSpectrumInclusion R)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.