forget₂_algebra_map — Mathlib

English

Duplicate statement: the forgetful functor from BialgCat to AlgCat sends a morphism f to the corresponding AlgHom obtained from the BialgHom underlying f.

Русский

Дублирующее утверждение: забывающий функтор отображает морфизм в соответствующий AlgHom через BialgHom.

LaTeX

$$$\mathrm{forget}_2^{\mathrm{Alg}}(f) = \mathrm{AlgCat}.ofHom(f.{toBialgHom})$$$

Lean4

@[simp]
theorem forget₂_algebra_map (X Y : BialgCat R) (f : X ⟶ Y) :
    (forget₂ (BialgCat R) (AlgCat R)).map f = AlgCat.ofHom f.toBialgHom :=
  rfl

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