Monoidal closed structure induced by equivalence

Stream: general

[Antoine Labelle]

Hi,
I'm trying to provide basic simp lemmas for the monoidal closed structure induced by a monoidal equivalence and would appreciate some help with the use of haveI in lemma statements. Here is my attempt so far; the first lemma works fine but in the second one I can't figure out how to tell Lean that the morphisms on both sides of the equal sign have the same source and the same target.

import category_theory.closed.monoidal

universes u₁ v₁ u₂ v₂

open category_theory category_theory.monoidal_closed

variables {C : Type u₂} [category.{v₂} C] [monoidal_category.{v₂} C]
variables {D : Type u₂} [category.{v₂} D] [monoidal_category.{v₂} D]

lemma of_equiv_ihom_obj (F : monoidal_functor C D) [is_equivalence F.to_functor] [h : monoidal_closed D]
  (X Y : C) :
  (by haveI := of_equiv F; exact (ihom X).obj Y) =
  F.inv.obj ((ihom (F.obj X)).obj (F.obj Y)) := rfl

example (F : monoidal_functor C D) [is_equivalence F.to_functor] [h : monoidal_closed D]
  (X : C) {Y Z : C} (f : Y ⟶ Z) :
  (by haveI := of_equiv F; exact (ihom X).map f) =
  F.inv.map ((ihom (F.obj X)).map (F.map f)) := rfl

[Adam Topaz]

just change the haveI to a letI.

[Adam Topaz]

These instances involve data (some adjoints)

[Adam Topaz]

the first haveI should also be a letI btw

[Antoine Labelle]

Thanks for the answer, that works. Now I'm having trouble applying these lemmas. In the following code, how can I get Lean to simplify using of_equiv_ihom_obj?

import category_theory.closed.functor_category
import representation_theory.Action

universes u u₁ u₂ v₁ v₂

section

open category_theory category_theory.monoidal_closed

variables {C : Type u₂} [category.{v₂} C] [monoidal_category.{v₂} C]
variables {D : Type u₂} [category.{v₂} D] [monoidal_category.{v₂} D]

@[simp] lemma of_equiv_ihom_obj (F : monoidal_functor C D) [is_equivalence F.to_functor] [h : monoidal_closed D]
  (X Y : C) :
  (by letI := of_equiv F; exact (ihom X).obj Y) =
  F.inv.obj ((ihom (F.obj X)).obj (F.obj Y)) := rfl

end

section

open category_theory Action

variables (V : Type (u+1)) [large_category V] [monoidal_category V]
variables (H : Group.{u})

noncomputable theory

instance [monoidal_closed V] : monoidal_closed (single_obj (H : Mon.{u}) ⥤ V) :=
by { change monoidal_closed (single_obj H ⥤ V), apply_instance }

instance [monoidal_closed V] : monoidal_closed (Action V H) :=
  monoidal_closed.of_equiv (functor_category_monoidal_equivalence V H)

lemma ihom_obj_ρ [monoidal_closed V] (X Y : Action V H) (g : H) :
  ((ihom X).obj Y).ρ g =
  (monoidal_closed.pre (X.ρ (g⁻¹ : H))).app Y.V ≫ (ihom X.V).map (Y.ρ g) :=
begin
  rw [of_equiv_ihom_obj (functor_category_monoidal_equivalence V H) X Y], --fails
  sorry
end

end

[Adam Topaz]

i think it would be better to obtain isomorphisms between internal homs when you have a monoidal equivalence between monoidal closed categories, and work with those isomorhpisms instead.

[Eric Wieser]

I think haveI is fine here

[Eric Wieser]

have vs let only makes a difference within a tactic block, not between different tactic blocks

[Adam Topaz]

Well there is obviously some difference in this case, beucase haveI doesn't work, but letI does.

[Antoine Labelle]

Adam Topaz said:

i think it would be better to obtain isomorphisms between internal homs when you have a monoidal equivalence between monoidal closed categories, and work with those isomorhpisms instead.

So

lemma ihom_obj_V [monoidal_closed V] (X Y : Action V H) :
  ((ihom X).obj Y).V = ((ihom X.V).obj Y.V) := rfl

should be an isomorphism and ihom_obj_ρ should be stated in terms of conjugation by this isomorphism? I guess that makes sense, though it quickly makes very messy statements.