Definition df-mndtc 48741

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 48743), 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 48744, mndtchom 48747, mndtcco 48748. 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 48740	. 2 class MndToCat
2		vm	. . 3 setvar 𝑚
3		cmnd 18766	. . 3 class Mnd
4		cnx 17234	. . . . . 6 class ndx
5		cbs 17252	. . . . . 6 class Base
6	4, 5	cfv 6568	. . . . 5 class (Base‘ndx)
7	2	cv 1536	. . . . . 6 class 𝑚
8	7	csn 4648	. . . . 5 class {𝑚}
9	6, 8	cop 4654	. . . 4 class ⟨(Base‘ndx), {𝑚}⟩
10		chom 17316	. . . . . 6 class Hom
11	4, 10	cfv 6568	. . . . 5 class (Hom ‘ndx)
12	7, 5	cfv 6568	. . . . . . 7 class (Base‘𝑚)
13	7, 7, 12	cotp 4656	. . . . . 6 class ⟨𝑚, 𝑚, (Base‘𝑚)⟩
14	13	csn 4648	. . . . 5 class {⟨𝑚, 𝑚, (Base‘𝑚)⟩}
15	11, 14	cop 4654	. . . 4 class ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩
16		cco 17317	. . . . . 6 class comp
17	4, 16	cfv 6568	. . . . 5 class (comp‘ndx)
18	7, 7, 7	cotp 4656	. . . . . . 7 class ⟨𝑚, 𝑚, 𝑚⟩
19		cplusg 17305	. . . . . . . 8 class +g
20	7, 19	cfv 6568	. . . . . . 7 class (+g‘𝑚)
21	18, 20	cop 4654	. . . . . 6 class ⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩
22	21	csn 4648	. . . . 5 class {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}
23	17, 22	cop 4654	. . . 4 class ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩
24	9, 15, 23	ctp 4652	. . 3 class {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩}
25	2, 3, 24	cmpt 5249	. 2 class (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})
26	1, 25	wceq 1537	1 wff MndToCat = (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})

This definition is referenced by:  mndtcval  48742