freeLocus_eq_univ — Mathlib

English

If R-module M is finitely presented and flat, freeLocus(R,M) = Spec(R) iff M is projective.

Русский

Если модуль M над R конечно представлен и плосок, то свободный локус равен спектру тогда, когда M проективен.

LaTeX

$$$[Module.FinitePresentation\ R\ M] \land [Module.Flat\ R\ M] \Rightarrow (\mathrm{freeLocus}(R,M) = \mathrm{Spec}(R) \iff \mathrm{Projective}(R,M))$$$

Lean4

theorem freeLocus_eq_univ [Module.FinitePresentation R M] [Module.Flat R M] : freeLocus R M = Set.univ :=
  by
  simp_rw [Set.eq_univ_iff_forall, mem_freeLocus]
  exact fun x ↦ Module.free_of_flat_of_isLocalRing

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