English
Let EssFiniteType R S. Then IsUnramifiedAt R q is equivalent to IsSeparable p.ResidueField q.ResidueField and p maps to maximalIdeal in Localization.AtPrime q.
Русский
Пусть R,S удовлетворяют EssFiniteType. Тогда IsUnramifiedAt R q эквивалентно IsSeparable p.ResidueField q.ResidueField и отображение p в Localization.AtPrime q равно максимальному идеалу.
LaTeX
$$$\\text{IsUnramifiedAt } R q \\iff (\\text{IsSeparable } p.ResidueField q.ResidueField) \\land (p.map (algebraMap R (Localization.AtPrime q)) = maximalIdeal _)$$$
Lean4
/-- 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`. -/
theorem isUnramifiedAt_iff_map_eq [EssFiniteType R S] (p : Ideal R) [p.IsPrime] (q : Ideal S) [q.IsPrime]
[q.LiesOver p] :
Algebra.IsUnramifiedAt R q ↔
Algebra.IsSeparable p.ResidueField q.ResidueField ∧
p.map (algebraMap R (Localization.AtPrime q)) = maximalIdeal _ :=
by
letI : Algebra (Localization.AtPrime p) (Localization.AtPrime q) :=
(Localization.localRingHom p q (algebraMap R S) Ideal.LiesOver.over).toAlgebra
have : IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime q) :=
.of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map p q (algebraMap R S) Ideal.LiesOver.over x).symm
letI : IsLocalHom (algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) :=
Localization.isLocalHom_localRingHom _ _ _ Ideal.LiesOver.over
have : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q) := .of_comp R _ _
trans Algebra.FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)
· exact ⟨fun _ ↦ .of_comp R _ _, fun _ ↦ Algebra.FormallyUnramified.comp _ (Localization.AtPrime p) _⟩
rw [FormallyUnramified.iff_map_maximalIdeal_eq]
congr!
rw [RingHom.algebraMap_toAlgebra, ← Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_map,
Localization.localRingHom, IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
