instFullForgetType

Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Types.instFullForgetType

English

The forgetful functor forgetting the structure of Type u to a base concrete category is a full functor.

Русский

Забывающий функтор из категорий типов в базовую конкретную категорию является полным.

LaTeX

$$$\\text{Full}(\\mathrm{forget}:\\mathrm{Type}_u \\to \\text{ConcreteCategory})$$$

Lean4

instance : (@forget (Type u) _ ConcreteCategory.toHasForget).Full :=
  Functor.Full.id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru