instIsLeftAdjointForget — Mathlib

English

The forgetful functor from TopCat to Type has a left adjoint, given by equipping a type with the indiscrete topology. For all Type X and TopCat Y, Hom_TopCat(Indiscrete X, Y) ≅ Hom_Type(X, Forget Y).

Русский

У забывающего функтор TopCat → Type существует левый сопряжённый, задаваемый индискретной топологией. Для любых типа X и TopCat Y имеем биоотношение Hom_TopCat(Indiscrete X, Y) ≅ Hom_Type(X, Forget Y).

LaTeX

$$$\\mathrm{Indiscrete} \\dashv \\mathrm{Forget}$$$

Lean4

instance : (forget TopCat.{u}).IsLeftAdjoint :=
  ⟨_, ⟨adj₂⟩⟩

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