English
A specialization describing how localization maps interact with modules and their induced morphisms under a domain isomorphism.
Русский
Специализация, описывающая взаимодействие локализационных отображений с модулями и индуцируемыми морфизмами при доменном изоморфизме.
LaTeX
$$$f.mulEquivOfMulEquiv_mk' (H) (x) = ...$$$
Lean4
/-- Natural homomorphism sending `x : M`, `M` a `CommMonoid`, to the equivalence class of
`(x, 1)` in the Localization of `M` at a Submonoid. -/
@[to_additive /-- Natural homomorphism sending `x : M`, `M` an `AddCommMonoid`, to the equivalence class of
`(x, 0)` in the Localization of `M` at a Submonoid. -/
]
def monoidOf : Submonoid.LocalizationMap S (Localization S) :=
{ (r S).mk'.comp <| MonoidHom.inl M S with
toFun := fun x ↦ mk x 1
map_one' := mk_one
map_mul' := fun x y ↦ by rw [mk_mul, mul_one]
map_units' := fun y ↦ isUnit_iff_exists_inv.2 ⟨mk 1 y, by rw [mk_mul, mul_one, one_mul, mk_self]⟩
surj' := fun z ↦ induction_on z fun x ↦ ⟨x, by rw [mk_mul, mul_comm x.fst, ← mk_mul, mk_self, one_mul]⟩
exists_of_eq := fun x y ↦ Iff.mp <| mk_eq_mk_iff.trans <| r_iff_exists.trans <| by simp }
