Transposes of powers and exponentials of endomorphisms

Transposition f ↦ f.dualMap reverses composition of linear maps, so it carries the powers of a single endomorphism f to the powers of its transpose. Hence the transpose of a nilpotent endomorphism is nilpotent, and over a ℚ-algebra the transpose of its exponential is the exponential of its transpose:

(exp f)ᵀ = exp fᵀ.

This is the identity by which a unipotent automorphism exp f of a module M acts on the polynomial functions S(M*) on M.

Main results

• LinearMap.dualMap_pow: (f ^ n)ᵀ = fᵀ ^ n.
• IsNilpotent.dualMap: the transpose of a nilpotent endomorphism is nilpotent.
• LinearMap.dualMap_exp: (exp f)ᵀ = exp fᵀ for nilpotent f.

theorem LinearMap.dualMap_pow {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) (n : ℕ) : dualMap (f ^ n) = dualMap f ^ n

The transpose of a power of an endomorphism is the power of its transpose.

theorem IsNilpotent.dualMap {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {f : Module.End R M} (hf : IsNilpotent f) : IsNilpotent (LinearMap.dualMap f)

The transpose of a nilpotent endomorphism is nilpotent.

theorem LinearMap.dualMap_exp {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Algebra ℚ R] [Module ℚ M] {f : Module.End R M} (hf : IsNilpotent f) : dualMap (IsNilpotent.exp f) = IsNilpotent.exp (dualMap f)

The transpose of the exponential of a nilpotent endomorphism is the exponential of its transpose.