enrichedNatTransYoneda — Mathlib

Lean4
/-- A presheaf isomorphic to the Yoneda embedding of
the `V`-object of natural transformations from `F` to `G`.
-/
@[simps]
def enrichedNatTransYoneda (F G : EnrichedFunctor V C D) : Vᵒᵖ ⥤ Type max u₁ w
    where
  obj A := GradedNatTrans ((Center.ofBraided V).obj (unop A)) F G
  map f
    σ :=
    { app := fun X => f.unop ≫ σ.app X
      naturality := fun X Y => by
        have p := σ.naturality X Y
        dsimp at p ⊢
        rw [← id_tensor_comp_tensor_id (f.unop ≫ σ.app Y) _, id_tensor_comp, Category.assoc, Category.assoc, ←
          braiding_naturality_assoc, id_tensor_comp_tensor_id_assoc, p, tensorHom_comp_tensorHom_assoc,
          Category.id_comp] }
      -- TODO assuming `[HasLimits C]` construct the actual object of natural transformations
      -- and show that the functor category is `V`-enriched.
Похожие утверждения