instIsLeftAdjointCoalgebraForget — Mathlib

English

The forgetful functor from G- Coalgebras to C is left adjoint to the cofree coalgebra functor; the adjunction is given by G.adj.

Русский

Забывающий функтор из G-коалгебр в C является левым сопряжённым к кофривной функтору; сопряжение задаётся через G.adj.

LaTeX

$$$\\mathrm{Forget}_{G} \\dashv \\mathrm{CoFree}_{G} \\quad\\text{с сопряжением, задаваемым } G.\\mathrm{adj}.$$$

Lean4

instance : G.forget.IsLeftAdjoint :=
  ⟨_, ⟨G.adj⟩⟩

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