setAbAdjunction — Mathlib

English

There is an adjunction between the free condensed abelian group functor and the forgetful functor to condensed sets: freeAb ⊣ abForget.

Русский

Существует сопряжённость между свободным функтором конденсированных абелевых групп и забывающим функтором: freeAb ⊣ abForget.

LaTeX

$$$\mathrm{freeAb} \dashv \mathrm{abForget}$$$

Lean4

/-- The free-forgetful adjunction for condensed abelian groups. -/
noncomputable abbrev setAbAdjunction : freeAb ⊣ abForget :=
  freeForgetAdjunction _

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