R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K ≤ ⊥ ↔ IsIntegrallyClosed R
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K = ⊥ ↔ IsIntegrallyClosed R
refine' eq_bot_iff.trans _
case mp
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K ≤ ⊥ → IsIntegrallyClosed R

case mpr
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ IsIntegrallyClosed R → integralClosure R K ≤ ⊥
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K ≤ ⊥ ↔ IsIntegrallyClosed R
constructor
case mp
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
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
case mp
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ integralClosure R K ≤ ⊥ → IsIntegrallyClosed R
rw [isIntegrallyClosed_iff K]
case mp
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
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
case mp
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
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
intro h x hx
no goals
case mp
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
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
exact Set.mem_range.mp (Algebra.mem_bot.mp (h hx))
case mpr
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
h : IsIntegrallyClosed R
x : K
hx : x ∈ integralClosure R K
⊢ x ∈ ⊥
case mpr
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
⊢ IsIntegrallyClosed R → integralClosure R K ≤ ⊥
intro h x hx
case mpr
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
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
case mpr
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra R K
ifr : IsFractionRing R K
h : IsIntegrallyClosed R
x : K
hx : x ∈ integralClosure R K
⊢ x ∈ ⊥
rw [Algebra.mem_bot, Set.mem_range]
no goals
case mpr
R : Type u_2
inst✝² : CommRing R
id : IsDomain R
iic : IsIntegrallyClosed R
K : Type u_1
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
exact isIntegral_iff.mp hx