Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit a627569

Browse files
kim-emkim-em
committed
feat(category_theory/monoidal): adjunctions in rigid categories (#13707)
We construct the bijection on hom-sets `(Yᘁ ⊗ X ⟶ Z) ≃ (X ⟶ Y ⊗ Z)` given by "pulling the string on the left" down or up, using right duals in a right rigid category. As consequences, we show that a left rigid category is monoidal closed (it seems our lefts and rights have got mixed up!!), and that functors from a groupoid to a rigid category is again a rigid category. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent fe44576 commit a627569

5 files changed

Lines changed: 396 additions & 4 deletions

File tree

‎src/algebra/category/FinVect.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Jakob von Raumer. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jakob von Raumer
55
-/
6-
import category_theory.monoidal.rigid
6+
import category_theory.monoidal.rigid.basic
77
import linear_algebra.tensor_product_basis
88
import linear_algebra.coevaluation
99
import algebra.category.Module.monoidal

‎src/category_theory/monoidal/coherence.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -263,6 +263,11 @@ begin
263263
cases w,
264264
end
265265

266+
lemma insert_id_lhs {C : Type*} [category C] {X Y : C} (f g : X ⟶ Y) (w : f ≫ 𝟙 _ = g) : f = g :=
267+
by simpa using w
268+
lemma insert_id_rhs {C : Type*} [category C] {X Y : C} (f g : X ⟶ Y) (w : f = g ≫ 𝟙 _) : f = g :=
269+
by simpa using w
270+
266271
end coherence
267272

268273
open coherence
@@ -300,6 +305,8 @@ do
300305
-- Then check that either `g₀` is identically `g₁`,
301306
reflexivity <|> (do
302307
-- or that both are compositions,
308+
(do `(_ ≫ _ = _) ← target, skip) <|> `[apply tactic.coherence.insert_id_lhs],
309+
(do `(_ = _ ≫ _) ← target, skip) <|> `[apply tactic.coherence.insert_id_rhs],
303310
`(_ ≫ _ = _ ≫ _) ← target |
304311
fail "`coherence` tactic failed, non-structural morphisms don't match",
305312
tactic.congr_core',
@@ -323,6 +330,9 @@ example {U V W X Y : C} (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y)
323330
f ⊗≫ g = f ≫ (α_ _ _ _).inv ≫ g :=
324331
by coherence
325332

333+
example {U : C} (f : U ⟶ 𝟙_ C) : f ≫ (ρ_ (𝟙_ C)).inv ≫ (λ_ (𝟙_ C)).hom = f :=
334+
by coherence
335+
326336
example (W X Y Z : C) (f) :
327337
((α_ W X Y).hom ⊗ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom ≫ (𝟙 W ⊗ (α_ X Y Z).hom) ≫ f ≫
328338
(α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom =

src/category_theory/monoidal/rigid.lean renamed to src/category_theory/monoidal/rigid/basic.lean

Lines changed: 308 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jakob von Raumer
55
-/
66
import category_theory.monoidal.coherence_lemmas
7+
import category_theory.closed.monoidal
8+
import tactic.apply_fun
79

810
/-!
911
# Rigid (autonomous) monoidal categories
@@ -34,11 +36,17 @@ exact pairings and duals.
3436
* Show that `X ⊗ Y` and `Yᘁ ⊗ Xᘁ` form an exact pairing.
3537
* Show that the left adjoint mate of the right adjoint mate of a morphism is the morphism itself.
3638
* Simplify constructions in the case where a symmetry or braiding is present.
37-
* Connect this definition to `monoidal_closed`: an object with a (left?) dual is
38-
a closed object `X` such that the right adjoint of `X ⊗ -` is given by `Y ⊗ -` for some `Y`.
3939
* Show that `ᘁ` gives an equivalence of categories `C ≅ (Cᵒᵖ)ᴹᵒᵖ`.
4040
* Define pivotal categories (rigid categories equipped with a natural isomorphism `ᘁᘁ ≅ 𝟙 C`).
4141
42+
## Notes
43+
44+
Although we construct the adjunction `tensor_left Y ⊣ tensor_left X` from `exact_pairing X Y`,
45+
this is not a bijective correspondence.
46+
I think the correct statement is that `tensor_left Y` and `tensor_left X` are
47+
module endofunctors of `C` as a right `C` module category,
48+
and `exact_pairing X Y` is in bijection with adjunctions compatible with this right `C` action.
49+
4250
## References
4351
4452
* <https://ncatlab.org/nlab/show/rigid+monoidal+category>
@@ -227,6 +235,298 @@ begin
227235
right_unitor_naturality_assoc, ←unitors_equal, ←category.assoc, ←category.assoc], simp
228236
end
229237

238+
/--
239+
Given an exact pairing on `Y Y'`,
240+
we get a bijection on hom-sets `(Y' ⊗ X ⟶ Z) ≃ (X ⟶ Y ⊗ Z)`
241+
by "pulling the string on the left" up or down.
242+
243+
This gives the adjunction `tensor_left_adjunction Y Y' : tensor_left Y' ⊣ tensor_left Y`.
244+
245+
This adjunction is often referred to as "Frobenius reciprocity" in the
246+
fusion categories / planar algebras / subfactors literature.
247+
-/
248+
def tensor_left_hom_equiv (X Y Y' Z : C) [exact_pairing Y Y'] :
249+
(Y' ⊗ X ⟶ Z) ≃ (X ⟶ Y ⊗ Z) :=
250+
{ to_fun := λ f, (λ_ _).inv ≫ (η_ _ _ ⊗ 𝟙 _) ≫ (α_ _ _ _).hom ≫ (𝟙 _ ⊗ f),
251+
inv_fun := λ f, (𝟙 Y' ⊗ f) ≫ (α_ _ _ _).inv ≫ (ε_ _ _ ⊗ 𝟙 _) ≫ (λ_ _).hom,
252+
left_inv := λ f, begin
253+
dsimp,
254+
simp only [id_tensor_comp],
255+
slice_lhs 4 5 { rw associator_inv_naturality, },
256+
slice_lhs 5 6 { rw [tensor_id, id_tensor_comp_tensor_id, ←tensor_id_comp_id_tensor], },
257+
slice_lhs 2 5 { simp only [←tensor_id, associator_inv_conjugation], },
258+
have c : (α_ Y' (Y ⊗ Y') X).hom ≫ (𝟙 Y' ⊗ (α_ Y Y' X).hom) ≫ (α_ Y' Y (Y' ⊗ X)).inv ≫
259+
(α_ (Y' ⊗ Y) Y' X).inv = (α_ _ _ _).inv ⊗ 𝟙 _, pure_coherence,
260+
slice_lhs 4 7 { rw c, },
261+
slice_lhs 3 5 { rw [←comp_tensor_id, ←comp_tensor_id, coevaluation_evaluation], },
262+
simp only [left_unitor_conjugation],
263+
coherence,
264+
end,
265+
right_inv := λ f, begin
266+
dsimp,
267+
simp only [id_tensor_comp],
268+
slice_lhs 3 4 { rw ←associator_naturality, },
269+
slice_lhs 2 3 { rw [tensor_id, tensor_id_comp_id_tensor, ←id_tensor_comp_tensor_id], },
270+
slice_lhs 3 6 { simp only [←tensor_id, associator_inv_conjugation], },
271+
have c : (α_ (Y ⊗ Y') Y Z).hom ≫ (α_ Y Y' (Y ⊗ Z)).hom ≫ (𝟙 Y ⊗ (α_ Y' Y Z).inv) ≫
272+
(α_ Y (Y' ⊗ Y) Z).inv = (α_ _ _ _).hom ⊗ 𝟙 Z, pure_coherence,
273+
slice_lhs 5 8 { rw c, },
274+
slice_lhs 4 6 { rw [←comp_tensor_id, ←comp_tensor_id, evaluation_coevaluation], },
275+
simp only [left_unitor_conjugation],
276+
coherence,
277+
end, }
278+
279+
/--
280+
Given an exact pairing on `Y Y'`,
281+
we get a bijection on hom-sets `(X ⊗ Y ⟶ Z) ≃ (X ⟶ Z ⊗ Y')`
282+
by "pulling the string on the right" up or down.
283+
-/
284+
def tensor_right_hom_equiv (X Y Y' Z : C) [exact_pairing Y Y'] :
285+
(X ⊗ Y ⟶ Z) ≃ (X ⟶ Z ⊗ Y') :=
286+
{ to_fun := λ f, (ρ_ _).inv ≫ (𝟙 _ ⊗ η_ _ _) ≫ (α_ _ _ _).inv ≫ (f ⊗ 𝟙 _),
287+
inv_fun := λ f, (f ⊗ 𝟙 _) ≫ (α_ _ _ _).hom ≫ (𝟙 _ ⊗ ε_ _ _) ≫ (ρ_ _).hom,
288+
left_inv := λ f, begin
289+
dsimp,
290+
simp only [comp_tensor_id],
291+
slice_lhs 4 5 { rw associator_naturality, },
292+
slice_lhs 5 6 { rw [tensor_id, tensor_id_comp_id_tensor, ←id_tensor_comp_tensor_id], },
293+
slice_lhs 2 5 { simp only [←tensor_id, associator_conjugation], },
294+
have c : (α_ X (Y ⊗ Y') Y).inv ≫ ((α_ X Y Y').inv ⊗ 𝟙 Y) ≫ (α_ (X ⊗ Y) Y' Y).hom ≫
295+
(α_ X Y (Y' ⊗ Y)).hom = 𝟙 _ ⊗ (α_ _ _ _).hom, pure_coherence,
296+
slice_lhs 4 7 { rw c, },
297+
slice_lhs 3 5 { rw [←id_tensor_comp, ←id_tensor_comp, evaluation_coevaluation], },
298+
simp only [right_unitor_conjugation],
299+
coherence,
300+
end,
301+
right_inv := λ f, begin
302+
dsimp,
303+
simp only [comp_tensor_id],
304+
slice_lhs 3 4 { rw ←associator_inv_naturality, },
305+
slice_lhs 2 3 { rw [tensor_id, id_tensor_comp_tensor_id, ←tensor_id_comp_id_tensor], },
306+
slice_lhs 3 6 { simp only [←tensor_id, associator_conjugation], },
307+
have c : (α_ Z Y' (Y ⊗ Y')).inv ≫ (α_ (Z ⊗ Y') Y Y').inv ≫ ((α_ Z Y' Y).hom ⊗ 𝟙 Y') ≫
308+
(α_ Z (Y' ⊗ Y) Y').hom = 𝟙 _ ⊗ (α_ _ _ _).inv, pure_coherence,
309+
slice_lhs 5 8 { rw c, },
310+
slice_lhs 4 6 { rw [←id_tensor_comp, ←id_tensor_comp, coevaluation_evaluation], },
311+
simp only [right_unitor_conjugation],
312+
coherence,
313+
end, }
314+
315+
lemma tensor_left_hom_equiv_naturality
316+
{X Y Y' Z Z' : C} [exact_pairing Y Y'] (f : Y' ⊗ X ⟶ Z) (g : Z ⟶ Z') :
317+
(tensor_left_hom_equiv X Y Y' Z') (f ≫ g) =
318+
(tensor_left_hom_equiv X Y Y' Z) f ≫ (𝟙 Y ⊗ g) :=
319+
begin
320+
dsimp [tensor_left_hom_equiv],
321+
simp only [id_tensor_comp, category.assoc],
322+
end
323+
324+
lemma tensor_left_hom_equiv_symm_naturality {X X' Y Y' Z : C} [exact_pairing Y Y']
325+
(f : X ⟶ X') (g : X' ⟶ Y ⊗ Z) :
326+
(tensor_left_hom_equiv X Y Y' Z).symm (f ≫ g) =
327+
(𝟙 _ ⊗ f) ≫ (tensor_left_hom_equiv X' Y Y' Z).symm g :=
328+
begin
329+
dsimp [tensor_left_hom_equiv],
330+
simp only [id_tensor_comp, category.assoc],
331+
end
332+
333+
lemma tensor_right_hom_equiv_naturality {X Y Y' Z Z' : C} [exact_pairing Y Y']
334+
(f : X ⊗ Y ⟶ Z) (g : Z ⟶ Z') :
335+
(tensor_right_hom_equiv X Y Y' Z') (f ≫ g) =
336+
(tensor_right_hom_equiv X Y Y' Z) f ≫ (g ⊗ 𝟙 Y') :=
337+
begin
338+
dsimp [tensor_right_hom_equiv],
339+
simp only [comp_tensor_id, category.assoc],
340+
end
341+
342+
lemma tensor_right_hom_equiv_symm_naturality
343+
{X X' Y Y' Z : C} [exact_pairing Y Y'] (f : X ⟶ X') (g : X' ⟶ Z ⊗ Y') :
344+
((tensor_right_hom_equiv X Y Y' Z).symm) (f ≫ g) =
345+
(f ⊗ 𝟙 Y) ≫ ((tensor_right_hom_equiv X' Y Y' Z).symm) g :=
346+
begin
347+
dsimp [tensor_right_hom_equiv],
348+
simp only [comp_tensor_id, category.assoc],
349+
end
350+
351+
/--
352+
If `Y Y'` have an exact pairing,
353+
then the functor `tensor_left Y'` is left adjoint to `tensor_left Y`.
354+
-/
355+
def tensor_left_adjunction (Y Y' : C) [exact_pairing Y Y'] : tensor_left Y' ⊣ tensor_left Y :=
356+
adjunction.mk_of_hom_equiv
357+
{ hom_equiv := λ X Z, tensor_left_hom_equiv X Y Y' Z,
358+
hom_equiv_naturality_left_symm' :=
359+
λ X X' Z f g, tensor_left_hom_equiv_symm_naturality f g,
360+
hom_equiv_naturality_right' :=
361+
λ X Z Z' f g, tensor_left_hom_equiv_naturality f g, }
362+
363+
/--
364+
If `Y Y'` have an exact pairing,
365+
then the functor `tensor_right Y` is left adjoint to `tensor_right Y'`.
366+
-/
367+
def tensor_right_adjunction (Y Y' : C) [exact_pairing Y Y'] : tensor_right Y ⊣ tensor_right Y' :=
368+
adjunction.mk_of_hom_equiv
369+
{ hom_equiv := λ X Z, tensor_right_hom_equiv X Y Y' Z,
370+
hom_equiv_naturality_left_symm' :=
371+
λ X X' Z f g, tensor_right_hom_equiv_symm_naturality f g,
372+
hom_equiv_naturality_right' :=
373+
λ X Z Z' f g, tensor_right_hom_equiv_naturality f g, }
374+
375+
@[priority 100]
376+
instance closed_of_has_left_dual (Y : C) [has_left_dual Y] : closed Y :=
377+
{ is_adj := ⟨_, tensor_left_adjunction (ᘁY) Y⟩, }
378+
379+
/-- `tensor_left_hom_equiv` commutes with tensoring on the right -/
380+
lemma tensor_left_hom_equiv_tensor {X X' Y Y' Z Z' : C} [exact_pairing Y Y']
381+
(f : X ⟶ Y ⊗ Z) (g : X' ⟶ Z') :
382+
(tensor_left_hom_equiv (X ⊗ X') Y Y' (Z ⊗ Z')).symm ((f ⊗ g) ≫ (α_ _ _ _).hom) =
383+
(α_ _ _ _).inv ≫ ((tensor_left_hom_equiv X Y Y' Z).symm f ⊗ g) :=
384+
begin
385+
dsimp [tensor_left_hom_equiv],
386+
simp only [id_tensor_comp],
387+
simp only [associator_inv_conjugation],
388+
slice_lhs 2 2 { rw ←id_tensor_comp_tensor_id, },
389+
conv_rhs { rw [←id_tensor_comp_tensor_id, comp_tensor_id, comp_tensor_id], },
390+
simp, coherence,
391+
end
392+
393+
/-- `tensor_right_hom_equiv` commutes with tensoring on the left -/
394+
lemma tensor_right_hom_equiv_tensor {X X' Y Y' Z Z' : C} [exact_pairing Y Y']
395+
(f : X ⟶ Z ⊗ Y') (g : X' ⟶ Z') :
396+
(tensor_right_hom_equiv (X' ⊗ X) Y Y' (Z' ⊗ Z)).symm ((g ⊗ f) ≫ (α_ _ _ _).inv) =
397+
(α_ _ _ _).hom ≫ (g ⊗ (tensor_right_hom_equiv X Y Y' Z).symm f) :=
398+
begin
399+
dsimp [tensor_right_hom_equiv],
400+
simp only [comp_tensor_id],
401+
simp only [associator_conjugation],
402+
slice_lhs 2 2 { rw ←tensor_id_comp_id_tensor, },
403+
conv_rhs { rw [←tensor_id_comp_id_tensor, id_tensor_comp, id_tensor_comp], },
404+
simp only [←tensor_id, associator_conjugation],
405+
simp, coherence,
406+
end
407+
408+
@[simp]
409+
lemma tensor_left_hom_equiv_symm_coevaluation_comp_id_tensor
410+
{Y Y' Z : C} [exact_pairing Y Y'] (f : Y' ⟶ Z) :
411+
(tensor_left_hom_equiv _ _ _ _).symm (η_ _ _ ≫ (𝟙 Y ⊗ f)) = (ρ_ _).hom ≫ f :=
412+
begin
413+
dsimp [tensor_left_hom_equiv],
414+
rw id_tensor_comp,
415+
slice_lhs 2 3 { rw associator_inv_naturality, },
416+
slice_lhs 3 4 { rw [tensor_id, id_tensor_comp_tensor_id, ←tensor_id_comp_id_tensor], },
417+
slice_lhs 1 3 { rw coevaluation_evaluation, },
418+
simp,
419+
end
420+
421+
@[simp]
422+
lemma tensor_left_hom_equiv_symm_coevaluation_comp_tensor_id
423+
{X Y : C} [has_right_dual X] [has_right_dual Y] (f : X ⟶ Y) :
424+
(tensor_left_hom_equiv _ _ _ _).symm (η_ _ _ ≫ (f ⊗ 𝟙 Xᘁ)) = (ρ_ _).hom ≫ fᘁ :=
425+
begin
426+
dsimp [tensor_left_hom_equiv, right_adjoint_mate],
427+
simp,
428+
end
429+
430+
@[simp]
431+
lemma tensor_right_hom_equiv_symm_coevaluation_comp_id_tensor
432+
{X Y : C} [has_left_dual X] [has_left_dual Y] (f : X ⟶ Y) :
433+
(tensor_right_hom_equiv _ (ᘁY) _ _).symm (η_ (ᘁX) X ≫ (𝟙 (ᘁX) ⊗ f)) = (λ_ _).hom ≫ (ᘁf) :=
434+
begin
435+
dsimp [tensor_right_hom_equiv, left_adjoint_mate],
436+
simp,
437+
end
438+
439+
@[simp]
440+
lemma tensor_right_hom_equiv_symm_coevaluation_comp_tensor_id
441+
{Y Y' Z : C} [exact_pairing Y Y'] (f : Y ⟶ Z) :
442+
(tensor_right_hom_equiv _ Y _ _).symm (η_ Y Y' ≫ (f ⊗ 𝟙 Y')) = (λ_ _).hom ≫ f :=
443+
begin
444+
dsimp [tensor_right_hom_equiv],
445+
rw comp_tensor_id,
446+
slice_lhs 2 3 { rw associator_naturality, },
447+
slice_lhs 3 4 { rw [tensor_id, tensor_id_comp_id_tensor, ←id_tensor_comp_tensor_id], },
448+
slice_lhs 1 3 { rw evaluation_coevaluation, },
449+
simp,
450+
end
451+
452+
@[simp]
453+
lemma tensor_left_hom_equiv_id_tensor_comp_evaluation
454+
{Y Z : C} [has_left_dual Z] (f : Y ⟶ (ᘁZ)) :
455+
(tensor_left_hom_equiv _ _ _ _) ((𝟙 Z ⊗ f) ≫ ε_ _ _) = f ≫ (ρ_ _).inv :=
456+
begin
457+
dsimp [tensor_left_hom_equiv],
458+
rw id_tensor_comp,
459+
slice_lhs 3 4 { rw ←associator_naturality, },
460+
slice_lhs 2 3 { rw [tensor_id, tensor_id_comp_id_tensor, ←id_tensor_comp_tensor_id], },
461+
slice_lhs 3 5 { rw evaluation_coevaluation, },
462+
simp,
463+
end
464+
465+
@[simp]
466+
lemma tensor_left_hom_equiv_tensor_id_comp_evaluation
467+
{X Y : C} [has_left_dual X] [has_left_dual Y] (f : X ⟶ Y) :
468+
(tensor_left_hom_equiv _ _ _ _) ((f ⊗ 𝟙 _) ≫ ε_ _ _) = (ᘁf) ≫ (ρ_ _).inv :=
469+
begin
470+
dsimp [tensor_left_hom_equiv, left_adjoint_mate],
471+
simp,
472+
end
473+
474+
@[simp]
475+
lemma tensor_right_hom_equiv_id_tensor_comp_evaluation
476+
{X Y : C} [has_right_dual X] [has_right_dual Y] (f : X ⟶ Y) :
477+
(tensor_right_hom_equiv _ _ _ _) ((𝟙 Yᘁ ⊗ f) ≫ ε_ _ _) = fᘁ ≫ (λ_ _).inv :=
478+
begin
479+
dsimp [tensor_right_hom_equiv, right_adjoint_mate],
480+
simp,
481+
end
482+
483+
@[simp]
484+
lemma tensor_right_hom_equiv_tensor_id_comp_evaluation
485+
{X Y : C} [has_right_dual X] (f : Y ⟶ Xᘁ) :
486+
(tensor_right_hom_equiv _ _ _ _) ((f ⊗ 𝟙 X) ≫ ε_ X Xᘁ) = f ≫ (λ_ _).inv :=
487+
begin
488+
dsimp [tensor_right_hom_equiv],
489+
rw comp_tensor_id,
490+
slice_lhs 3 4 { rw ←associator_inv_naturality, },
491+
slice_lhs 2 3 { rw [tensor_id, id_tensor_comp_tensor_id, ←tensor_id_comp_id_tensor], },
492+
slice_lhs 3 5 { rw coevaluation_evaluation, },
493+
simp,
494+
end
495+
496+
-- Next four lemmas passing `fᘁ` or `ᘁf` through (co)evaluations.
497+
498+
lemma coevaluation_comp_right_adjoint_mate
499+
{X Y : C} [has_right_dual X] [has_right_dual Y] (f : X ⟶ Y) :
500+
η_ Y Yᘁ ≫ (𝟙 _ ⊗ fᘁ) = η_ _ _ ≫ (f ⊗ 𝟙 _) :=
501+
begin
502+
apply_fun (tensor_left_hom_equiv _ Y Yᘁ _).symm,
503+
simp,
504+
end
505+
506+
lemma left_adjoint_mate_comp_evaluation
507+
{X Y : C} [has_left_dual X] [has_left_dual Y] (f : X ⟶ Y) :
508+
(𝟙 X ⊗ (ᘁf)) ≫ ε_ _ _ = (f ⊗ 𝟙 _) ≫ ε_ _ _ :=
509+
begin
510+
apply_fun (tensor_left_hom_equiv _ (ᘁX) X _),
511+
simp,
512+
end
513+
514+
lemma coevaluation_comp_left_adjoint_mate
515+
{X Y : C} [has_left_dual X] [has_left_dual Y] (f : X ⟶ Y) :
516+
η_ (ᘁY) Y ≫ ((ᘁf) ⊗ 𝟙 Y) = η_ (ᘁX) X ≫ (𝟙 (ᘁX) ⊗ f) :=
517+
begin
518+
apply_fun (tensor_right_hom_equiv _ (ᘁY) Y _).symm,
519+
simp,
520+
end
521+
522+
lemma right_adjoint_mate_comp_evaluation
523+
{X Y : C} [has_right_dual X] [has_right_dual Y] (f : X ⟶ Y) :
524+
(fᘁ ⊗ 𝟙 X) ≫ ε_ X Xᘁ = (𝟙 Yᘁ ⊗ f) ≫ ε_ Y Yᘁ :=
525+
begin
526+
apply_fun (tensor_right_hom_equiv _ X (Xᘁ) _),
527+
simp,
528+
end
529+
230530
/-- Transport an exact pairing across an isomorphism in the first argument. -/
231531
def exact_pairing_congr_left {X X' Y : C} [exact_pairing X' Y] (i : X ≅ X') : exact_pairing X Y :=
232532
{ evaluation := (𝟙 Y ⊗ i.hom) ≫ ε_ _ _,
@@ -318,6 +618,12 @@ class left_rigid_category (C : Type u) [category.{v} C] [monoidal_category.{v} C
318618
attribute [instance, priority 100] right_rigid_category.right_dual
319619
attribute [instance, priority 100] left_rigid_category.left_dual
320620

621+
@[priority 100]
622+
instance monoidal_closed_of_left_rigid_category
623+
(C : Type u) [category.{v} C] [monoidal_category.{v} C] [left_rigid_category C] :
624+
monoidal_closed C :=
625+
{ closed' := λ X, by apply_instance, }
626+
321627
/-- A rigid monoidal category is a monoidal category which is left rigid and right rigid. -/
322628
class rigid_category (C : Type u) [category.{v} C] [monoidal_category.{v} C]
323629
extends right_rigid_category C, left_rigid_category C

0 commit comments

Comments
 (0)