Etale locus of an algebra

Main results

Let A be a R-algebra.

• Algebra.etaleLocus : The set of primes of A where it is étale over R.
• Algebra.basicOpen_subset_etaleLocus_iff : D(f) is contained in the etale locus if and only if A_f is formally etale over R.
• Algebra.etaleLocus_eq_univ_iff : The etale locus is the whole spectrum if and only if A is formally etale over R.
• Algebra.isOpen_etaleLocus : If A is of finite type over R, then the etale locus is open.

@[reducible, inline]

abbrev Algebra.IsEtaleAt (R : Type u_1) {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (q : Ideal A) [q.IsPrime] : Prop

We say that an R-algebra A is etale at a prime q of A if A_q is formally etale over R.

def Algebra.etaleLocus (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] : Set (PrimeSpectrum A)

Algebra.etaleLocus R A is the set of primes p of A that are etale.

@[simp]

theorem Algebra.mem_etaleLocus_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {p : PrimeSpectrum A} : p ∈ etaleLocus R A ↔ IsEtaleAt R p.asIdeal

theorem Algebra.IsEtaleAt.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (p : Ideal A) (P : Ideal B) [P.LiesOver p] [p.IsPrime] [P.IsPrime] [IsEtaleAt R p] [IsEtaleAt A P] : IsEtaleAt R P

theorem Algebra.etaleLocus_eq_unramfiedLocus_inter_smoothLocus {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] : etaleLocus R A = unramifiedLocus R A ∩ smoothLocus R A

theorem Algebra.etaleLocus_eq_compl_support {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] : etaleLocus R A = (Module.support A Ω[A⁄R])ᶜ ∩ (Module.support A (H1Cotangent R A))ᶜ

theorem Algebra.basicOpen_subset_etaleLocus_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {f : A} : ↑(PrimeSpectrum.basicOpen f) ⊆ etaleLocus R A ↔ FormallyEtale R (Localization.Away f)

theorem Algebra.etaleLocus_eq_univ_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] : etaleLocus R A = Set.univ ↔ FormallyEtale R A

theorem Algebra.isOpen_etaleLocus {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] : IsOpen (etaleLocus R A)

theorem Algebra.basicOpen_subset_etaleLocus_iff_etale {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] {f : A} : ↑(PrimeSpectrum.basicOpen f) ⊆ etaleLocus R A ↔ Etale R (Localization.Away f)

theorem Algebra.etaleLocus_eq_univ_iff_etale {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] : etaleLocus R A = Set.univ ↔ Etale R A

theorem Algebra.exists_etale_of_isEtaleAt {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [FinitePresentation R A] (P : Ideal A) [P.IsPrime] [IsEtaleAt R P] : ∃ f ∉ P, Etale R (Localization.Away f)