Mathoverflow 486451

Reference: mathoverflow/486451 asked by user Junyan Xu

theorem Mathoverflow486451.exists_semiring_unique_left_maximal_not_unique_right_maximal : ∃ (R : Type) (x : Semiring R), (∃! I : Ideal R, I.IsMaximal) ∧ ∃ (I : Ideal Rᵐᵒᵖ) (J : Ideal Rᵐᵒᵖ), I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J

There exists a semiring with a unique left maximal ideal but more than one right maximal ideals.

theorem Mathoverflow486451.exists_semiring_unique_left_right_maximal_ne : True ↔ ∃ (R : Type) (x : Semiring R) (hI : ∃! I : Ideal R, I.IsMaximal) (hJ : ∃! J : Ideal Rᵐᵒᵖ, J.IsMaximal), ↑(Exists.choose hI) ≠ MulOpposite.op ⁻¹' ↑(Exists.choose hJ)

There exists a semiring with a unique left maximal ideal and a unique right maximal ideal which are not the same as sets.

This has been shown by Goran Žužić and Moritz Firsching using an experimental pipeline: An example is the monoid algebra of the monoid of maps from $\mathbb{N}$ to $\mathbb{N}$ over $\mathbb{N}$.