Theorems · Theorem · algebraic geometry

Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective

∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (Q : Ideal S)
  [inst_3 : Q.IsPrime] [Module.Finite R S] [Algebra.IsUnramifiedAt R Q],
  ∃ x,
    (Ideal.under (↥R[x]) Q).primesOver S = {Q} ∧
      Function.Bijective ⇑(algebraMap (Ideal.under (↥R[x]) Q).ResidueField Q.ResidueField)

Let S be an finite R-algebra that is unramified at some prime Q. Then there exists some x : S such that Q is the unique prime lying over P := Q ∩ R⟨x⟩ and κ(P) = κ(Q).

Defined in

Mathlib.RingTheory.Unramified.LocalStructure

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIdeal.IsPrimeModule.FiniteAlgebra.IsUnramifiedAt