Polynomials in intertwined endomorphisms

A (semi)linear map f intertwining two endomorphisms g and g₂ intertwines every polynomial in them: polynomial evaluation at g₂ after f agrees with f after evaluation at g, with the coefficients transported along the ring homomorphism of f. This extends Mathlib's Module.End.commute_pow_left_of_commute from powers to polynomials, and generalizes Polynomial.aeval_comp_eq_comp_aeval from linear to semilinear maps.

Consequently a linear map intertwining two endomorphisms with coprime minimal polynomials is zero (Module.End.eq_zero_of_comp_eq_of_isCoprime_minpoly): the minimal polynomial of the source endomorphism kills it, while evaluated at the target endomorphism it is invertible.

theorem Module.End.aeval_map_comp_of_comp_eq {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] {R₂ : Type u_4} [CommSemiring R₂] [Module R₂ M₂] {σ : R →+* R₂} {f : M →ₛₗ[σ] M₂} {g : End R M} {g₂ : End R₂ M₂} (h : g₂ ∘ₛₗ f = f ∘ₛₗ g) (p : Polynomial R) : (Polynomial.aeval g₂) (Polynomial.map σ p) ∘ₛₗ f = f ∘ₛₗ (Polynomial.aeval g) p

A semilinear map intertwining two endomorphisms intertwines every polynomial in them, with coefficients transported along the ring homomorphism.

theorem Module.End.eq_zero_of_comp_eq_of_isCoprime_minpoly {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {f : M →ₗ[R] M₂} {g : End R M} {g₂ : End R M₂} (h : g₂ ∘ₗ f = f ∘ₗ g) (hc : IsCoprime (minpoly R g) (minpoly R g₂)) : f = 0

A linear map intertwining two endomorphisms with coprime minimal polynomials is zero.