enrichedOrdinaryCategory — Mathlib

Lean4
/-- If for a lax monoidal functor `F : V ⥤ W` the canonical function
`(𝟙_ V ⟶ v) → (𝟙_ W ⟶ F.obj v)` is bijective, and `C` is an enriched ordinary category on `V`,
then `F` induces the structure of a `W`-enriched ordinary category on `TransportEnrichment F C`,
i.e. on the same underlying category `C`. -/
noncomputable def enrichedOrdinaryCategory
    (h : ∀ v : V, Function.Bijective fun (f : 𝟙_ V ⟶ v) => Functor.LaxMonoidal.ε F ≫ F.map f) :
    EnrichedOrdinaryCategory W (TransportEnrichment F C)
    where
  homEquiv {X Y} := (eHomEquiv V (C := C)).trans <| Equiv.ofBijective _ (h (Hom (C := C) X Y))
  homEquiv_comp f
    g := by
    simp [← tensorHom_comp_tensorHom, eHomEquiv_comp, eComp_eq, tensorHom_def (Functor.LaxMonoidal.ε F),
      unitors_inv_equal]
Похожие утверждения