partialLeftAdjoint — Mathlib

Lean4
/-- Given `F : D ⥤ C`, this is the partial adjoint functor `F.PartialLeftAdjointSource ⥤ D`. -/
@[simps]
noncomputable def partialLeftAdjoint : F.PartialLeftAdjointSource ⥤ D
    where
  obj := F.partialLeftAdjointObj
  map := F.partialLeftAdjointMap
  map_id
    X := by
    apply F.partialLeftAdjointHomEquiv.injective
    dsimp
    rw [partialLeftAdjointHomEquiv_map]
    erw [id_comp]
  map_comp {X Y Z} f
    g := by
    apply F.partialLeftAdjointHomEquiv.injective
    dsimp
    rw [partialLeftAdjointHomEquiv_map, partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map, assoc]
    erw [assoc]
    rw [← F.partialLeftAdjointHomEquiv_comp, id_comp, partialLeftAdjointHomEquiv_map]
Похожие утверждения