case h
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (AlgHom.comp g f) x i = comap f (comap g x) i
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (AlgHom.comp g f) x = comap f (comap g x)
funext i
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (AlgHom.comp g f) x i = ↑(aeval x) (↑(aeval fun i => ↑g (X i)) (↑f (X i)))

σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(aeval x) (↑(aeval fun i => ↑g (X i)) (↑f (X i))) = comap f (comap g x) i
case h
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (AlgHom.comp g f) x i = comap f (comap g x) i
trans aeval x (aeval (fun i => g (X i)) (f (X i)))
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(AlgHom.comp g f) (X i) = ↑(aeval fun i => ↑g (X i)) (↑f (X i))
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (AlgHom.comp g f) x i = ↑(aeval x) (↑(aeval fun i => ↑g (X i)) (↑f (X i)))
apply eval₂Hom_congr rfl rfl
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑g (↑f (X i)) = ↑(aeval fun i => ↑g (X i)) (↑f (X i))
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(AlgHom.comp g f) (X i) = ↑(aeval fun i => ↑g (X i)) (↑f (X i))
rw [AlgHom.comp_apply]
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ g = aeval fun i => ↑g (X i)
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑g (↑f (X i)) = ↑(aeval fun i => ↑g (X i)) (↑f (X i))
suffices g = aeval fun i => g (X i) by rw [← this]
no goals
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ g = aeval fun i => ↑g (X i)
exact aeval_unique g
no goals
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
this : g = aeval fun i => ↑g (X i)
⊢ ↑g (↑f (X i)) = ↑(aeval fun i => ↑g (X i)) (↑f (X i))
rw [← this]
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(eval₂Hom (RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R))) fun i =>
          ↑(eval₂Hom (algebraMap R R) x) (↑g (X i)))
      (↑f (X i)) =
    ↑(eval₂Hom (algebraMap R R) fun i => ↑(eval₂Hom (algebraMap R R) x) (↑g (X i))) (↑f (X i))
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(aeval x) (↑(aeval fun i => ↑g (X i)) (↑f (X i))) = comap f (comap g x) i
simp only [comap, aeval_eq_eval₂Hom, map_eval₂Hom, AlgHom.comp_apply]
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)) = algebraMap R R
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(eval₂Hom (RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R))) fun i =>
          ↑(eval₂Hom (algebraMap R R) x) (↑g (X i)))
      (↑f (X i)) =
    ↑(eval₂Hom (algebraMap R R) fun i => ↑(eval₂Hom (algebraMap R R) x) (↑g (X i))) (↑f (X i))
refine' eval₂Hom_congr _ rfl rfl
case a
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
r : R
⊢ ↑(RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R))) r = ↑(algebraMap R R) r
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)) = algebraMap R R
ext r
no goals
case a
σ : Type u_2
τ : Type u_3
υ : Type u_4
R : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
r : R
⊢ ↑(RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R))) r = ↑(algebraMap R R) r
apply aeval_C