Skip to content

Commit ff28278

Browse files
arnoudvanderleerarnoudvanderleer
committed
Add the construction of an equivalence from a fully faithful and split essentially surjective functor
1 parent e0d9f01 commit ff28278

File tree

2 files changed

+263
-0
lines changed

2 files changed

+263
-0
lines changed

‎src/category-theory.lagda.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@ open import category-theory.embeddings-precategories public
5050
open import category-theory.endomorphisms-in-categories public
5151
open import category-theory.endomorphisms-in-precategories public
5252
open import category-theory.epimorphisms-in-large-precategories public
53+
open import category-theory.equivalence-from-fully-faithful-and-split-essentially-surjective-functor public
5354
open import category-theory.equivalences-of-categories public
5455
open import category-theory.equivalences-of-large-precategories public
5556
open import category-theory.equivalences-of-precategories public

‎src/category-theory/equivalence-from-fully-faithful-and-split-essentially-surjective-functor.lagda.md

Lines changed: 262 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,262 @@
1+
# File title
2+
3+
```agda
4+
module category-theory.equivalence-from-fully-faithful-and-split-essentially-surjective-functor where
5+
```
6+
7+
<details><summary>Imports</summary>
8+
9+
```agda
10+
open import category-theory.equivalences-of-precategories
11+
open import category-theory.fully-faithful-functors-precategories
12+
open import category-theory.functors-precategories
13+
open import category-theory.isomorphisms-in-precategories
14+
open import category-theory.maps-precategories
15+
open import category-theory.natural-isomorphisms-functors-precategories
16+
open import category-theory.natural-transformations-functors-precategories
17+
open import category-theory.precategories
18+
open import category-theory.split-essentially-surjective-functors-precategories
19+
20+
open import foundation.action-on-identifications-functions
21+
open import foundation.dependent-pair-types
22+
open import foundation.equivalences
23+
open import foundation.identity-types
24+
open import foundation.universe-levels
25+
```
26+
27+
</details>
28+
29+
## Idea
30+
31+
A functor `F : C → D` that is fully faithful (it induces equivalences
32+
`φ : C(c₁, c₂) ≃ D(F(c₁), F(c₂))` on homsets) and essentially surjective (for
33+
every `x : D`, we have some `G(x) : C` and an isomorphism `εₓ : F(G(x)) ≅ x`) is
34+
an equivalence of categories. The construction proceeds along the following
35+
lines:
36+
37+
- The inverse functor `G` sends objects `x : D` to `G(x) : C`;
38+
- Morpisms `f: D(x₁, x₂)` are sent to `φ⁻¹(εₓ₂⁻¹ ∘ f ∘ εₓ₁) : C(G(x₁), G(x₂))`;
39+
- The unit is given on `c : C` by the preimage along `φ` of `ε` at `F(c)`;
40+
- The counit is given on `x : D` by `εₓ`.
41+
42+
## Definition
43+
44+
```agda
45+
module _
46+
{l1 l2 : Level}
47+
(C D : Precategory l1 l2)
48+
(F : functor-Precategory C D)
49+
(HFF : is-fully-faithful-functor-Precategory C D F)
50+
(HES : is-split-essentially-surjective-functor-Precategory C D F)
51+
where
52+
53+
private
54+
infixl 10 _∘C_
55+
56+
_∘C_ : {x y z : obj-Precategory C}
57+
→ hom-Precategory C y z
58+
→ hom-Precategory C x y
59+
→ hom-Precategory C x z
60+
_∘C_ f g = comp-hom-Precategory C f g
61+
62+
infixl 10 _∘D_
63+
_∘D_ : {x y z : obj-Precategory D}
64+
→ hom-Precategory D y z
65+
→ hom-Precategory D x y
66+
→ hom-Precategory D x z
67+
_∘D_ f g = comp-hom-Precategory D f g
68+
69+
F₀ : obj-Precategory C → obj-Precategory D
70+
F₀ = obj-functor-Precategory C D F
71+
72+
F₁ : {x y : obj-Precategory C}
73+
→ hom-Precategory C x y
74+
→ hom-Precategory D (F₀ x) (F₀ y)
75+
F₁ = hom-functor-Precategory C D F
76+
77+
F₁⁻¹ : {x y : obj-Precategory C}
78+
→ hom-Precategory D (F₀ x) (F₀ y)
79+
→ hom-Precategory C x y
80+
F₁⁻¹ = map-inv-hom-is-fully-faithful-functor-Precategory C D F HFF
81+
82+
G : obj-Precategory D → obj-Precategory C
83+
G d = pr1 (HES d)
84+
85+
ε :
86+
(d : obj-Precategory D)
87+
→ iso-Precategory D (F₀ (G d)) d
88+
ε d = pr2 (HES d)
89+
90+
obj-functor-ff-es-equiv : obj-Precategory D → obj-Precategory C
91+
obj-functor-ff-es-equiv = G
92+
93+
hom-functor-ff-es-equiv :
94+
{x y : obj-Precategory D}
95+
→ hom-Precategory D x y
96+
→ hom-Precategory C (obj-functor-ff-es-equiv x) (obj-functor-ff-es-equiv y)
97+
hom-functor-ff-es-equiv {x} {y} f =
98+
F₁⁻¹ (hom-inv-iso-Precategory D (ε y) ∘D f ∘D hom-iso-Precategory D (ε x))
99+
100+
map-functor-ff-es-equiv : map-Precategory D C
101+
pr1 map-functor-ff-es-equiv = obj-functor-ff-es-equiv
102+
pr2 map-functor-ff-es-equiv = hom-functor-ff-es-equiv
103+
104+
opaque
105+
preserves-comp-hom-functor-ff-es-equiv :
106+
preserves-comp-hom-map-Precategory D C map-functor-ff-es-equiv
107+
preserves-comp-hom-functor-ff-es-equiv {x} {y} {z} g f = inv (
108+
fully-faithful-inv-preserves-comp C D F HFF _ _
109+
∙ ap F₁⁻¹ (
110+
associative-comp-hom-Precategory D _ _ _
111+
∙ ap (λ a → _ ∘D _ ∘D a)
112+
(inv (associative-comp-hom-Precategory D _ _ _))
113+
∙ ap (λ a → _ ∘D _ ∘D (a ∘D _))
114+
(inv (associative-comp-hom-Precategory D _ _ _))
115+
∙ ap (λ a → _ ∘D _ ∘D (a ∘D _ ∘D _))
116+
(is-section-hom-inv-iso-Precategory D (ε y))
117+
∙ ap (λ a → _ ∘D (a ∘D _))
118+
(left-unit-law-comp-hom-Precategory D _)
119+
∙ associative-comp-hom-Precategory D _ g _
120+
∙ ap (λ a → _ ∘D a)
121+
(inv (associative-comp-hom-Precategory D _ _ _))
122+
∙ inv (associative-comp-hom-Precategory D _ _ _)
123+
))
124+
125+
preserves-id-hom-functor-ff-es-equiv :
126+
preserves-id-hom-map-Precategory D C map-functor-ff-es-equiv
127+
preserves-id-hom-functor-ff-es-equiv x =
128+
ap F₁⁻¹ (
129+
ap (λ a → a ∘D _) (right-unit-law-comp-hom-Precategory D _)
130+
∙ is-retraction-hom-inv-iso-Precategory D (ε x)
131+
) ∙ inv (fully-faithful-inv-preserves-id C D F HFF _)
132+
133+
functor-ff-es-equiv : functor-Precategory D C
134+
pr1 functor-ff-es-equiv = obj-functor-ff-es-equiv
135+
pr1 (pr2 functor-ff-es-equiv) = hom-functor-ff-es-equiv
136+
pr1 (pr2 (pr2 functor-ff-es-equiv)) = preserves-comp-hom-functor-ff-es-equiv
137+
pr2 (pr2 (pr2 functor-ff-es-equiv)) = preserves-id-hom-functor-ff-es-equiv
138+
139+
module _
140+
(x : obj-Precategory C)
141+
where
142+
143+
iso-unit-ff-es-equiv :
144+
iso-Precategory C
145+
(obj-functor-Precategory C C
146+
(comp-functor-Precategory C D C functor-ff-es-equiv F) x)
147+
x
148+
iso-unit-ff-es-equiv =
149+
(is-essentially-injective-is-fully-faithful-functor-Precategory
150+
C D F HFF _ _ (ε (F₀ x)))
151+
152+
hom-unit-ff-es-equiv :
153+
hom-Precategory C
154+
(obj-functor-Precategory C C
155+
(comp-functor-Precategory C D C functor-ff-es-equiv F) x)
156+
x
157+
hom-unit-ff-es-equiv = hom-iso-Precategory C iso-unit-ff-es-equiv
158+
159+
is-iso-unit-ff-es-equiv : is-iso-Precategory C hom-unit-ff-es-equiv
160+
is-iso-unit-ff-es-equiv = is-iso-iso-Precategory C iso-unit-ff-es-equiv
161+
162+
opaque
163+
is-natural-unit-ff-es-equiv :
164+
is-natural-transformation-Precategory C C
165+
(comp-functor-Precategory C D C functor-ff-es-equiv F)
166+
(id-functor-Precategory C)
167+
hom-unit-ff-es-equiv
168+
is-natural-unit-ff-es-equiv {x} {y} f = equational-reasoning
169+
f ∘C hom-unit-ff-es-equiv x
170+
＝ F₁⁻¹ (F₁ f) ∘C hom-unit-ff-es-equiv x
171+
by ap (λ a → a ∘C _)
172+
(inv (is-retraction-map-section-is-equiv (HFF _ _) f))
173+
＝ F₁⁻¹ (F₁ f ∘D (hom-iso-Precategory D (ε (F₀ x))))
174+
by fully-faithful-inv-preserves-comp C D F HFF _ _
175+
＝ F₁⁻¹ (
176+
(id-hom-Precategory D)
177+
∘D (F₁ f)
178+
∘D (hom-iso-Precategory D (ε (F₀ x))))
179+
by ap (λ a → F₁⁻¹ (a ∘D _))
180+
(inv (left-unit-law-comp-hom-Precategory D _))
181+
＝ F₁⁻¹ (
182+
(hom-iso-Precategory D (ε (F₀ y)))
183+
∘D (hom-inv-iso-Precategory D (ε (F₀ y)))
184+
∘D (F₁ f)
185+
∘D (hom-iso-Precategory D (ε (F₀ x))))
186+
by ap (λ a → F₁⁻¹ (a ∘D _ ∘D _))
187+
(inv (is-section-hom-inv-iso-Precategory D (ε (F₀ y))))
188+
＝ F₁⁻¹ (
189+
(hom-iso-Precategory D (ε (F₀ y)))
190+
∘D (
191+
(hom-inv-iso-Precategory D (ε (F₀ y)))
192+
∘D (F₁ f)
193+
∘D (hom-iso-Precategory D (ε (F₀ x)))))
194+
by ap F₁⁻¹ (
195+
associative-comp-hom-Precategory D _ _ _
196+
∙ associative-comp-hom-Precategory D _ _ _
197+
∙ ap (λ a → _ ∘D a) (inv (associative-comp-hom-Precategory D _ _ _)))
198+
＝ (hom-unit-ff-es-equiv y) ∘C (hom-functor-ff-es-equiv (F₁ f))
199+
by inv (fully-faithful-inv-preserves-comp C D F HFF _ _)
200+
201+
unit-ff-es-equiv :
202+
natural-isomorphism-Precategory C C
203+
(comp-functor-Precategory C D C functor-ff-es-equiv F)
204+
(id-functor-Precategory C)
205+
pr1 (pr1 unit-ff-es-equiv) = hom-unit-ff-es-equiv
206+
pr2 (pr1 unit-ff-es-equiv) = is-natural-unit-ff-es-equiv
207+
pr2 unit-ff-es-equiv = is-iso-unit-ff-es-equiv
208+
209+
hom-counit-ff-es-equiv :
210+
(d : obj-Precategory D)
211+
→ hom-Precategory D
212+
(obj-functor-Precategory D D
213+
(comp-functor-Precategory D C D F functor-ff-es-equiv) d) d
214+
hom-counit-ff-es-equiv d = hom-iso-Precategory D (ε d)
215+
216+
is-iso-counit-ff-es-equiv :
217+
(d : obj-Precategory D)
218+
→ is-iso-Precategory D (hom-counit-ff-es-equiv d)
219+
is-iso-counit-ff-es-equiv d = is-iso-iso-Precategory D (ε d)
220+
221+
opaque
222+
is-natural-counit-ff-es-equiv :
223+
is-natural-transformation-Precategory D D
224+
(comp-functor-Precategory D C D F functor-ff-es-equiv)
225+
(id-functor-Precategory D)
226+
hom-counit-ff-es-equiv
227+
is-natural-counit-ff-es-equiv {x} {y} f = equational-reasoning
228+
f ∘D (hom-counit-ff-es-equiv x)
229+
＝ (id-hom-Precategory D) ∘D f ∘D (hom-counit-ff-es-equiv x)
230+
by ap (λ a → a ∘D _) (inv (left-unit-law-comp-hom-Precategory D f))
231+
＝ (hom-iso-Precategory D (ε y))
232+
∘D (hom-inv-iso-Precategory D (ε y))
233+
∘D f
234+
∘D (hom-counit-ff-es-equiv x)
235+
by ap (λ a → a ∘D _ ∘D _)
236+
(inv (is-section-hom-inv-iso-Precategory D (ε y)))
237+
＝ (hom-iso-Precategory D (ε y))
238+
∘D (
239+
(hom-inv-iso-Precategory D (ε y))
240+
∘D f
241+
∘D (hom-iso-Precategory D (ε x)))
242+
by associative-comp-hom-Precategory D _ _ _
243+
∙ associative-comp-hom-Precategory D _ _ _
244+
∙ ap (λ a → _ ∘D a) (inv (associative-comp-hom-Precategory D _ _ _))
245+
＝ (hom-counit-ff-es-equiv y) ∘D (F₁ (hom-functor-ff-es-equiv f))
246+
by ap (λ a → _ ∘D a) (inv (is-section-map-section-is-equiv (HFF _ _) _))
247+
248+
counit-ff-es-equiv :
249+
natural-isomorphism-Precategory D D
250+
(comp-functor-Precategory D C D F functor-ff-es-equiv)
251+
(id-functor-Precategory D)
252+
pr1 (pr1 counit-ff-es-equiv) = hom-counit-ff-es-equiv
253+
pr2 (pr1 counit-ff-es-equiv) = is-natural-counit-ff-es-equiv
254+
pr2 counit-ff-es-equiv = is-iso-counit-ff-es-equiv
255+
256+
result : equiv-Precategory C D
257+
pr1 result = F
258+
pr1 (pr1 (pr2 result)) = functor-ff-es-equiv
259+
pr2 (pr1 (pr2 result)) = unit-ff-es-equiv
260+
pr1 (pr2 (pr2 result)) = functor-ff-es-equiv
261+
pr2 (pr2 (pr2 result)) = counit-ff-es-equiv
262+
```

0 commit comments

Comments
 (0)