Skip to content

Commit 26f1b3d

Browse files
AlizterAlizter
committed
monoids and comonoids
Signed-off-by: Ali Caglayan <[email protected]>
1 parent 71f9cb8 commit 26f1b3d

File tree

7 files changed

+509
-64
lines changed

7 files changed

+509
-64
lines changed

‎theories/Algebra/Categorical/MonoidObject.v‎

Lines changed: 197 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,197 @@
1+
Require Import Basics.Overture Basics.Tactics.
2+
Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor
3+
WildCat.NatTrans WildCat.Opposite WildCat.Products.
4+
Require Import abstract_algebra.
5+
6+
(** * Monoids and Comonoids *)
7+
8+
(** Here we define a monoid internal to a monoidal category. Various algebraic theories such as groups and rings may also be internalized, however these specifically require a cartesian monoidal structure. The theory of monoids however has no such requirement and can therefore be developed in much greater generality. This can be used to define a range of objects such as R-algebras, H-spaces, Hopf algebras and more. *)
9+
10+
(** * Monoid objects *)
11+
12+
Section MonoidObject.
13+
Context {A : Type} {tensor : A -> A -> A} {unit : A}
14+
`{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor}
15+
`{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit}.
16+
17+
(** An object [x] of [A] is a monoid object if it comes with the following data: *)
18+
Class IsMonoidObject (x : A) := {
19+
(** A multiplication map from the tensor product of [x] with itself to [x]. *)
20+
mo_mult : tensor x x $-> x;
21+
(** A unit of the multplication. *)
22+
mo_unit : unit $-> x;
23+
(** The multiplication map is associative. *)
24+
mo_assoc : mo_mult $o fmap10 tensor mo_mult x $o associator x x x
25+
$== mo_mult $o fmap01 tensor x mo_mult;
26+
(** The multiplication map is left unital. *)
27+
mo_left_unit : mo_mult $o fmap10 tensor mo_unit x $== left_unitor x;
28+
(** The multiplication map is right unital. *)
29+
mo_right_unit : mo_mult $o fmap01 tensor x mo_unit $== right_unitor x;
30+
}.
31+
32+
Context `{!Braiding tensor}.
33+
34+
(** An object [x] of [A] is a commutative monoid object if: *)
35+
Class IsCommutativeMonoidObject (x : A) := {
36+
(** It is a monoid object. *)
37+
cmo_mo :: IsMonoidObject x;
38+
(** The multiplication map is commutative. *)
39+
cmo_comm : mo_mult $o braid x x $== mo_mult;
40+
}.
41+
42+
End MonoidObject.
43+
44+
Arguments IsMonoidObject {A} tensor unit {_ _ _ _ _ _ _ _ _ _} x.
45+
Arguments IsCommutativeMonoidObject {A} tensor unit {_ _ _ _ _ _ _ _ _ _ _} x.
46+
47+
Section ComonoidObject.
48+
Context {A : Type} (tensor : A -> A -> A) (unit : A)
49+
`{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor}
50+
`{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit}.
51+
52+
(** A comonoid object is a monoid object in the opposite category. *)
53+
Class IsComonoidObject (x : A)
54+
:= ismonoid_comonoid_op :: IsMonoidObject (A:=A^op) tensor unit x.
55+
56+
(** We can build comonoid objects from the following data: *)
57+
Definition Build_IsComonoidObject (x : A)
58+
(** A comultplication map. *)
59+
(co_comult : x $-> tensor x x)
60+
(** A counit. *)
61+
(co_counit : x $-> unit)
62+
(** The comultiplication is coassociative. *)
63+
(co_coassoc : associator x x x $o fmap01 tensor x co_comult $o co_comult
64+
$== fmap10 tensor co_comult x $o co_comult)
65+
(** The comultiplication is left counital. *)
66+
(co_left_counit : left_unitor x $o fmap10 tensor co_counit x $o co_comult $== Id x)
67+
(** The comultiplication is right counital. *)
68+
(co_right_counit : right_unitor x $o fmap01 tensor x co_counit $o co_comult $== Id x)
69+
: IsComonoidObject x.
70+
Proof.
71+
snrapply Build_IsMonoidObject.
72+
- exact co_comult.
73+
- exact co_counit.
74+
- nrapply cate_moveR_eV.
75+
symmetry.
76+
nrefine (cat_assoc _ _ _ $@ _).
77+
rapply co_coassoc.
78+
- simpl; nrefine (_ $@ cat_idr _).
79+
nrapply cate_moveL_Ve.
80+
nrefine (cat_assoc_opp _ _ _ $@ _).
81+
exact co_left_counit.
82+
- simpl; nrefine (_ $@ cat_idr _).
83+
nrapply cate_moveL_Ve.
84+
nrefine (cat_assoc_opp _ _ _ $@ _).
85+
exact co_right_counit.
86+
Defined.
87+
88+
(** Comultiplication *)
89+
Definition co_comult {x : A} `{!IsComonoidObject x} : x $-> tensor x x
90+
:= mo_mult (A:=A^op) (tensor:=tensor) (unit:=unit) (x:=x).
91+
92+
(** Counit *)
93+
Definition co_counit {x : A} `{!IsComonoidObject x} : x $-> unit
94+
:= mo_unit (A:=A^op) (tensor:=tensor) (unit:=unit) (x:=x).
95+
96+
Context `{!Braiding tensor}.
97+
98+
(** A cocommutative comonoid objects is a commutative monoid object in the opposite category. *)
99+
Class IsCocommutativeComonoidObject (x : A)
100+
:= iscommuatativemonoid_cocomutativemonoid_op
101+
:: IsCommutativeMonoidObject (A:=A^op) tensor unit x.
102+
103+
(** We can build cocommutative comonoid objects from the following data: *)
104+
Definition Build_IsCocommutativeComonoidObject (x : A)
105+
(** A comonoid. *)
106+
`{!IsComonoidObject x}
107+
(** Together with a proof of cocommutativity. *)
108+
(cco_cocomm : braid x x $o co_comult $== co_comult)
109+
: IsCocommutativeComonoidObject x.
110+
Proof.
111+
snrapply Build_IsCommutativeMonoidObject.
112+
- exact _.
113+
- exact cco_cocomm.
114+
Defined.
115+
116+
End ComonoidObject.
117+
118+
(** ** Monoid enrichment *)
119+
120+
(** A hom [x $-> y] in a cartesian category where [y] is a monoid object has the structure of a monoid. Equivalently, a hom [x $-> y] in a cartesian category where [x] is a comonoid object has the structure of a monoid. *)
121+
122+
Section MonoidEnriched.
123+
Context {A : Type} `{HasEquivs A} `{!HasBinaryProducts A}
124+
(unit : A) `{!IsTerminal unit} {x y : A}
125+
`{!HasMorExt A} `{forall x y, IsHSet (x $-> y)}.
126+
127+
Section Monoid.
128+
Context `{!IsMonoidObject _ _ y}.
129+
130+
Local Instance sgop_hom : SgOp (x $-> y)
131+
:= fun f g => mo_mult $o cat_binprod_corec f g.
132+
133+
Local Instance monunit_hom : MonUnit (x $-> y) := mo_unit $o mor_terminal _ _.
134+
135+
Local Instance associative_hom : Associative sgop_hom.
136+
Proof.
137+
intros f g h.
138+
unfold sgop_hom.
139+
rapply path_hom.
140+
refine ((_ $@L cat_binprod_fmap01_corec _ _ _)^$ $@ _).
141+
nrefine (cat_assoc_opp _ _ _ $@ _).
142+
refine ((mo_assoc $@R _)^$ $@ _).
143+
nrefine (_ $@ (_ $@L cat_binprod_fmap10_corec _ _ _)).
144+
refine (cat_assoc _ _ _ $@ (_ $@L _) $@ cat_assoc _ _ _).
145+
nrapply cat_binprod_associator_corec.
146+
Defined.
147+
148+
Local Instance leftidentity_hom : LeftIdentity sgop_hom mon_unit.
149+
Proof.
150+
intros f.
151+
unfold sgop_hom, mon_unit.
152+
rapply path_hom.
153+
refine ((_ $@L (cat_binprod_fmap10_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _).
154+
nrefine (((mo_left_unit $@ _) $@R _) $@ _).
155+
1: nrapply cate_buildequiv_fun.
156+
unfold trans_nattrans.
157+
nrefine ((((_ $@R _) $@ _) $@R _) $@ _).
158+
1: nrapply cate_buildequiv_fun.
159+
1: nrapply cat_binprod_beta_pr1.
160+
nrapply cat_binprod_beta_pr2.
161+
Defined.
162+
163+
Local Instance rightidentity_hom : RightIdentity sgop_hom mon_unit.
164+
Proof.
165+
intros f.
166+
unfold sgop_hom, mon_unit.
167+
rapply path_hom.
168+
refine ((_ $@L (cat_binprod_fmap01_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _).
169+
nrefine (((mo_right_unit $@ _) $@R _) $@ _).
170+
1: nrapply cate_buildequiv_fun.
171+
nrapply cat_binprod_beta_pr1.
172+
Defined.
173+
174+
Local Instance issemigroup_hom : IsSemiGroup (x $-> y) := {}.
175+
Local Instance ismonoid_hom : IsMonoid (x $-> y) := {}.
176+
177+
End Monoid.
178+
179+
Context `{!IsCommutativeMonoidObject _ _ y}.
180+
Local Existing Instances sgop_hom monunit_hom ismonoid_hom.
181+
182+
Local Instance commutative_hom : Commutative sgop_hom.
183+
Proof.
184+
intros f g.
185+
unfold sgop_hom.
186+
rapply path_hom.
187+
refine ((_ $@L _^$) $@ cat_assoc_opp _ _ _ $@ (cmo_comm $@R _)).
188+
nrapply cat_binprod_swap_corec.
189+
Defined.
190+
191+
Local Instance iscommutativemonoid_hom : IsCommutativeMonoid (x $-> y) := {}.
192+
193+
End MonoidEnriched.
194+
195+
196+
197+

