The reversed characteristic polynomial on a finite projective module

For an endomorphism f of a finite projective module M over a commutative ring R, this file defines the reversed characteristic polynomial

LinearMap.projectiveCharpolyRev f = det (1 - X f) ∈ R[X],

the determinant LinearMap.projectiveDet of 1 - X f on R[X] ⊗[R] M. On a free module of finite rank it is the reverse of LinearMap.charpoly f. Its constant coefficient is 1, while its degree is only bounded by the ranks of M at the points of Spec R, which need not be constant. For the same reason det (X - f) need not be monic, and the reversed form is the one used here.

If π : R ^ n → M and σ : M → R ^ n split M off a free module, then projectiveCharpolyRev f is the reversed characteristic polynomial of the matrix of σ ∘ f ∘ π (LinearMap.projectiveCharpolyRev_eq_charpolyRev_toMatrix). Through this description:

• its value at 1 is the determinant of 1 - f (LinearMap.eval_one_projectiveCharpolyRev);
• it commutes with base change (LinearMap.projectiveCharpolyRev_baseChange);
• its degree is at most any bound for the ranks of M at the points of Spec R (LinearMap.natDegree_projectiveCharpolyRev_le); on a free module its coefficient in degree finrank R M is (-1) ^ finrank R M * det f, so the degree is the rank exactly when det f ≠ 0, in particular when f is invertible (LinearMap.natDegree_projectiveCharpolyRev_eq_finrank_iff);
• it is transported along semilinear isomorphisms (LinearMap.projectiveCharpolyRev_eq_map_of_comp_eq);
• Cayley–Hamilton: for some n bounding its degree, the reflection X ^ n · Q(1/X) of Q = projectiveCharpolyRev f is a monic polynomial killing f (LinearMap.exists_aeval_reflect_projectiveCharpolyRev_eq_zero, LinearMap.monic_reflect_projectiveCharpolyRev).

The last statement turns a norm into an integral equation: an element of a finite projective R-algebra is a root of a monic polynomial whose coefficients are those of the reversed characteristic polynomial of multiplication by it. This is how integrality over rings of invariants is proved for finite locally free group actions and equivalence relations.

Main definitions

• LinearMap.projectiveCharpolyRev: the reversed characteristic polynomial det (1 - X f).

References

• O. Goldman, Determinants in projective modules, Nagoya Math. J. 18 (1961), 27–36.
• The Stacks Project, Tag 03BK.

