English
Let R, S, K, L be rings with R, S commutative, K a field, L a ring, and with algebras R ↪ S, R ↪ K, S ↪ L, K ↪ L, and IsScalarTower structures R ↪ K ↪ L and R ↪ S ↪ L. For s ∈ S, the minimal polynomial of algebraMap S L(s) over K divides the image in K[X] of minpoly_R(s) under algebraMap R K. In symbols, minpoly K(algebraMap S L s) ∣ map(algebraMap R K)(minpoly R s).
Русский
Пусть данные кольца R, S, K, L образуют цепочку скаляров с тождественными отображениями и т. д. Для элемента s ∈ S минимальный полином x = algebraMap S L s над K делит изображение minpoly_R(s) в K[X] по отображению algebraMap R K.
LaTeX
$$$\\minpoly K(\\operatorname{algebraMap} S L\,s) \\mid \\operatorname{map}(\\operatorname{algebraMap} R K) (\\minpoly R s)$$$
Lean4
theorem dvd_map_of_isScalarTower' (R : Type*) {S : Type*} (K L : Type*) [CommRing R] [CommRing S] [Field K] [Ring L]
[Algebra R S] [Algebra R K] [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L]
(s : S) : minpoly K (algebraMap S L s) ∣ map (algebraMap R K) (minpoly R s) :=
by
apply minpoly.dvd K (algebraMap S L s)
rw [← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
