English
If x is a root of a monic polynomial f ∈ R[X], then the span of the first natDegree(f) powers of x equals the underlying submodule of the subalgebra generated by x.
Русский
Если x является корнем моноического многочлена f ∈ R[X], то линейная оболочка первых мономов x степеней равна подмодуля подпалгебры, порожденной x.
LaTeX
$$$\\operatorname{span}_R\\{x^k : 0\\le k < \\operatorname{natDegree}(f)\\} = \\operatorname{submodule}(\\operatorname{Algebra.adjoin}_R\\{x\\})$$$
Lean4
theorem span_range_natDegree_eq_adjoin {R A} [CommRing R] [Semiring A] [Algebra R A] {x : A} {f : R[X]} (hf : f.Monic)
(hfx : aeval x f = 0) :
span R (Finset.image (x ^ ·) (Finset.range (natDegree f))) = Subalgebra.toSubmodule (Algebra.adjoin R { x }) :=
by
nontriviality A
have hf1 : f ≠ 1 := by rintro rfl; simp [one_ne_zero' A] at hfx
refine (span_le.mpr fun s hs ↦ ?_).antisymm fun r hr ↦ ?_
· rcases Finset.mem_image.1 hs with ⟨k, -, rfl⟩
exact (Algebra.adjoin R { x }).pow_mem (Algebra.subset_adjoin rfl) k
rw [Subalgebra.mem_toSubmodule, Algebra.adjoin_singleton_eq_range_aeval] at hr
rcases (aeval x).mem_range.mp hr with ⟨p, rfl⟩
rw [← modByMonic_add_div p hf, map_add, map_mul, hfx, zero_mul, add_zero, ← sum_C_mul_X_pow_eq (p %ₘ f), aeval_def,
eval₂_sum, sum_def]
refine sum_mem fun k hkq ↦ ?_
rw [C_mul_X_pow_eq_monomial, eval₂_monomial, ← Algebra.smul_def]
exact
smul_mem _ _
(subset_span <|
Finset.mem_image_of_mem _ <|
Finset.mem_range.mpr <| (le_natDegree_of_mem_supp _ hkq).trans_lt <| natDegree_modByMonic_lt p hf hf1)
