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 47190
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 47192), 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 47193, mndtchom 47196, mndtcco 47197. 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 47189 . 2 class MndToCat
2 vm . . 3 setvar π‘š
3 cmnd 18561 . . 3 class Mnd
4 cnx 17070 . . . . . 6 class ndx
5 cbs 17088 . . . . . 6 class Base
64, 5cfv 6497 . . . . 5 class (Baseβ€˜ndx)
72cv 1541 . . . . . 6 class π‘š
87csn 4587 . . . . 5 class {π‘š}
96, 8cop 4593 . . . 4 class ⟨(Baseβ€˜ndx), {π‘š}⟩
10 chom 17149 . . . . . 6 class Hom
114, 10cfv 6497 . . . . 5 class (Hom β€˜ndx)
127, 5cfv 6497 . . . . . . 7 class (Baseβ€˜π‘š)
137, 7, 12cotp 4595 . . . . . 6 class βŸ¨π‘š, π‘š, (Baseβ€˜π‘š)⟩
1413csn 4587 . . . . 5 class {βŸ¨π‘š, π‘š, (Baseβ€˜π‘š)⟩}
1511, 14cop 4593 . . . 4 class ⟨(Hom β€˜ndx), {βŸ¨π‘š, π‘š, (Baseβ€˜π‘š)⟩}⟩
16 cco 17150 . . . . . 6 class comp
174, 16cfv 6497 . . . . 5 class (compβ€˜ndx)
187, 7, 7cotp 4595 . . . . . . 7 class βŸ¨π‘š, π‘š, π‘šβŸ©
19 cplusg 17138 . . . . . . . 8 class +g
207, 19cfv 6497 . . . . . . 7 class (+gβ€˜π‘š)
2118, 20cop 4593 . . . . . 6 class βŸ¨βŸ¨π‘š, π‘š, π‘šβŸ©, (+gβ€˜π‘š)⟩
2221csn 4587 . . . . 5 class {βŸ¨βŸ¨π‘š, π‘š, π‘šβŸ©, (+gβ€˜π‘š)⟩}
2317, 22cop 4593 . . . 4 class ⟨(compβ€˜ndx), {βŸ¨βŸ¨π‘š, π‘š, π‘šβŸ©, (+gβ€˜π‘š)⟩}⟩
249, 15, 23ctp 4591 . . 3 class {⟨(Baseβ€˜ndx), {π‘š}⟩, ⟨(Hom β€˜ndx), {βŸ¨π‘š, π‘š, (Baseβ€˜π‘š)⟩}⟩, ⟨(compβ€˜ndx), {βŸ¨βŸ¨π‘š, π‘š, π‘šβŸ©, (+gβ€˜π‘š)⟩}⟩}
252, 3, 24cmpt 5189 . 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  47191
  Copyright terms: Public domain W3C validator