English
If a subfield F of E contains all coefficients of minpoly_E(a) for some a ∈ A and ha: a is integral over F, then the base-change of minpoly_F(a) along F→E equals minpoly_E(a): (minpoly F a).map(algebraMap F E) = minpoly_E(a).
Русский
Если подполе F ⊆ E содержит все коэффициенты minpoly_E(a) для некоторого a ∈ A и a интеграл над F, то перенос minpoly_F(a) по отображению F→E равен minpoly_E(a).
LaTeX
$$$(\\minpoly F a).map(\\mathrm{algebraMap} F E) = \\minpoly E a$$$
Lean4
/-- If a subfield `F` of `E` contains all the coefficients of `minpoly E a`, then
`minpoly F a` maps to `minpoly E a` via `algebraMap F E`. -/
theorem map_algebraMap {F E A : Type*} [Field F] [Field E] [CommRing A] [Algebra F E] [Algebra E A] [Algebra F A]
[IsScalarTower F E A] {a : A} (ha : IsIntegral F a) (h : minpoly E a ∈ lifts (algebraMap F E)) :
(minpoly F a).map (algebraMap F E) = minpoly E a :=
by
refine
eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic ha.tower_top)
((algebraMap F E).injective.monic_map_iff.mp <| minpoly.monic ha) (minpoly.dvd E a (by simp)) ?_
obtain ⟨g, hg, hgdeg, hgmon⟩ := lifts_and_natDegree_eq_and_monic h (minpoly.monic ha.tower_top)
rw [natDegree_map, ← hgdeg]
refine natDegree_le_of_dvd (minpoly.dvd F a ?_) hgmon.ne_zero
rw [← aeval_map_algebraMap A, IsScalarTower.algebraMap_eq F E A, ← coe_mapRingHom, ← mapRingHom_comp,
RingHom.comp_apply, coe_mapRingHom, coe_mapRingHom, hg, aeval_map_algebraMap, minpoly.aeval]
