hasForgetToAlgebra — Mathlib

English

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

Русский

Функтор забывания из BialgCat в AlgCat отображает морфизм f в соответствующий AlgHom, получаемый из базового BialgHom для f.

LaTeX

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

Lean4

instance hasForgetToAlgebra : HasForget₂ (BialgCat R) (AlgCat R) where
  forget₂ :=
    { obj := fun X => AlgCat.of R X
      map := fun {X Y} f => AlgCat.ofHom f.toBialgHom }

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