English
There is a canonical linear isomorphism between PolynomialModule R R and R[X].
Русский
Существует каноническое линейное изоморфизм между PolynomialModule R R и R[X].
LaTeX
$$PolynomialModule.equivPolynomialSelf : PolynomialModule R R ≃ₗ[R[X]] R[X]$$
Lean4
/-- `PolynomialModule R R` is isomorphic to `R[X]` as an `R[X]` module. -/
noncomputable def equivPolynomialSelf : PolynomialModule R R ≃ₗ[R[X]] R[X] :=
{ (Polynomial.toFinsuppIso R).symm with
map_smul' := fun r x => by
dsimp
rw [← RingEquiv.coe_toEquiv_symm, RingEquiv.coe_toEquiv]
induction x using induction_linear with
| zero => rw [smul_zero, map_zero, mul_zero]
| add _ _ hp hq => rw [smul_add, map_add, map_add, mul_add, hp, hq]
| single n a =>
ext i
simp only [coeff_ofFinsupp, smul_single_apply, toFinsuppIso_symm_apply, coeff_ofFinsupp, single_apply,
smul_eq_mul, Polynomial.coeff_mul, mul_ite, mul_zero]
split_ifs with hn
· rw [Finset.sum_eq_single (i - n, n)]
· simp only [ite_true]
· rintro ⟨p, q⟩ hpq1 hpq2
rw [Finset.mem_antidiagonal] at hpq1
split_ifs with H
· dsimp at H
exfalso
apply hpq2
rw [← hpq1, H]
simp only [add_tsub_cancel_right]
· rfl
· intro H
exfalso
apply H
rw [Finset.mem_antidiagonal, tsub_add_cancel_of_le hn]
· symm
rw [Finset.sum_ite_of_false, Finset.sum_const_zero]
grind [Finset.mem_antidiagonal] }
