Definition df-mndtc 50389

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 50391), 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 50392, mndtchom 50395, mndtcco 50396. 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.)

Assertion

Ref	Expression
df-mndtc	⊢ MndToCat = (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})

Detailed syntax breakdown of Definition df-mndtc

Step	Hyp	Ref	Expression
1		cmndtc 50388	. 2 class MndToCat
2		vm	. . 3 setvar 𝑚
3		cmnd 18813	. . 3 class Mnd
4		cnx 17270	. . . . . 6 class ndx
5		cbs 17286	. . . . . 6 class Base
6	4, 5	cfv 6540	. . . . 5 class (Base‘ndx)
7	2	cv 1569	. . . . . 6 class 𝑚
8	7	csn 4591	. . . . 5 class {𝑚}
9	6, 8	cop 4597	. . . 4 class ⟨(Base‘ndx), {𝑚}⟩
10		chom 17338	. . . . . 6 class Hom
11	4, 10	cfv 6540	. . . . 5 class (Hom ‘ndx)
12	7, 5	cfv 6540	. . . . . . 7 class (Base‘𝑚)
13	7, 7, 12	cotp 4599	. . . . . 6 class ⟨𝑚, 𝑚, (Base‘𝑚)⟩
14	13	csn 4591	. . . . 5 class {⟨𝑚, 𝑚, (Base‘𝑚)⟩}
15	11, 14	cop 4597	. . . 4 class ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩
16		cco 17339	. . . . . 6 class comp
17	4, 16	cfv 6540	. . . . 5 class (comp‘ndx)
18	7, 7, 7	cotp 4599	. . . . . . 7 class ⟨𝑚, 𝑚, 𝑚⟩
19		cplusg 17327	. . . . . . . 8 class +g
20	7, 19	cfv 6540	. . . . . . 7 class (+g‘𝑚)
21	18, 20	cop 4597	. . . . . 6 class ⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩
22	21	csn 4591	. . . . 5 class {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}
23	17, 22	cop 4597	. . . 4 class ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩
24	9, 15, 23	ctp 4595	. . 3 class {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩}
25	2, 3, 24	cmpt 5194	. 2 class (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})
26	1, 25	wceq 1570	1 wff MndToCat = (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})

This definition is used by:  mndtcval  50390