mem_freeLocus_of_isLocalization — Mathlib

English

For a localization at prime p, the freeness of the localized module equals the membership in freeLocus.

Русский

Для локализации по p условие свободы локализованного модуля эквивалентно принадлежности к свободному локусу.

LaTeX

$$$p \in \mathrm{freeLocus}(R,M) \Leftrightarrow \mathrm{Free}(\mathrm{Localization.AtPrime}(p.asIdeal)) (\mathrm{LocalizedModule}(p.asIdeal.primeCompl M))$$$

Lean4

theorem mem_freeLocus_of_isLocalization (p : PrimeSpectrum R) (Rₚ Mₚ) [CommRing Rₚ] [Algebra R Rₚ]
    [IsLocalization.AtPrime Rₚ p.asIdeal] [AddCommGroup Mₚ] [Module R Mₚ] (f : M →ₗ[R] Mₚ)
    [IsLocalizedModule p.asIdeal.primeCompl f] [Module Rₚ Mₚ] [IsScalarTower R Rₚ Mₚ] :
    p ∈ freeLocus R M ↔ Module.Free Rₚ Mₚ :=
  by
  apply
    Module.Free.iff_of_ringEquiv
      (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv
  refine { __ := IsLocalizedModule.iso p.asIdeal.primeCompl f, map_smul' := ?_ }
  intro r x
  obtain ⟨r, s, rfl⟩ := IsLocalization.mk'_surjective p.asIdeal.primeCompl r
  apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units f s)).1
  simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe, algebraMap_end_apply,
    AlgEquiv.toRingEquiv_eq_coe, AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_coe, IsLocalization.algEquiv_apply,
    IsLocalization.map_id_mk']
  simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul]

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