forget — Mathlib

Lean4
/-- An enriched functor induces an honest functor of the underlying categories,
by mapping the `(𝟙_ W)`-shaped morphisms.
-/
@[simps]
def forget (F : EnrichedFunctor W C D) : ForgetEnrichment W C ⥤ ForgetEnrichment W D
    where
  obj X := ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X))
  map
    f :=
    ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f ≫ F.map (ForgetEnrichment.to W _) (ForgetEnrichment.to W _))
  map_comp f
    g := by
    dsimp
    apply_fun ForgetEnrichment.homTo W
    · simp only [Iso.cancel_iso_inv_left, Category.assoc, ← tensorHom_comp_tensorHom, ForgetEnrichment.homTo_homOf,
        EnrichedFunctor.map_comp, ForgetEnrichment.homTo_comp]
      rfl
    · intro f g w; apply_fun ForgetEnrichment.homOf W at w; simpa using w
Похожие утверждения