English
If S ≤ T are submonoids of R and for each x in T there is m with m x ∈ S, localization from S to T holds; more generally, a localized map for S extends to a localization for T with suitable compatibility data.
Русский
Если S ⊆ T — подмонойды R и для каждого x ∈ T существует m такой, что m x ∈ S, то локализация от S к T существует; обобщённо, локализованная карта S распростирается до локализации T с необходимой совместимостью.
LaTeX
$$$S \\le T \\Rightarrow (\\forall x\\in T, \\exists m\\in R, m x \\in S) \\Rightarrow \\text{IsLocalizedModule } T f.$$$
Lean4
/-- If `(M', f : M ⟶ M')` satisfies universal property of localized module, there is a canonical
map `LocalizedModule S M ⟶ M'`.
-/
noncomputable def fromLocalizedModule' : LocalizedModule S M → M' := fun p =>
p.liftOn (fun x => (IsLocalizedModule.map_units f x.2).unit⁻¹.val (f x.1))
(by
rintro ⟨a, b⟩ ⟨a', b'⟩ ⟨c, eq1⟩
dsimp
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← map_smul, ← map_smul,
Module.End.algebraMap_isUnit_inv_apply_eq_iff', ← map_smul]
exact (IsLocalizedModule.eq_iff_exists S f).mpr ⟨c, eq1.symm⟩)
