ι : Type u_1
ι' : Type ?u.541666
R : Type u_2
K : Type ?u.541672
A : Type u_3
A' : Type ?u.541678
A'' : Type ?u.541681
V : Type u
V' : Type ?u.541686
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
s : Set ι
this : aeval (x ∘ Subtype.val) = AlgHom.comp (aeval x) (rename Subtype.val)
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ (p : MvPolynomial ι R), p ∈ supported R s → ↑(aeval x) p = 0 → p = 0
ι : Type u_1
ι' : Type ?u.541666
R : Type u_2
K : Type ?u.541672
A : Type u_3
A' : Type ?u.541678
A'' : Type ?u.541681
V : Type u
V' : Type ?u.541686
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
s : Set ι
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ (p : MvPolynomial ι R), p ∈ supported R s → ↑(aeval x) p = 0 → p = 0
have : (aeval (x ∘ (↑) : s → A) : _ →ₐ[R] _) = (aeval x).comp (rename (↑)) := by ext; simp
ι : Type u_1
ι' : Type ?u.541666
R : Type u_2
K : Type ?u.541672
A : Type u_3
A' : Type ?u.541678
A'' : Type ?u.541681
V : Type u
V' : Type ?u.541686
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
s : Set ι
this✝ : aeval (x ∘ Subtype.val) = AlgHom.comp (aeval x) (rename Subtype.val)
this : ∀ (p : MvPolynomial (↑s) R), ↑(rename Subtype.val) p = 0 ↔ p = 0
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ (p : MvPolynomial ι R), p ∈ supported R s → ↑(aeval x) p = 0 → p = 0
ι : Type u_1
ι' : Type ?u.541666
R : Type u_2
K : Type ?u.541672
A : Type u_3
A' : Type ?u.541678
A'' : Type ?u.541681
V : Type u
V' : Type ?u.541686
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
s : Set ι
this : aeval (x ∘ Subtype.val) = AlgHom.comp (aeval x) (rename Subtype.val)
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ (p : MvPolynomial ι R), p ∈ supported R s → ↑(aeval x) p = 0 → p = 0
have : ∀ p : MvPolynomial s R, rename ((↑) : s → ι) p = 0 ↔ p = 0 :=
  (injective_iff_map_eq_zero' (rename ((↑) : s → ι) : MvPolynomial s R →ₐ[R] _).toRingHom).1
    (rename_injective _ Subtype.val_injective)
no goals
ι : Type u_1
ι' : Type ?u.541666
R : Type u_2
K : Type ?u.541672
A : Type u_3
A' : Type ?u.541678
A'' : Type ?u.541681
V : Type u
V' : Type ?u.541686
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
s : Set ι
this✝ : aeval (x ∘ Subtype.val) = AlgHom.comp (aeval x) (rename Subtype.val)
this : ∀ (p : MvPolynomial (↑s) R), ↑(rename Subtype.val) p = 0 ↔ p = 0
⊢ AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ (p : MvPolynomial ι R), p ∈ supported R s → ↑(aeval x) p = 0 → p = 0
simp [algebraicIndependent_iff, supported_eq_range_rename, *]
case hf
ι : Type u_1
ι' : Type ?u.541666
R : Type u_2
K : Type ?u.541672
A : Type u_3
A' : Type ?u.541678
A'' : Type ?u.541681
V : Type u
V' : Type ?u.541686
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
s : Set ι
i✝ : ↑s
⊢ ↑(aeval (x ∘ Subtype.val)) (X i✝) = ↑(AlgHom.comp (aeval x) (rename Subtype.val)) (X i✝)
ι : Type u_1
ι' : Type ?u.541666
R : Type u_2
K : Type ?u.541672
A : Type u_3
A' : Type ?u.541678
A'' : Type ?u.541681
V : Type u
V' : Type ?u.541686
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
s : Set ι
⊢ aeval (x ∘ Subtype.val) = AlgHom.comp (aeval x) (rename Subtype.val)
ext
no goals
case hf
ι : Type u_1
ι' : Type ?u.541666
R : Type u_2
K : Type ?u.541672
A : Type u_3
A' : Type ?u.541678
A'' : Type ?u.541681
V : Type u
V' : Type ?u.541686
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
s : Set ι
i✝ : ↑s
⊢ ↑(aeval (x ∘ Subtype.val)) (X i✝) = ↑(AlgHom.comp (aeval x) (rename Subtype.val)) (X i✝)
simp