English
Suppose S is Noetherian and Q is a prime of S; if S/R is unramified at Q, then two Frobenius endomorphisms φ, ψ at Q coincide: φ = ψ.
Русский
Пусть S ноetherian, Q — простый идеал, и S/R неразветвляется в Q; тогда две Фробениус-отображения по Q совпадают: φ = ψ.
LaTeX
$$φ = ψ under the stated hypotheses$$
Lean4
/-- Suppose `S` is Noetherian and `Q` is a prime of `S` containing all zero divisors.
If `S/R` is unramified at `Q`, then the Frobenius `φ : S →ₐ[R] S` over `Q` is unique. -/
theorem eq_of_isUnramifiedAt (H' : ψ.IsArithFrobAt Q) [Q.IsPrime] (hQ : Q.primeCompl ≤ S⁰) [Algebra.IsUnramifiedAt R Q]
[IsNoetherianRing S] : φ = ψ :=
by
have : H.localize = H'.localize :=
by
have : IsNoetherianRing (Localization.AtPrime Q) := IsLocalization.isNoetherianRing Q.primeCompl _ inferInstance
apply
Algebra.FormallyUnramified.ext_of_iInf _
(Ideal.iInf_pow_eq_bot_of_isLocalRing (maximalIdeal _) Ideal.IsPrime.ne_top')
intro x
rw [H.isArithFrobAt_localize.mk_apply, H'.isArithFrobAt_localize.mk_apply]
ext x
apply IsLocalization.injective (Localization.AtPrime Q) hQ
rw [← H.localize_algebraMap, ← H'.localize_algebraMap, this]
