SchemeTheory.exists_etale_away_of_isEtaleAt_fiber
If an integral finitely presented algebra is etale at every prime over p, it is etale on the preimage of a principal neighborhood of p.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace SchemeTheory
universe u vLean source · statement
theorem exists_etale_away_of_isEtaleAt_fiber
{R : Type u} {B : Type v} [CommRing R] [CommRing B]
[Algebra R B] [Algebra.IsIntegral R B] [Algebra.FinitePresentation R B]
(p : PrimeSpectrum R)
(hetale : ∀ P : PrimeSpectrum B,
PrimeSpectrum.comap (algebraMap R B) P = p → Algebra.IsEtaleAt R P.asIdeal) :
∃ r : R, r ∉ p.asIdeal ∧ Algebra.Etale R (Localization.Away (algebraMap R B r))