English
For f: M → M linear over R, and A a commutative ring with R-structure, the characteristic polynomial of the base-changed map is the base change of the polynomial: charpoly(f.baseChange A) = charpoly(f) map (algebraMap R A).
Русский
Для линейного отображения f: M → M над R и кольца A, совместимо с R, характеристический многочлен базового перехода f.baseChange A равен отображению базового перехода многочлена f: charpoly(f.baseChange A) = charpoly(f).map (algebraMap R A).
LaTeX
$$$\operatorname{charpoly}(f.baseChange A) = \operatorname{charpoly}(f)\;\big|\;\text{map}(\mathrm{algebraMap}\; R\; A).$$$
Lean4
@[simp]
theorem charpoly_baseChange {R M} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M]
(f : M →ₗ[R] M) (A) [CommRing A] [Algebra R A] : (f.baseChange A).charpoly = f.charpoly.map (algebraMap R A) :=
by
nontriviality A
have := (algebraMap R A).domain_nontrivial
let I := Module.Free.ChooseBasisIndex R M
let b : Module.Basis I R M := Module.Free.chooseBasis R M
rw [← f.charpoly_toMatrix b, ← (f.baseChange A).charpoly_toMatrix (b.baseChange A), ← Matrix.charpoly_map]
congr 1
ext i j
simp [LinearMap.toMatrix_apply, ← Algebra.algebraMap_eq_smul_one]
