NYLL
Module

GeometricStalkUnibranchCriterion.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkUnibranchCriterion
2 declarations indexed from sourceView source ↗

Module documentation

Geometric unibranchness implies irreducibility of the actual strict stalk

The original definition is phrased using the normalization of the reduction. Its canonical normalization map supplies the integral normal extension used in the proved étale-neighborhood and geometric-stalk irreducibility results. In particular the base ring need not be reduced or Noetherian.

Imports3
Imported by2

Declarations

theorem

geometricStalk_nilradical_isPrime_of_geometricallyUnibranch

L33 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalk_nilradical_isPrime_of_geometricallyUnibranch
Documentation

Geometric unibranchness in the original normalization definition makes the nilradical of the actual geometric stalk prime.

Source context 5 commands

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

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

geometricStalk_irreducibleSpace_of_geometricallyUnibranch

L70 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalk_irreducibleSpace_of_geometricallyUnibranch
Documentation

The spectrum of the actual strict stalk of a geometrically unibranch local ring is irreducible. The field-valued point may have any overfield.

Source context 5 commands

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

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

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