English
Let q be a submodule of a module M that is closed under the action of an algebra A via lsmul by a. Then applying the A-linear evaluation aeval a to any polynomial p yields an element of q when acting on any m ∈ q.
Русский
Пусть q — подмодуль M, удовлетворяющий устойчивости по действию алгебры A через lsmul. Тогда применение аeval a к полиномy p и последующее гармоничное действие на элемент m ∈ q остается в q.
LaTeX
$$$ aeval\ a\ p\; \cdot m \in q \quad\text{при} \ m \in q \text{ и } q \le q.comap (lsmul\ R\ R\ M\ a) $$$
Lean4
theorem aeval_apply_smul_mem_of_le_comap' [Semiring A] [Algebra R A] [Module A M] [IsScalarTower R A M] (hm : m ∈ q)
(p : R[X]) (a : A) (hq : q ≤ q.comap (Algebra.lsmul R R M a)) : aeval a p • m ∈ q := by
induction p using Polynomial.induction_on with
| C a => simpa using SMulMemClass.smul_mem a hm
| add f₁ f₂ h₁ h₂ =>
simp_rw [map_add, add_smul]
exact Submodule.add_mem q h₁ h₂
| monomial n t hmq =>
dsimp only at hmq ⊢
rw [pow_succ', mul_left_comm, map_mul, aeval_X, mul_smul]
solve_by_elim
