freeLocus_eq_univ_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem freeLocus_eq_univ_iff [Module.FinitePresentation R M] : freeLocus R M = Set.univ ↔ Module.Projective R M :=
  by
  simp_rw [Set.eq_univ_iff_forall, mem_freeLocus]
  exact
    ⟨fun H ↦
      Module.projective_of_localization_maximal fun I hI ↦
        have := H ⟨I, hI.isPrime⟩;
        .of_free,
      fun H x ↦ Module.free_of_flat_of_isLocalRing⟩

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