LinearMap.aeval_eq_aeval_mod_charpoly
theorem LinearMap.aeval_eq_aeval_mod_charpoly :
∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M) (p : Polynomial R),
(Polynomial.aeval f) p = (Polynomial.aeval f) (p.modByMonic f.charpoly)
The theorem `LinearMap.aeval_eq_aeval_mod_charpoly` states that for any endomorphism polynomial `p` in a ring `R` and a module `M` which is both free and finite, when `p` is evaluated under a linear map `f`, it is equivalent to evaluating `p` modulo the characteristic polynomial of `f`. In other words, the polynomial `p` behaves as if its degree is less than the dimension of the module, because when it is evaluated using the endomorphism given by `f`, any terms of degree higher than the degree of the characteristic polynomial of `f` are effectively reduced modulo the characteristic polynomial of `f`.
More concisely: For any endomorphism polynomial `p` in a ring `R`, evaluating `p` under a linear map `f` over a free and finite module `M` is equivalent to evaluating `p` modulo the characteristic polynomial of `f`.
|
LinearMap.pow_eq_aeval_mod_charpoly
theorem LinearMap.pow_eq_aeval_mod_charpoly :
∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M) (k : ℕ),
f ^ k = (Polynomial.aeval f) ((Polynomial.X ^ k).modByMonic f.charpoly)
This theorem states that for any endomorphism `f` on a module `M` over a commutative ring `R`, and for any natural number `k`, the `k`-th power of `f` can be represented as the application of the algebra evaluation function `aeval` to the result of the modulo operation of the `k`-th power of the polynomial variable by the monic characteristic polynomial of `f`.
In other words, if you have an endomorphism `f` (a self-mapping on `M` that preserves the structure of `M`) and you raise it to the power `k`, this is equivalent to taking the `k`-th power of the polynomial variable, computing its remainder when divided by `f`'s characteristic polynomial (assuming the polynomial is monic), and then evaluating this polynomial at `f` using the `aeval` function. This theorem holds for all modules that are free and finite over the ring `R`.
More concisely: For any endomorphism `f` on a free and finite module `M` over a commutative ring `R`, the `k`-th power of `f` equals the application of `aeval` to the remainder of `x^k` modulo the monic characteristic polynomial of `f` in `R[x]`.
|
LinearMap.aeval_self_charpoly
theorem LinearMap.aeval_self_charpoly :
∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M), (Polynomial.aeval f) f.charpoly = 0
The theorem `LinearMap.aeval_self_charpoly` is a formalization of the well-known Cayley-Hamilton Theorem in the context of linear maps. The theorem states that for any commutative ring `R` and any `R`-module `M`, if `f` is a linear map from `M` to `M`, the characteristic polynomial of `f`, when evaluated at `f` itself, yields zero. This can be thought of as the linear map satisfying its own characteristic equation. This theorem is closely related to the equivalent statement about matrices, `Matrix.aeval_self_charpoly`.
More concisely: For any commutative ring `R` and `R`-module `M`, if `f` is a linear map from `M` to `M`, then the characteristic polynomial of `f` evaluated at `f` is zero.
|