‎theories/WildCat/Adjoint.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -388,7 +388,7 @@ Proof.
388388
snrapply Build_Adjunction_natequiv_nat_right.
389389
{ intros y.
390390
refine (natequiv_compose (natequiv_adjunction_l adj _) _).
391-
rapply (natequiv_postwhisker _ (natequiv_op _ _ e)). }
391+
rapply (natequiv_postwhisker _ (natequiv_op e)). }
392392
intros x.
393393
rapply is1natural_comp.
394394
Defined.

‎theories/WildCat/Bifunctor.v‎

Lines changed: 84 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
Require Import Basics.Overture Basics.Tactics.
22
Require Import Types.Forall Types.Prod.
3-
Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans WildCat.Square.
3+
Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans
4+
WildCat.Square WildCat.Opposite.
45

56
(** * Bifunctors between WildCats *)
67

@@ -14,6 +15,11 @@ Class Is0Bifunctor {A B C : Type}
1415
is0functor10_bifunctor :: forall b, Is0Functor (flip F b);
1516
}.
1617

18+
Arguments Is0Bifunctor {A B C _ _ _} F.
19+
Arguments is0functor_bifunctor_uncurried {A B C _ _ _} F {_}.
20+
Arguments is0functor01_bifunctor {A B C _ _ _} F {_} a : rename.
21+
Arguments is0functor10_bifunctor {A B C _ _ _} F {_} b : rename.
22+
1723
(** We provide two alternate constructors, allowing the user to provide just the first field or the last two fields. *)
1824
Definition Build_Is0Bifunctor' {A B C : Type}
1925
`{Is01Cat A, Is01Cat B, IsGraph C} (F : A -> B -> C)
@@ -72,6 +78,9 @@ Class Is1Bifunctor {A B C : Type}
7278

7379
Arguments Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {Is0Bifunctor} : rename.
7480
Arguments Build_Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_} _ _ _ _ _.
81+
Arguments is1functor_bifunctor_uncurried {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _}.
82+
Arguments is1functor01_bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _} a : rename.
83+
Arguments is1functor10_bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _} b : rename.
7584
Arguments fmap11_is_fmap01_fmap10 {A B C _ _ _ _ _ _ _ _ _ _ _ _} F
7685
{Is0Bifunctor Is1Bifunctor} {a0 a1} f {b0 b1} g : rename.
7786
Arguments fmap11_is_fmap10_fmap01 {A B C _ _ _ _ _ _ _ _ _ _ _ _} F
@@ -285,14 +294,14 @@ Global Instance is0bifunctor_postcompose {A B C D : Type}
285294
`{IsGraph A, IsGraph B, IsGraph C, IsGraph D}
286295
(F : A -> B -> C) {bf : Is0Bifunctor F}
287296
(G : C -> D) `{!Is0Functor G}
288-
: Is0Bifunctor (fun a b => G (F a b))
297+
: Is0Bifunctor (fun a b => G (F a b)) | 10
289298
:= {}.
290299

291300
Global Instance is1bifunctor_postcompose {A B C D : Type}
292301
`{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D}
293302
(F : A -> B -> C) (G : C -> D) `{!Is0Functor G, !Is1Functor G}
294303
`{!Is0Bifunctor F} {bf : Is1Bifunctor F}
295-
: Is1Bifunctor (fun a b => G (F a b)).
304+
: Is1Bifunctor (fun a b => G (F a b)) | 10.
296305
Proof.
297306
snrapply Build_Is1Bifunctor.
298307
1-3: exact _.
@@ -306,7 +315,7 @@ Global Instance is0bifunctor_precompose {A B C D E : Type}
306315
`{IsGraph A, IsGraph B, IsGraph C, IsGraph D, IsGraph E}
307316
(G : A -> B) (K : E -> C) (F : B -> C -> D)
308317
`{!Is0Functor G, !Is0Bifunctor F, !Is0Functor K}
309-
: Is0Bifunctor (fun a b => F (G a) (K b)).
318+
: Is0Bifunctor (fun a b => F (G a) (K b)) | 10.
310319
Proof.
311320
snrapply Build_Is0Bifunctor.
312321
- change (Is0Functor (uncurry F o functor_prod G K)).
@@ -322,7 +331,7 @@ Global Instance is1bifunctor_precompose {A B C D E : Type}
322331
(G : A -> B) (K : E -> C) (F : B -> C -> D)
323332
`{!Is0Functor G, !Is1Functor G, !Is0Bifunctor F, !Is1Bifunctor F,
324333
!Is0Functor K, !Is1Functor K}
325-
: Is1Bifunctor (fun a b => F (G a) (K b)).
334+
: Is1Bifunctor (fun a b => F (G a) (K b)) | 10.
326335
Proof.
327336
snrapply Build_Is1Bifunctor.
328337
- change (Is1Functor (uncurry F o functor_prod G K)).
@@ -372,10 +381,8 @@ Definition fmap11_square {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
372381
(** We can show that an uncurried natural transformation between uncurried bifunctors by composing the naturality square in each variable. *)
373382
Global Instance is1natural_uncurry {A B C : Type}
374383
`{Is1Cat A, Is1Cat B, Is1Cat C}
375-
(F : A -> B -> C)
376-
`{!Is0Bifunctor F, !Is1Bifunctor F}
377-
(G : A -> B -> C)
378-
`{!Is0Bifunctor G, !Is1Bifunctor G}
384+
(F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
385+
(G : A -> B -> C) `{!Is0Bifunctor G, !Is1Bifunctor G}
379386
(alpha : uncurry F $=> uncurry G)
380387
(nat_l : forall b, Is1Natural (flip F b) (flip G b) (fun x : A => alpha (x, b)))
381388
(nat_r : forall a, Is1Natural (F a) (G a) (fun y : B => alpha (a, y)))
@@ -389,3 +396,71 @@ Proof.
389396
2: rapply (fmap11_is_fmap01_fmap10 G).
390397
exact (hconcat (nat_l _ _ _ f) (nat_r _ _ _ f')).
391398
Defined.
399+
400+
(** Flipping a natural transformation between bifunctors. *)
401+
Definition nattrans_flip {A B C : Type}
402+
`{Is1Cat A, Is1Cat B, Is1Cat C}
403+
{F : A -> B -> C} `{!Is0Bifunctor F, !Is1Bifunctor F}
404+
{G : B -> A -> C} `{!Is0Bifunctor G, !Is1Bifunctor G}
405+
: NatTrans (uncurry F) (uncurry (flip G))
406+
-> NatTrans (uncurry (flip F)) (uncurry G).
407+
Proof.
408+
intros [alpha nat].
409+
snrapply Build_NatTrans.
410+
- exact (alpha o equiv_prod_symm _ _).
411+
- intros [b a] [b' a'] [g f].
412+
exact (nat (a, b) (a', b') (f, g)).
413+
Defined.
414+
415+
Definition nattrans_flip' {A B C : Type}
416+
`{Is1Cat A, Is1Cat B, Is1Cat C}
417+
{F : A -> B -> C} `{!Is0Bifunctor F, !Is1Bifunctor F}
418+
{G : B -> A -> C} `{!Is0Bifunctor G, !Is1Bifunctor G}
419+
: NatTrans (uncurry (flip F)) (uncurry G)
420+
-> NatTrans (uncurry F) (uncurry (flip G))
421+
:= nattrans_flip (F:=flip F) (G:=flip G).
422+
423+
(** ** Opposite Bifunctors *)
424+
425+
(** There are a few more combinations we can do for this, such as profunctors, but we will leave those for later. *)
426+
427+
Global Instance is0bifunctor_op A B C (F : A -> B -> C) `{Is0Bifunctor A B C F}
428+
: Is0Bifunctor (F : A^op -> B^op -> C^op).
429+
Proof.
430+
snrapply Build_Is0Bifunctor.
431+
- exact (is0functor_op _ _ (uncurry F)).
432+
- intros a.
433+
nrapply is0functor_op.
434+
exact (is0functor01_bifunctor F a).
435+
- intros b.
436+
nrapply is0functor_op.
437+
exact (is0functor10_bifunctor F b).
438+
Defined.
439+
440+
Global Instance is1bifunctor_op A B C (F : A -> B -> C) `{Is1Bifunctor A B C F}
441+
: Is1Bifunctor (F : A^op -> B^op -> C^op).
442+
Proof.
443+
snrapply Build_Is1Bifunctor.
444+
- exact (is1functor_op _ _ (uncurry F)).
445+
- intros a.
446+
nrapply is1functor_op.
447+
exact (is1functor01_bifunctor F a).
448+
- intros b.
449+
nrapply is1functor_op.
450+
exact (is1functor10_bifunctor F b).
451+
- intros a0 a1 f b0 b1 g; cbn in f, g.
452+
exact (fmap11_is_fmap10_fmap01 F f g).
453+
- intros a0 a1 f b0 b1 g; cbn in f, g.
454+
exact (fmap11_is_fmap01_fmap10 F f g).
455+
Defined.
456+
457+
Global Instance is0bifunctor_op' A B C (F : A^op -> B^op -> C^op)
458+
`{IsGraph A, IsGraph B, IsGraph C, Fop : !Is0Bifunctor (F : A^op -> B^op -> C^op)}
459+
: Is0Bifunctor (F : A -> B -> C)
460+
:= is0bifunctor_op A^op B^op C^op F.
461+
462+
Global Instance is1bifunctor_op' A B C (F : A^op -> B^op -> C^op)
463+
`{Is1Cat A, Is1Cat B, Is1Cat C,
464+
!Is0Bifunctor (F : A^op -> B^op -> C^op), !Is1Bifunctor (F : A^op -> B^op -> C^op)}
465+
: Is1Bifunctor (F : A -> B -> C)
466+
:= is1bifunctor_op A^op B^op C^op F.

‎theories/WildCat/Equiv.v‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -413,6 +413,13 @@ Proof.
413413
apply cate_inv_adjointify.
414414
Defined.
415415

416+
Definition cate_inv_compose' {A} `{HasEquivs A} {a b c : A} (e : a $<~> b) (f : b $<~> c)
417+
: cate_fun (f $oE e)^-1$ $== e^-1$ $o f^-1$.
418+
Proof.
419+
nrefine (_ $@ cate_buildequiv_fun _).
420+
nrapply cate_inv_compose.
421+
Defined.
422+
416423
Definition cate_inv_V {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
417424
: cate_fun (e^-1$)^-1$ $== cate_fun e.
418425
Proof.

0 commit comments

Comments
 (0)