freeLocus — Mathlib

English

If M is finitely presented, free locus is open in Spec R.

Русский

Если M конечно представим, свободная локализация открыта в спектре R.

LaTeX

$$$\mathrm{IsOpen}(\mathrm{freeLocus}(R,M))$$$

Lean4

/-- The free locus of a module, i.e. the set of primes `p` such that `Mₚ` is free over `Rₚ`. -/
def freeLocus : Set (PrimeSpectrum R) :=
  {p | Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M)}

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