forget₂_obj — Mathlib

English

The forgetful functor sends an object X in CoalgCat R to the corresponding Module object, i.e., forget₂.obj X = ModuleCat.of R X.

Русский

Забывающий функтор переводит объект X в CoalgCat R в соответствующий объект модуля, то есть forget₂.obj X = ModuleCat.of R X.

LaTeX

$$$$ (forget₂ (CoalgCat R) (ModuleCat R)).obj X = ModuleCat.of R X. $$$$

Lean4

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

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