Lean4
/-- Auxiliary definition for `rightAdjointObjIsDefined_of_isLimit`. -/
noncomputable def representableByCompYonedaObjOfIsLimit {J : Type*} [Category J] {R : J ⥤ F.PartialRightAdjointSource}
{c : Cone (R ⋙ ObjectProperty.ι _)} (hc : IsLimit c) {c' : Cone (R ⋙ F.partialRightAdjoint)} (hc' : IsLimit c') :
(F.op ⋙ yoneda.obj c.pt).RepresentableBy c'.pt
where
homEquiv
{Y} :=
{ toFun := fun f ↦
hc.lift
(Cone.mk _
{ app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j)
naturality := fun j j' φ ↦ by
dsimp
rw [id_comp, ← c'.w φ, ← partialRightAdjointHomEquiv_map_comp, ← assoc]
dsimp })
invFun := fun g ↦
hc'.lift
(Cone.mk _
{ app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j)
naturality := fun j j' φ ↦ by
apply F.partialRightAdjointHomEquiv.injective
have := c.w φ
dsimp at this ⊢
rw [id_comp, Equiv.apply_symm_apply, partialRightAdjointHomEquiv_map_comp, Equiv.apply_symm_apply,
assoc, this] })
left_inv := fun f ↦ hc'.hom_ext (fun j ↦ by simp)
right_inv := fun g ↦ hc.hom_ext (fun j ↦ by simp) }
homEquiv_comp {Y Y'} g
f :=
hc.hom_ext
(fun j ↦ by
dsimp
simp only [IsLimit.fac, partialRightAdjointHomEquiv_comp, assoc])
