ι : Type u_1
ι' : Type ?u.74821
R : Type u_2
K : Type ?u.74827
A : Type u_3
A' : Type ?u.74833
A'' : Type ?u.74836
V : Type u
V' : Type ?u.74841
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
inst✝ : IsEmpty ι
this : aeval x = AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)
⊢ AlgebraicIndependent R x ↔ Injective ↑(algebraMap R A)
ι : Type u_1
ι' : Type ?u.74821
R : Type u_2
K : Type ?u.74827
A : Type u_3
A' : Type ?u.74833
A'' : Type ?u.74836
V : Type u
V' : Type ?u.74841
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
inst✝ : IsEmpty ι
⊢ AlgebraicIndependent R x ↔ Injective ↑(algebraMap R A)
have : aeval x = (Algebra.ofId R A).comp (@isEmptyAlgEquiv R ι _ _).toAlgHom := by
  ext i
  exact IsEmpty.elim' ‹IsEmpty ι› i
ι : Type u_1
ι' : Type ?u.74821
R : Type u_2
K : Type ?u.74827
A : Type u_3
A' : Type ?u.74833
A'' : Type ?u.74836
V : Type u
V' : Type ?u.74841
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
inst✝ : IsEmpty ι
this : aeval x = AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)
⊢ Injective ↑(AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)) ↔ Injective (↑(algebraMap R A) ∘ ↑(isEmptyAlgEquiv R ι))
ι : Type u_1
ι' : Type ?u.74821
R : Type u_2
K : Type ?u.74827
A : Type u_3
A' : Type ?u.74833
A'' : Type ?u.74836
V : Type u
V' : Type ?u.74841
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
inst✝ : IsEmpty ι
this : aeval x = AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)
⊢ AlgebraicIndependent R x ↔ Injective ↑(algebraMap R A)
rw [AlgebraicIndependent, this, ← Injective.of_comp_iff' _ (@isEmptyAlgEquiv R ι _ _).bijective]
no goals
ι : Type u_1
ι' : Type ?u.74821
R : Type u_2
K : Type ?u.74827
A : Type u_3
A' : Type ?u.74833
A'' : Type ?u.74836
V : Type u
V' : Type ?u.74841
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
inst✝ : IsEmpty ι
this : aeval x = AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)
⊢ Injective ↑(AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)) ↔ Injective (↑(algebraMap R A) ∘ ↑(isEmptyAlgEquiv R ι))
rfl
case hf
ι : Type u_1
ι' : Type ?u.74821
R : Type u_2
K : Type ?u.74827
A : Type u_3
A' : Type ?u.74833
A'' : Type ?u.74836
V : Type u
V' : Type ?u.74841
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
inst✝ : IsEmpty ι
i : ι
⊢ ↑(aeval x) (X i) = ↑(AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)) (X i)
ι : Type u_1
ι' : Type ?u.74821
R : Type u_2
K : Type ?u.74827
A : Type u_3
A' : Type ?u.74833
A'' : Type ?u.74836
V : Type u
V' : Type ?u.74841
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
inst✝ : IsEmpty ι
⊢ aeval x = AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)
ext i
no goals
case hf
ι : Type u_1
ι' : Type ?u.74821
R : Type u_2
K : Type ?u.74827
A : Type u_3
A' : Type ?u.74833
A'' : Type ?u.74836
V : Type u
V' : Type ?u.74841
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
inst✝ : IsEmpty ι
i : ι
⊢ ↑(aeval x) (X i) = ↑(AlgHom.comp (ofId R A) ↑(isEmptyAlgEquiv R ι)) (X i)
exact IsEmpty.elim' ‹IsEmpty ι› i