English
The supremum and kernel relations described above capture how polynomials act on a module via evaluation maps.
Русский
Супремум и ядра описывают, как полиномы действуют на модуль через отображения оценки.
LaTeX
$$sup and ker relations for aeval give structural decomposition of module actions$$
Lean4
theorem sup_ker_aeval_le_ker_aeval_mul {f : M →ₗ[R] M} {p q : R[X]} :
LinearMap.ker (aeval f p) ⊔ LinearMap.ker (aeval f q) ≤ LinearMap.ker (aeval f (p * q)) :=
by
intro v hv
rcases Submodule.mem_sup.1 hv with ⟨x, hx, y, hy, hxy⟩
have h_eval_x : aeval f (p * q) x = 0 := by
rw [mul_comm, aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hx, LinearMap.map_zero]
have h_eval_y : aeval f (p * q) y = 0 := by
rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hy, LinearMap.map_zero]
rw [LinearMap.mem_ker, ← hxy, LinearMap.map_add, h_eval_x, h_eval_y, add_zero]
