-- Mathlib/RingTheory/Frobenius.lean
/-- 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. -/
lemma eq_of_isUnramifiedAt
    (H' : ψ.IsArithFrobAt Q) [Q.IsPrime] (hQ : Q.primeCompl ≤ S⁰)
    [Algebra.IsUnramifiedAt R Q] [IsNoetherianRing S] : φ = ψ

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
⊢ φ = ψ

Tactic:
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]

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
⊢ φ = ψ

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : IsNoetherianRing (Localization.AtPrime Q)
⊢ ∀ (x : Localization.AtPrime Q),
    (Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q))) (H.localize x) =
      (Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q))) (H'.localize x)

Tactic:
intro x

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : IsNoetherianRing (Localization.AtPrime Q)
x : Localization.AtPrime Q
⊢ (Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q))) (H.localize x) =
    (Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q))) (H'.localize x)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
⊢ H.localize = H'.localize

Tactic:
have : IsNoetherianRing (Localization.AtPrime Q) :=
  IsLocalization.isNoetherianRing Q.primeCompl _ inferInstance

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : IsNoetherianRing (Localization.AtPrime Q)
⊢ H.localize = H'.localize

Proof state:
case H.a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
x : S
⊢ (algebraMap S (Localization.AtPrime Q)) (φ x) = (algebraMap S (Localization.AtPrime Q)) (ψ x)

Tactic:
rw [← H.localize_algebraMap, ← H'.localize_algebraMap, this]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : IsNoetherianRing (Localization.AtPrime Q)
⊢ H.localize = H'.localize

Tactic:
apply Algebra.FormallyUnramified.ext_of_iInf _
  (Ideal.iInf_pow_eq_bot_of_isLocalRing (maximalIdeal _) Ideal.IsPrime.ne_top')

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : IsNoetherianRing (Localization.AtPrime Q)
⊢ ∀ (x : Localization.AtPrime Q),
    (Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q))) (H.localize x) =
      (Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q))) (H'.localize x)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
⊢ φ = ψ

Tactic:
ext x

Result:
case H
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
x : S
⊢ φ x = ψ x

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : IsNoetherianRing (Localization.AtPrime Q)
x : Localization.AtPrime Q
⊢ (Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q))) (H.localize x) =
    (Ideal.Quotient.mk (maximalIdeal (Localization.AtPrime Q))) (H'.localize x)

Tactic:
rw [H.isArithFrobAt_localize.mk_apply, H'.isArithFrobAt_localize.mk_apply]

Result:
no goals

Proof state:
case H
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
x : S
⊢ φ x = ψ x

Tactic:
apply IsLocalization.injective (Localization.AtPrime Q) hQ

Result:
case H.a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
x : S
⊢ (algebraMap S (Localization.AtPrime Q)) (φ x) = (algebraMap S (Localization.AtPrime Q)) (ψ x)