/
evaluation.lean
155 lines (131 loc) · 4.73 KB
/
evaluation.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
/-
Copyright (c) 2021 Adam Topaz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam Topaz
-/
import category_theory.limits.shapes.products
import category_theory.functor.epi_mono
/-!
# Adjunctions involving evaluation
We show that evaluation of functors have adjoints, given the existence of (co)products.
-/
namespace category_theory
open category_theory.limits
universes v₁ v₂ u₁ u₂
variables {C : Type u₁} [category.{v₁} C] (D : Type u₂) [category.{v₂} D]
noncomputable theory
section
variables [∀ (a b : C), has_coproducts_of_shape (a ⟶ b) D]
/-- The left adjoint of evaluation. -/
@[simps]
def evaluation_left_adjoint (c : C) : D ⥤ C ⥤ D :=
{ obj := λ d,
{ obj := λ t, ∐ (λ i : c ⟶ t, d),
map := λ u v f, sigma.desc $ λ g, sigma.ι (λ _, d) $ g ≫ f,
map_id' := begin
intros, ext ⟨j⟩, simp only [cofan.mk_ι_app, colimit.ι_desc, category.comp_id],
congr' 1, rw category.comp_id,
end,
map_comp' := begin
intros, ext, simp only [cofan.mk_ι_app, colimit.ι_desc_assoc, colimit.ι_desc],
congr' 1, rw category.assoc,
end },
map := λ d₁ d₂ f,
{ app := λ e, sigma.desc $ λ h, f ≫ sigma.ι (λ _, d₂) h,
naturality' := by { intros, ext, dsimp, simp } },
map_id' := by { intros, ext x ⟨j⟩, dsimp, simp },
map_comp' := by { intros, ext, dsimp, simp } }
/-- The adjunction showing that evaluation is a right adjoint. -/
@[simps unit_app counit_app_app]
def evaluation_adjunction_right (c : C) :
evaluation_left_adjoint D c ⊣ (evaluation _ _).obj c :=
adjunction.mk_of_hom_equiv
{ hom_equiv := λ d F,
{ to_fun := λ f, sigma.ι (λ _, d) (𝟙 _) ≫ f.app c,
inv_fun := λ f,
{ app := λ e, sigma.desc $ λ h, f ≫ F.map h,
naturality' := by { intros, ext, dsimp, simp } },
left_inv := begin
intros f,
ext x ⟨g⟩,
dsimp,
simp only [colimit.ι_desc, limits.cofan.mk_ι_app, category.assoc, ← f.naturality,
evaluation_left_adjoint_obj_map, colimit.ι_desc_assoc, cofan.mk_ι_app],
congr' 2,
rw category.id_comp
end,
right_inv := λ f, by { dsimp, simp } },
hom_equiv_naturality_left_symm' := by { intros, ext, dsimp, simp },
hom_equiv_naturality_right' := by { intros, dsimp, simp } }
instance evaluation_is_right_adjoint (c : C) :
is_right_adjoint ((evaluation _ D).obj c) :=
⟨_, evaluation_adjunction_right _ _⟩
lemma nat_trans.mono_iff_app_mono {F G : C ⥤ D} (η : F ⟶ G) :
mono η ↔ (∀ c, mono (η.app c)) :=
begin
split,
{ introsI h c,
exact (infer_instance : mono (((evaluation _ _).obj c).map η)) },
{ introsI _,
apply nat_trans.mono_app_of_mono }
end
end
section
variables [∀ (a b : C), has_products_of_shape (a ⟶ b) D]
/-- The right adjoint of evaluation. -/
@[simps]
def evaluation_right_adjoint (c : C) : D ⥤ C ⥤ D :=
{ obj := λ d,
{ obj := λ t, ∏ (λ i : t ⟶ c, d),
map := λ u v f, pi.lift $ λ g, pi.π _ $ f ≫ g,
map_id' := begin
intros, ext ⟨j⟩, dsimp,
simp only [limit.lift_π, category.id_comp, fan.mk_π_app],
congr, simp,
end,
map_comp' := begin
intros, ext ⟨j⟩, dsimp,
simp only [limit.lift_π, fan.mk_π_app, category.assoc],
congr' 1, simp,
end },
map := λ d₁ d₂ f,
{ app := λ t, pi.lift $ λ g, pi.π _ g ≫ f,
naturality' := by { intros, ext, dsimp, simp } },
map_id' := by { intros, ext x ⟨j⟩, dsimp, simp },
map_comp' := by { intros, ext, dsimp, simp } }
/-- The adjunction showing that evaluation is a left adjoint. -/
@[simps unit_app_app counit_app]
def evaluation_adjunction_left (c : C) :
(evaluation _ _).obj c ⊣ evaluation_right_adjoint D c :=
adjunction.mk_of_hom_equiv
{ hom_equiv := λ F d,
{ to_fun := λ f,
{ app := λ t, pi.lift $ λ g, F.map g ≫ f,
naturality' := by { intros, ext, dsimp, simp } },
inv_fun := λ f, f.app _ ≫ pi.π _ (𝟙 _),
left_inv := λ f, by { dsimp, simp },
right_inv := begin
intros f,
ext x ⟨g⟩,
dsimp,
simp only [limit.lift_π, evaluation_right_adjoint_obj_map,
nat_trans.naturality_assoc, fan.mk_π_app],
congr,
rw category.comp_id
end },
hom_equiv_naturality_left_symm' := by { intros, dsimp, simp },
hom_equiv_naturality_right' := by { intros, ext, dsimp, simp } }
instance evaluation_is_left_adjoint (c : C) :
is_left_adjoint ((evaluation _ D).obj c) :=
⟨_, evaluation_adjunction_left _ _⟩
lemma nat_trans.epi_iff_app_epi {F G : C ⥤ D} (η : F ⟶ G) :
epi η ↔ (∀ c, epi (η.app c)) :=
begin
split,
{ introsI h c,
exact (infer_instance : epi (((evaluation _ _).obj c).map η)) },
{ introsI,
apply nat_trans.epi_app_of_epi }
end
end
end category_theory