toAlgHom_injective — Mathlib

English

If the acting monoid M acts faithfully on A, then the map sending m to the corresponding AlgHom is injective: distinct m give distinct endomorphisms.

Русский

Если действие монадного множества M на A верно, то отображение m ↦ toAlgHom m инъективно: разные m дают разные эндоморфизмы.

LaTeX

$$$ \\text{Injective } (m \\mapsto toAlgHom(m)) $$$

Lean4

theorem toAlgHom_injective [FaithfulSMul M A] : Function.Injective (MulSemiringAction.toAlgHom R A : M → A →ₐ[R] A) :=
  fun _m₁ _m₂ h => eq_of_smul_eq_smul fun r => AlgHom.ext_iff.1 h r

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