English
If M contains a non-torsion element, then the characteristic of the endomorphism ring End_R(M) equals the characteristic of R.
Русский
Если в модуле M существует элемент без тorsion, то характеристика кольца линейных эндоморфизм End_R(M) равна характеристике R.
LaTeX
$$CharP(End_R(M)) = CharP(R)$$
Lean4
/-- For a commutative semiring `R` and a `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`. -/
theorem charP_end {p : ℕ} [hchar : CharP R p] (htorsion : ∃ x : M, Ideal.torsionOf R M x = ⊥) : CharP (M →ₗ[R] M) p
where
cast_eq_zero_iff
n :=
by
have exact : (n : M →ₗ[R] M) = (n : R) • 1 := by simp only [Nat.cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]
rw [exact, LinearMap.ext_iff, ← hchar.1]
exact
⟨fun h ↦ htorsion.casesOn fun x hx ↦ by simpa [← Ideal.mem_torsionOf_iff, hx] using h x, fun h ↦
(congrArg (fun t ↦ ∀ x, t • x = 0) h).mpr fun x ↦ zero_smul R x⟩
