R : Type u
S✝ : Type v
T : Type w
a b : R
n : ℕ
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
p✝ q : R[X]
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ ↑(aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ ↑(aeval (↑f x)) p = 0
R : Type u
S✝ : Type v
T : Type w
a b : R
n : ℕ
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
p✝ q : R[X]
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : x ∈ rootSet p S
⊢ ↑f x ∈ rootSet p S'
rw [mem_rootSet'] at hx⊢
R : Type u
S✝ : Type v
T : Type w
a b : R
n : ℕ
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
p✝ q : R[X]
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ ↑(aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ 0 = 0
R : Type u
S✝ : Type v
T : Type w
a b : R
n : ℕ
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
p✝ q : R[X]
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ ↑(aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ ↑(aeval (↑f x)) p = 0
rw [aeval_algHom, AlgHom.comp_apply, hx.2, _root_.map_zero]
no goals
R : Type u
S✝ : Type v
T : Type w
a b : R
n : ℕ
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
p✝ q : R[X]
inst✝⁶ : CommRing T
p : T[X]
S : Type u_1
S' : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra T S
inst✝² : CommRing S'
inst✝¹ : IsDomain S'
inst✝ : Algebra T S'
hp : map (algebraMap T S') p = 0 → map (algebraMap T S) p = 0
f : S →ₐ[T] S'
x : S
hx : map (algebraMap T S) p ≠ 0 ∧ ↑(aeval x) p = 0
⊢ map (algebraMap T S') p ≠ 0 ∧ 0 = 0
exact ⟨mt hp hx.1, rfl⟩