forget₂_coalgebra_obj — Mathlib

English

Under the forgetful functor to coalgebras, objects map to their underlying coalgebra objects.

Русский

Объекты переходят под забывающий функтор в базовые коалгебры.

LaTeX

$$$ (\mathrm{forget}_2 (\mathrm{BialgCat}\, R)\, \mathrm{toCoalgebra}) \!\! .\mathrm{obj}(X) = \mathrm{CoalgCat}.of(R, X)$$

Lean4

@[simp]
theorem forget₂_coalgebra_obj (X : BialgCat R) : (forget₂ (BialgCat R) (CoalgCat R)).obj X = CoalgCat.of R X :=
  rfl

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