Mathoverflow 486451

Reference: mathoverflow/486451 asked by user Junyan Xu

theorem 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 exists_semiring_unique_left_right_maximal_ne : (∃ (R : Type) (x : Semiring R), (∃! I : Ideal R, I.IsMaximal) ∧ (∃! J : Ideal Rᵐᵒᵖ, J.IsMaximal) ∧ ∃ (I : Ideal R) (J : Ideal Rᵐᵒᵖ), ↑I ≠ MulOpposite.op ⁻¹' ↑J) ↔ sorry

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