isLocalization_algebraMapSubmonoid_map_algHom

English

An induced localization map on algebras exists: an algebra map A → B yields a localized algebra map A_p → B_p between the corresponding localizations.

Русский

Существует индуцированное отображение локализации на алгебрах: алгебраическое отображение $A \\to B$ порождает локализованное отображение $A_p \\to B_p$ между локализациями.

LaTeX

$$$\\map\\_\\mathsf{A}: A_p \\to_{R_p} B_p \quad (\\text{induced by } f: A \\to B)$$$

Lean4

instance isLocalization_algebraMapSubmonoid_map_algHom (f : A →ₐ[R] B) :
    IsLocalization ((algebraMapSubmonoid A M).map f.toRingHom) Bₚ :=
  by
  rw [AlgHom.toRingHom_eq_coe, ← Submonoid.map_coe_toMonoidHom, AlgHom.toRingHom_toMonoidHom,
    Submonoid.map_coe_toMonoidHom, algebraMapSubmonoid_map_eq M f]
  infer_instance

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