projective_of_localization_maximal'

English

If a family of localized modules is projectively equivalent to a fixed target, the global module is projective.

Русский

Локализованные модули эквивалентны проективному существованию над базовым кольцом.

LaTeX

$$$\\text{projective equivalence under localization implies global projectivity}$$$

Lean4

/-- A variant of `Module.projective_of_localization_maximal` that accepts `IsLocalizedModule`.
-/
theorem projective_of_localization_maximal' (H : ∀ (I : Ideal R) (_ : I.IsMaximal), Module.Projective (Rₚ I) (Mₚ I))
    [Module.FinitePresentation R M] : Module.Projective R M :=
  by
  apply Module.projective_of_localization_maximal
  intro P hP
  refine
    Module.Projective.of_ringEquiv (M := Mₚ P)
      (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
      { __ := IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)
        map_smul' := ?_ }
  · intro r m
    obtain ⟨r, s, rfl⟩ := IsLocalization.mk'_surjective P.primeCompl r
    apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap P.primeCompl M) s)).1
    dsimp
    simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul, IsLocalization.map_id_mk']

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