English
Given a functor G and objects A in C, B in D, if each structured-arrow category on G has an initial object, there is a canonical equivalence between morphisms from the initial object to B in the right side and morphisms A → G(B).
Русский
Пусть G — функтор, A ∈ C, B ∈ D. Если в каждой категории структурированной стрелки над G есть начальный объект, существует каноническое эквивалентность между морфизмами от начального объекта к B и отображениями A → G(B).
LaTeX
$$$\\text{Equiv}((\\perp_{StructuredArrow\\,A\\,G}).right \\to B, A \\to G(B))$$$
Lean4
/-- Implementation: If each structured arrow category on `G` has an initial object, an equivalence
which is helpful for constructing a left adjoint to `G`.
-/
@[simps]
def leftAdjointOfStructuredArrowInitialsAux (A : C) (B : D) : ((⊥_ StructuredArrow A G).right ⟶ B) ≃ (A ⟶ G.obj B)
where
toFun g := (⊥_ StructuredArrow A G).hom ≫ G.map g
invFun f := CommaMorphism.right (initial.to (StructuredArrow.mk f))
left_inv
g := by
let B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
let g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g rfl
have : initial.to _ = g' := by cat_disch
change CommaMorphism.right (initial.to B') = _
rw [this]
rfl
right_inv
f := by
let B' : StructuredArrow A G := StructuredArrow.mk f
apply (CommaMorphism.w (initial.to B')).symm.trans (Category.id_comp _)
