Theorems · Theorem · commutative algebra

Algebra.isUnramifiedAt_iff_map_eq

∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S] (p : Ideal R) [inst_4 : p.IsPrime] (q : Ideal S) [inst_5 : q.IsPrime]
  [inst_6 : q.LiesOver p] [inst_7 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_8 : Localization.AtPrime.IsLiesOverAlgebra p q],
  Algebra.IsUnramifiedAt R q ↔
    Algebra.IsSeparable p.ResidueField q.ResidueField ∧
      Ideal.map (algebraMap R (Localization.AtPrime q)) p = IsLocalRing.maximalIdeal (Localization.AtPrime q)

Let A be an essentially of finite type R-algebra, q be a prime over p. Then A is unramified at p if and only if κ(q)/κ(p) is separable, and pS_q = qS_q.

Defined in

Mathlib.RingTheory.Unramified.LocalRing

Cited by

2 results in Mathlib

Foundations

Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraAlgebra.EssFiniteTypeIdeal.IsPrimeIdeal.IsPrimeIdeal.LiesOverAlgebraLocalization.AtPrime.IsLiesOverAlgebra