English
Under suitable initials conditions, there exists a left adjoint to G constructed from adjunctions coming from the initial arrows.
Русский
При подходящих условиях начальных стрелок существует левая адъюнктность к G, построенная из адъюнкций, связывающих начальные стрелки.
LaTeX
$$Construction of a left adjoint to G from structured arrow initials yields an adjunction$$
Lean4
/-- Implementation: If each costructured arrow category on `G` has a terminal object, an equivalence
which is helpful for constructing a right adjoint to `G`.
-/
@[simps]
def rightAdjointOfCostructuredArrowTerminalsAux (B : D) (A : C) : (G.obj B ⟶ A) ≃ (B ⟶ (⊤_ CostructuredArrow G A).left)
where
toFun g := CommaMorphism.left (terminal.from (CostructuredArrow.mk g))
invFun g := G.map g ≫ (⊤_ CostructuredArrow G A).hom
left_inv := by cat_disch
right_inv
g := by
let B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
let g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g rfl
have : terminal.from _ = g' := by cat_disch
change CommaMorphism.left (terminal.from B') = _
rw [this]
rfl
