Definition df-mndtc 48812

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 48814), 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 48815, mndtchom 48818, mndtcco 48819. 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 48811	. 2 class MndToCat
2		vm	. . 3 setvar 𝑚
3		cmnd 18749	. . 3 class Mnd
4		cnx 17217	. . . . . 6 class ndx
5		cbs 17235	. . . . . 6 class Base
6	4, 5	cfv 6559	. . . . 5 class (Base‘ndx)
7	2	cv 1534	. . . . . 6 class 𝑚
8	7	csn 4631	. . . . 5 class {𝑚}
9	6, 8	cop 4637	. . . 4 class ⟨(Base‘ndx), {𝑚}⟩
10		chom 17299	. . . . . 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 4639	. . . . . 6 class ⟨𝑚, 𝑚, (Base‘𝑚)⟩
14	13	csn 4631	. . . . 5 class {⟨𝑚, 𝑚, (Base‘𝑚)⟩}
15	11, 14	cop 4637	. . . 4 class ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩
16		cco 17300	. . . . . 6 class comp
17	4, 16	cfv 6559	. . . . 5 class (comp‘ndx)
18	7, 7, 7	cotp 4639	. . . . . . 7 class ⟨𝑚, 𝑚, 𝑚⟩
19		cplusg 17288	. . . . . . . 8 class +g
20	7, 19	cfv 6559	. . . . . . 7 class (+g‘𝑚)
21	18, 20	cop 4637	. . . . . 6 class ⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩
22	21	csn 4631	. . . . 5 class {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}
23	17, 22	cop 4637	. . . 4 class ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩
24	9, 15, 23	ctp 4635	. . 3 class {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩}
25	2, 3, 24	cmpt 5233	. 2 class (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})
26	1, 25	wceq 1535	1 wff MndToCat = (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g‘𝑚)⟩}⟩})

This definition is referenced by:  mndtcval  48813