coe_algHom_injective — Mathlib

English

The coercion to the algebra-hom structure is injective from BialgHom to the algebra-hom level.

Русский

Взаимное отображение к структуре алгомоморфизмов инъективно из BialgHom в AlgHom.

LaTeX

$$$\\mathrm{Injective}((\\uparrow) : (A \\to_{R}^{\\!c} B) \\to (A \\to_{R} B))$$$

Lean4

theorem coe_algHom_injective : Function.Injective ((↑) : (A →ₐc[R] B) → A →ₐ[R] B) := fun φ₁ φ₂ H =>
  coe_fn_injective <| show ((φ₁ : A →ₐ[R] B) : A → B) = ((φ₂ : A →ₐ[R] B) : A → B) from congr_arg _ H

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