Module

EtalePrimeLocalization.lean

Nyll.SchemeTheory.RingTheory.Descent.EtalePrimeLocalization

2 declarations indexed from sourceView source ↗

Module documentation

Etaleness at a point from localization on the base

The prime-local comparison is extracted from EtaleFundamentalGroups.Purity.SpecialLocal.BaseMinimalPrimePuncturedPurity. It uses the actual iterated-localization isomorphism and requires no normality, finiteness, or global geometric hypotheses.

Imports3

Mathlib.RingTheory.Etale.Locus
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.Localization.LocalizationLocalization

Imported by5

theorem

isEtaleAt_under_of_localizedAlgebra_etale

L29 ↗

SchemeTheory.isEtaleAt_under_of_localizedAlgebra_etale

Documentation

Etaleness of the simultaneous localization at a base prime descends, after localizing once more, to the original map at the prime below a target prime.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u

Lean source · statement

theorem isEtaleAt_under_of_localizedAlgebra_etale
    {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S]
    (p : PrimeSpectrum R)
    (hEtale : Algebra.Etale (Localization.AtPrime p.asIdeal)
      (Localization
        (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl)))
    (Q : PrimeSpectrum
      (Localization
        (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl))) :
    Algebra.IsEtaleAt R
      (PrimeSpectrum.comap
        (algebraMap S
          (Localization
            (Algebra.algebraMapSubmonoid S p.asIdeal.primeCompl))) Q).asIdeal

theorem

isEtaleAt_of_localizedAlgebra_etale

L66 ↗

SchemeTheory.isEtaleAt_of_localizedAlgebra_etale