abForget — Mathlib

English

There is a forgetful functor from the category of condensed abelian groups to the category of condensed sets; it sends each condensed abelian group to its underlying condensed set.

Русский

Существует забывающий функтор из категории конденсированных абелевых групп в категорию конденсированных множеств; он выводит конденсированное множество из конденсированной абелевой группы.

LaTeX

$$$\mathrm{abForget} : \mathrm{CondensedAb} \to \mathrm{CondensedSet}$$$

Lean4

/-- The forgetful functor from condensed abelian groups to condensed sets. -/
abbrev abForget : CondensedAb ⥤ CondensedSet :=
  forget _

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