toBialgHom_injective — Mathlib

English

The map Hom.toBialgHom is injective: two HopfAlgCat morphisms are equal if their underlying BialgHom are equal.

Русский

Отображение Hom.toBialgHom инъективно: два морфизма в HopfAlgCat равны, если их базовые BialgHom равны.

LaTeX

$$$\forall V,W : \mathrm{HopfAlgCat R},\; \mathrm{Hom}_{HopfAlgCat}(V,W) \to \mathrm{BialgHom}_{R}(V.carrier,W.carrier)$ является инъективным$$

Lean4

theorem toBialgHom_injective (V W : HopfAlgCat.{v} R) : Function.Injective (Hom.toBialgHom : Hom V W → _) :=
  fun ⟨f⟩ ⟨g⟩ _ => by congr

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