noncomputable def LinearMap.projectiveCharpolyRev {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (f : Module.End R M) : Polynomial R

The reversed characteristic polynomial det (1 - X f) of an endomorphism f of a finite projective module: the determinant LinearMap.projectiveDet of 1 - X f on R[X] ⊗[R] M. On a free module of finite rank it is the reverse of LinearMap.charpoly f (projectiveCharpolyRev_eq_reverse_charpoly).

theorem LinearMap.projectiveCharpolyRev_def {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (f : Module.End R M) : projectiveCharpolyRev f = projectiveDet (1 - Polynomial.X • baseChange (Polynomial R) f)

The reversed characteristic polynomial is the determinant LinearMap.projectiveDet of 1 - X f on R[X] ⊗[R] M.

theorem LinearMap.projectiveCharpolyRev_eq_charpolyRev_toMatrix {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {ι : Type u_3} {F : Type u_4} [Fintype ι] [DecidableEq ι] [AddCommGroup F] [Module R F] (b : Module.Basis ι R F) (π : F →ₗ[R] M) (σ : M →ₗ[R] F) (h : π ∘ₗ σ = id) (f : Module.End R M) : projectiveCharpolyRev f = ((toMatrix b b) (σ ∘ₗ f ∘ₗ π)).charpolyRev

If π : F → M and σ : M → F split M off a free module F with basis b, the reversed characteristic polynomial of f is that of the matrix of σ ∘ f ∘ π in b.

theorem LinearMap.projectiveCharpolyRev_eq_charpolyRev {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) (f : Module.End R M) : projectiveCharpolyRev f = ((toMatrix b b) f).charpolyRev

If M has a finite basis b, the reversed characteristic polynomial of f is that of its matrix in b.

theorem LinearMap.projectiveCharpolyRev_eq_reverse_charpoly {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Module.Free R M] (f : Module.End R M) : projectiveCharpolyRev f = (charpoly f).reverse

On a free module of finite rank, the reversed characteristic polynomial is the reverse of the characteristic polynomial.

@[simp]

theorem LinearMap.coeff_projectiveCharpolyRev_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (f : Module.End R M) : (projectiveCharpolyRev f).coeff 0 = 1

The constant coefficient of the reversed characteristic polynomial is 1.

@[simp]

theorem LinearMap.eval_one_projectiveCharpolyRev {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (f : Module.End R M) : Polynomial.eval 1 (projectiveCharpolyRev f) = projectiveDet (1 - f)

The value at 1 of the reversed characteristic polynomial det (1 - X f) is the determinant of 1 - f.

@[simp]

theorem LinearMap.projectiveCharpolyRev_baseChange {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (A : Type u_3) [CommRing A] [Algebra R A] (f : Module.End R M) : (baseChange A f).projectiveCharpolyRev = Polynomial.map (algebraMap R A) (projectiveCharpolyRev f)

The reversed characteristic polynomial commutes with base change.

theorem LinearMap.natDegree_projectiveCharpolyRev_le {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {n : ℕ} (hn : ∀ (p : PrimeSpectrum R), Module.rankAtStalk M p ≤ n) (f : Module.End R M) : (projectiveCharpolyRev f).natDegree ≤ n

The degree of the reversed characteristic polynomial is at most any bound for the ranks of M at the points of Spec R.

theorem LinearMap.coeff_projectiveCharpolyRev_finrank {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Module.Free R M] (f : Module.End R M) : (projectiveCharpolyRev f).coeff (Module.finrank R M) = (-1) ^ Module.finrank R M * LinearMap.det f

On a free module, the coefficient of det (1 - X f) in degree finrank R M is (-1) ^ finrank R M times the determinant of f.

theorem LinearMap.natDegree_projectiveCharpolyRev_le_finrank {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Module.Free R M] (f : Module.End R M) : (projectiveCharpolyRev f).natDegree ≤ Module.finrank R M

On a free module, the degree of det (1 - X f) is at most the rank.

theorem LinearMap.natDegree_projectiveCharpolyRev_eq_finrank_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Nontrivial R] [Module.Free R M] (f : Module.End R M) : (projectiveCharpolyRev f).natDegree = Module.finrank R M ↔ LinearMap.det f ≠ 0

On a free module over a nontrivial ring, the degree of det (1 - X f) equals the rank exactly when the determinant of f is nonzero.

theorem LinearMap.natDegree_projectiveCharpolyRev_eq_finrank_of_isUnit {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] [Nontrivial R] [Module.Free R M] {f : Module.End R M} (hf : IsUnit f) : (projectiveCharpolyRev f).natDegree = Module.finrank R M

On a free module over a nontrivial ring, the degree of det (1 - X f) is the rank when f is invertible.

theorem LinearMap.projectiveCharpolyRev_eq_map_of_comp_eq {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] {R' : Type u_3} {M' : Type u_4} [CommRing R'] [AddCommGroup M'] [Module R' M'] [Module.Finite R' M'] [Module.Projective R' M'] {θ : R →+* R'} {θ' : R' →+* R} [RingHomInvPair θ θ'] [RingHomInvPair θ' θ] (e : M ≃ₛₗ[θ] M') {f : Module.End R M} {g : Module.End R' M'} (hfg : ∀ (x : M), g (e x) = e (f x)) : projectiveCharpolyRev g = Polynomial.map θ (projectiveCharpolyRev f)

Transport along a semilinear isomorphism. If a θ-semilinear isomorphism e : M ≃ M' over a ring isomorphism θ : R ≃ R' carries f to g, that is g ∘ e = e ∘ f, then the reversed characteristic polynomial of g is that of f with θ applied to its coefficients.

theorem LinearMap.exists_aeval_reflect_projectiveCharpolyRev_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (f : Module.End R M) : ∃ (n : ℕ), (projectiveCharpolyRev f).natDegree ≤ n ∧ (Polynomial.aeval f) (Polynomial.reflect n (projectiveCharpolyRev f)) = 0

Cayley–Hamilton on a finite projective module. For some n bounding the degree of the reversed characteristic polynomial Q of f, the reflection X ^ n · Q(1/X) of Q kills f; it is monic (monic_reflect_projectiveCharpolyRev).

theorem LinearMap.monic_reflect_projectiveCharpolyRev {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (f : Module.End R M) {n : ℕ} (hn : (projectiveCharpolyRev f).natDegree ≤ n) : (Polynomial.reflect n (projectiveCharpolyRev f)).Monic

The reflection X ^ n · Q(1/X) of the reversed characteristic polynomial Q of f is monic whenever n bounds the degree of Q.