leftAdjointObjIsDefined_of_adjunction

English

If there is an adjunction with G ⊣ F, then F is a right adjoint object; precisely, F.rightAdjointObjIsDefined Y holds for all Y.

Русский

Если существует адъюнкция G ⊣ F, то F образует правый соседний объект; для всех Y выполняется F.rightAdjointObjIsDefined Y.

LaTeX

$$$\forall Y,\ F.rightAdjointObjIsDefined\; Y$$$

Lean4

theorem leftAdjointObjIsDefined_of_adjunction {G : C ⥤ D} (adj : G ⊣ F) (X : C) : F.leftAdjointObjIsDefined X :=
  (adj.corepresentableBy X).isCorepresentable

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