English
Let f be a linear endomorphism of a module over a commutative ring, and let p and q be coprime polynomials. Then the join of the kernels of the endomorphisms aeval_f(p) and aeval_f(q) equals the kernel of aeval_f(p q).
Русский
Пусть f — линейное отображение M → M над коммутативным кольцом, а p и q — взаимно простые полиномы. Тогда сумма (объединение) ядер отображений aeval_f(p) и aeval_f(q) равна ядру aeval_f(p q).
LaTeX
$$$\ker(\mathrm{aeval}_f(p)) \sqcup \ker(\mathrm{aeval}_f(q)) = \ker(\mathrm{aeval}_f(pq))$$$
Lean4
theorem sup_ker_aeval_eq_ker_aeval_mul_of_coprime (f : M →ₗ[R] M) {p q : R[X]} (hpq : IsCoprime p q) :
LinearMap.ker (aeval f p) ⊔ LinearMap.ker (aeval f q) = LinearMap.ker (aeval f (p * q)) :=
by
apply le_antisymm sup_ker_aeval_le_ker_aeval_mul
intro v hv
rw [Submodule.mem_sup]
rcases hpq with ⟨p', q', hpq'⟩
have h_eval₂_qpp' :=
calc
aeval f (q * (p * p')) v = aeval f (p' * (p * q)) v := by
rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
_ = 0 := by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, LinearMap.map_zero]
have h_eval₂_pqq' :=
calc
aeval f (p * (q * q')) v = aeval f (q' * (p * q)) v := by rw [← mul_assoc, mul_comm]
_ = 0 := by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, LinearMap.map_zero]
rw [aeval_mul] at h_eval₂_qpp' h_eval₂_pqq'
refine
⟨aeval f (q * q') v, LinearMap.mem_ker.1 h_eval₂_pqq', aeval f (p * p') v, LinearMap.mem_ker.1 h_eval₂_qpp', ?_⟩
rw [add_comm, mul_comm p p', mul_comm q q']
simpa only [map_add, map_mul, aeval_one] using congr_arg (fun p : R[X] => aeval f p v) hpq'
