R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
⊢ False
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
⊢ False
let f0 : FreeAlgebra R X →ₐ[R] R := lift R 0
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
⊢ False
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
⊢ False
let f1 : FreeAlgebra R X →ₐ[R] R := lift R 1
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : ↑f0 (ι R x) = 0
⊢ False
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
⊢ False
have hf0 : f0 (ι R x) = 0 := lift_ι_apply _ _
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : ↑f0 (ι R x) = 0
hf1 : ↑f1 (ι R x) = 1
⊢ False
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : ↑f0 (ι R x) = 0
⊢ False
have hf1 : f1 (ι R x) = 1 := lift_ι_apply _ _
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : r = 0
hf1 : ↑f1 (ι R x) = 1
⊢ False
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : ↑f0 (ι R x) = 0
hf1 : ↑f1 (ι R x) = 1
⊢ False
rw [h, f0.commutes, Algebra.id.map_eq_self] at hf0
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : r = 0
hf1 : r = 1
⊢ False
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : r = 0
hf1 : ↑f1 (ι R x) = 1
⊢ False
rw [h, f1.commutes, Algebra.id.map_eq_self] at hf1
no goals
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.733161
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : r = 0
hf1 : r = 1
⊢ False
exact zero_ne_one (hf0.symm.trans hf1)