showing that internalizeHom ≫ evaluation map = original hom

Stream: new members

[Matt Diamond]

I'm learning about category theory and I'm having trouble proving the following basic fact:

import Mathlib

open CategoryTheory MonoidalCategory CartesianMonoidalCategory

variable {C : Type*} [Category C]
  [CartesianMonoidalCategory C]
  [CartesianClosed C]
  {A B : C}

example {x : 𝟙_ C ⟶ A} {f : A ⟶ B}
  : lift x (internalizeHom f) ≫ (exp.ev A).app B = x ≫ f := sorry

I'm guessing there's a very elegant one-liner that can solve this (something involving adjunctions?) but I'm not sure what it is.

[Aaron Liu]

I'm not very familiar with this part of the library. This is what I came up with:

import Mathlib

theorem CategoryTheory.MonoidalCategory.tensorLeft_map
    {C : Type u} [CategoryTheory.Category.{v, u} C]
    [CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
    (f : Y ⟶ Z) :
    (tensorLeft X).map f = whiskerLeft X f := rfl

open CategoryTheory MonoidalCategory CartesianMonoidalCategory

variable {C : Type*} [Category C]
  [CartesianMonoidalCategory C]
  [CartesianClosed C]
  {A B : C}

example {x : 𝟙_ C ⟶ A} {f : A ⟶ B} : lift x (internalizeHom f) ≫ (exp.ev A).app B = x ≫ f := by
  rw [← CartesianClosed.uncurry_id_eq_ev, internalizeHom,
    CartesianClosed.curry, CartesianClosed.uncurry,
    (exp.adjunction A).homEquiv_naturality_right,
    (exp.adjunction A).homEquiv_symm_id,
    (exp.adjunction A).homEquiv_apply,
    ← Category.comp_id x, Category.assoc,
    ← (exp A).map_comp, ← lift_map, id_tensorHom,
    ← tensorLeft_map, Category.assoc,
    (exp.adjunction A).counit_naturality,
    ← Category.comp_id x,
    ← Category.id_comp ((exp.adjunction A).unit.app (𝟙_ C)),
    ← lift_map, id_tensorHom, ← tensorLeft_map, Category.assoc,
    (exp.adjunction A).left_triangle_components_assoc (𝟙_ C),
    Category.comp_id, Category.comp_id, ← lift_fst_assoc x (𝟙 (𝟙_ C)) f]
  rfl

[Matt Diamond]

Man, that was... more complicated than I thought it would be. Could be a good golfing exercise. Thanks a lot!

[Bhavik Mehta]

import Mathlib

open CategoryTheory MonoidalCategory CartesianMonoidalCategory CartesianClosed

variable {C : Type*} [Category C] [CartesianMonoidalCategory C] [CartesianClosed C] {A B : C}

example {x : 𝟙_ C ⟶ A} {f : A ⟶ B} : lift x (internalizeHom f) ≫ (exp.ev A).app B = x ≫ f := calc
  _ = lift x (𝟙 _) ≫ uncurry (internalizeHom f) := by simp [uncurry_eq]
  _ = x ≫ f := by simp [internalizeHom]