English
Let A be a commutative ring with an R-algebra structure, and φ a linear map L → End_R(M). Then the characteristic polynomial after base change to A with basis b in L corresponds to applying the map that sends coefficients via algebraMap R A to the polynomial polyCharpoly φ b.
Русский
Пусть A — коммутативное кольцо с структурой алгебры над R, и пусть φ: L → End_R(M) — линейное отображение. Тогда характеристический полином после базового перехода к A с базисом b в L соответствует применению отображения полиномов, переводящего коэффициенты через алгебраическое отображение R → A к polyCharpoly φ b.
LaTeX
$$$\polyCharpoly (tensorProduct _ _ _ _ \circ_ᵥ φ.\text{baseChange } A) (\text{basis } A b) = (\polyCharpoly φ b).map (MvPolynomial.map (\text{algebraMap } R A))$$$
Lean4
theorem polyCharpoly_baseChange (A : Type*) [CommRing A] [Algebra R A] :
polyCharpoly (tensorProduct _ _ _ _ ∘ₗ φ.baseChange A) (basis A b) =
(polyCharpoly φ b).map (MvPolynomial.map (algebraMap R A)) :=
by
unfold polyCharpoly
rw [← φ.polyCharpolyAux_baseChange]
apply polyCharpolyAux_basisIndep
