English
A second variant of polyCharpolyAux_map_aeval asserts the same compatibility for a different base-change setup.
Русский
Второй вариант polyCharpolyAux_map_aeval утверждает ту же совместимость для иного базисного перехода.
LaTeX
$$ polyCharpolyAux_map_aeval ...$$
Lean4
/-- `LinearMap.polyCharpolyAux` is independent of the choice of basis of the target module.
Proof strategy:
1. Rewrite `polyCharpolyAux` as the (honest, ordinary) characteristic polynomial
of the basechange of `φ` to the multivariate polynomial ring `MvPolynomial ι R`.
2. Use that the characteristic polynomial of a linear map is independent of the choice of basis.
This independence result is used transitively via
`LinearMap.polyCharpolyAux_map_aeval` and `LinearMap.polyCharpolyAux_map_eq_charpoly`. -/
theorem polyCharpolyAux_basisIndep {ιM' : Type*} [Fintype ιM'] [DecidableEq ιM'] (bₘ' : Basis ιM' R M) :
polyCharpolyAux φ b bₘ = polyCharpolyAux φ b bₘ' :=
by
let f : Polynomial (MvPolynomial ι R) → Polynomial (MvPolynomial ι R) :=
Polynomial.map (MvPolynomial.aeval X).toRingHom
have hf : Function.Injective f :=
by
simp only [f, aeval_X_left, AlgHom.toRingHom_eq_coe, AlgHom.id_toRingHom]
exact Polynomial.map_injective (RingHom.id _) Function.injective_id
apply hf
let _h1 : Module.Finite (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) :=
Module.Finite.of_basis (basis (MvPolynomial ι R) bₘ)
let _h2 : Module.Free (MvPolynomial ι R) (TensorProduct R (MvPolynomial ι R) M) :=
Module.Free.of_basis (basis (MvPolynomial ι R) bₘ)
simp only [f, polyCharpolyAux_map_aeval, polyCharpolyAux_map_aeval]
