ev_app — Mathlib

Lean4
/-- Given `ℌ : DayConvolutionInternalHom F H`, if we think of `H.obj G`
as the internal hom `[F, G]`, then this is the transformation
corresponding to the component at `G` of the "evaluation" natural morphism
`F ⊛ [F, _] ⟶ 𝟭`. -/
def ev_app : F ⊛ H ⟶ G :=
  DayConvolution.corepresentableBy F H |>.homEquiv.symm <|
    { app x := MonoidalClosed.uncurry <| ℌ.π x.2 x.1
      naturality {x y}
        f := by
        have := congrArg (fun t ↦ F.obj x.1 ◁ t) <| ℌ.hπ x.2 f.1
        dsimp at this ⊢
        simp only [whiskerLeft_comp] at this
        simp only [Category.assoc, MonoidalClosed.uncurry_eq, Functor.id_obj, ← whiskerLeft_comp_assoc, map_comp_π]
        simp only [whiskerLeft_comp, Category.assoc, ihom.ev_naturality, Functor.comp_obj, curriedTensor_obj_obj,
          Functor.id_obj, ← whisker_exchange_assoc, tensorHom_def, Functor.map_comp, ← ihom.ev_naturality_assoc]
        rw [reassoc_of% this]
        simp }
Похожие утверждения