ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
⊢ AlgebraicIndependent R (↑f ∘ x)
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
⊢ AlgebraicIndependent R (↑f ∘ x)
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x) p ∈ AlgHom.range (aeval Subtype.val)
⊢ AlgebraicIndependent R (↑f ∘ x)
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
⊢ AlgebraicIndependent R (↑f ∘ x)
have h : ∀ p : MvPolynomial ι R, aeval x p ∈ (@aeval R _ _ _ _ _ ((↑) : range x → A)).range := by
  intro p
  rw [AlgHom.mem_range]
  refine' ⟨MvPolynomial.rename (codRestrict x (range x) mem_range_self) p, _⟩
  simp [Function.comp, aeval_rename]
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x✝ : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x✝))
this : aeval (↑f ∘ x✝) = AlgHom.comp f (aeval x✝)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x✝) p ∈ AlgHom.range (aeval Subtype.val)
x y : MvPolynomial ι R
hxy : ↑(aeval (↑f ∘ x✝)) x = ↑(aeval (↑f ∘ x✝)) y
⊢ x = y
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x) p ∈ AlgHom.range (aeval Subtype.val)
⊢ AlgebraicIndependent R (↑f ∘ x)
intro x y hxy
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x✝ : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x✝))
this : aeval (↑f ∘ x✝) = AlgHom.comp f (aeval x✝)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x✝) p ∈ AlgHom.range (aeval Subtype.val)
x y : MvPolynomial ι R
hxy : ↑(AlgHom.comp f (aeval x✝)) x = ↑(AlgHom.comp f (aeval x✝)) y
⊢ x = y
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x✝ : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x✝))
this : aeval (↑f ∘ x✝) = AlgHom.comp f (aeval x✝)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x✝) p ∈ AlgHom.range (aeval Subtype.val)
x y : MvPolynomial ι R
hxy : ↑(aeval (↑f ∘ x✝)) x = ↑(aeval (↑f ∘ x✝)) y
⊢ x = y
rw [this] at hxy
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x✝ : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(AlgHom.range (aeval Subtype.val))
this : aeval (↑f ∘ x✝) = AlgHom.comp f (aeval x✝)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x✝) p ∈ AlgHom.range (aeval Subtype.val)
x y : MvPolynomial ι R
hxy : ↑(AlgHom.comp f (aeval x✝)) x = ↑(AlgHom.comp f (aeval x✝)) y
⊢ x = y
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x✝ : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x✝))
this : aeval (↑f ∘ x✝) = AlgHom.comp f (aeval x✝)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x✝) p ∈ AlgHom.range (aeval Subtype.val)
x y : MvPolynomial ι R
hxy : ↑(AlgHom.comp f (aeval x✝)) x = ↑(AlgHom.comp f (aeval x✝)) y
⊢ x = y
rw [adjoin_eq_range] at hf_inj
no goals
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x✝ : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x✝
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(AlgHom.range (aeval Subtype.val))
this : aeval (↑f ∘ x✝) = AlgHom.comp f (aeval x✝)
h : ∀ (p : MvPolynomial ι R), ↑(aeval x✝) p ∈ AlgHom.range (aeval Subtype.val)
x y : MvPolynomial ι R
hxy : ↑(AlgHom.comp f (aeval x✝)) x = ↑(AlgHom.comp f (aeval x✝)) y
⊢ x = y
exact hx (hf_inj (h x) (h y) hxy)
case hf
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
i✝ : ι
⊢ ↑(aeval (↑f ∘ x)) (X i✝) = ↑(AlgHom.comp f (aeval x)) (X i✝)
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
⊢ aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
ext
no goals
case hf
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
i✝ : ι
⊢ ↑(aeval (↑f ∘ x)) (X i✝) = ↑(AlgHom.comp f (aeval x)) (X i✝)
simp
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
p : MvPolynomial ι R
⊢ ↑(aeval x) p ∈ AlgHom.range (aeval Subtype.val)
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
⊢ ∀ (p : MvPolynomial ι R), ↑(aeval x) p ∈ AlgHom.range (aeval Subtype.val)
intro p
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
p : MvPolynomial ι R
⊢ ∃ x_1, ↑(aeval Subtype.val) x_1 = ↑(aeval x) p
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
p : MvPolynomial ι R
⊢ ↑(aeval x) p ∈ AlgHom.range (aeval Subtype.val)
rw [AlgHom.mem_range]
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
p : MvPolynomial ι R
⊢ ↑(aeval Subtype.val) (↑(rename (codRestrict x (range x) (_ : ∀ (i : ι), x i ∈ range fun x_1 => x x_1))) p) =
    ↑(aeval x) p
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
p : MvPolynomial ι R
⊢ ∃ x_1, ↑(aeval Subtype.val) x_1 = ↑(aeval x) p
refine' ⟨MvPolynomial.rename (codRestrict x (range x) mem_range_self) p, _⟩
no goals
ι : Type u_4
ι' : Type ?u.209986
R : Type u_1
K : Type ?u.209992
A : Type u_2
A' : Type u_3
A'' : Type ?u.210001
V : Type u
V' : Type ?u.210006
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ↑f ↑(adjoin R (range x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
p : MvPolynomial ι R
⊢ ↑(aeval Subtype.val) (↑(rename (codRestrict x (range x) (_ : ∀ (i : ι), x i ∈ range fun x_1 => x x_1))) p) =
    ↑(aeval x) p
simp [Function.comp, aeval_rename]