-
Notifications
You must be signed in to change notification settings - Fork 298
/
Adjunctions.lean
426 lines (364 loc) · 15.5 KB
/
Adjunctions.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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
/-
Copyright (c) 2021 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Johan Commelin
-/
import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
import Mathlib.CategoryTheory.Monoidal.Functorial
import Mathlib.CategoryTheory.Monoidal.Types.Basic
import Mathlib.LinearAlgebra.DirectSum.Finsupp
import Mathlib.CategoryTheory.Linear.LinearFunctor
#align_import algebra.category.Module.adjunctions from "leanprover-community/mathlib"@"95a87616d63b3cb49d3fe678d416fbe9c4217bf4"
/-!
The functor of forming finitely supported functions on a type with values in a `[Ring R]`
is the left adjoint of
the forgetful functor from `R`-modules to types.
-/
set_option linter.uppercaseLean3 false -- `Module`
noncomputable section
open CategoryTheory
namespace ModuleCat
universe u
open Classical
variable (R : Type u)
section
variable [Ring R]
/-- The free functor `Type u ⥤ ModuleCat R` sending a type `X` to the
free `R`-module with generators `x : X`, implemented as the type `X →₀ R`.
-/
@[simps]
def free : Type u ⥤ ModuleCat R where
obj X := ModuleCat.of R (X →₀ R)
map {X Y} f := Finsupp.lmapDomain _ _ f
map_id := by intros; exact Finsupp.lmapDomain_id _ _
map_comp := by intros; exact Finsupp.lmapDomain_comp _ _ _ _
#align Module.free ModuleCat.free
/-- The free-forgetful adjunction for R-modules.
-/
def adj : free R ⊣ forget (ModuleCat.{u} R) :=
Adjunction.mkOfHomEquiv
{ homEquiv := fun X M => (Finsupp.lift M R X).toEquiv.symm
homEquiv_naturality_left_symm := fun {_ _} M f g =>
Finsupp.lhom_ext' fun x =>
LinearMap.ext_ring
(Finsupp.sum_mapDomain_index_addMonoidHom fun y => (smulAddHom R M).flip (g y)).symm }
#align Module.adj ModuleCat.adj
instance : IsRightAdjoint (forget (ModuleCat.{u} R)) :=
⟨_, adj R⟩
end
namespace Free
open MonoidalCategory
variable [CommRing R]
attribute [local ext] TensorProduct.ext
/-- (Implementation detail) The unitor for `Free R`. -/
def ε : 𝟙_ (ModuleCat.{u} R) ⟶ (free R).obj (𝟙_ (Type u)) :=
Finsupp.lsingle PUnit.unit
#align Module.free.ε ModuleCat.Free.ε
@[simp]
theorem ε_apply (r : R) : ε R r = Finsupp.single PUnit.unit r :=
rfl
#align Module.free.ε_apply ModuleCat.Free.ε_apply
/-- (Implementation detail) The tensorator for `Free R`. -/
def μ (α β : Type u) : (free R).obj α ⊗ (free R).obj β ≅ (free R).obj (α ⊗ β) :=
(finsuppTensorFinsupp' R α β).toModuleIso
#align Module.free.μ ModuleCat.Free.μ
theorem μ_natural {X Y X' Y' : Type u} (f : X ⟶ Y) (g : X' ⟶ Y') :
((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom = (μ R X X').hom ≫ (free R).map (f ⊗ g) := by
intros
-- Porting note: broken ext
apply TensorProduct.ext
apply Finsupp.lhom_ext'
intro x
apply LinearMap.ext_ring
apply Finsupp.lhom_ext'
intro x'
apply LinearMap.ext_ring
apply Finsupp.ext
intro ⟨y, y'⟩
-- Porting note: used to be dsimp [μ]
change (finsuppTensorFinsupp' R Y Y')
(Finsupp.mapDomain f (Finsupp.single x 1) ⊗ₜ[R] Finsupp.mapDomain g (Finsupp.single x' 1)) _
= (Finsupp.mapDomain (f ⊗ g) (finsuppTensorFinsupp' R X X'
(Finsupp.single x 1 ⊗ₜ[R] Finsupp.single x' 1))) _
simp_rw [Finsupp.mapDomain_single, finsuppTensorFinsupp'_single_tmul_single, mul_one,
Finsupp.mapDomain_single, CategoryTheory.tensor_apply]
#align Module.free.μ_natural ModuleCat.Free.μ_natural
theorem left_unitality (X : Type u) :
(λ_ ((free R).obj X)).hom =
(ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).obj (λ_ X).hom := by
intros
-- Porting note: broken ext
apply TensorProduct.ext
apply LinearMap.ext_ring
apply Finsupp.lhom_ext'
intro x
apply LinearMap.ext_ring
apply Finsupp.ext
intro x'
-- Porting note: used to be dsimp [ε, μ]
let q : X →₀ R := ((λ_ (of R (X →₀ R))).hom) (1 ⊗ₜ[R] Finsupp.single x 1)
change q x' = Finsupp.mapDomain (λ_ X).hom (finsuppTensorFinsupp' R (𝟙_ (Type u)) X
(Finsupp.single PUnit.unit 1 ⊗ₜ[R] Finsupp.single x 1)) x'
simp_rw [finsuppTensorFinsupp'_single_tmul_single,
ModuleCat.MonoidalCategory.leftUnitor_hom_apply, mul_one,
Finsupp.mapDomain_single, CategoryTheory.leftUnitor_hom_apply, one_smul]
#align Module.free.left_unitality ModuleCat.Free.left_unitality
theorem right_unitality (X : Type u) :
(ρ_ ((free R).obj X)).hom =
(𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).obj (ρ_ X).hom := by
intros
-- Porting note: broken ext
apply TensorProduct.ext
apply Finsupp.lhom_ext'
intro x
apply LinearMap.ext_ring
apply LinearMap.ext_ring
apply Finsupp.ext
intro x'
-- Porting note: used to be dsimp [ε, μ]
let q : X →₀ R := ((ρ_ (of R (X →₀ R))).hom) (Finsupp.single x 1 ⊗ₜ[R] 1)
change q x' = Finsupp.mapDomain (ρ_ X).hom (finsuppTensorFinsupp' R X (𝟙_ (Type u))
(Finsupp.single x 1 ⊗ₜ[R] Finsupp.single PUnit.unit 1)) x'
simp_rw [finsuppTensorFinsupp'_single_tmul_single,
ModuleCat.MonoidalCategory.rightUnitor_hom_apply, mul_one,
Finsupp.mapDomain_single, CategoryTheory.rightUnitor_hom_apply, one_smul]
#align Module.free.right_unitality ModuleCat.Free.right_unitality
theorem associativity (X Y Z : Type u) :
((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom =
(α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
(𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom := by
intros
-- Porting note: broken ext
apply TensorProduct.ext
apply TensorProduct.ext
apply Finsupp.lhom_ext'
intro x
apply LinearMap.ext_ring
apply Finsupp.lhom_ext'
intro y
apply LinearMap.ext_ring
apply Finsupp.lhom_ext'
intro z
apply LinearMap.ext_ring
apply Finsupp.ext
intro a
-- Porting note: used to be dsimp [μ]
change Finsupp.mapDomain (α_ X Y Z).hom (finsuppTensorFinsupp' R (X ⊗ Y) Z
(finsuppTensorFinsupp' R X Y
(Finsupp.single x 1 ⊗ₜ[R] Finsupp.single y 1) ⊗ₜ[R] Finsupp.single z 1)) a =
finsuppTensorFinsupp' R X (Y ⊗ Z)
(Finsupp.single x 1 ⊗ₜ[R]
finsuppTensorFinsupp' R Y Z (Finsupp.single y 1 ⊗ₜ[R] Finsupp.single z 1)) a
simp_rw [finsuppTensorFinsupp'_single_tmul_single, Finsupp.mapDomain_single, mul_one,
CategoryTheory.associator_hom_apply]
#align Module.free.associativity ModuleCat.Free.associativity
-- In fact, it's strong monoidal, but we don't yet have a typeclass for that.
/-- The free R-module functor is lax monoidal. -/
@[simps]
instance : LaxMonoidal.{u} (free R).obj where
-- Send `R` to `PUnit →₀ R`
ε := ε R
-- Send `(α →₀ R) ⊗ (β →₀ R)` to `α × β →₀ R`
μ X Y := (μ R X Y).hom
μ_natural {_} {_} {_} {_} f g := μ_natural R f g
left_unitality := left_unitality R
right_unitality := right_unitality R
associativity := associativity R
instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by
refine' ⟨⟨Finsupp.lapply PUnit.unit, ⟨_, _⟩⟩⟩
· -- Porting note: broken ext
apply LinearMap.ext_ring
-- Porting note: simp used to be able to close this goal
dsimp
erw [ModuleCat.comp_def, LinearMap.comp_apply, ε_apply, Finsupp.lapply_apply,
Finsupp.single_eq_same, id_apply]
· -- Porting note: broken ext
apply Finsupp.lhom_ext'
intro ⟨⟩
apply LinearMap.ext_ring
apply Finsupp.ext
intro ⟨⟩
-- Porting note: simp used to be able to close this goal
dsimp
erw [ModuleCat.comp_def, LinearMap.comp_apply, ε_apply, Finsupp.lapply_apply,
Finsupp.single_eq_same]
end Free
open MonoidalCategory
variable [CommRing R]
/-- The free functor `Type u ⥤ ModuleCat R`, as a monoidal functor. -/
def monoidalFree : MonoidalFunctor (Type u) (ModuleCat.{u} R) :=
{ LaxMonoidalFunctor.of (free R).obj with
-- Porting note: used to be dsimp
ε_isIso := (by infer_instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _))
μ_isIso := fun X Y => by dsimp; infer_instance }
#align Module.monoidal_free ModuleCat.monoidalFree
example (X Y : Type u) : (free R).obj (X × Y) ≅ (free R).obj X ⊗ (free R).obj Y :=
((monoidalFree R).μIso X Y).symm
end ModuleCat
namespace CategoryTheory
universe v u
/-- `Free R C` is a type synonym for `C`, which, given `[CommRing R]` and `[Category C]`,
we will equip with a category structure where the morphisms are formal `R`-linear combinations
of the morphisms in `C`.
-/
-- Porting note: Removed has_nonempty_instance nolint
@[nolint unusedArguments]
def Free (_ : Type*) (C : Type u) :=
C
#align category_theory.Free CategoryTheory.Free
/-- Consider an object of `C` as an object of the `R`-linear completion.
It may be preferable to use `(Free.embedding R C).obj X` instead;
this functor can also be used to lift morphisms.
-/
def Free.of (R : Type*) {C : Type u} (X : C) : Free R C :=
X
#align category_theory.Free.of CategoryTheory.Free.of
variable (R : Type*) [CommRing R] (C : Type u) [Category.{v} C]
open Finsupp
-- Conceptually, it would be nice to construct this via "transport of enrichment",
-- using the fact that `ModuleCat.Free R : Type ⥤ ModuleCat R` and `ModuleCat.forget` are both lax
-- monoidal. This still seems difficult, so we just do it by hand.
instance categoryFree : Category (Free R C) where
Hom := fun X Y : C => (X ⟶ Y) →₀ R
id := fun X : C => Finsupp.single (𝟙 X) 1
comp {X Y Z : C} f g :=
(f.sum (fun f' s => g.sum (fun g' t => Finsupp.single (f' ≫ g') (s * t))) : (X ⟶ Z) →₀ R)
assoc {W X Y Z} f g h := by
dsimp
-- This imitates the proof of associativity for `MonoidAlgebra`.
simp only [sum_sum_index, sum_single_index, single_zero, single_add, eq_self_iff_true,
forall_true_iff, forall₃_true_iff, add_mul, mul_add, Category.assoc, mul_assoc,
zero_mul, mul_zero, sum_zero, sum_add]
#align category_theory.category_Free CategoryTheory.categoryFree
namespace Free
section
-- Porting note: removed local reducible attribute for categoryFree, adjusted dsimp invocations
-- accordingly
instance : Preadditive (Free R C) where
homGroup X Y := Finsupp.addCommGroup
add_comp X Y Z f f' g := by
dsimp [CategoryTheory.categoryFree]
rw [Finsupp.sum_add_index'] <;> · simp [add_mul]
comp_add X Y Z f g g' := by
dsimp [CategoryTheory.categoryFree]
rw [← Finsupp.sum_add]
congr; ext r h
rw [Finsupp.sum_add_index'] <;> · simp [mul_add]
instance : Linear R (Free R C) where
homModule X Y := Finsupp.module _ R
smul_comp X Y Z r f g := by
dsimp [CategoryTheory.categoryFree]
rw [Finsupp.sum_smul_index] <;> simp [Finsupp.smul_sum, mul_assoc]
comp_smul X Y Z f r g := by
dsimp [CategoryTheory.categoryFree]
simp_rw [Finsupp.smul_sum]
congr; ext h s
rw [Finsupp.sum_smul_index] <;> simp [Finsupp.smul_sum, mul_left_comm]
theorem single_comp_single {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r s : R) :
(single f r ≫ single g s : Free.of R X ⟶ Free.of R Z) = single (f ≫ g) (r * s) := by
dsimp [CategoryTheory.categoryFree]; simp
#align category_theory.Free.single_comp_single CategoryTheory.Free.single_comp_single
end
attribute [local simp] single_comp_single
/-- A category embeds into its `R`-linear completion.
-/
@[simps]
def embedding : C ⥤ Free R C where
obj X := X
map {X Y} f := Finsupp.single f 1
map_id X := rfl
map_comp {X Y Z} f g := by
-- Porting note: simp used to be able to close this goal
dsimp only []
rw [single_comp_single, one_mul]
#align category_theory.Free.embedding CategoryTheory.Free.embedding
variable {C} {D : Type u} [Category.{v} D] [Preadditive D] [Linear R D]
open Preadditive Linear
/-- A functor to an `R`-linear category lifts to a functor from its `R`-linear completion.
-/
@[simps]
def lift (F : C ⥤ D) : Free R C ⥤ D where
obj X := F.obj X
map {X Y} f := f.sum fun f' r => r • F.map f'
map_id := by dsimp [CategoryTheory.categoryFree]; simp
map_comp {X Y Z} f g := by
apply Finsupp.induction_linear f
· -- Porting note: simp used to be able to close this goal
dsimp
rw [Limits.zero_comp, sum_zero_index, Limits.zero_comp]
· intro f₁ f₂ w₁ w₂
rw [add_comp]
dsimp at *
rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
· simp only [w₁, w₂, add_comp]
· intros; rw [zero_smul]
· intros; simp only [add_smul]
· intros; rw [zero_smul]
· intros; simp only [add_smul]
· intro f' r
apply Finsupp.induction_linear g
· -- Porting note: simp used to be able to close this goal
dsimp
rw [Limits.comp_zero, sum_zero_index, Limits.comp_zero]
· intro f₁ f₂ w₁ w₂
rw [comp_add]
dsimp at *
rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
· simp only [w₁, w₂, comp_add]
· intros; rw [zero_smul]
· intros; simp only [add_smul]
· intros; rw [zero_smul]
· intros; simp only [add_smul]
· intro g' s
rw [single_comp_single _ _ f' g' r s]
simp [mul_comm r s, mul_smul]
#align category_theory.Free.lift CategoryTheory.Free.lift
theorem lift_map_single (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) (r : R) :
(lift R F).map (single f r) = r • F.map f := by simp
#align category_theory.Free.lift_map_single CategoryTheory.Free.lift_map_single
instance lift_additive (F : C ⥤ D) : (lift R F).Additive where
map_add {X Y} f g := by
dsimp
rw [Finsupp.sum_add_index'] <;> simp [add_smul]
#align category_theory.Free.lift_additive CategoryTheory.Free.lift_additive
instance lift_linear (F : C ⥤ D) : (lift R F).Linear R where
map_smul {X Y} f r := by
dsimp
rw [Finsupp.sum_smul_index] <;> simp [Finsupp.smul_sum, mul_smul]
#align category_theory.Free.lift_linear CategoryTheory.Free.lift_linear
/-- The embedding into the `R`-linear completion, followed by the lift,
is isomorphic to the original functor.
-/
def embeddingLiftIso (F : C ⥤ D) : embedding R C ⋙ lift R F ≅ F :=
NatIso.ofComponents fun X => Iso.refl _
#align category_theory.Free.embedding_lift_iso CategoryTheory.Free.embeddingLiftIso
/-- Two `R`-linear functors out of the `R`-linear completion are isomorphic iff their
compositions with the embedding functor are isomorphic.
-/
-- Porting note: used to be @[ext]
def ext {F G : Free R C ⥤ D} [F.Additive] [F.Linear R] [G.Additive] [G.Linear R]
(α : embedding R C ⋙ F ≅ embedding R C ⋙ G) : F ≅ G :=
NatIso.ofComponents (fun X => α.app X)
(by
intro X Y f
apply Finsupp.induction_linear f
· -- Porting note: simp used to be able to close this goal
rw [Functor.map_zero, Limits.zero_comp, Functor.map_zero, Limits.comp_zero]
· intro f₁ f₂ w₁ w₂
-- Porting note: Using rw instead of simp
rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, comp_add]
· intro f' r
rw [Iso.app_hom, Iso.app_hom, ← smul_single_one, F.map_smul, G.map_smul, smul_comp,
comp_smul]
change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f'
rw [α.hom.naturality f'])
#align category_theory.Free.ext CategoryTheory.Free.ext
/-- `Free.lift` is unique amongst `R`-linear functors `Free R C ⥤ D`
which compose with `embedding ℤ C` to give the original functor.
-/
def liftUnique (F : C ⥤ D) (L : Free R C ⥤ D) [L.Additive] [L.Linear R]
(α : embedding R C ⋙ L ≅ F) : L ≅ lift R F :=
ext R (α.trans (embeddingLiftIso R F).symm)
#align category_theory.Free.lift_unique CategoryTheory.Free.liftUnique
end Free
end CategoryTheory