Skip to content

Commit 7622f00

Browse files
callesonnecallesonne
committed
feat(Bicategory/Opposites): add 1-cell opposite bicategory (#25901)
This PR adds the 1-cell opposite bicategory, where only the 1-morphisms are reversed.
1 parent 0a5a3f8 commit 7622f00

File tree

3 files changed

+268
-13
lines changed

3 files changed

+268
-13
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2173,6 +2173,7 @@ import Mathlib.CategoryTheory.Bicategory.Monad.Basic
21732173
import Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
21742174
import Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
21752175
import Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Strong
2176+
import Mathlib.CategoryTheory.Bicategory.Opposites
21762177
import Mathlib.CategoryTheory.Bicategory.SingleObj
21772178
import Mathlib.CategoryTheory.Bicategory.Strict
21782179
import Mathlib.CategoryTheory.Bicategory.Strict.Basic

‎Mathlib/CategoryTheory/Bicategory/Opposites.lean‎

Lines changed: 227 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,227 @@
1+
/-
2+
Copyright (c) 2025 Calle Sönne. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Calle Sönne
5+
-/
6+
7+
import Mathlib.CategoryTheory.Bicategory.Basic
8+
import Mathlib.CategoryTheory.Opposites
9+
10+
/-!
11+
# Opposite bicategories
12+
13+
We construct the 1-cell opposite of a bicategory `B`, called `Bᵒᵖ`. It is defined as follows
14+
* The objects of `Bᵒᵖ` correspond to objects of `B`.
15+
* The morphisms `X ⟶ Y` in `Bᵒᵖ` are the morphisms `Y ⟶ X` in `B`.
16+
* The 2-morphisms `f ⟶ g` in `Bᵒᵖ` are the 2-morphisms `f ⟶ g` in `B`. In other words, the
17+
directions of the 2-morphisms are preserved.
18+
19+
# Remarks
20+
There are multiple notions of opposite categories for bicategories.
21+
- There is 1-cell dual `Bᵒᵖ` as defined above.
22+
- There is the 2-cell dual, `Cᶜᵒ` where only the natural transformations are reversed
23+
- There is the bi-dual `Cᶜᵒᵒᵖ` where the directions of both the morphisms and the natural
24+
transformations are reversed.
25+
26+
## TODO
27+
28+
* Define the 2-cell dual `Cᶜᵒ`.
29+
* Provide various lemmas for going between `LocallyDiscrete Cᵒᵖ` and `(LocallyDiscrete C)ᵒᵖ`.
30+
31+
Note: `Cᶜᵒᵒᵖ` is WIP by Christian Merten.
32+
33+
-/
34+
35+
universe w v u
36+
37+
open CategoryTheory Bicategory Opposite
38+
39+
namespace Bicategory.Opposite
40+
41+
variable {B : Type u} [Bicategory.{w, v} B]
42+
43+
/-- Type synonym for 2-morphisms in the opposite bicategory. -/
44+
structure Hom2 {a b : Bᵒᵖ} (f g : a ⟶ b) where
45+
op2' ::
46+
/-- `Bᵒᵖ` preserves the direction of all 2-morphisms in `B` -/
47+
unop2 : f.unop ⟶ g.unop
48+
49+
open Hom2
50+
51+
@[simps!]
52+
instance homCategory (a b : Bᵒᵖ) : Category.{w} (a ⟶ b) where
53+
Hom f g := Hom2 f g
54+
id f := op2' (𝟙 f.unop)
55+
comp η θ := op2' (η.unop2 ≫ θ.unop2)
56+
57+
/-- Synonym for constructor of `Hom2` where the 1-morphisms `f` and `g` lie in `B` and not `Bᵒᵖ`. -/
58+
def op2 {a b : B} {f g : a ⟶ b} (η : f ⟶ g) : f.op ⟶ g.op :=
59+
op2' η
60+
61+
@[simp]
62+
theorem unop2_op2 {a b : B} {f g : a ⟶ b} (η : f ⟶ g) : (op2 η).unop2 = η :=
63+
rfl
64+
65+
@[simp]
66+
theorem op2_unop2 {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f ⟶ g) : op2 η.unop2 = η :=
67+
rfl
68+
69+
@[simp]
70+
theorem op2_comp {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) :
71+
op2 (η ≫ θ) = (op2 η) ≫ (op2 θ) :=
72+
rfl
73+
74+
@[simp]
75+
theorem op2_id {a b : B} {f : a ⟶ b} : op2 (𝟙 f) = 𝟙 f.op :=
76+
rfl
77+
78+
@[simp]
79+
theorem unop2_comp {a b : Bᵒᵖ} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) :
80+
unop2 (η ≫ θ) = unop2 η ≫ unop2 θ :=
81+
rfl
82+
83+
@[simp]
84+
theorem unop2_id {a b : Bᵒᵖ} {f : a ⟶ b} : unop2 (𝟙 f) = 𝟙 f.unop :=
85+
rfl
86+
87+
@[simp]
88+
theorem unop2_id_bop {a b : B} {f : a ⟶ b} : unop2 (𝟙 f.op) = 𝟙 f :=
89+
rfl
90+
91+
@[simp]
92+
theorem op2_id_unbop {a b : Bᵒᵖ} {f : a ⟶ b} : op2 (𝟙 f.unop) = 𝟙 f :=
93+
rfl
94+
95+
/-- The natural functor from the hom-category `a ⟶ b` in `B` to its bicategorical opposite
96+
`bop b ⟶ bop a`. -/
97+
@[simps]
98+
def opFunctor (a b : B) : (a ⟶ b) ⥤ (op b ⟶ op a) where
99+
obj f := f.op
100+
map η := op2 η
101+
102+
/-- The functor from the hom-category `a ⟶ b` in `Bᵒᵖ` to its bicategorical opposite
103+
`unop b ⟶ unop a`. -/
104+
@[simps]
105+
def unopFunctor (a b : Bᵒᵖ) : (a ⟶ b) ⥤ (unop b ⟶ unop a) where
106+
obj f := f.unop
107+
map η := unop2 η
108+
109+
end Bicategory.Opposite
110+
111+
namespace CategoryTheory.Iso
112+
113+
open Bicategory.Opposite
114+
115+
variable {B : Type u} [Bicategory.{w, v} B]
116+
117+
/-- A 2-isomorphism in `B` gives a 2-isomorphism in `Bᵒᵖ` -/
118+
@[simps!]
119+
abbrev op2 {a b : B} {f g : a ⟶ b} (η : f ≅ g) : f.op ≅ g.op := (opFunctor a b).mapIso η
120+
121+
/-- A 2-isomorphism in `B` gives a 2-isomorphism in `Bᵒᵖ` -/
122+
@[simps!]
123+
abbrev op2_unop {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f.unop ≅ g.unop) : f ≅ g :=
124+
(opFunctor b.unop a.unop).mapIso η
125+
126+
/-- A 2-isomorphism in `Bᵒᵖ` gives a 2-isomorphism in `B` -/
127+
@[simps!]
128+
abbrev unop2 {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f ≅ g) : f.unop ≅ g.unop :=
129+
(unopFunctor a b).mapIso η
130+
131+
/-- A 2-isomorphism in `Bᵒᵖ` gives a 2-isomorphism in `B` -/
132+
@[simps!]
133+
abbrev unop2_op {a b : B} {f g : a ⟶ b} (η : f.op ≅ g.op) : f ≅ g :=
134+
(unopFunctor (op b) (op a)).mapIso η
135+
136+
@[simp]
137+
theorem unop2_op2 {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f ≅ g) : η.unop2.op2 = η := rfl
138+
139+
end CategoryTheory.Iso
140+
141+
namespace Bicategory.Opposite
142+
143+
open Hom2
144+
145+
variable {B : Type u} [Bicategory.{w, v} B]
146+
147+
/-- The 1-cell dual bicategory `Bᵒᵖ`.
148+
149+
It is defined as follows.
150+
* The objects of `Bᵒᵖ` correspond to objects of `B`.
151+
* The morphisms `X ⟶ Y` in `Bᵒᵖ` are the morphisms `Y ⟶ X` in `B`.
152+
* The 2-morphisms `f ⟶ g` in `Bᵒᵖ` are the 2-morphisms `f ⟶ g` in `B`. In other words, the
153+
directions of the 2-morphisms are preserved.
154+
-/
155+
@[simps! homCategory_id_unop2 homCategory_comp_unop2 whiskerLeft_unop2 whiskerRight_unop2
156+
associator_hom_unop2 associator_inv_unop2 leftUnitor_hom_unop2 leftUnitor_inv_unop2
157+
rightUnitor_hom_unop2 rightUnitor_inv_unop2]
158+
instance bicategory : Bicategory.{w, v} Bᵒᵖ where
159+
homCategory := homCategory
160+
whiskerLeft f g h η := op2 <| (unop2 η) ▷ f.unop
161+
whiskerRight η h := op2 <| h.unop ◁ unop2 η
162+
associator f g h := (associator h.unop g.unop f.unop).op2_unop.symm
163+
leftUnitor f := (rightUnitor f.unop).op2_unop
164+
rightUnitor f := (leftUnitor f.unop).op2_unop
165+
whisker_exchange η θ := congrArg op2 <| (whisker_exchange _ _).symm
166+
whisker_assoc f g g' η i := congrArg op2 <| by simp
167+
pentagon f g h i := congrArg op2 <| by simp
168+
triangle f g := congrArg op2 <| by simp
169+
170+
@[simp]
171+
lemma op2_whiskerLeft {a b c : B} {f : a ⟶ b} {g g' : b ⟶ c} (η : g ⟶ g') :
172+
op2 (f ◁ η) = (op2 η) ▷ f.op :=
173+
rfl
174+
175+
@[simp]
176+
lemma op2_whiskerRight {a b c : B} {f f' : a ⟶ b} {g : b ⟶ c} (η : f ⟶ f') :
177+
op2 (η ▷ g) = g.op ◁ (op2 η) :=
178+
rfl
179+
180+
@[simp]
181+
lemma op2_associator {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
182+
(α_ f g h).op2 = (α_ h.op g.op f.op).symm :=
183+
rfl
184+
185+
@[simp]
186+
lemma op2_associator_hom {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
187+
op2 (α_ f g h).hom = (α_ h.op g.op f.op).symm.hom :=
188+
rfl
189+
190+
@[simp]
191+
lemma op2_associator_inv {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
192+
op2 (α_ f g h).inv = (α_ h.op g.op f.op).symm.inv :=
193+
rfl
194+
195+
@[simp]
196+
lemma op2_leftUnitor {a b : B} (f : a ⟶ b) :
197+
(λ_ f).op2 = ρ_ f.op :=
198+
rfl
199+
200+
@[simp]
201+
lemma op2_leftUnitor_hom {a b : B} (f : a ⟶ b) :
202+
op2 (λ_ f).hom = (ρ_ f.op).hom :=
203+
rfl
204+
205+
@[simp]
206+
lemma op2_leftUnitor_inv {a b : B} (f : a ⟶ b) :
207+
op2 (λ_ f).inv = (ρ_ f.op).inv :=
208+
rfl
209+
210+
@[simp]
211+
lemma op2_rightUnitor {a b : B} (f : a ⟶ b) :
212+
(ρ_ f).op2 = λ_ f.op :=
213+
rfl
214+
215+
@[simp]
216+
lemma op2_rightUnitor_hom {a b : B} (f : a ⟶ b) :
217+
op2 (ρ_ f).hom = (λ_ f.op).hom :=
218+
rfl
219+
220+
@[simp]
221+
lemma op2_rightUnitor_inv {a b : B} (f : a ⟶ b) :
222+
op2 (ρ_ f).inv = (λ_ f.op).inv :=
223+
rfl
224+
225+
end Opposite
226+
227+
end Bicategory

‎Mathlib/CategoryTheory/Opposites.lean‎

Lines changed: 40 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -58,40 +58,67 @@ end Quiver
5858

5959
namespace CategoryTheory
6060

61-
open Functor
61+
section
6262

63-
variable [Category.{v₁} C]
63+
variable [CategoryStruct.{v₁} C]
6464

65-
/-- The opposite category. -/
66-
@[stacks 001M]
67-
instance Category.opposite : Category.{v₁} Cᵒᵖ where
65+
/-- The opposite `CategoryStruct`. -/
66+
instance CategoryStruct.opposite : CategoryStruct.{v₁} Cᵒᵖ where
6867
comp f g := (g.unop ≫ f.unop).op
6968
id X := (𝟙 (unop X)).op
7069

71-
@[simp, reassoc]
72-
theorem op_comp {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g).op = g.op ≫ f.op :=
70+
@[simp]
71+
theorem unop_id {X : Cᵒᵖ} : (𝟙 X).unop = 𝟙 (unop X) :=
7372
rfl
7473

7574
@[simp]
76-
theorem op_id {X : C} : (𝟙 X).op = 𝟙 (op X) :=
75+
theorem op_id_unop {X : Cᵒᵖ} : (𝟙 (unop X)).op = 𝟙 X :=
7776
rfl
7877

79-
@[simp, reassoc]
80-
theorem unop_comp {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g).unop = g.unop ≫ f.unop :=
78+
@[simp]
79+
theorem op_comp {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g).op = g.op ≫ f.op :=
8180
rfl
8281

8382
@[simp]
84-
theorem unop_id {X : Cᵒᵖ} : (𝟙 X).unop = 𝟙 (unop X) :=
83+
theorem op_id {X : C} : (𝟙 X).op = 𝟙 (op X) :=
8584
rfl
8685

8786
@[simp]
88-
theorem unop_id_op {X : C} : (𝟙 (op X)).unop = 𝟙 X :=
87+
theorem unop_comp {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g).unop = g.unop ≫ f.unop :=
8988
rfl
9089

9190
@[simp]
92-
theorem op_id_unop {X : Cᵒᵖ} : (𝟙 (unop X)).op = 𝟙 X :=
91+
theorem unop_id_op {X : C} : (𝟙 (op X)).unop = 𝟙 X :=
9392
rfl
9493

94+
-- This lemma is needed to prove `Category.opposite` below.
95+
theorem op_comp_unop {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) : (g.unop ≫ f.unop).op = f ≫ g :=
96+
rfl
97+
98+
end
99+
100+
open Functor
101+
102+
variable [Category.{v₁} C]
103+
104+
/-- The opposite category. -/
105+
@[stacks 001M]
106+
instance Category.opposite : Category.{v₁} Cᵒᵖ where
107+
__ := CategoryStruct.opposite
108+
comp_id f := by rw [← op_comp_unop, unop_id, id_comp, Quiver.Hom.op_unop]
109+
id_comp f := by rw [← op_comp_unop, unop_id, comp_id, Quiver.Hom.op_unop]
110+
assoc f g h := by simp only [← op_comp_unop, Quiver.Hom.unop_op, assoc]
111+
112+
-- Note: these need to be proven manually as the original lemmas are only stated in terms
113+
-- of `CategoryStruct`s!
114+
theorem op_comp_assoc {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {Z' : Cᵒᵖ} {h : op X ⟶ Z'} :
115+
(f ≫ g).op ≫ h = g.op ≫ f.op ≫ h := by
116+
simp only [op_comp, Category.assoc]
117+
118+
theorem unop_comp_assoc {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} {Z' : C} {h : unop X ⟶ Z'} :
119+
(f ≫ g).unop ≫ h = g.unop ≫ f.unop ≫ h := by
120+
simp only [unop_comp, Category.assoc]
121+
95122
section
96123

97124
variable (C)

0 commit comments

Comments
 (0)