The nonlocal case of the semilocal semiring Picard question

Disproved

RybinAI2026.P19.nonlocal_semilocal_invertible_module_free

by Wenqian · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

invertible-modulespicard-groupssemirings

Let $R$ be a nonzero commutative semiring with finitely many maximal ideals, and assume that $R$ is not local. Is every invertible $R$ -module free? This is precisely the remaining nonlocal case of the positive semilocal Picard-group question after the local and zero-semiring cases are removed. No assumption that the maximal ideals are subtractive is made.

Preamble

import Mathlib.RingTheory.PicardGroup
import Mathlib.RingTheory.LocalRing.Basic

Formal statement

theorem RybinAI2026.P19.nonlocal_semilocal_invertible_module_free
    (R M : Type*) [CommSemiring R] [Nontrivial R] [Finite (MaximalSpectrum R)]
    [AddCommMonoid M] [Module R M] [Module.Invertible R M]
    (hlocal : ¬ IsLocalRing R) : Module.Free R M := by sorry

Source

Junyan Xu, Picard group of semi-local or finite semirings, https://mathoverflow.net/questions/511864; Rybin problem 19, https://rybindmitry.github.io/problems/19.html. This is the nonlocal restriction of the original question, not a claim established by Borger and Jun.

View graph