English
Let R,S,T be rings with R a domain and S,T also domains, and let f: R ≃+* A and g: S ≃+* T be ring isomorphisms satisfying a compatibility condition between algebra maps. Then for x ∈ S, map f applied to the minimal polynomial minpoly R x equals minpoly A (g x).
Русский
Пусть R,S,T кольца; f: R ≃+* A и g: S ≃+* T — изоморфизмы колец, удовлетворяющие совместимости между отображениями алгебр. Тогда для x ∈ S выполняется map f(minpoly_R x) = minpoly_A(g x).
LaTeX
$$$\operatorname{map} f(\minpoly_R x) = \minpoly_A( g(x) )$$$
Lean4
theorem map_eq_of_equiv_equiv {R S T : Type*} [CommRing R] [IsDomain R] [Ring S] [Ring T] [IsDomain S] [IsDomain T]
[Algebra R S] [Algebra A T] [Algebra.IsIntegral R S] {f : R ≃+* A} {g : S ≃+* T}
(hcomp : (algebraMap A T).comp f = (g : S →+* T).comp (algebraMap R S)) (x : S) :
map f (minpoly R x) = minpoly A (g x) :=
by
refine minpoly.eq_of_irreducible_of_monic ?_ ?_ ?_
· rw [← mapEquiv_apply, MulEquiv.irreducible_iff]
exact minpoly.irreducible (Algebra.IsIntegral.isIntegral x)
· simpa using (map_aeval_eq_aeval_map hcomp (minpoly R x) x).symm
· exact (monic (Algebra.IsIntegral.isIntegral x)).map _
