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)