localization_comap_isEmbedding — Mathlib

English

The localization-induced comap is an embedding, i.e., it is inducing and injective.

Русский

Компом локализации образует вложение: индуцирующее и инъективное.

LaTeX

$$IsEmbedding (comap (algebraMap R S)).$$

Lean4

theorem localization_comap_isEmbedding [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
    IsEmbedding (comap (algebraMap R S)) :=
  ⟨localization_comap_isInducing S M, localization_comap_injective S M⟩

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