subsingleton_iff — Mathlib

English

Picard group is subsingleton iff every invertible module is free.

Русский

Группа Пикарда является пододной, если каждый инвертируемый модуль свободен.

LaTeX

$$$ \\operatorname{Subsingleton}(\\mathrm{Pic}(R)) \\iff \\forall M [\\mathrm{AddCommGroup} M] [\\mathrm{Module} R M], \\; \\mathrm{Module.Invertible} R M \\rightarrow \\mathrm{Free} R M. $$$

Lean4

theorem subsingleton_iff :
    Subsingleton (Pic R) ↔ ∀ (M : Type u) [AddCommGroup M] [Module R M], Module.Invertible R M → Free R M :=
  .trans
      ⟨fun _ M _ _ _ ↦ Subsingleton.elim .., fun h ↦
        ⟨fun M N ↦ by rw [← mk_eq_self (M := M), ← mk_eq_self (M := N), h, h]⟩⟩ <|
    forall₄_congr fun _ _ _ _ ↦ mk_eq_one_iff.trans Invertible.free_iff_linearEquiv.symm

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