Characteristic of the ring of linear Maps

This file contains properties of the characteristic of the ring of linear maps. The characteristic of the ring of linear maps is determined by its base ring.

Main Results

• Module.charP_end : For a commutative semiring R and an R-module M, the characteristic of R is equal to the characteristic of the R-linear endomorphisms of M when M contains a non-torsion element x.

Notation

• R is a commutative semiring
• M is an R-module

Implementation Notes

One can also deduce similar result via charP_of_injective_ringHom and R → (M →ₗ[R] M) : r ↦ (fun (x : M) ↦ r • x). But this will require stronger condition compared to Module.charP_end.

theorem Module.charP_end {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {p : ℕ} [hchar : CharP R p] (htorsion : ∃ (x : M), Ideal.torsionOf R M x = ⊥) : CharP (M →ₗ[R] M) p

For a commutative semiring R and an R-module M, if M contains an element x that is not torsion, then the characteristic of R is equal to the characteristic of the R-linear endomorphisms of M.

instance instCharPLinearMapSubtypeMemSubringCenterId {D : Type u_1} [DivisionRing D] {p : ℕ} [CharP D p] : CharP (D →ₗ[↥(Subring.center D)] D) p

For a division ring D with center k, the ring of k-linear endomorphisms of D has the same characteristic as D

instance instExpCharLinearMapSubtypeMemSubringCenterId {D : Type u_1} [DivisionRing D] {p : ℕ} [ExpChar D p] : ExpChar (D →ₗ[↥(Subring.center D)] D) p