isRightAdjoint_of_leftAdjointObjIsDefined_eq_top

English

If F.leftAdjointObjIsDefined is top, then F.IsRightAdjoint; i.e., a left-defined object implies right adjointness.

Русский

Если F.leftAdjointObjIsDefined равна верхнему элементу, то F является правым сопряжённым; т.е. существование левого определённого объекта влечёт существование правого сопряжённого.

LaTeX

$$$F.leftAdjointObjIsDefined = \top \Rightarrow F.IsRightAdjoint$$$

Lean4

theorem isRightAdjoint_of_leftAdjointObjIsDefined_eq_top (h : F.leftAdjointObjIsDefined = ⊤) : F.IsRightAdjoint :=
  by
  replace h : ∀ X, IsCorepresentable (F ⋙ coyoneda.obj (op X)) := fun X ↦ by
    simp only [← leftAdjointObjIsDefined_iff, h, Pi.top_apply, «Prop».top_eq_true]
  exact
    (Adjunction.adjunctionOfEquivLeft (fun X Y ↦ (F ⋙ coyoneda.obj (op X)).corepresentableBy.homEquiv)
        (fun X Y Y' g f ↦ by apply CorepresentableBy.homEquiv_comp)).isRightAdjoint

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