feat(RingTheory/PicardGroup): invertible modules over semirings are locally free (leanprover-community#41528)

Theorem 10.7 in *Facets of module theory over semirings* (Borger & Jun, https://arxiv.org/abs/2405.18645, Adv Math). Aristotle [discovered](https://aristotle.harmonic.fun/dashboard/requests/3e3dc70f-a9aa-4b84-a6fd-a812851c3bfb) a simpler proof using `Invertible.bijective_of_surjective` available in Mathlib. (The task started at 01:37 AM and Aristotle found the proof at 01:46 AM.)

Also generalizes lemmas and adds a new def about local semirings.

Co-authored-by: Aristotle (Harmonic) [aristotle-harmonic@harmonic.fun](mailto:aristotle-harmonic@harmonic.fun)

Author: alreadydone

Mathlib/RingTheory/LocalRing/Basic.lean

@@ -36,6 +36,27 @@ theorem of_nonunits_add [Nontrivial R]
   isUnit_or_isUnit_of_add_one {a b} hab :=
     or_iff_not_and_not.2 fun H => h a b H.1 H.2 <| hab.symm ▸ isUnit_one
 
+variable [IsLocalRing R]
+
+theorem isUnit_or_isUnit_of_isUnit_add {a b : R} (h : IsUnit (a + b)) : IsUnit a ∨ IsUnit b := by
+  rcases h with ⟨u, hu⟩
+  rw [← Units.inv_mul_eq_one, mul_add] at hu
+  apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu) <;> exact (u⁻¹.isUnit_units_mul _).mp
+
+theorem nonunits_add {a b : R} (ha : a ∈ nonunits R) (hb : b ∈ nonunits R) : a + b ∈ nonunits R :=
+  fun H ↦ not_or_intro ha hb (isUnit_or_isUnit_of_isUnit_add H)
+
+variable (R) in
+/-- The nonunits of a local semiring form an additive submonoid. -/
+@[expose] def nonunitsAddSubmonoid : AddSubmonoid R where
+  carrier := nonunits R
+  zero_mem' := by simp
+  add_mem' := nonunits_add
+
+theorem exists_of_isUnit_sum {ι : Type*} {s : Finset ι} {f : ι → R}
+    (h : IsUnit (∑ i ∈ s, f i)) : ∃ i ∈ s, IsUnit (f i) := by
+  contrapose! h; exact (nonunitsAddSubmonoid R).sum_mem h
+
 end Semiring
 
 section CommSemiring
@@ -66,16 +87,6 @@ theorem of_unique_nonzero_prime (h : ∃! P : Ideal R, P ≠ ⊥ ∧ Ideal.IsPri
       · rintro rfl
         exact hPnot_top (hM.1.2 P (bot_lt_iff_ne_bot.2 hPnonzero)))
 
-variable [IsLocalRing R]
-
-theorem isUnit_or_isUnit_of_isUnit_add {a b : R} (h : IsUnit (a + b)) : IsUnit a ∨ IsUnit b := by
-  rcases h with ⟨u, hu⟩
-  rw [← Units.inv_mul_eq_one, mul_add] at hu
-  apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu) <;> exact isUnit_of_mul_isUnit_right
-
-theorem nonunits_add {a b : R} (ha : a ∈ nonunits R) (hb : b ∈ nonunits R) : a + b ∈ nonunits R :=
-  fun H => not_or_intro ha hb (isUnit_or_isUnit_of_isUnit_add H)
-
 end CommSemiring
 
 section Ring

Mathlib/RingTheory/LocalRing/MaximalIdeal/Defs.lean

@@ -28,9 +28,7 @@ variable (R : Type*) [CommSemiring R] [IsLocalRing R]
 
 /-- The ideal of elements that are not units. -/
 def maximalIdeal : Ideal R where
-  carrier := nonunits R
-  zero_mem' := zero_mem_nonunits.2 <| zero_ne_one
-  add_mem' {_ _} hx hy := nonunits_add hx hy
+  __ := nonunitsAddSubmonoid R
   smul_mem' _ _ := mul_mem_nonunits_right
 
 end IsLocalRing

Mathlib/RingTheory/PicardGroup.lean

@@ -367,6 +367,35 @@ instance (L) [AddCommMonoid L] [Module R L] [Module A L] [IsScalarTower R A L]
     [Module.Invertible A L] : Module.Invertible A (L ⊗[R] M) :=
   .congr (AlgebraTensorModule.cancelBaseChange R A A L M)
 
