instFreeOfSubsingleton — Mathlib

English

If Pic(R) is subsingleton, then every finite R-module M is free.

Русский

Если Pic(R) пододин, то каждый конечный R-модуль M свободен.

LaTeX

$$$ [\\operatorname{Subsingleton}(\\mathrm{Pic}(R))] \\Rightarrow \\forall M, \\; \\mathrm{Free} R M. $$$

Lean4

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 an invertible module over a (commutative) local semiring is free;
        in fact invertible modules over a semiring are Zariski-locally free.
        See [BorgerJun2024], Theorem 11.7. -/

Похожие утверждения