isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top

English

If F.rightAdjointObjIsDefined = ⊤, then F is left adjoint; i.e., there exists a left adjoint structure.

Русский

Если F.rightAdjointObjIsDefined = ⊤, то F является левым сопряжённым; существует структура левого сопряжённого.

LaTeX

$$$F.IsLeftAdjoint$ при $F.rightAdjointObjIsDefined = \top$$$

Lean4

theorem isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top (h : F.rightAdjointObjIsDefined = ⊤) : F.IsLeftAdjoint :=
  by
  replace h : ∀ X, IsRepresentable (F.op ⋙ yoneda.obj X) := fun X ↦ by
    simp only [← rightAdjointObjIsDefined_iff, h, Pi.top_apply, «Prop».top_eq_true]
  exact
    (Adjunction.adjunctionOfEquivRight (fun X Y ↦ (F.op ⋙ yoneda.obj Y).representableBy.homEquiv.symm)
        (fun X Y Y' g f ↦ (RepresentableBy.comp_homEquiv_symm ..).symm)).isLeftAdjoint

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