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

Commit e245254

Browse files
kim-emkim-em
committed
feat(category_theory/monoidal): λ_ (𝟙_ C) = ρ_ (𝟙_ C) (#3556)
The incredibly tedious proof from the axioms that `λ_ (𝟙_ C) = ρ_ (𝟙_ C)` in any monoidal category. One would hope that it falls out from a coherence theorem, but we're not close to having one, and I suspect that this result might be a step in any proof. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent 2e6c488 commit e245254

File tree

2 files changed

+161
-0
lines changed

2 files changed

+161
-0
lines changed

‎src/category_theory/monoidal/category.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -159,6 +159,14 @@ begin
159159
rw [right_unitor_naturality, ←category.assoc, iso.inv_hom_id, category.id_comp]
160160
end
161161

162+
@[simp]
163+
lemma right_unitor_conjugation {X Y : C} (f : X ⟶ Y) : (ρ_ X).inv ≫ (f ⊗ (𝟙 (𝟙_ C))) ≫ (ρ_ Y).hom = f :=
164+
by rw [right_unitor_naturality, ←category.assoc, iso.inv_hom_id, category.id_comp]
165+
166+
@[simp]
167+
lemma left_unitor_conjugation {X Y : C} (f : X ⟶ Y) : (λ_ X).inv ≫ ((𝟙 (𝟙_ C)) ⊗ f) ≫ (λ_ Y).hom = f :=
168+
by rw [left_unitor_naturality, ←category.assoc, iso.inv_hom_id, category.id_comp]
169+
162170
@[simp] lemma tensor_left_iff
163171
{X Y : C} (f g : X ⟶ Y) :
164172
((𝟙 (𝟙_ C)) ⊗ f = (𝟙 (𝟙_ C)) ⊗ g) ↔ (f = g) :=

‎src/category_theory/monoidal/unitors.lean‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
/-
2+
Copyright (c) 2020 Scott Morrison. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Scott Morrison
5+
-/
6+
import category_theory.monoidal.category
7+
8+
/-!
9+
# The two morphisms `λ_ (𝟙_ C)` and `ρ_ (𝟙_ C)` from `𝟙_ C ⊗ 𝟙_ C` to `𝟙_ C` are equal.
10+
11+
This is suprisingly difficult to prove directly from the usual axioms for a monoidal category!
12+
13+
This proof follows the diagram given at
14+
https://people.math.osu.edu/penneys.2/QS2019/VicaryHandout.pdf
15+
16+
It should be a consequence of the coherence theorem for monoidal categories
17+
(although quite possibly it is a necessary building block of any proof).
18+
-/
19+
20+
universes v u
21+
22+
namespace category_theory.monoidal_category
23+
24+
open category_theory
25+
open category_theory.category
26+
open category_theory.monoidal_category
27+
28+
variables {C : Type u} [category.{v} C] [monoidal_category.{v} C]
29+
30+
namespace unitors_equal
31+
32+
lemma cells_1_2 :
33+
(ρ_ (𝟙_ C)).hom =
34+
(λ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv ≫ ((𝟙 (𝟙_ C)) ⊗ (ρ_ (𝟙_ C)).hom) ≫ (λ_ (𝟙_ C)).hom :=
35+
by rw [left_unitor_conjugation]
36+
37+
lemma cells_4 :
38+
(λ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv ≫ ((𝟙 (𝟙_ C)) ⊗ ((λ_ (𝟙_ C)).hom)) =
39+
(λ_ (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).inv :=
40+
by rw [←left_unitor_inv_naturality, iso.hom_inv_id]
41+
42+
lemma cells_4' :
43+
(λ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv =
44+
(λ_ (𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).inv ≫ ((𝟙 (𝟙_ C)) ⊗ ((λ_ (𝟙_ C)).inv)) :=
45+
by rw [←assoc, ←cells_4, assoc, ←id_tensor_comp, iso.hom_inv_id, tensor_id, comp_id]
46+
47+
lemma cells_3_4 :
48+
(λ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv = (𝟙 (𝟙_ C)) ⊗ ((λ_ (𝟙_ C)).inv) :=
49+
by rw [cells_4', ←assoc, iso.hom_inv_id, id_comp]
50+
51+
lemma cells_1_4 :
52+
(ρ_ (𝟙_ C)).hom =
53+
((𝟙 (𝟙_ C)) ⊗ ((λ_ (𝟙_ C)).inv)) ≫ ((𝟙 (𝟙_ C)) ⊗ (ρ_ (𝟙_ C)).hom) ≫ (λ_ (𝟙_ C)).hom :=
54+
begin
55+
rw [←cells_3_4],
56+
conv_lhs { rw [cells_1_2] },
57+
end
58+
59+
lemma cells_6 :
60+
((ρ_ (𝟙_ C)).inv ⊗ (𝟙 (𝟙_ C))) ≫ (ρ_ ((𝟙_ C) ⊗ (𝟙_ C))).hom =
61+
(ρ_ (𝟙_ C)).hom ≫ (ρ_ (𝟙_ C)).inv :=
62+
by rw [right_unitor_naturality, iso.hom_inv_id]
63+
64+
lemma cells_6' :
65+
((ρ_ (𝟙_ C)).inv ⊗ (𝟙 (𝟙_ C))) =
66+
(ρ_ (𝟙_ C)).hom ≫ (ρ_ (𝟙_ C)).inv ≫ (ρ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv :=
67+
by {rw [←assoc, ←cells_6, assoc, iso.hom_inv_id, comp_id], }
68+
69+
lemma cells_5_6 : ((ρ_ (𝟙_ C)).inv ⊗ (𝟙 (𝟙_ C))) = (ρ_ (𝟙_ C ⊗ 𝟙_ C)).inv :=
70+
by rw [cells_6', ←assoc, iso.hom_inv_id, id_comp]
71+
72+
lemma cells_7 :
73+
((𝟙 (𝟙_ C)) ⊗ ((λ_ (𝟙_ C)).inv)) =
74+
((ρ_ (𝟙_ C)).inv ⊗ (𝟙 (𝟙_ C))) ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom :=
75+
by simp only [triangle_assoc_comp_right_inv, tensor_left_iff]
76+
77+
lemma cells_1_7 :
78+
(ρ_ (𝟙_ C)).hom =
79+
(ρ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv ≫ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ≫
80+
((𝟙 (𝟙_ C)) ⊗ (ρ_ (𝟙_ C)).hom) ≫ (λ_ (𝟙_ C)).hom :=
81+
begin
82+
conv_lhs { rw [cells_1_4] },
83+
conv_lhs { congr, rw [cells_7] },
84+
conv_lhs { congr, congr, rw [cells_5_6] },
85+
conv_rhs { rw [←assoc] }
86+
end
87+
88+
lemma cells_8 :
89+
(α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom =
90+
(ρ_ (((𝟙_ C) ⊗ (𝟙_ C)) ⊗ (𝟙_ C))).inv ≫ ((α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) ≫
91+
(ρ_ ((𝟙_ C) ⊗ ((𝟙_ C) ⊗ (𝟙_ C)))).hom :=
92+
by rw [right_unitor_conjugation].
93+
94+
lemma cells_14 :
95+
(ρ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv ≫ (ρ_ (((𝟙_ C) ⊗ (𝟙_ C)) ⊗ (𝟙_ C))).inv =
96+
(ρ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv ≫ ((ρ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv ⊗ (𝟙 (𝟙_ C))) :=
97+
by rw [right_unitor_inv_naturality]
98+
99+
lemma cells_9 :
100+
((α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) =
101+
(α_ ((𝟙_ C) ⊗ (𝟙_ C)) (𝟙_ C) (𝟙_ C)).hom ≫ (α_ (𝟙_ C) (𝟙_ C) ((𝟙_ C) ⊗ (𝟙_ C))).hom ≫
102+
((𝟙 (𝟙_ C)) ⊗ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).inv) ≫ (α_ (𝟙_ C) ((𝟙_ C) ⊗ (𝟙_ C)) (𝟙_ C)).inv :=
103+
begin
104+
slice_rhs 1 2 { rw ←(monoidal_category.pentagon (𝟙_ C) (𝟙_ C) (𝟙_ C) (𝟙_ C)) },
105+
slice_rhs 3 4 { rw [←id_tensor_comp, iso.hom_inv_id], },
106+
simp,
107+
end
108+
109+
lemma cells_10_13 :
110+
((ρ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv ⊗ (𝟙 (𝟙_ C))) ≫ (α_ ((𝟙_ C) ⊗ (𝟙_ C)) (𝟙_ C) (𝟙_ C)).hom ≫
111+
(α_ (𝟙_ C) (𝟙_ C) ((𝟙_ C) ⊗ (𝟙_ C))).hom ≫ ((𝟙 (𝟙_ C)) ⊗ (α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).inv) ≫
112+
(α_ (𝟙_ C) ((𝟙_ C) ⊗ (𝟙_ C)) (𝟙_ C)).inv =
113+
((𝟙 (𝟙_ C)) ⊗ (ρ_ (𝟙_ C)).inv) ⊗ (𝟙 (𝟙_ C)) :=
114+
begin
115+
slice_lhs 1 2 { simp, },
116+
slice_lhs 1 2 { rw [←tensor_id, associator_naturality], },
117+
slice_lhs 2 3 { rw [←id_tensor_comp], simp, },
118+
slice_lhs 1 2 { rw ←associator_naturality, },
119+
simp,
120+
end
121+
122+
lemma cells_9_13 :
123+
((ρ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv ⊗ (𝟙 (𝟙_ C))) ≫ ((α_ (𝟙_ C) (𝟙_ C) (𝟙_ C)).hom ⊗ 𝟙 (𝟙_ C)) =
124+
((𝟙 (𝟙_ C)) ⊗ (ρ_ (𝟙_ C)).inv) ⊗ (𝟙 (𝟙_ C)) :=
125+
begin
126+
rw [cells_9, ←cells_10_13]
127+
end
128+
129+
lemma cells_15 :
130+
(ρ_ ((𝟙_ C) ⊗ (𝟙_ C))).inv ≫ (((𝟙 (𝟙_ C)) ⊗ (ρ_ (𝟙_ C)).inv) ⊗ (𝟙 (𝟙_ C))) ≫
131+
(ρ_ ((𝟙_ C) ⊗ ((𝟙_ C) ⊗ (𝟙_ C)))).hom ≫ ((𝟙 (𝟙_ C)) ⊗ (ρ_ (𝟙_ C)).hom) =
132+
𝟙 _ :=
133+
begin
134+
slice_lhs 1 2 { rw [←right_unitor_inv_naturality] },
135+
slice_lhs 2 3 { rw [iso.inv_hom_id] },
136+
rw [id_comp, ←id_tensor_comp, iso.inv_hom_id, tensor_id],
137+
end
138+
139+
end unitors_equal
140+
141+
open unitors_equal
142+
143+
lemma unitors_equal : (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom :=
144+
begin
145+
rw cells_1_7,
146+
rw cells_8,
147+
slice_rhs 1 2 { rw cells_14 },
148+
slice_rhs 2 3 { rw cells_9_13 },
149+
slice_rhs 1 4 { rw cells_15 },
150+
rw id_comp,
151+
end
152+
153+
end category_theory.monoidal_category

0 commit comments

Comments
 (0)