+/-- An invertible module over a commutative semiring is Zariski-locally free of rank 1.
+Theorem 10.7 in [BorgerJun2024].
+
+More precisely, there is a finite set of elements of `R` that generate the unit ideal,
+and localizing `M` at any one of them yields a free module.
+
+Finite projective modules over a local commutative semiring may not be free,
+see Remark 7.10, Example 9.6 and 9.8. -/
+theorem exists_finset_free_localization :
+    ∃ s : Finset R, Ideal.span (s : Set R) = ⊤ ∧
+      ∀ r ∈ s, Free (Localization.Away r) (LocalizedModule.Away r M) := by
+  classical
+  -- write 1 = ∑ᵢ fᵢ(mᵢ) with `mᵢ : M` and `fᵢ : Dual R M`
+  obtain ⟨S, hS⟩ := ((linearEquiv R M).symm 1).exists_finset
+  refine ⟨S.image fun i ↦ i.1 i.2, ?_, fun r hr ↦ ?_⟩
+  -- Part 1: The evaluations fᵢ(mᵢ) generate the unit ideal
+  · simpa [Ideal.eq_top_iff_one, (LinearEquiv.symm_apply_eq _).mp hS, linearEquiv]
+      using Ideal.sum_mem _ fun i hi ↦ Ideal.subset_span (Finset.mem_image_of_mem _ hi)
+  -- Part 2: After localizing at any f(m), the module becomes free
+  obtain ⟨⟨f, m⟩, _, rfl⟩ := Finset.mem_image.mp hr
+  -- Extend f to a R_{f(m)}-linear functional f' on the localized module
+  let f' : Dual (Localization.Away (f m)) (LocalizedModule.Away (f m) M) :=
+    .extendScalarsOfIsLocalization (.powers (f m)) _ <| IsLocalizedModule.map
+      (.powers (f m)) (LocalizedModule.mkLinearMap _ M) (Algebra.linearMap R _) f
+  -- f'(m/1) = f(m)/1 is a unit in R_{f(m)}, so f' is surjective and therefore bijective
+  have surj : Function.Surjective f' := LinearMap.range_eq_top.mp <| Ideal.eq_top_of_isUnit_mem
+    _ ⟨_, IsLocalizedModule.map_apply ..⟩ (IsLocalization.Away.algebraMap_isUnit (f m))
+  exact .of_equiv <| .symm <| .ofBijective f' (bijective_of_surjective surj)
+
 end CommSemiring
 
 end Algebra
@@ -404,8 +433,7 @@ open CommRing (Pic)
 
 noncomputable instance : CommGroup (Pic R) := fast_instance% (equivShrink _).symm.commGroup
 
-variable (M N : Type*) [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
-  [Module.Invertible R M] [Module.Invertible R N]
+variable [Module.Invertible R M] [Module.Invertible R N]
 
 instance : Module.Invertible R (Finite.reprₛ R M) := .congr (Finite.reprEquivₛ R M).symm
 
@@ -503,11 +531,14 @@ instance [Subsingleton (Pic R)] : Free R M :=
   have := subsingleton_iffₛ.mp ‹_› (Finite.reprₛ R M) inferInstance
   .of_equiv (Finite.reprEquivₛ R M)
 
-/- TODO: it's still true that the Picard group of a (commutative) local semiring is trivial;
-in fact invertible modules over a semiring are Zariski-locally free (but projective module may
-not be). See Remark 7.10, Example 9.6 and 9.8, and Theorem 11.7 in [BorgerJun2024]. -/
-instance (R) [CommRing R] [IsLocalRing R] : Subsingleton (Pic R) :=
-  subsingleton_iff.mpr fun _ _ _ _ ↦ free_of_flat_of_isLocalRing
+/-- The Picard group of a local semiring is trivial. -/
+instance [IsLocalRing R] : Subsingleton (Pic R) := subsingleton_iffₛ.mpr fun M _ _ _ ↦ by
+  obtain ⟨S, hS⟩ := ((Invertible.linearEquiv R M).symm 1).exists_finset
+  replace hS : 1 = ∑ i ∈ S, i.1 i.2 := by
+    simpa [LinearEquiv.symm_apply_eq, Invertible.linearEquiv] using hS
+  obtain ⟨⟨f, m⟩, mem, hfm⟩ := IsLocalRing.exists_of_isUnit_sum (hS ▸ isUnit_one)
+  exact .of_equiv <| .symm <| .ofBijective f (Invertible.bijective_of_surjective <|
+    LinearMap.range_eq_top.mp <| Ideal.eq_top_of_isUnit_mem _ ⟨m, rfl⟩ hfm)
 
 /-- The Picard group of a semilocal ring is trivial. -/
 instance (R) [CommRing R] [Finite (MaximalSpectrum R)] : Subsingleton (Pic R) :=
@@ -592,18 +623,15 @@ end PicardGroup
 
 namespace Module.Invertible
 
-variable (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] [Module.Invertible R M]
+variable [Module.Invertible R M]
 
-set_option backward.defeqAttrib.useBackward true in
--- TODO: generalize to CommSemiring by generalizing `CommRing.Pic.instSubsingletonOfIsLocalRing`
 theorem tensorProductComm_eq_refl : TensorProduct.comm R M M = .refl .. := by
   let f (P : Ideal R) [P.IsMaximal] := LocalizedModule.mkLinearMap P.primeCompl M
   let ff (P : Ideal R) [P.IsMaximal] := TensorProduct.map (f P) (f P)
   refine LinearEquiv.toLinearMap_injective <| LinearMap.eq_of_localization_maximal _ ff _ ff _ _
     fun P _ ↦ .trans (b := (TensorProduct.comm ..).toLinearMap) ?_ ?_
   · apply IsLocalizedModule.linearMap_ext P.primeCompl (ff P) (ff P)
-    ext; dsimp
-    apply IsLocalizedModule.map_apply
+    ext; exact IsLocalizedModule.map_apply _ (ff P) ..
   let Rp := Localization P.primeCompl
   have ⟨e⟩ := free_iff_linearEquiv.mp (inferInstance : Free Rp (LocalizedModule P.primeCompl M))
   have e := e.restrictScalars R