LinearMap.exists_monic_aeval_eq_zero_map_eq_prod_of_residual_diagonal
A finite spanning family on which an endomorphism is diagonal modulo an ideal gives an annihilating polynomial with the corresponding prescribed reduction.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open Polynomial
universe u v w
namespace LinearMapLean source · statement
theorem exists_monic_aeval_eq_zero_map_eq_prod_of_residual_diagonal
{R : Type u} {M : Type v} {ι : Type w}
[CommRing R] [AddCommGroup M] [Module R M] [Fintype ι]
(I : Ideal R) (f : Module.End R M) (v : ι → M)
(hv : Submodule.span R (Set.range v) = ⊤) (d : ι → R)
(hres : ∀ j, f (v j) - d j • v j ∈ I • (⊤ : Submodule R M)) :
∃ p : R[X], p.Monic ∧ aeval f p = 0 ∧
p.map (Ideal.Quotient.mk I) =
∏ j, (X - C (Ideal.Quotient.mk I (d j)))