The Jacobson radical of a noncommutative local ring

In a Dedekind-finite local ring the nonunits form the unique maximal left ideal, hence agree with the ring Jacobson radical. Finite-dimensional algebras over a field are Dedekind-finite.

theorem MagnitudeConjecture.mulOpposite_isLocalRing {R : Type u_1} [Ring R] [IsLocalRing R] : IsLocalRing Rᵐᵒᵖ

Reversing multiplication preserves the noncommutative local-ring property.

def MagnitudeConjecture.nonunitsIdeal (R : Type u_1) [Ring R] [IsDedekindFiniteMonoid R] [IsLocalRing R] : Ideal R

The left ideal of nonunits.

@[simp]

theorem MagnitudeConjecture.mem_nonunitsIdeal_iff_not_isUnit (R : Type u_1) [Ring R] [IsDedekindFiniteMonoid R] [IsLocalRing R] (x : R) : x ∈ nonunitsIdeal R ↔ ¬IsUnit x

instance MagnitudeConjecture.nonunitsIdeal_isTwoSided (R : Type u_1) [Ring R] [IsDedekindFiniteMonoid R] [IsLocalRing R] : (nonunitsIdeal R).IsTwoSided

instance MagnitudeConjecture.nonunitsIdeal_isMaximal (R : Type u_1) [Ring R] [IsDedekindFiniteMonoid R] [IsLocalRing R] : (nonunitsIdeal R).IsMaximal

theorem MagnitudeConjecture.Ideal.IsMaximal.eq_nonunitsIdeal (R : Type u_1) [Ring R] [IsDedekindFiniteMonoid R] [IsLocalRing R] {I : Ideal R} (hI : I.IsMaximal) : I = nonunitsIdeal R

Every maximal left ideal is the ideal of nonunits.

theorem MagnitudeConjecture.ringJacobson_eq_nonunitsIdeal (R : Type u_1) [Ring R] [IsDedekindFiniteMonoid R] [IsLocalRing R] : Ring.jacobson R = nonunitsIdeal R

The ring Jacobson radical is the ideal of nonunits.

theorem MagnitudeConjecture.mem_ringJacobson_iff_not_isUnit (R : Type u_1) [Ring R] [IsDedekindFiniteMonoid R] [IsLocalRing R] (x : R) : x ∈ Ring.jacobson R ↔ ¬IsUnit x

Jacobson-radical membership is failure to be a unit.