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 45866
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 45868) , 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 45869, mndtchom 45871, mndtcco 45872. 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 45865 . 2 class MndToCat
2 vm . . 3 setvar 𝑚
3 cmnd 18039 . . 3 class Mnd
4 cnx 16595 . . . . . 6 class ndx
5 cbs 16598 . . . . . 6 class Base
64, 5cfv 6349 . . . . 5 class (Base‘ndx)
72cv 1541 . . . . . 6 class 𝑚
87csn 4526 . . . . 5 class {𝑚}
96, 8cop 4532 . . . 4 class ⟨(Base‘ndx), {𝑚}⟩
10 chom 16691 . . . . . 6 class Hom
114, 10cfv 6349 . . . . 5 class (Hom ‘ndx)
127, 5cfv 6349 . . . . . . 7 class (Base‘𝑚)
137, 7, 12cotp 4534 . . . . . 6 class 𝑚, 𝑚, (Base‘𝑚)⟩
1413csn 4526 . . . . 5 class {⟨𝑚, 𝑚, (Base‘𝑚)⟩}
1511, 14cop 4532 . . . 4 class ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩
16 cco 16692 . . . . . 6 class comp
174, 16cfv 6349 . . . . 5 class (comp‘ndx)
187, 7, 7cotp 4534 . . . . . . 7 class 𝑚, 𝑚, 𝑚
19 cplusg 16680 . . . . . . . 8 class +g
207, 19cfv 6349 . . . . . . 7 class (+g𝑚)
2118, 20cop 4532 . . . . . 6 class ⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩
2221csn 4526 . . . . 5 class {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩}
2317, 22cop 4532 . . . 4 class ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩}⟩
249, 15, 23ctp 4530 . . 3 class {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩}⟩}
252, 3, 24cmpt 5120 . 2 class (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩}⟩})
261, 25wceq 1542 1 wff MndToCat = (𝑚 ∈ Mnd ↦ {⟨(Base‘ndx), {𝑚}⟩, ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩}⟩})
Colors of variables: wff setvar class
This definition is referenced by:  mndtcval  45867
  Copyright terms: Public domain W3C validator