-
Notifications
You must be signed in to change notification settings - Fork 297
/
types.lean
136 lines (112 loc) · 4.53 KB
/
types.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
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import algebra.category.Mon.basic
import category_theory.monoidal.CommMon_
import category_theory.monoidal.types
/-!
# `Mon_ (Type u) ≌ Mon.{u}`
The category of internal monoid objects in `Type`
is equivalent to the category of "native" bundled monoids.
Moreover, this equivalence is compatible with the forgetful functors to `Type`.
-/
universes v u
open category_theory
namespace Mon_Type_equivalence_Mon
instance Mon_monoid (A : Mon_ (Type u)) : monoid (A.X) :=
{ one := A.one punit.star,
mul := λ x y, A.mul (x, y),
one_mul := λ x, by convert congr_fun A.one_mul (punit.star, x),
mul_one := λ x, by convert congr_fun A.mul_one (x, punit.star),
mul_assoc := λ x y z, by convert congr_fun A.mul_assoc ((x, y), z), }
/--
Converting a monoid object in `Type` to a bundled monoid.
-/
def functor : Mon_ (Type u) ⥤ Mon.{u} :=
{ obj := λ A, ⟨A.X⟩,
map := λ A B f,
{ to_fun := f.hom,
map_one' := congr_fun f.one_hom punit.star,
map_mul' := λ x y, congr_fun f.mul_hom (x, y), }, }
/--
Converting a bundled monoid to a monoid object in `Type`.
-/
def inverse : Mon.{u} ⥤ Mon_ (Type u) :=
{ obj := λ A,
{ X := A,
one := λ _, 1,
mul := λ p, p.1 * p.2,
one_mul' := by { ext ⟨_, _⟩, dsimp, simp, },
mul_one' := by { ext ⟨_, _⟩, dsimp, simp, },
mul_assoc' := by { ext ⟨⟨x, y⟩, z⟩, simp [mul_assoc], }, },
map := λ A B f,
{ hom := f, }, }
end Mon_Type_equivalence_Mon
open Mon_Type_equivalence_Mon
/--
The category of internal monoid objects in `Type`
is equivalent to the category of "native" bundled monoids.
-/
def Mon_Type_equivalence_Mon : Mon_ (Type u) ≌ Mon.{u} :=
{ functor := functor,
inverse := inverse,
unit_iso := nat_iso.of_components
(λ A, { hom := { hom := 𝟙 _, }, inv := { hom := 𝟙 _, }, })
(by tidy),
counit_iso := nat_iso.of_components (λ A,
{ hom := { to_fun := id, map_one' := rfl, map_mul' := λ x y, rfl, },
inv := { to_fun := id, map_one' := rfl, map_mul' := λ x y, rfl, }, }) (by tidy), }
/--
The equivalence `Mon_ (Type u) ≌ Mon.{u}`
is naturally compatible with the forgetful functors to `Type u`.
-/
def Mon_Type_equivalence_Mon_forget :
Mon_Type_equivalence_Mon.functor ⋙ forget Mon ≅ Mon_.forget (Type u) :=
nat_iso.of_components (λ A, iso.refl _) (by tidy)
instance Mon_Type_inhabited : inhabited (Mon_ (Type u)) :=
⟨Mon_Type_equivalence_Mon.inverse.obj (Mon.of punit)⟩
namespace CommMon_Type_equivalence_CommMon
instance CommMon_comm_monoid (A : CommMon_ (Type u)) : comm_monoid (A.X) :=
{ mul_comm := λ x y, by convert congr_fun A.mul_comm (y, x),
..Mon_Type_equivalence_Mon.Mon_monoid A.to_Mon_ }
/--
Converting a commutative monoid object in `Type` to a bundled commutative monoid.
-/
def functor : CommMon_ (Type u) ⥤ CommMon.{u} :=
{ obj := λ A, ⟨A.X⟩,
map := λ A B f, Mon_Type_equivalence_Mon.functor.map f, }
/--
Converting a bundled commutative monoid to a commutative monoid object in `Type`.
-/
def inverse : CommMon.{u} ⥤ CommMon_ (Type u) :=
{ obj := λ A,
{ mul_comm' := by { ext ⟨x, y⟩, exact comm_monoid.mul_comm y x, },
..Mon_Type_equivalence_Mon.inverse.obj ((forget₂ CommMon Mon).obj A), },
map := λ A B f, Mon_Type_equivalence_Mon.inverse.map f, }
end CommMon_Type_equivalence_CommMon
open CommMon_Type_equivalence_CommMon
/--
The category of internal commutative monoid objects in `Type`
is equivalent to the category of "native" bundled commutative monoids.
-/
def CommMon_Type_equivalence_CommMon : CommMon_ (Type u) ≌ CommMon.{u} :=
{ functor := functor,
inverse := inverse,
unit_iso := nat_iso.of_components
(λ A, { hom := { hom := 𝟙 _, }, inv := { hom := 𝟙 _, }, })
(by tidy),
counit_iso := nat_iso.of_components (λ A,
{ hom := { to_fun := id, map_one' := rfl, map_mul' := λ x y, rfl, },
inv := { to_fun := id, map_one' := rfl, map_mul' := λ x y, rfl, }, }) (by tidy), }
/--
The equivalences `Mon_ (Type u) ≌ Mon.{u}` and `CommMon_ (Type u) ≌ CommMon.{u}`
are naturally compatible with the forgetful functors to `Mon` and `Mon_ (Type u)`.
-/
def CommMon_Type_equivalence_CommMon_forget :
CommMon_Type_equivalence_CommMon.functor ⋙ forget₂ CommMon Mon ≅
CommMon_.forget₂_Mon_ (Type u) ⋙ Mon_Type_equivalence_Mon.functor :=
nat_iso.of_components (λ A, iso.refl _) (by tidy)
instance CommMon_Type_inhabited : inhabited (CommMon_ (Type u)) :=
⟨CommMon_Type_equivalence_CommMon.inverse.obj (CommMon.of punit)⟩