map_injective — Mathlib

English

Mapping a subalgebra S along the identity algebra homomorphism yields S itself: map id_R,A S = S.

Русский

Отображение подалгебры S по тождественному гомоморфизму дает саму S: map id_R A S = S.

LaTeX

$$$\operatorname{map}(\mathrm{AlgHom.id}\,R\,A,\,S) = S$$$

Lean4

theorem map_injective {f : A →ₐ[R] B} (hf : Function.Injective f) : Function.Injective (map f) := fun _S₁ _S₂ ih =>
  ext <| Set.ext_iff.1 <| Set.image_injective.2 hf <| Set.ext <| SetLike.ext_iff.mp ih

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