Matrices of invertible finite order over a ring with a local retraction

Let R be a commutative A-algebra with an A-algebra retraction ε : R → A that is a local homomorphism, i.e. x is a unit as soon as ε x is. A typical example is a group algebra A[Q] of a finite p-group Q over a local ring A of residue characteristic p, with ε the augmentation.

If a square matrix M over R satisfies M ^ m = 1, where m is invertible in A, then M is conjugate to its constant part N, the matrix obtained by applying algebraMap A R ∘ ε to the entries of M. The intertwiner is the averaging sum T = ∑_{i < m} M ^ i * N ^ (m - 1 - i), which satisfies M * T = T * N; its image under ε is m • ε(M) ^ (m - 1), which is invertible, so T is invertible because ε is local. In particular the trace of M lies in A.

In other words, a representation over R of a cyclic group whose order is invertible in A is isomorphic to the base change along algebraMap A R of its image under ε.

Main results

• Matrix.exists_isUnit_mul_eq_mul_map_of_pow_eq_one: M is conjugate to its constant part.
• Matrix.trace_eq_algebraMap_of_pow_eq_one: the trace of M is the constant ε (trace M).
• LinearMap.trace_eq_algebraMap_of_pow_eq_one: the same for an endomorphism of a free module.
• LinearMap.trace_restrictScalars_smul_of_pow_eq_one: if moreover R is free over A, the A-trace of c • f is ε (trace f) * Tr_{R/A}(c).

theorem Matrix.exists_isUnit_mul_eq_mul_map_of_pow_eq_one {A : Type u_1} {R : Type u_2} {n : Type u_3} [CommRing A] [CommRing R] [Algebra A R] [Fintype n] [DecidableEq n] (M : Matrix n n R) (ε : R →ₐ[A] A) [IsLocalHom ε] {m : ℕ} (hm : IsUnit ↑m) (hM : M ^ m = 1) : ∃ (T : Matrix n n R), IsUnit T ∧ M * T = T * M.map (⇑(algebraMap A R) ∘ ⇑ε)

A matrix of invertible finite order is conjugate to its constant part. If ε : R → A is a local A-algebra retraction and M ^ m = 1 with m invertible in A, then M is conjugate, by an invertible matrix over R, to the matrix of constants algebraMap A R (ε (M i j)).

theorem Matrix.trace_eq_algebraMap_of_pow_eq_one {A : Type u_1} {R : Type u_2} {n : Type u_3} [CommRing A] [CommRing R] [Algebra A R] [Fintype n] [DecidableEq n] (M : Matrix n n R) (ε : R →ₐ[A] A) [IsLocalHom ε] {m : ℕ} (hm : IsUnit ↑m) (hM : M ^ m = 1) : M.trace = (algebraMap A R) (ε M.trace)

The trace of a matrix of invertible finite order is constant. If ε : R → A is a local A-algebra retraction and M ^ m = 1 with m invertible in A, then the trace of M is the image of ε (trace M) in R.

theorem LinearMap.trace_eq_algebraMap_of_pow_eq_one {A : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing A] [CommRing R] [Algebra A R] [AddCommMonoid M] [Module R M] [Module.Free R M] (f : M →ₗ[R] M) (ε : R →ₐ[A] A) [IsLocalHom ε] {m : ℕ} (hm : IsUnit ↑m) (hf : f ^ m = 1) : (trace R M) f = (algebraMap A R) (ε ((trace R M) f))

The trace of an endomorphism of invertible finite order is constant. If ε : R → A is a local A-algebra retraction and f ^ m = 1 with m invertible in A, then the trace of the endomorphism f of a free R-module is the image of ε (trace f) in R.

theorem LinearMap.trace_restrictScalars_smul_of_pow_eq_one {A : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing A] [CommRing R] [Algebra A R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Free A R] [Module A M] [IsScalarTower A R M] (f : M →ₗ[R] M) (ε : R →ₐ[A] A) [IsLocalHom ε] {m : ℕ} (hm : IsUnit ↑m) (hf : f ^ m = 1) (c : R) : (trace A M) (↑A (c • f)) = ε ((trace R M) f) * (Algebra.trace A R) c

The trace over A of a multiple of an endomorphism of invertible finite order. If R is free over A, ε : R → A is a local A-algebra retraction and f ^ m = 1 with m invertible in A, then for every c ∈ R the A-trace of c • f is ε (trace f) times the algebra trace of c.