[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
hX : Closed X
hY : Closed Y
⊢ IsLeftAdjoint (tensorLeft (X ⊗ Y))
[PROOFSTEP]
haveI := hX.isAdj
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
hX : Closed X
hY : Closed Y
this : IsLeftAdjoint (tensorLeft X)
⊢ IsLeftAdjoint (tensorLeft (X ⊗ Y))
[PROOFSTEP]
haveI := hY.isAdj
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
hX : Closed X
hY : Closed Y
this✝ : IsLeftAdjoint (tensorLeft X)
this : IsLeftAdjoint (tensorLeft Y)
⊢ IsLeftAdjoint (tensorLeft (X ⊗ Y))
[PROOFSTEP]
exact Adjunction.leftAdjointOfNatIso (MonoidalCategory.tensorLeftTensor _ _).symm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X x✝ : C
⊢ Function.LeftInverse (fun a => (λ_ X).hom ≫ a) fun a => (λ_ X).inv ≫ a
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X x✝ : C
⊢ Function.RightInverse (fun a => (λ_ X).hom ≫ a) fun a => (λ_ X).inv ≫ a
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X'✝ X✝ Y✝ : C
f : X'✝ ⟶ X✝
g : X✝ ⟶ (𝟭 C).obj Y✝
⊢ ↑((fun X x =>
              { toFun := fun a => (λ_ X).inv ≫ a, invFun := fun a => (λ_ X).hom ≫ a,
                left_inv := (_ : ∀ (x_1 : (tensorLeft (𝟙_ C)).obj X ⟶ x), (λ_ X).hom ≫ (λ_ X).inv ≫ x_1 = x_1),
                right_inv := (_ : ∀ (x_1 : X ⟶ (𝟭 C).obj x), (λ_ X).inv ≫ (λ_ X).hom ≫ x_1 = x_1) })
            X'✝ Y✝).symm
      (f ≫ g) =
    (tensorLeft (𝟙_ C)).map f ≫
      ↑((fun X x =>
                { toFun := fun a => (λ_ X).inv ≫ a, invFun := fun a => (λ_ X).hom ≫ a,
                  left_inv := (_ : ∀ (x_1 : (tensorLeft (𝟙_ C)).obj X ⟶ x), (λ_ X).hom ≫ (λ_ X).inv ≫ x_1 = x_1),
                  right_inv := (_ : ∀ (x_1 : X ⟶ (𝟭 C).obj x), (λ_ X).inv ≫ (λ_ X).hom ≫ x_1 = x_1) })
              X✝ Y✝).symm
        g
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X'✝ X✝ Y✝ : C
f : X'✝ ⟶ X✝
g : X✝ ⟶ (𝟭 C).obj Y✝
⊢ (λ_ X'✝).hom ≫ f ≫ g = (𝟙 (𝟙_ C) ⊗ f) ≫ (λ_ X✝).hom ≫ g
[PROOFSTEP]
rw [leftUnitor_naturality_assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A B X X' Y Y' Z : C
inst✝ : Closed A
⊢ uncurry (𝟙 ((ihom A).obj X)) = NatTrans.app (ihom.ev A) X
[PROOFSTEP]
rw [uncurry_eq, tensor_id, id_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A B X X' Y Y' Z : C
inst✝ : Closed A
⊢ curry (𝟙 (A ⊗ (𝟭 C).obj X)) = NatTrans.app (ihom.coev A) X
[PROOFSTEP]
rw [curry_eq, (ihom A).map_id (A ⊗ _)]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A B X X' Y Y' Z : C
inst✝ : Closed A
⊢ NatTrans.app (ihom.coev A) ((𝟭 C).obj X) ≫ 𝟙 ((ihom A).obj (A ⊗ (𝟭 C).obj X)) = NatTrans.app (ihom.coev A) X
[PROOFSTEP]
apply comp_id
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝¹ : Closed A
inst✝ : Closed B
f : B ⟶ A
X : C
⊢ uncurry (NatTrans.app (pre f) X) = (f ⊗ 𝟙 ((ihom A).obj X)) ≫ NatTrans.app (ihom.ev A) X
[PROOFSTEP]
rw [uncurry_eq, id_tensor_pre_app_comp_ev]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A✝ B X X' Y Y' Z : C
inst✝² : Closed A✝
inst✝¹ : Closed B
A : C
inst✝ : Closed A
⊢ pre (𝟙 A) = 𝟙 (ihom A)
[PROOFSTEP]
simp only [pre, Functor.map_id]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A✝ B X X' Y Y' Z : C
inst✝² : Closed A✝
inst✝¹ : Closed B
A : C
inst✝ : Closed A
⊢ ↑(transferNatTransSelf (ihom.adjunction A) (ihom.adjunction A)) (𝟙 ((tensoringLeft C).obj A)) = 𝟙 (ihom A)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A✝ B X X' Y Y' Z : C
inst✝² : Closed A✝
inst✝¹ : Closed B
A : C
inst✝ : Closed A
⊢ ↑(transferNatTransSelf (ihom.adjunction A) (ihom.adjunction A)) (𝟙 (tensorLeft A)) = 𝟙 (ihom A)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
A B X X' Y Y' Z : C
inst✝⁴ : Closed A
inst✝³ : Closed B
A₁ A₂ A₃ : C
inst✝² : Closed A₁
inst✝¹ : Closed A₂
inst✝ : Closed A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ pre (f ≫ g) = pre g ≫ pre f
[PROOFSTEP]
rw [pre, pre, pre, transferNatTransSelf_comp, (tensoringLeft C).map_comp]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
A B X✝ X' Y✝ Y' Z✝ : C
inst✝³ : Closed A
inst✝² : Closed B
W X Y Z : C
inst✝¹ : Closed W
inst✝ : Closed X
f : W ⟶ X
g : Y ⟶ Z
⊢ NatTrans.app (pre f) Y ≫ (ihom W).map g = (ihom X).map g ≫ NatTrans.app (pre f) Z
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝³ : Closed A
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
h : MonoidalClosed D
X : C
⊢ IsLeftAdjoint (tensorLeft X)
[PROOFSTEP]
haveI q : Closed (F.obj X) := inferInstance
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝³ : Closed A
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
h : MonoidalClosed D
X : C
q : Closed (F.obj X)
⊢ IsLeftAdjoint (tensorLeft X)
[PROOFSTEP]
haveI : IsLeftAdjoint (tensorLeft (F.obj X)) := q.isAdj
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝³ : Closed A
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
h : MonoidalClosed D
X : C
q : Closed (F.obj X)
this : IsLeftAdjoint (tensorLeft (F.obj X))
⊢ IsLeftAdjoint (tensorLeft X)
[PROOFSTEP]
have i := compInvIso (MonoidalFunctor.commTensorLeft F X)
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝³ : Closed A
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
h : MonoidalClosed D
X : C
q : Closed (F.obj X)
this : IsLeftAdjoint (tensorLeft (F.obj X))
i : (F.toFunctor ⋙ tensorLeft (F.obj X)) ⋙ Functor.inv F.toFunctor ≅ tensorLeft X
⊢ IsLeftAdjoint (tensorLeft X)
[PROOFSTEP]
exact Adjunction.leftAdjointOfNatIso i
