Local rings that are not commutative

This file records basic facts about possibly noncommutative local rings. Their only idempotents are 0 and 1, and locality transfers along a ring equivalence; these facts apply to endomorphism rings in the Krull-Schmidt theorem. In characteristic two the idempotent criterion identifies the zeros of the Artin–Schreier map t ↦ t² + t, without a finiteness assumption.

Main results

• TauCeti.IsLocalRing.eq_zero_or_eq_one_of_isIdempotentElem: an idempotent of a local ring is 0 or 1.
• TauCeti.IsLocalRing.isDedekindFiniteMonoid: a local ring is Dedekind-finite.
• TauCeti.IsLocalRing.sq_add_self_eq_zero_iff: in characteristic two, t² + t = 0 exactly when t = 0 or t = 1.
• TauCeti.IsLocalRing.of_ringEquiv: a semiring equivalent to a local semiring is local.
• TauCeti.IsLocalRing.isUnit_natCast_of_not_dvd: if the prime p is not a unit, every natural number prime to p is a unit.

theorem TauCeti.IsLocalRing.eq_zero_or_eq_one_of_isIdempotentElem {R : Type u_1} [Ring R] [IsLocalRing R] {a : R} (ha : IsIdempotentElem a) : a = 0 ∨ a = 1

An idempotent of a local ring is 0 or 1. Mathlib's IsLocalRing.isUnit_or_isUnit_one_sub_self is stated over a commutative ring, so the splitting of 1 = a + (1 - a) is taken here from IsLocalRing.isUnit_or_isUnit_of_isUnit_add, which holds over any semiring.

instance TauCeti.IsLocalRing.isDedekindFiniteMonoid {R : Type u_1} [Ring R] [IsLocalRing R] : IsDedekindFiniteMonoid R

A local ring is Dedekind-finite: a left inverse is also a right inverse.

@[simp]

theorem TauCeti.IsLocalRing.sq_add_self_eq_zero_iff {R : Type u_1} [Ring R] [IsLocalRing R] [CharP R 2] (t : R) : t ^ 2 + t = 0 ↔ t = 0 ∨ t = 1

Over a local ring of characteristic two, the zeros of t ↦ t² + t are 0 and 1.

theorem TauCeti.IsLocalRing.of_ringEquiv {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [IsLocalRing R] (e : R ≃+* S) : IsLocalRing S

A semiring equivalent to a local semiring is local. Mathlib's RingEquiv.isLocalRing asks the source to be commutative, since it goes through IsLocalRing.of_surjective; transporting the defining condition on a pair of elements summing to a unit needs no commutativity.

theorem TauCeti.IsLocalRing.isUnit_natCast_of_not_dvd {R : Type u_1} [Ring R] [IsLocalRing R] {p : ℕ} (hp : Nat.Prime p) (hpR : ¬IsUnit ↑p) {m : ℕ} (hpm : ¬p ∣ m) : IsUnit ↑m

In a local ring in which the prime p is not a unit, every natural number prime to p is a unit.