English
The transpose component of the composition in MonoidalClosed is given by a standard expression involving associators and evaluation maps.
Русский
Транспонированный компонент композиции в замкнутой монойальной структуре задаётся обычным выражением с ассоциаторами и отображениями вычисления.
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 currying map `Hom(X ⊗ Y, Z) → Hom(Y, (X ⟶[C] Z))`. (`X ⟶[C] Z` is defined to be
`F⁻¹(F(X) ⟶[D] F(Z))`, so currying in `C` is given by essentially conjugating currying in
`D` by `F.`) -/
theorem ofEquiv_curry_def {X Y Z : C} (f : X ⊗ Y ⟶ Z) :
letI := ofEquiv F adj
MonoidalClosed.curry f =
adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z))
(MonoidalClosed.curry
(adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z
((Iso.compInverseIso (H := adj.toEquivalence) (Functor.Monoidal.commTensorLeft F X)).hom.app Y ≫ f))) :=
by
-- This whole proof used to be `rfl` before https://github.com/leanprover-community/mathlib4/pull/16317.
change
((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).ofNatIsoLeft _).homEquiv _ _ _ =
_
dsimp only [Adjunction.ofNatIsoLeft]
rw [Adjunction.mkOfHomEquiv_homEquiv]
dsimp
rw [Adjunction.comp_homEquiv, Adjunction.comp_homEquiv]
rfl
