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

• CharP_if : For a commutative semiring R and a R-module M, the characteristic of R is equal to the characteristic of the R-linear endomorphisms of M when M contains an element x such that r • x = 0 implies r = 0.

Notations

• R is a commutative semiring
• M is a 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 CharP_if.

theorem Module.charP_end {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {p : ℕ} [hchar : CharP R p] (hreduction : ∃ (x : M), ∀ (r : R), r • x = 0 → r = 0) : CharP (M →ₗ[R] M) p

For a commutative semiring R and a R-module M, if M contains an element x such that r • x = 0 implies r = 0 (finding such element usually depends on specific •), 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