English
For any polynomials p, q, the join of the kernels of aeval f p and aeval f q is contained in the kernel of aeval f (p q).
Русский
Для любых p, q объединение ядер aeval f p и aeval f q входит в ядро aeval f (p q).
LaTeX
$$ker(aeval f p) ⊔ ker(aeval f q) ≤ ker(aeval f (p q))$$
Lean4
theorem sup_aeval_range_eq_top_of_isCoprime (f : M →ₗ[R] M) {p q : R[X]} (hpq : IsCoprime p q) :
LinearMap.range (aeval f p) ⊔ LinearMap.range (aeval f q) = ⊤ :=
by
rw [eq_top_iff]
intro v _
rw [Submodule.mem_sup]
rcases hpq with ⟨p', q', hpq'⟩
use aeval f (p * p') v
use LinearMap.mem_range.2 ⟨aeval f p' v, by simp only [Module.End.mul_apply, aeval_mul]⟩
use aeval f (q * q') v
use LinearMap.mem_range.2 ⟨aeval f q' v, by simp only [Module.End.mul_apply, aeval_mul]⟩
simpa only [mul_comm p p', mul_comm q q', aeval_one, aeval_add] using congr_arg (fun p : R[X] => aeval f p v) hpq'
