Köthe conjecture

Reference: Wikipedia

def Koethe.IsNil {R : Type u_1} [Ring R] {S : Type u_2} [SetLike S R] (I : S) : Prop

Say a subset I of a ring R is nilpotent if all its elements are nilpotent.

Equations

• Koethe.IsNil I = ∀ i ∈ I, IsNilpotent i

def Koethe.KotheRadical (R : Type u_1) [Ring R] : TwoSidedIdeal R

The Kothe Radical of a ring R is the sum of all (two-sided) nil ideals of R. Tags: Kothe Radical, upper nilradical

Equations

• Koethe.KotheRadical R = sSup {I : TwoSidedIdeal R | Koethe.IsNil I}

theorem Koethe.KotheConjecture {R : Type u_1} [Ring R] (I J : Ideal R) (hI : IsNil I) (hJ : IsNil J) : IsNil (I + J)

The Köthe conjecture: In any ring, the sum of two nil left ideals is nil.

theorem Koethe.KotherConjecture.variants.le_KotherRadical {R : Type u_1} [Ring R] {I : Ideal R} (hI : IsNil I) : ↑I ⊆ ↑(KotheRadical R)

The Köthe conjecture: every left nil radical is contained in the Köthe radical.

theorem Koethe.KotherConjecture.variants.general_matrix {R : Type u_1} [Ring R] {I : TwoSidedIdeal R} (hI : IsNil I) (n : Type u_2) [Fintype n] : IsNil (TwoSidedIdeal.matricesOver n I)

The Köthe conjecture: for any nil ideal I of R, the matrix ideal M_n(I) is a nil ideal of the matrix ring M_n(R).

theorem Koethe.KotherConjecture.variants.two_by_two_matrix {R : Type u_1} [Ring R] {I : TwoSidedIdeal R} (hI : IsNil I) : IsNil (TwoSidedIdeal.matricesOver (Fin 2) I)

The Köthe conjecture: for any nil ideal I of R, the matrix ideal M_2(I) is a nil ideal of the matrix ring M_2(R).

theorem Koethe.KotherConjecture.variants.matrixOver_KotherRadical {R : Type u_1} [Ring R] {I : TwoSidedIdeal R} (hI : IsNil I) (n : Type u_2) [Fintype n] : TwoSidedIdeal.matricesOver n (KotheRadical R) = KotheRadical (Matrix n n R)

The Köthe conjecture: for any positive integer n, the Köthe radical of R is the matrix ideal M_2(Nil*(R)).

theorem Koethe.amitsur_conjecture {R : Type u_1} [Ring R] (J : TwoSidedIdeal R) (hJ : IsNil J) : IsNil (TwoSidedIdeal.map Polynomial.C J)

The Amitsur Conjecture: If J is a nil ideal in R, then J[x] is a nil ideal of the polynomial ring R[x]. This is known to be false, see Agata Smoktunowicz, Polynomial rings over nil rings need not be nil.