NYLL
Module

GeometricStalkUnibranchIrreducible.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkUnibranchIrreducible
1 declaration indexed from sourceView source ↗

Module documentation

Irreducibility of the actual geometric stalk from normalization data

The base local ring need not be reduced. An integral local map to a normal local domain with purely inseparable residue field and nilpotent kernel elements gives irreducible local étale neighborhoods. A nilpotence relation between actual stalk germs descends to one of these neighborhoods.

For a geometrically unibranch local ring, the normalization of its reduction supplies the extension used here. All comparison maps and the étale neighborhoods are actual constructions, not assumed conclusions.

Imports7
Imported by2

Declarations

theorem

geometricStalk_nilradical_isPrime_of_integral_normal_extension

L43 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalk_nilradical_isPrime_of_integral_normal_extension
Documentation

The nilradical of the actual geometric stalk is prime when the base maps integrally and locally to a normal local domain with purely inseparable residue field and a kernel consisting of nilpotents.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsLocalRing R]
  [Field Ω] (φ : R →+* Ω) [IsLocalHom φ]
Lean source · statement
theorem geometricStalk_nilradical_isPrime_of_integral_normal_extension
    (N : Type u) [CommRing N] [IsLocalRing N] [IsDomain N] [IsIntegrallyClosed N]
    [Algebra R N] [Algebra.IsIntegral R N] [IsLocalHom (algebraMap R N)]
    [IsPurelyInseparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField N)]
    (hker : RingHom.ker (algebraMap R N) ≤ nilradical R) :
    (nilradical (geometricStalk (Spec.map (CommRingCat.ofHom φ)))).IsPrime

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