epi' — Mathlib

English

Another formulation: for any submonoid M in a commutative ring R, the induced morphism to Localization M is epi in CommRingCat.

Русский

Еще одна формулировка: для любого подмономода M в кольце R индуцированное отображение в Localization M является эпиморфизмом в CommRingCat.

LaTeX

$$$\mathrm{Localization}.epi'\; M$$$

Lean4

instance epi' {R : CommRingCat} (M : Submonoid R) :
    @Epi CommRingCat _ R _ (CommRingCat.ofHom <| algebraMap R <| Localization M :) :=
  by
  rcases R with ⟨α, str⟩
  exact IsLocalization.epi M _

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