English
Given a commutative monoid hom f : M →* N, along with data ensuring that f sends S to units, and a surjectivity-like condition and a compatibility condition, there exists a LocalizationMap S N turning f into a localization map with the required properties.
Русский
Дано гомоморфизм f: M →* N, при условии, что S отображается в единицы и прочие условия, существует LocalizationMap S N, превращающая f в отображение локализации.
LaTeX
$$$\\text{toLocalizationMap}(f,H_1,H_2,H_3) : S. LocalizationMap\\ N$.$$
Lean4
/-- Makes a localization map from a `CommMonoid` hom satisfying the characteristic predicate. -/
@[to_additive /-- Makes a localization map from an `AddCommMonoid` hom satisfying the
characteristic predicate. -/
]
def toLocalizationMap (f : M →* N) (H1 : ∀ y : S, IsUnit (f y)) (H2 : ∀ z, ∃ x : M × S, z * f x.2 = f x.1)
(H3 : ∀ x y, f x = f y → ∃ c : S, ↑c * x = ↑c * y) : Submonoid.LocalizationMap S N :=
{ f with
map_units' := H1
surj' := H2
exists_of_eq := H3 }
