English
Specialized expression for compTranspose in MonoidalClosed: it equals the inverse of the associator composed with evaluation maps as in the standard formula.
Русский
Уравнение для compTranspose в MonoidalClosed: оно равно обратному отображению ассоциатора, скомпонованному с отображениями вычисления согласно стандартной формуле.
LaTeX
$$$ \\mathrm{compTranspose}(x,y,z) = (\\alpha_{x,y,z})^{-1} \\circ (\\mathrm{ihom.ev}(x)).app y \\; \\triangleright\\; (\\mathrm{ihom.ev}(y)).app z. $$$
Lean4
/-- Suppose we have a monoidal equivalence `F : C ≌ D`, with `D` monoidal closed. We can pull the
monoidal closed instance back along the equivalence. For `X, Y, Z : C`, this lemma describes the
resulting uncurrying map `Hom(Y, (X ⟶[C] Z)) → Hom(X ⊗ Y ⟶ Z)`. (`X ⟶[C] Z` is
defined to be `F⁻¹(F(X) ⟶[D] F(Z))`, so uncurrying in `C` is given by essentially conjugating
uncurrying in `D` by `F.`) -/
theorem ofEquiv_uncurry_def {X Y Z : C} :
letI := ofEquiv F adj
∀ (f : Y ⟶ (ihom X).obj Z),
MonoidalClosed.uncurry f =
((Iso.compInverseIso (H := adj.toEquivalence) (Functor.Monoidal.commTensorLeft F X)).inv.app Y) ≫
(adj.toEquivalence.symm.toAdjunction.homEquiv _ _).symm
(MonoidalClosed.uncurry ((adj.homEquiv _ _).symm f)) :=
by
intro f
change
(((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).ofNatIsoLeft _).homEquiv _
_).symm
_ =
_
dsimp only [Adjunction.ofNatIsoLeft]
rw [Adjunction.mkOfHomEquiv_homEquiv]
dsimp
rw [Adjunction.comp_homEquiv, Adjunction.comp_homEquiv]
rfl
