English
Under base change by A, the polyCharpolyAux polynomial behaves compatibly with map (MvPolynomial.map (algebraMap R A)).
Русский
При базисном переходе по A полином polyCharpolyAux совместим с отображением через MvPolynomial.map (algebraMap R A).
LaTeX
$$polyCharpolyAux (tensorProduct R A M M) (Algebra.TensorProduct.basis A b) (Algebra.TensorProduct.basis A b_m) = (polyCharpolyAux φ b b_m).map (MvPolynomial.map (algebraMap R A))$$
Lean4
theorem polyCharpolyAux_baseChange (A : Type*) [CommRing A] [Algebra R A] :
polyCharpolyAux (tensorProduct _ _ _ _ ∘ₗ φ.baseChange A) (basis A b) (basis A bₘ) =
(polyCharpolyAux φ b bₘ).map (MvPolynomial.map (algebraMap R A)) :=
by
simp only [polyCharpolyAux]
rw [← charpoly.univ_map_map _ (algebraMap R A)]
simp only [Polynomial.map_map]
congr 1
apply ringHom_ext
· intro r
simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, map_C, bind₁_C_right]
· rintro ij
simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, map_X, bind₁_X_right]
classical
rw [toMvPolynomial_comp _ (basis A (Basis.end bₘ)), ← toMvPolynomial_baseChange]
suffices
toMvPolynomial (M₂ := (Module.End A (TensorProduct R A M))) (basis A bₘ.end) (basis A bₘ).end
(tensorProduct R A M M) ij =
X ij
by rw [this, bind₁_X_right]
simp only [toMvPolynomial, Matrix.toMvPolynomial]
suffices ∀ kl, (toMatrix (basis A bₘ.end) (basis A bₘ).end) (tensorProduct R A M M) ij kl = if kl = ij then 1 else 0
by
rw [Finset.sum_eq_single ij]
· rw [this, if_pos rfl, X]
· rintro kl - H
rw [this, if_neg H, map_zero]
· grind
intro kl
rw [toMatrix_apply, tensorProduct, TensorProduct.AlgebraTensorModule.lift_apply, basis_apply,
TensorProduct.lift.tmul, coe_restrictScalars]
dsimp only [coe_mk, AddHom.coe_mk, smul_apply, baseChangeHom_apply]
rw [one_smul, Basis.baseChange_end, Basis.repr_self_apply]
