Definition df-mndtc

Description: Definition of the function converting a monoid to a category. Example 3.3(4.e) of Adamek p. 24.

The definition of the base set is arbitrary. The whole extensible structure becomes the object here (see mndtcbasval ) , instead of just the base set, as is the case in Example 3.3(4.e) of Adamek p. 24.

The resulting category is defined entirely, up to isomorphism, by mndtcbas , mndtchom , mndtcco . Use those instead.

See example 3.26(3) of Adamek p. 33 for more on isomorphism.

"MndToCat" was taken instead of "MndCat" because the latter might mean the category of monoids. (Contributed by Zhi Wang, 22-Sep-2024) (New usage is discouraged.)

	Ref	Expression
Assertion	df-mndtc	|- MndToCat = ( m e. Mnd |-> { <. ( Base ` ndx ) , { m } >. , <. ( Hom ` ndx ) , { <. m , m , ( Base ` m ) >. } >. , <. ( comp ` ndx ) , { <. <. m , m , m >. , ( +g ` m ) >. } >. } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmndtc	|- MndToCat
1		vm	|- m
2		cmnd	|- Mnd
3		cbs	|- Base
4		cnx	|- ndx
5	4 3	cfv	|- ( Base ` ndx )
6	1	cv	|- m
7	6	csn	|- { m }
8	5 7	cop	|- <. ( Base ` ndx ) , { m } >.
9		chom	|- Hom
10	4 9	cfv	|- ( Hom ` ndx )
11	6 3	cfv	|- ( Base ` m )
12	6 6 11	cotp	|- <. m , m , ( Base ` m ) >.
13	12	csn	|- { <. m , m , ( Base ` m ) >. }
14	10 13	cop	|- <. ( Hom ` ndx ) , { <. m , m , ( Base ` m ) >. } >.
15	14	cv	|- <. ( Hom ` ndx ) , { <. m , m , ( Base ` m ) >. } >.
16		cco	|- comp
17	4 16	cfv	|- ( comp ` ndx )
18	17	cv	|- ( comp ` ndx )
19	1 1 6	cotp	|- <. m , m , m >.
20		cplusg	|- +g
21	6 20	cfv	|- ( +g ` m )
22	19 21	cop	|- <. <. m , m , m >. , ( +g ` m ) >.
23	22	csn	|- { <. <. m , m , m >. , ( +g ` m ) >. }
24	18 23	cop	|- <. ( comp ` ndx ) , { <. <. m , m , m >. , ( +g ` m ) >. } >.
25	8 15 24	ctp	|- { <. ( Base ` ndx ) , { m } >. , <. ( Hom ` ndx ) , { <. m , m , ( Base ` m ) >. } >. , <. ( comp ` ndx ) , { <. <. m , m , m >. , ( +g ` m ) >. } >. }
26	1 2 25	cmpt	|- ( m e. Mnd |-> { <. ( Base ` ndx ) , { m } >. , <. ( Hom ` ndx ) , { <. m , m , ( Base ` m ) >. } >. , <. ( comp ` ndx ) , { <. <. m , m , m >. , ( +g ` m ) >. } >. } )
27	0 26	wceq	|- MndToCat = ( m e. Mnd |-> { <. ( Base ` ndx ) , { m } >. , <. ( Hom ` ndx ) , { <. m , m , ( Base ` m ) >. } >. , <. ( comp ` ndx ) , { <. <. m , m , m >. , ( +g ` m ) >. } >. } )