mem_freeLocus_iff_tensor — Mathlib

English

The freeness of the tensor product M over R_p with R_p equals freeness of the localization M_p.

Русский

Свобода модуля в тензорном произведении равна свободности локализации модуля.

LaTeX

$$$p \in \mathrm{freeLocus}(R,M) \iff \mathrm{Free}(R_p, (R_p \otimes_R M))$$$

Lean4

theorem mem_freeLocus_iff_tensor (p : PrimeSpectrum R) (Rₚ) [CommRing Rₚ] [Algebra R Rₚ]
    [IsLocalization.AtPrime Rₚ p.asIdeal] : p ∈ freeLocus R M ↔ Module.Free Rₚ (Rₚ ⊗[R] M) :=
  by
  have := (isLocalizedModule_iff_isBaseChange p.asIdeal.primeCompl _ _).mpr (TensorProduct.isBaseChange R M Rₚ)
  exact mem_freeLocus_of_isLocalization p Rₚ (f := TensorProduct.mk R Rₚ M 1)

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