R✝ : Type ?u.130170
A : Type ?u.130173
B : Type ?u.130176
S✝ : Type ?u.130179
inst✝¹¹ : CommRing R✝
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ A
inst✝⁶ : Algebra R✝ B
f : R✝ →+* S✝
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : CommRing U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
a : S
ha : ∃ p, Monic p ∧ eval₂ (algebraMap R S) a p = 0
⊢ ∃ p, Monic p ∧ eval₂ (algebraMap T ((fun x => U) a)) (↑ψ a) p = 0
R✝ : Type ?u.130170
A : Type ?u.130173
B : Type ?u.130176
S✝ : Type ?u.130179
inst✝¹¹ : CommRing R✝
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ A
inst✝⁶ : Algebra R✝ B
f : R✝ →+* S✝
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : CommRing U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
a : S
ha : IsIntegral R a
⊢ IsIntegral T (↑ψ a)
rw [IsIntegral, RingHom.IsIntegralElem] at ha⊢
case intro
R✝ : Type ?u.130170
A : Type ?u.130173
B : Type ?u.130176
S✝ : Type ?u.130179
inst✝¹¹ : CommRing R✝
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ A
inst✝⁶ : Algebra R✝ B
f : R✝ →+* S✝
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : CommRing U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
a : S
p : R[X]
hp : Monic p ∧ eval₂ (algebraMap R S) a p = 0
⊢ ∃ p, Monic p ∧ eval₂ (algebraMap T ((fun x => U) a)) (↑ψ a) p = 0
R✝ : Type ?u.130170
A : Type ?u.130173
B : Type ?u.130176
S✝ : Type ?u.130179
inst✝¹¹ : CommRing R✝
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ A
inst✝⁶ : Algebra R✝ B
f : R✝ →+* S✝
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : CommRing U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
a : S
ha : ∃ p, Monic p ∧ eval₂ (algebraMap R S) a p = 0
⊢ ∃ p, Monic p ∧ eval₂ (algebraMap T ((fun x => U) a)) (↑ψ a) p = 0
obtain ⟨p, hp⟩ := ha
case intro
R✝ : Type ?u.130170
A : Type ?u.130173
B : Type ?u.130176
S✝ : Type ?u.130179
inst✝¹¹ : CommRing R✝
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ A
inst✝⁶ : Algebra R✝ B
f : R✝ →+* S✝
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : CommRing U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
a : S
p : R[X]
hp : Monic p ∧ eval₂ (algebraMap R S) a p = 0
⊢ eval₂ (algebraMap T ((fun x => U) a)) (↑ψ a) (Polynomial.map φ p) = 0
case intro
R✝ : Type ?u.130170
A : Type ?u.130173
B : Type ?u.130176
S✝ : Type ?u.130179
inst✝¹¹ : CommRing R✝
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ A
inst✝⁶ : Algebra R✝ B
f : R✝ →+* S✝
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : CommRing U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
a : S
p : R[X]
hp : Monic p ∧ eval₂ (algebraMap R S) a p = 0
⊢ ∃ p, Monic p ∧ eval₂ (algebraMap T ((fun x => U) a)) (↑ψ a) p = 0
refine' ⟨p.map φ, hp.left.map _, _⟩
no goals
case intro
R✝ : Type ?u.130170
A : Type ?u.130173
B : Type ?u.130176
S✝ : Type ?u.130179
inst✝¹¹ : CommRing R✝
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : CommRing S✝
inst✝⁷ : Algebra R✝ A
inst✝⁶ : Algebra R✝ B
f : R✝ →+* S✝
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : CommRing U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)
a : S
p : R[X]
hp : Monic p ∧ eval₂ (algebraMap R S) a p = 0
⊢ eval₂ (algebraMap T ((fun x => U) a)) (↑ψ a) (Polynomial.map φ p) = 0
rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.right,
  RingHom.map_zero]