[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
let e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ _ _
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ IsIntegrallyClosed R → ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
rintro ⟨cl⟩
[GOAL]
case mp.mk
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
⊢ ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
refine' fun hx => _
[GOAL]
case mp.mk
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
x✝ : K
hx : IsIntegral R x✝
⊢ ∃ y, ↑(algebraMap R K) y = x✝
[PROOFSTEP]
obtain ⟨y, hy⟩ := cl ((isIntegral_algEquiv e).mpr hx)
[GOAL]
case mp.mk.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
x✝ : K
hx : IsIntegral R x✝
y : R
hy : ↑(algebraMap R (FractionRing R)) y = ↑e x✝
⊢ ∃ y, ↑(algebraMap R K) y = x✝
[PROOFSTEP]
exact ⟨y, e.algebraMap_eq_apply.mp hy⟩
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
⊢ (∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x) → IsIntegrallyClosed R
[PROOFSTEP]
rintro cl
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
⊢ IsIntegrallyClosed R
[PROOFSTEP]
refine' ⟨fun hx => _⟩
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : FractionRing R
hx : IsIntegral R x✝
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = x✝
[PROOFSTEP]
obtain ⟨y, hy⟩ := cl ((isIntegral_algEquiv e.symm).mpr hx)
[GOAL]
case mpr.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
e : K ≃ₐ[R] FractionRing R := IsLocalization.algEquiv R⁰ K (FractionRing R)
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : FractionRing R
hx : IsIntegral R x✝
y : R
hy : ↑(algebraMap R K) y = ↑(AlgEquiv.symm e) x✝
⊢ ∃ y, ↑(algebraMap R (FractionRing R)) y = x✝
[PROOFSTEP]
exact ⟨y, e.symm.algebraMap_eq_apply.mp hy⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ (∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x) ↔ IsIntegralClosure R R K
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ (∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x) → IsIntegralClosure R R K
[PROOFSTEP]
intro cl
[GOAL]
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
⊢ IsIntegralClosure R R K
[PROOFSTEP]
refine' ⟨IsFractionRing.injective R K, ⟨cl, _⟩⟩
[GOAL]
case mp
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
⊢ (∃ y, ↑(algebraMap R K) y = x✝) → IsIntegral R x✝
[PROOFSTEP]
rintro ⟨y, y_eq⟩
[GOAL]
case mp.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
y : R
y_eq : ↑(algebraMap R K) y = x✝
⊢ IsIntegral R x✝
[PROOFSTEP]
rw [← y_eq]
[GOAL]
case mp.intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
cl : ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
x✝ : K
y : R
y_eq : ↑(algebraMap R K) y = x✝
⊢ IsIntegral R (↑(algebraMap R K) y)
[PROOFSTEP]
exact isIntegral_algebraMap
[GOAL]
case mpr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ IsIntegralClosure R R K → ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
rintro ⟨-, cl⟩ x hx
[GOAL]
case mpr.mk
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
cl : ∀ {x : K}, IsIntegral R x ↔ ∃ y, ↑(algebraMap R K) y = x
x : K
hx : IsIntegral R x
⊢ ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
exact cl.mp hx
[GOAL]
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K = ⊥ ↔ IsIntegrallyClosed R
[PROOFSTEP]
refine' eq_bot_iff.trans _
[GOAL]
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K ≤ ⊥ ↔ IsIntegrallyClosed R
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K ≤ ⊥ → IsIntegrallyClosed R
[PROOFSTEP]
rw [isIntegrallyClosed_iff K]
[GOAL]
case mp
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K ≤ ⊥ → ∀ {x : K}, IsIntegral R x → ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
intro h x hx
[GOAL]
case mp
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
h : integralClosure R K ≤ ⊥
x : K
hx : IsIntegral R x
⊢ ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
exact Set.mem_range.mp (Algebra.mem_bot.mp (h hx))
[GOAL]
case mpr
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ IsIntegrallyClosed R → integralClosure R K ≤ ⊥
[PROOFSTEP]
intro h x hx
[GOAL]
case mpr
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
h : IsIntegrallyClosed R
x : K
hx : x ∈ integralClosure R K
⊢ x ∈ ⊥
[PROOFSTEP]
rw [Algebra.mem_bot, Set.mem_range]
[GOAL]
case mpr
R : Type u_1
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
h : IsIntegrallyClosed R
x : K
hx : x ∈ integralClosure R K
⊢ ∃ y, ↑(algebraMap R K) y = x
[PROOFSTEP]
exact isIntegral_iff.mp hx
