English
There is a canonical map from LocalizedModule S M to M' given by p ↦ IsLocalizedModule.map_units f p.2 etc., capturing the universal property of localization.
Русский
Существует каноничное отображение из LocalizedModule S M в M' заданное через маппинг единиц и сопоставления, отражающее универсальное свойство локализации.
LaTeX
$$$\\mathrm{fromLocalizedModule'}: \\mathrm{LocalizedModule}(S,M) \\to M'\\text{ with } p \\mapsto (\\mathrm{IsLocalizedModule.map_units}\\ f\\ p.2).unit^{-1}.(f(p.1)).$$$
Lean4
theorem of_exists_mul_mem {N : Type*} [AddCommMonoid N] [Module R N] (S T : Submonoid R) (h : S ≤ T)
(h' : ∀ x : T, ∃ m : R, m * x ∈ S) (f : M →ₗ[R] N) [IsLocalizedModule S f] : IsLocalizedModule T f
where
map_units
x := by
obtain ⟨m, mx⟩ := h' x
have := IsLocalizedModule.map_units f ⟨_, mx⟩
rw [map_mul, (Algebra.commute_algebraMap_left _ _).isUnit_mul_iff] at this
exact this.2
surj
y := by
obtain ⟨⟨x, t⟩, e⟩ := IsLocalizedModule.surj S f y
exact ⟨⟨x, ⟨t, h t.2⟩⟩, e⟩
exists_of_eq {x₁ x₂}
e := by
obtain ⟨c, hc⟩ := IsLocalizedModule.exists_of_eq (S := S) (f := f) e
exact ⟨⟨c, h c.2⟩, hc⟩
