NYLL
Module

GeometricStalkUnibranchDomain.lean

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

Module documentation

The actual geometric stalk from normalization data

The base local ring need not be normal. An injective integral local map to a normal local domain with purely inseparable residue field gives domain local étale neighborhoods. A zero-product relation between actual geometric-stalk germs descends to one of these neighborhoods, where one factor vanishes.

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

Imports7
Imported by1

Declarations

theorem

geometricStalk_isDomain_of_integral_normal_extension

L42 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalk_isDomain_of_integral_normal_extension
Documentation

The actual geometric stalk is a domain when the base embeds integrally and locally into a normal local domain with purely inseparable residue field.

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_isDomain_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)]
    (hinj : Function.Injective (algebraMap R N)) :
    IsDomain (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.