Definition df-mndtc 49610

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 49612), 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 49613, mndtchom 49616, mndtcco 49617. 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 49609	. 2 class MndToCat
2		vm	. . 3 setvar 𝑚
3		cmnd 18637	. . 3 class Mnd
4		cnx 17099	. . . . . 6 class ndx
5		cbs 17115	. . . . . 6 class Base
6	4, 5	cfv 6476	. . . . 5 class (Base‘ndx)
7	2	cv 1540	. . . . . 6 class 𝑚
8	7	csn 4571	. . . . 5 class {𝑚}
9	6, 8	cop 4577	. . . 4 class ⟨(Base‘ndx), {𝑚}⟩
10		chom 17167	. . . . . 6 class Hom
11	4, 10	cfv 6476	. . . . 5 class (Hom ‘ndx)
12	7, 5	cfv 6476	. . . . . . 7 class (Base‘𝑚)
13	7, 7, 12	cotp 4579	. . . . . 6 class ⟨𝑚, 𝑚, (Base‘𝑚)⟩
14	13	csn 4571	. . . . 5 class {⟨𝑚, 𝑚, (Base‘𝑚)⟩}
15	11, 14	cop 4577	. . . 4 class ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩
16		cco 17168	. . . . . 6 class comp
17	4, 16	cfv 6476	. . . . 5 class (comp‘ndx)
18	7, 7, 7	cotp 4579	. . . . . . 7 class ⟨𝑚, 𝑚, 𝑚⟩
19		cplusg 17156	. . . . . . . 8 class +g
20	7, 19	cfv 6476	. . . . . . 7 class (+g‘𝑚)
21	18, 20	cop 4577	. . . . . 6 class ⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩
22	21	csn 4571	. . . . 5 class {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}
23	17, 22	cop 4577	. . . 4 class ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩
24	9, 15, 23	ctp 4575	. . 3 class {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩}
25	2, 3, 24	cmpt 5167	. 2 class (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})
26	1, 25	wceq 1541	1 wff MndToCat = (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})

This definition is referenced by:  mndtcval  49611