English
Equality of the polynomial-level map induced by an equivariant map with the underlying polynomial map; i.e., the coe of polynomial map equals the map on polynomials.
Русский
Равенство отображения на уровне многочленов, индуцированного эквиариантным отображением, и соответствующего отображения на полиномах.
LaTeX
$$$g.polynomial : P[X] \to Q[X] = map g$.$$
Lean4
/-- An equivariant map induces an equivariant map on polynomials. -/
protected noncomputable def polynomial (g : P →+*[M] Q) : P[X] →+*[M] Q[X]
where
toFun := map g
map_smul' m
p :=
Polynomial.induction_on p
(fun b ↦ by rw [MonoidHom.id_apply, smul_C, map_C, coe_fn_coe, g.map_smul, map_C, coe_fn_coe, smul_C])
(fun p q ihp ihq ↦ by rw [smul_add, Polynomial.map_add, ihp, ihq, Polynomial.map_add, smul_add]) fun n b _ ↦ by
rw [MonoidHom.id_apply, smul_mul', smul_C, smul_pow', smul_X, Polynomial.map_mul, map_C, Polynomial.map_pow,
map_X, coe_fn_coe, g.map_smul, Polynomial.map_mul, map_C, Polynomial.map_pow, map_X, smul_mul', smul_C,
smul_pow', smul_X, coe_fn_coe]
map_zero' := Polynomial.map_zero (g : P →+* Q)
map_add' _ _ := Polynomial.map_add (g : P →+* Q)
map_one' := Polynomial.map_one (g : P →+* Q)
map_mul' _ _ := Polynomial.map_mul (g : P →+* Q)
