LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul
theorem LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul :
∀ {M : Type u_2} [inst : AddCommGroup M] (R : Type u_3) [inst_1 : CommRing R] [inst_2 : Module R M]
[inst_3 : Module.Finite R M] (f : Module.End R M) (I : Ideal R),
LinearMap.range f ≤ I • ⊤ →
∃ p, p.Monic ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (Polynomial.aeval f) p = 0
The **Cayley-Hamilton Theorem** for finitely generated modules over arbitrary rings states that given a ring `R`, a module `M` over `R`, an `R`-endomorphism `φ` (a linear transformation from `M` to `M`), and an ideal `I` of `R` such that the range of `φ` is contained within the space spanned by `I` and `M`, there exists a monic polynomial `p` whose coefficients are in the powers of `I`, and the evaluation of `p` at `φ` equals zero. In other words, `φ` satisfies its characteristic polynomial. This version of the theorem is a generalization suitable for modules, compared to the common version for square matrices, and is referenced from Eisenbud 4.3. The theorem does not provide constraints on the degree of the polynomial `p`.
More concisely: Given a ring `R`, a finitely generated `R`-module `M`, an `R`-endomorphism `φ` of `M` with range in the submodule `IM ⊎ M`, there exists a monic polynomial `p` in `R[X]` such that `p(φ) = 0`.
|
Matrix.Represents.eq
theorem Matrix.Represents.eq :
∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
[inst_3 : Module R M] {b : ι → M},
Submodule.span R (Set.range b) = ⊤ →
∀ [inst_4 : DecidableEq ι] {A : Matrix ι ι R} {f f' : Module.End R M},
Matrix.Represents b A f → Matrix.Represents b A f' → f = f'
This theorem states that for any finite type `ι`, an additive commutative group `M`, a commutative ring `R`, and a module `M` over `R`, given a function `b` from `ι` to `M` such that the span of the range of `b` is the entire module `M`, and given a decidable equality on `ι`, if we have a matrix `A` and two endomorphisms `f` and `f'` of the module `M` such that the matrix `A` represents both `f` and `f'` with respect to the basis `b`, then `f` and `f'` must be equal. In other words, the representation of an endomorphism by a matrix with respect to a basis is unique.
More concisely: Given a finite type `ι`, an additive commutative group `M`, a commutative ring `R`, and an `R`-module `M` with basis `b` such that the span of `b` is `M` and decidable equality, if matrices `A` represent both endomorphisms `f` and `f'` of `M` with respect to `b`, then `f = f'`.
|