instIsRightAdjointAlgebraForget — Mathlib

English

The forgetful functor forget_T: Alg(T) → C is right adjoint to the free functor Free_T: C → Alg(T); the adjunction is given by T.adj.

Русский

Забывающий функтор forget_T: Alg(T) → C является правым сопряженным к свободному функтору Free_T: C → Alg(T); сопряженность задаётся через T.adj.

LaTeX

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

Lean4

instance : T.forget.IsRightAdjoint :=
  ⟨T.free, ⟨T.adj⟩⟩

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