Definition df-mndtc 49166

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 49168), 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 49169, mndtchom 49172, mndtcco 49173. 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 49165	. 2 class MndToCat
2		vm	. . 3 setvar 𝑚
3		cmnd 18743	. . 3 class Mnd
4		cnx 17226	. . . . . 6 class ndx
5		cbs 17243	. . . . . 6 class Base
6	4, 5	cfv 6559	. . . . 5 class (Base‘ndx)
7	2	cv 1539	. . . . . 6 class 𝑚
8	7	csn 4624	. . . . 5 class {𝑚}
9	6, 8	cop 4630	. . . 4 class ⟨(Base‘ndx), {𝑚}⟩
10		chom 17304	. . . . . 6 class Hom
11	4, 10	cfv 6559	. . . . 5 class (Hom ‘ndx)
12	7, 5	cfv 6559	. . . . . . 7 class (Base‘𝑚)
13	7, 7, 12	cotp 4632	. . . . . 6 class ⟨𝑚, 𝑚, (Base‘𝑚)⟩
14	13	csn 4624	. . . . 5 class {⟨𝑚, 𝑚, (Base‘𝑚)⟩}
15	11, 14	cop 4630	. . . 4 class ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩
16		cco 17305	. . . . . 6 class comp
17	4, 16	cfv 6559	. . . . 5 class (comp‘ndx)
18	7, 7, 7	cotp 4632	. . . . . . 7 class ⟨𝑚, 𝑚, 𝑚⟩
19		cplusg 17293	. . . . . . . 8 class +g
20	7, 19	cfv 6559	. . . . . . 7 class (+g‘𝑚)
21	18, 20	cop 4630	. . . . . 6 class ⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩
22	21	csn 4624	. . . . 5 class {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}
23	17, 22	cop 4630	. . . 4 class ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩
24	9, 15, 23	ctp 4628	. . 3 class {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩}
25	2, 3, 24	cmpt 5223	. 2 class (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})
26	1, 25	wceq 1540	1 wff MndToCat = (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})

This definition is referenced by:  mndtcval  49167