partialRightAdjoint — Mathlib

Lean4
/-- Given `F : C ⥤ D`, this is the partial adjoint functor `F.PartialLeftAdjointSource ⥤ C`. -/
@[simps]
noncomputable def partialRightAdjoint : F.PartialRightAdjointSource ⥤ C
    where
  obj := F.partialRightAdjointObj
  map := F.partialRightAdjointMap
  map_id
    X := by
    apply F.partialRightAdjointHomEquiv.injective
    dsimp
    rw [partialRightAdjointHomEquiv_map]
    erw [comp_id]
  map_comp {X Y Z} f
    g := by
    apply F.partialRightAdjointHomEquiv.injective
    dsimp
    rw [partialRightAdjointHomEquiv_map, partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_map, ← assoc]
    erw [← assoc]
    rw [← F.partialRightAdjointHomEquiv_comp, comp_id, partialRightAdjointHomEquiv_map]
Похожие утверждения