Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mndtc Structured version   Visualization version   GIF version

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
StepHypRef 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
64, 5cfv 6559 . . . . 5 class (Base‘ndx)
72cv 1539 . . . . . 6 class 𝑚
87csn 4624 . . . . 5 class {𝑚}
96, 8cop 4630 . . . 4 class ⟨(Base‘ndx), {𝑚}⟩
10 chom 17304 . . . . . 6 class Hom
114, 10cfv 6559 . . . . 5 class (Hom ‘ndx)
127, 5cfv 6559 . . . . . . 7 class (Base‘𝑚)
137, 7, 12cotp 4632 . . . . . 6 class 𝑚, 𝑚, (Base‘𝑚)⟩
1413csn 4624 . . . . 5 class {⟨𝑚, 𝑚, (Base‘𝑚)⟩}
1511, 14cop 4630 . . . 4 class ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩
16 cco 17305 . . . . . 6 class comp
174, 16cfv 6559 . . . . 5 class (comp‘ndx)
187, 7, 7cotp 4632 . . . . . . 7 class 𝑚, 𝑚, 𝑚
19 cplusg 17293 . . . . . . . 8 class +g
207, 19cfv 6559 . . . . . . 7 class (+g𝑚)
2118, 20cop 4630 . . . . . 6 class ⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩
2221csn 4624 . . . . 5 class {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩}
2317, 22cop 4630 . . . 4 class ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩}⟩
249, 15, 23ctp 4628 . . 3 class {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩}⟩}
252, 3, 24cmpt 5223 . 2 class (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩}⟩})
261, 25wceq 1540 1 wff MndToCat = (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩}⟩})
Colors of variables: wff setvar class
This definition is referenced by:  mndtcval  49167
  Copyright terms: Public domain W3C validator