NYLL
Module

GeometricStalkNormal.lean

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

Module documentation

Integral closedness of the actual geometric étale stalk

A monic integral equation and the numerator and denominator of a fraction have representatives on one actual pointed étale neighborhood. Clearing the denominator with Polynomial.scaleRoots gives an equality of sections, which descends to a further affine neighborhood. Its local ring at the selected prime is normal. Normality there supplies a quotient of the numerator by the denominator, and the localized germ map carries that divisibility equation back to the actual stalk.

The denominator is nonzero in the local stage because its germ is nonzero. No injectivity of localized germ maps, normalization comparison, or normality of the geometric stalk is assumed.

Imports10
Imported by1

Declarations

theorem

geometricStalk_exists_monic_and_pair

L46 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalk_exists_monic_and_pair
Documentation

Combine the existing monic-polynomial representative and a pair of germs using an actual common pointed neighborhood.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u
Lean source · statement
theorem geometricStalk_exists_monic_and_pair
    {S : Scheme.{u}} {Ω : Type u} [Field Ω]
    (s : Spec (.of Ω) ⟶ S) (p : (geometricStalk s)[X]) (hp : p.Monic)
    (a b : geometricStalk s) :
    ∃ (W : S.Etale) (t : (Scheme.pointEtaleNeighborhoods s).fiber.obj W)
      (q : Γ(W.left, ⊤)[X]) (aW bW : Γ(W.left, ⊤)),
      q.Monic ∧ q.map (geometricStalkGerm s W t).hom = p ∧
        geometricStalkGerm s W t aW = a ∧ geometricStalkGerm s W t bW = b
instance

geometricStalk_isIntegrallyClosed_of_normal

L90 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalk_isIntegrallyClosed_of_normal
Documentation

The actual geometric étale stalk over a normal domain is integrally closed. The proof descends an integral equation after clearing its denominator and uses normality of an actual prime-localized affine étale neighborhood.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [Field Ω] (φ : R →+* Ω)
Lean source · statement
instance geometricStalk_isIntegrallyClosed_of_normal :
    IsIntegrallyClosed (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.