Skip to content

Commit 0783216

Browse files
joelrioujoelriou
committed
feat: port CategoryTheory.Monoidal.Internal.FunctorCategory (#5093)
1 parent 3ecffe4 commit 0783216

File tree

2 files changed

+255
-0
lines changed

2 files changed

+255
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -975,6 +975,7 @@ import Mathlib.CategoryTheory.Monoidal.Free.Coherence
975975
import Mathlib.CategoryTheory.Monoidal.Functor
976976
import Mathlib.CategoryTheory.Monoidal.FunctorCategory
977977
import Mathlib.CategoryTheory.Monoidal.Functorial
978+
import Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
978979
import Mathlib.CategoryTheory.Monoidal.Limits
979980
import Mathlib.CategoryTheory.Monoidal.Linear
980981
import Mathlib.CategoryTheory.Monoidal.Mod_

‎Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean‎

Lines changed: 254 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,254 @@
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+
! This file was ported from Lean 3 source module category_theory.monoidal.internal.functor_category
7+
! leanprover-community/mathlib commit f153a85a8dc0a96ce9133fed69e34df72f7f191f
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.CategoryTheory.Monoidal.CommMon_
12+
import Mathlib.CategoryTheory.Monoidal.FunctorCategory
13+
14+
/-!
15+
# `Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D`
16+
17+
When `D` is a monoidal category,
18+
monoid objects in `C ⥤ D` are the same thing as functors from `C` into the monoid objects of `D`.
19+
20+
This is formalised as:
21+
* `monFunctorCategoryEquivalence : Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D`
22+
23+
The intended application is that as `Ring ≌ Mon_ Ab` (not yet constructed!),
24+
we have `presheaf Ring X ≌ presheaf (Mon_ Ab) X ≌ Mon_ (presheaf Ab X)`,
25+
and we can model a module over a presheaf of rings as a module object in `presheaf Ab X`.
26+
27+
## Future work
28+
Presumably this statement is not specific to monoids,
29+
and could be generalised to any internal algebraic objects,
30+
if the appropriate framework was available.
31+
-/
32+
33+
34+
universe v₁ v₂ u₁ u₂
35+
36+
open CategoryTheory MonoidalCategory
37+
38+
namespace CategoryTheory.Monoidal
39+
40+
variable (C : Type u₁) [Category.{v₁} C]
41+
42+
variable (D : Type u₂) [Category.{v₂} D] [MonoidalCategory.{v₂} D]
43+
44+
namespace MonFunctorCategoryEquivalence
45+
46+
variable {C D}
47+
48+
-- porting note: the `obj` field of `functor : Mon_ (C ⥤ D) ⥤ C ⥤ Mon_ D` defined below
49+
-- had to be defined separately as `Functor.obj` in order to speed up the compilation
50+
/-- A monoid object in a functor category induces a functor to the category of monoid objects. -/
51+
@[simps]
52+
def Functor.obj (A : Mon_ (C ⥤ D)) : C ⥤ Mon_ D where
53+
obj X :=
54+
{ X := A.X.obj X
55+
one := A.one.app X
56+
mul := A.mul.app X
57+
one_mul := congr_app A.one_mul X
58+
mul_one := congr_app A.mul_one X
59+
mul_assoc := congr_app A.mul_assoc X }
60+
map f :=
61+
{ hom := A.X.map f
62+
one_hom := by rw [← A.one.naturality, tensorUnit_map]; dsimp; rw [Category.id_comp]
63+
mul_hom := by dsimp; rw [← A.mul.naturality, tensorObj_map] }
64+
map_id X := by ext; dsimp; rw [CategoryTheory.Functor.map_id]
65+
map_comp f g := by ext; dsimp; rw [Functor.map_comp]
66+
67+
/-- Functor translating a monoid object in a functor category
68+
to a functor into the category of monoid objects.
69+
-/
70+
@[simps]
71+
def functor : Mon_ (C ⥤ D) ⥤ C ⥤ Mon_ D where
72+
obj := Functor.obj
73+
map f :=
74+
{ app := fun X =>
75+
{ hom := f.hom.app X
76+
one_hom := congr_app f.one_hom X
77+
mul_hom := congr_app f.mul_hom X } }
78+
set_option linter.uppercaseLean3 false in
79+
#align category_theory.monoidal.Mon_functor_category_equivalence.functor CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor
80+
81+
-- porting note: the `obj` field of `inverse : (C ⥤ Mon_ D) ⥤ Mon_ (C ⥤ D)` defined below
82+
-- had to be defined separately as `Inverse.obj` in order to speed up the compilation
83+
/-- A functor to the category of monoid objects can be translated as a monoid object
84+
in the functor category. -/
85+
@[simps]
86+
def Inverse.obj (F : C ⥤ Mon_ D) : Mon_ (C ⥤ D) where
87+
X := F ⋙ Mon_.forget D
88+
one := { app := fun X => (F.obj X).one }
89+
mul := { app := fun X => (F.obj X).mul }
90+
one_mul := by ext X; exact (F.obj X).one_mul
91+
mul_one := by ext X; exact (F.obj X).mul_one
92+
mul_assoc := by ext X; exact (F.obj X).mul_assoc
93+
94+
/-- Functor translating a functor into the category of monoid objects
95+
to a monoid object in the functor category
96+
-/
97+
@[simps]
98+
def inverse : (C ⥤ Mon_ D) ⥤ Mon_ (C ⥤ D) where
99+
obj := Inverse.obj
100+
map α :=
101+
{ hom :=
102+
{ app := fun X => (α.app X).hom
103+
naturality := fun X Y f => congr_arg Mon_.Hom.hom (α.naturality f) }
104+
one_hom := by ext x; dsimp; rw [(α.app x).one_hom]
105+
mul_hom := by ext x; dsimp; rw [(α.app x).mul_hom] }
106+
set_option linter.uppercaseLean3 false in
107+
#align category_theory.monoidal.Mon_functor_category_equivalence.inverse CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse
108+
109+
/-- The unit for the equivalence `Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D`.
110+
-/
111+
@[simps!]
112+
def unitIso : 𝟭 (Mon_ (C ⥤ D)) ≅ functor ⋙ inverse :=
113+
NatIso.ofComponents
114+
(fun A =>
115+
{ hom :=
116+
{ hom := { app := fun _ => 𝟙 _ }
117+
one_hom := by ext X; dsimp; simp only [Category.comp_id]
118+
mul_hom := by
119+
ext X; dsimp; simp only [tensor_id, Category.id_comp, Category.comp_id] }
120+
inv :=
121+
{ hom := { app := fun _ => 𝟙 _ }
122+
one_hom := by ext X; dsimp; simp only [Category.comp_id]
123+
mul_hom := by
124+
ext X
125+
dsimp
126+
simp only [tensor_id, Category.id_comp, Category.comp_id] } })
127+
fun f => by
128+
ext X
129+
simp only [Functor.id_map, Mon_.comp_hom', NatTrans.comp_app, Category.comp_id,
130+
Functor.comp_map, inverse_map_hom_app, functor_map_app_hom, Category.id_comp]
131+
set_option linter.uppercaseLean3 false in
132+
#align category_theory.monoidal.Mon_functor_category_equivalence.unit_iso CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso
133+
134+
/-- The counit for the equivalence `Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D`.
135+
-/
136+
@[simps!]
137+
def counitIso : inverse ⋙ functor ≅ 𝟭 (C ⥤ Mon_ D) :=
138+
NatIso.ofComponents
139+
(fun A =>
140+
NatIso.ofComponents
141+
(fun X =>
142+
{ hom := { hom := 𝟙 _ }
143+
inv := { hom := 𝟙 _ } })
144+
(by aesop_cat))
145+
(by aesop_cat)
146+
set_option linter.uppercaseLean3 false in
147+
#align category_theory.monoidal.Mon_functor_category_equivalence.counit_iso CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso
148+
149+
end MonFunctorCategoryEquivalence
150+
151+
open MonFunctorCategoryEquivalence
152+
153+
/-- When `D` is a monoidal category,
154+
monoid objects in `C ⥤ D` are the same thing
155+
as functors from `C` into the monoid objects of `D`.
156+
-/
157+
@[simps]
158+
def monFunctorCategoryEquivalence : Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D where
159+
functor := functor
160+
inverse := inverse
161+
unitIso := unitIso
162+
counitIso := counitIso
163+
set_option linter.uppercaseLean3 false in
164+
#align category_theory.monoidal.Mon_functor_category_equivalence CategoryTheory.Monoidal.monFunctorCategoryEquivalence
165+
166+
variable [BraidedCategory.{v₂} D]
167+
168+
namespace CommMonFunctorCategoryEquivalence
169+
170+
variable {C D}
171+
172+
/-- Functor translating a commutative monoid object in a functor category
173+
to a functor into the category of commutative monoid objects.
174+
-/
175+
@[simps!]
176+
def functor : CommMon_ (C ⥤ D) ⥤ C ⥤ CommMon_ D where
177+
obj A :=
178+
{ (monFunctorCategoryEquivalence C D).functor.obj A.toMon_ with
179+
obj := fun X =>
180+
{ ((monFunctorCategoryEquivalence C D).functor.obj A.toMon_).obj X with
181+
mul_comm := congr_app A.mul_comm X } }
182+
map f := { app := fun X => ((monFunctorCategoryEquivalence C D).functor.map f).app X }
183+
set_option linter.uppercaseLean3 false in
184+
#align category_theory.monoidal.CommMon_functor_category_equivalence.functor CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor
185+
186+
/-- Functor translating a functor into the category of commutative monoid objects
187+
to a commutative monoid object in the functor category
188+
-/
189+
@[simps!]
190+
def inverse : (C ⥤ CommMon_ D) ⥤ CommMon_ (C ⥤ D) where
191+
obj F :=
192+
{ (monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon_.forget₂Mon_ D) with
193+
mul_comm := by ext X; exact (F.obj X).mul_comm }
194+
map α := (monFunctorCategoryEquivalence C D).inverse.map (whiskerRight α _)
195+
set_option linter.uppercaseLean3 false in
196+
#align category_theory.monoidal.CommMon_functor_category_equivalence.inverse CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse
197+
198+
/-- The unit for the equivalence `CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D`.
199+
-/
200+
@[simps!]
201+
def unitIso : 𝟭 (CommMon_ (C ⥤ D)) ≅ functor ⋙ inverse :=
202+
NatIso.ofComponents
203+
(fun A =>
204+
{ hom :=
205+
{ hom := { app := fun _ => 𝟙 _ }
206+
one_hom := by ext X; dsimp; simp only [Category.comp_id]
207+
mul_hom := by ext X; dsimp; simp only [tensor_id, Category.id_comp, Category.comp_id] }
208+
inv :=
209+
{ hom := { app := fun _ => 𝟙 _ }
210+
one_hom := by ext X; dsimp; simp only [Category.comp_id]
211+
mul_hom := by
212+
ext X
213+
dsimp
214+
simp only [tensor_id, Category.id_comp, Category.comp_id] } })
215+
fun f => by
216+
ext X
217+
dsimp
218+
simp only [Category.id_comp, Category.comp_id]
219+
set_option linter.uppercaseLean3 false in
220+
#align category_theory.monoidal.CommMon_functor_category_equivalence.unit_iso CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso
221+
222+
/-- The counit for the equivalence `CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D`.
223+
-/
224+
@[simps!]
225+
def counitIso : inverse ⋙ functor ≅ 𝟭 (C ⥤ CommMon_ D) :=
226+
NatIso.ofComponents
227+
(fun A =>
228+
NatIso.ofComponents
229+
(fun X =>
230+
{ hom := { hom := 𝟙 _ }
231+
inv := { hom := 𝟙 _ } })
232+
(by aesop_cat))
233+
(by aesop_cat)
234+
set_option linter.uppercaseLean3 false in
235+
#align category_theory.monoidal.CommMon_functor_category_equivalence.counit_iso CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso
236+
237+
end CommMonFunctorCategoryEquivalence
238+
239+
open CommMonFunctorCategoryEquivalence
240+
241+
/-- When `D` is a braided monoidal category,
242+
commutative monoid objects in `C ⥤ D` are the same thing
243+
as functors from `C` into the commutative monoid objects of `D`.
244+
-/
245+
@[simps]
246+
def commMonFunctorCategoryEquivalence : CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D where
247+
functor := functor
248+
inverse := inverse
249+
unitIso := unitIso
250+
counitIso := counitIso
251+
set_option linter.uppercaseLean3 false in
252+
#align category_theory.monoidal.CommMon_functor_category_equivalence CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence
253+
254+
end CategoryTheory.Monoidal

0 commit comments

Comments
 (0)