NYLL
Module

FiniteNormalModelNeighborhood.lean

Nyll.EtaleFundamentalGroups.Normalization.FiniteNormalModelNeighborhood
1 declaration indexed from sourceView source ↗

Module documentation

Étale neighborhoods of finite domain models over a normal domain

Opening the unramified locus first avoids assuming finite presentation or Noetherianity. The dominant-domain criterion supplies étaleness afterwards. This is the spreading step for the original local criterion in Tag 0BTF.

Imports5
Imported by2

Declarations

theorem

exists_etale_away_of_finite_domain_localized_etale

L30 ↗
EtaleFundamentalGroups.exists_etale_away_of_finite_domain_localized_etale
Documentation

A finite domain faithful over a normal domain which becomes étale after localizing the base at a prime is étale on a principal neighborhood of that prime. No finite presentation or Noetherian assumption is needed.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem exists_etale_away_of_finite_domain_localized_etale
    {R C : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [CommRing C] [IsDomain C] [Algebra R C] [FaithfulSMul R C] [Module.Finite R C]
    (p : PrimeSpectrum R)
    (hEtale : Algebra.Etale (Localization.AtPrime p.asIdeal)
      (Localization (Algebra.algebraMapSubmonoid C p.asIdeal.primeCompl))) :
    ∃ r : R, r ∉ p.asIdeal ∧ Algebra.Etale R (Localization.Away (algebraMap R C r))

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