functorEnrichedHom — Mathlib

Lean4
/-- Given functors `F₁` and `F₂` in `J ⥤ C`, where `C` is a category enriched in `V`,
this is the enriched hom functor from `F₁` to `F₂` in `J ⥤ V`. -/
@[simps!]
noncomputable def functorEnrichedHom : J ⥤ V
    where
  obj j := enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)
  map f := precompEnrichedHom' V (Under.map f) (Iso.refl _) (Iso.refl _)
  map_id
    X := by
    ext j
    simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, end_.lift_π, Under.map_obj_right, Iso.refl_inv,
      NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom, eHomWhiskerLeft_id, comp_id, id_comp]
    congr 1
    simp [Under.map, Comma.mapLeft]
    rfl
  map_comp f
    g := by
    ext j
    simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, end_.lift_π, Under.map_obj_right, Iso.refl_inv,
      NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom, eHomWhiskerLeft_id, comp_id, assoc]
    congr 1
    simp [Under.map, Comma.mapLeft]
Похожие утверждения