Theorems · Definition · algebraic geometry

Algebra.IsEtaleAt

(R : Type u_1) →
  {A : Type u_2} → [inst : CommRing R] → [inst_1 : 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.

Defined in

Mathlib.RingTheory.Etale.Locus

Cited by

5 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

CommRingCommRingAlgebraIdeal.IsPrime