case h
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
⊢ y ∈ Subalgebra.map (↑f) (integralClosure R A) ↔ y ∈ integralClosure R B
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
⊢ Subalgebra.map (↑f) (integralClosure R A) = integralClosure R B
ext y
case h
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
⊢ (∃ x, x ∈ integralClosure R A ∧ ↑↑f x = y) ↔ y ∈ integralClosure R B
case h
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
⊢ y ∈ Subalgebra.map (↑f) (integralClosure R A) ↔ y ∈ integralClosure R B
rw [Subalgebra.mem_map]
case h.mp
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
⊢ (∃ x, x ∈ integralClosure R A ∧ ↑↑f x = y) → y ∈ integralClosure R B

case h.mpr
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
⊢ y ∈ integralClosure R B → ∃ x, x ∈ integralClosure R A ∧ ↑↑f x = y
case h
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
⊢ (∃ x, x ∈ integralClosure R A ∧ ↑↑f x = y) ↔ y ∈ integralClosure R B
constructor
case h.mp.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
x : A
hx : x ∈ integralClosure R A
⊢ ↑↑f x ∈ integralClosure R B
case h.mp
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
⊢ (∃ x, x ∈ integralClosure R A ∧ ↑↑f x = y) → y ∈ integralClosure R B
rintro ⟨x, hx, rfl⟩
no goals
case h.mp.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
x : A
hx : x ∈ integralClosure R A
⊢ ↑↑f x ∈ integralClosure R B
exact map_isIntegral f hx
case h.mpr
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
hy : y ∈ integralClosure R B
⊢ ∃ x, x ∈ integralClosure R A ∧ ↑↑f x = y
case h.mpr
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
⊢ y ∈ integralClosure R B → ∃ x, x ∈ integralClosure R A ∧ ↑↑f x = y
intro hy
case h.mpr
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
hy : y ∈ integralClosure R B
⊢ ↑↑f (↑(AlgEquiv.symm f) y) = y
case h.mpr
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
hy : y ∈ integralClosure R B
⊢ ∃ x, x ∈ integralClosure R A ∧ ↑↑f x = y
use f.symm y, map_isIntegral (f.symm : B →ₐ[R] A) hy
no goals
case h.mpr
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.725847
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : R →+* S
f : A ≃ₐ[R] B
y : B
hy : y ∈ integralClosure R B
⊢ ↑↑f (↑(AlgEquiv.symm f) y) = y
simp