Theorems · Theorem · commutative algebra

Module.Invertible.exists_finset_free_localization

∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M],
  ∃ s, Ideal.span ↑s = ⊤ ∧ ∀ r ∈ s, Module.Free (Localization.Away r) (LocalizedModule.Away r 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.

Defined in

Mathlib.RingTheory.PicardGroup

Cited by

0 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleModule.Invertible