forget₂_coalgebra_map — Mathlib

English

The map induced by forget₂ to CoalgCat on a morphism f is the corresponding CoalgHom obtained from the BialgHom underlying f.

Русский

Образ забывающего функторa на морфизме f — это соответствующий CoalgHom, полученный из BialgHom, лежащего в основе f.

LaTeX

$$$ (\mathrm{forget}_2 (\mathrm{BialgCat}\, R) \mathrm{toCoalgebra}).map f = \mathrm{CoalgCat}.ofHom (\mathrm{CoalgHomClass}.toCoalgHom (f.toBialgHom))$$$

Lean4

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

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