monoidHom_ext — Mathlib

English

If j and k are monoid homomorphisms from S to a monoid P and j ∘ algebraMap_R_S = k ∘ algebraMap_R_S, then j = k.

Русский

Если j и k — моноид-гомоморфизмы S→P и j ∘ algebraMap_R_S = k ∘ algebraMap_R_S, тогда j = k.

LaTeX

$$$ \\forall j,k : S \\to P,\\; j \\circ (\\mathrm{algebraMap}_{R,S}) = k \\circ (\\mathrm{algebraMap}_{R,S}) \\Rightarrow j = k. $$$

Lean4

/-- See note [partially-applied ext lemmas] -/
theorem monoidHom_ext {P : Type*} [Monoid P] ⦃j k : S →* P⦄
    (h : j.comp (algebraMap R S : R →* S) = k.comp (algebraMap R S)) : j = k :=
  (toLocalizationMap M S).epic_of_localizationMap h

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