English
From an R-linear map f: M → N satisfying f(a•m) = X•f(m), there is an R[X]-linear map AEval R M a → N extending f.
Русский
Из линейного отображения по R, удовлетворяющего условию совместимости с a, существует R[X]-острое отображение AEval R M a → N, расширяющее f.
LaTeX
$$$\exists \ell : AEval\ R\ M\ a \to_{R[X]} N\;\text{such that}\; \ell\circ (of\ R\ M\ a) = f \\ \text{and}\; \ell((X)\,\cdot m) = X\cdot \ell(m)$$$
Lean4
/-- Construct an `R[X]`-linear map out of `AEval R M a` from a `R`-linear map out of `M`. -/
def _root_.LinearMap.ofAEval {N} [AddCommMonoid N] [Module R N] [Module R[X] N] [IsScalarTower R R[X] N] (f : M →ₗ[R] N)
(hf : ∀ m : M, f (a • m) = (X : R[X]) • f m) : AEval R M a →ₗ[R[X]] N
where
__ := f ∘ₗ (of R M a).symm
map_smul'
p :=
p.induction_on (fun k m ↦ by simp [C_eq_algebraMap]) (fun p q hp hq m ↦ by simp_all [add_smul]) fun n k h m ↦
by
simp_rw [RingHom.id_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.comp_apply,
LinearEquiv.coe_toLinearMap] at h ⊢
simp_rw [pow_succ, ← mul_assoc, mul_smul _ X, ← hf, ← of_symm_X_smul, ← h]
