NYLL
Module

GeometricStalkNormalDomain.lean

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

Module documentation

The actual geometric étale stalk over a normal domain is a domain

A zero-product relation between two germs descends to an actual pointed étale neighborhood, then to an affine refinement. Localizing its sections at the prime selected by the geometric point gives a domain, by normality of prime localizations of étale algebras over a normal domain. Its localized germ map carries one of the two zero factors back to the geometric stalk.

No discrete valuation, Noetherianity, or localness of the base ring is needed. This supplies the domain needed to use the actual fraction field of a strict henselization over a normal local ring. Integral closedness of this stalk and the generic tensor comparison are separate results.

Imports7
Imported by10

Declarations

instance

geometricStalk_isDomain_of_normal

L45 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalk_isDomain_of_normal
Documentation

The actual étale stalk at any geometric point of a normal domain is a domain. The zero-product relation is descended to a localized affine étale neighborhood, whose domain property is already proved.

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] [IsDomain R] [IsIntegrallyClosed R]
  [Field Ω] (φ : R →+* Ω)
Lean source · statement
instance geometricStalk_isDomain_of_normal :
    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.