Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-natur Unicode version

Definition df-natur 25872
Description: A diagram is an indexed family of objects and morphisms in a category C. Maybe more than one morphism between two given objects, maybe none. One might choose a simple set with no structure for the set of indices as usual but we can also use a category. Let's call I this category. Morphisms of I are used as indices of morphisms of C and objects of I are used as indices of objects of C. With this convention a diagram is now a functor  e.  ( Func OLD `  <. I ,  C >. ).

Using a category for the indices is even a better solution than using a simple set because with the functions dom_ and cod_ it is easy to express the relationship between a morphism in C and its attached objects simply by naming the relationship between the morphism in I and its attached objects (let's recall a functor preserves the domain and codomain).

So ...

Let  d  e.  (
Func OLD `  <. i ,  c >. ) be a diagram, a source indexed by the objects of  i is said to be natural for the diagram provided that each morphism  m of  d and the morphisms of the source connected to its domain and codomain commute. Joy of Cats, def. 11.3, (1) p. 193. Goldblatt calls "cone" what Adamek, Herrlich and Strecker call "natural source". Experimental. (Contributed by FL, 27-Jun-2014.)

Assertion
Ref Expression
df-natur  |-  Natural  =  ( i  e.  Cat OLD  ,  t  e.  Cat OLD  |->  ( d  e.  (
Func OLD `  <. i ,  t >. )  |->  { s  e.  ( t  Source  dom  ( id_ `  i ) )  | 
A. m  e.  dom  ( dom_ `  i )
( ( ( dom_ `  t ) `  (
d `  m )
)  =  ( (
cod_ `  t ) `  ( s `  (
( dom_ `  i ) `  m ) ) )  /\  ( ( cod_ `  t ) `  (
d `  m )
)  =  ( (
cod_ `  t ) `  ( s `  (
( cod_ `  i ) `  m ) ) )  /\  ( ( d `
 m ) ( o_ `  t ) ( s `  (
( dom_ `  i ) `  m ) ) )  =  ( s `  ( ( cod_ `  i
) `  m )
) ) } ) )
Distinct variable group:    t, i, d, s, m

Detailed syntax breakdown of Definition df-natur
StepHypRef Expression
1 cntrl 25871 . 2  class  Natural
2 vi . . 3  set  i
3 vt . . 3  set  t
4 ccatOLD 25752 . . 3  class  Cat OLD
5 vd . . . 4  set  d
62cv 1622 . . . . . 6  class  i
73cv 1622 . . . . . 6  class  t
86, 7cop 3643 . . . . 5  class  <. i ,  t >.
9 cfuncOLD 25831 . . . . 5  class  Func OLD
108, 9cfv 5255 . . . 4  class  ( Func
OLD `  <. i ,  t >. )
11 vm . . . . . . . . . . 11  set  m
1211cv 1622 . . . . . . . . . 10  class  m
135cv 1622 . . . . . . . . . 10  class  d
1412, 13cfv 5255 . . . . . . . . 9  class  ( d `
 m )
15 cdom_ 25712 . . . . . . . . . 10  class  dom_
167, 15cfv 5255 . . . . . . . . 9  class  ( dom_ `  t )
1714, 16cfv 5255 . . . . . . . 8  class  ( (
dom_ `  t ) `  ( d `  m
) )
186, 15cfv 5255 . . . . . . . . . . 11  class  ( dom_ `  i )
1912, 18cfv 5255 . . . . . . . . . 10  class  ( (
dom_ `  i ) `  m )
20 vs . . . . . . . . . . 11  set  s
2120cv 1622 . . . . . . . . . 10  class  s
2219, 21cfv 5255 . . . . . . . . 9  class  ( s `
 ( ( dom_ `  i ) `  m
) )
23 ccod_ 25713 . . . . . . . . . 10  class  cod_
247, 23cfv 5255 . . . . . . . . 9  class  ( cod_ `  t )
2522, 24cfv 5255 . . . . . . . 8  class  ( (
cod_ `  t ) `  ( s `  (
( dom_ `  i ) `  m ) ) )
2617, 25wceq 1623 . . . . . . 7  wff  ( (
dom_ `  t ) `  ( d `  m
) )  =  ( ( cod_ `  t
) `  ( s `  ( ( dom_ `  i
) `  m )
) )
2714, 24cfv 5255 . . . . . . . 8  class  ( (
cod_ `  t ) `  ( d `  m
) )
286, 23cfv 5255 . . . . . . . . . . 11  class  ( cod_ `  i )
2912, 28cfv 5255 . . . . . . . . . 10  class  ( (
cod_ `  i ) `  m )
3029, 21cfv 5255 . . . . . . . . 9  class  ( s `
 ( ( cod_ `  i ) `  m
) )
3130, 24cfv 5255 . . . . . . . 8  class  ( (
cod_ `  t ) `  ( s `  (
( cod_ `  i ) `  m ) ) )
3227, 31wceq 1623 . . . . . . 7  wff  ( (
cod_ `  t ) `  ( d `  m
) )  =  ( ( cod_ `  t
) `  ( s `  ( ( cod_ `  i
) `  m )
) )
33 co_ 25715 . . . . . . . . . 10  class  o_
347, 33cfv 5255 . . . . . . . . 9  class  ( o_
`  t )
3514, 22, 34co 5858 . . . . . . . 8  class  ( ( d `  m ) ( o_ `  t
) ( s `  ( ( dom_ `  i
) `  m )
) )
3635, 30wceq 1623 . . . . . . 7  wff  ( ( d `  m ) ( o_ `  t
) ( s `  ( ( dom_ `  i
) `  m )
) )  =  ( s `  ( (
cod_ `  i ) `  m ) )
3726, 32, 36w3a 934 . . . . . 6  wff  ( ( ( dom_ `  t
) `  ( d `  m ) )  =  ( ( cod_ `  t
) `  ( s `  ( ( dom_ `  i
) `  m )
) )  /\  (
( cod_ `  t ) `  ( d `  m
) )  =  ( ( cod_ `  t
) `  ( s `  ( ( cod_ `  i
) `  m )
) )  /\  (
( d `  m
) ( o_ `  t ) ( s `
 ( ( dom_ `  i ) `  m
) ) )  =  ( s `  (
( cod_ `  i ) `  m ) ) )
3818cdm 4689 . . . . . 6  class  dom  ( dom_ `  i )
3937, 11, 38wral 2543 . . . . 5  wff  A. m  e.  dom  ( dom_ `  i
) ( ( (
dom_ `  t ) `  ( d `  m
) )  =  ( ( cod_ `  t
) `  ( s `  ( ( dom_ `  i
) `  m )
) )  /\  (
( cod_ `  t ) `  ( d `  m
) )  =  ( ( cod_ `  t
) `  ( s `  ( ( cod_ `  i
) `  m )
) )  /\  (
( d `  m
) ( o_ `  t ) ( s `
 ( ( dom_ `  i ) `  m
) ) )  =  ( s `  (
( cod_ `  i ) `  m ) ) )
40 cid_ 25714 . . . . . . . 8  class  id_
416, 40cfv 5255 . . . . . . 7  class  ( id_ `  i )
4241cdm 4689 . . . . . 6  class  dom  ( id_ `  i )
43 csrce 25865 . . . . . 6  class  Source
447, 42, 43co 5858 . . . . 5  class  ( t 
Source  dom  ( id_ `  i
) )
4539, 20, 44crab 2547 . . . 4  class  { s  e.  ( t  Source  dom  ( id_ `  i
) )  |  A. m  e.  dom  ( dom_ `  i ) ( ( ( dom_ `  t
) `  ( d `  m ) )  =  ( ( cod_ `  t
) `  ( s `  ( ( dom_ `  i
) `  m )
) )  /\  (
( cod_ `  t ) `  ( d `  m
) )  =  ( ( cod_ `  t
) `  ( s `  ( ( cod_ `  i
) `  m )
) )  /\  (
( d `  m
) ( o_ `  t ) ( s `
 ( ( dom_ `  i ) `  m
) ) )  =  ( s `  (
( cod_ `  i ) `  m ) ) ) }
465, 10, 45cmpt 4077 . . 3  class  ( d  e.  ( Func OLD ` 
<. i ,  t >.
)  |->  { s  e.  ( t  Source  dom  ( id_ `  i ) )  |  A. m  e. 
dom  ( dom_ `  i
) ( ( (
dom_ `  t ) `  ( d `  m
) )  =  ( ( cod_ `  t
) `  ( s `  ( ( dom_ `  i
) `  m )
) )  /\  (
( cod_ `  t ) `  ( d `  m
) )  =  ( ( cod_ `  t
) `  ( s `  ( ( cod_ `  i
) `  m )
) )  /\  (
( d `  m
) ( o_ `  t ) ( s `
 ( ( dom_ `  i ) `  m
) ) )  =  ( s `  (
( cod_ `  i ) `  m ) ) ) } )
472, 3, 4, 4, 46cmpt2 5860 . 2  class  ( i  e.  Cat OLD  , 
t  e.  Cat OLD  |->  ( d  e.  (
Func OLD `  <. i ,  t >. )  |->  { s  e.  ( t  Source  dom  ( id_ `  i ) )  | 
A. m  e.  dom  ( dom_ `  i )
( ( ( dom_ `  t ) `  (
d `  m )
)  =  ( (
cod_ `  t ) `  ( s `  (
( dom_ `  i ) `  m ) ) )  /\  ( ( cod_ `  t ) `  (
d `  m )
)  =  ( (
cod_ `  t ) `  ( s `  (
( cod_ `  i ) `  m ) ) )  /\  ( ( d `
 m ) ( o_ `  t ) ( s `  (
( dom_ `  i ) `  m ) ) )  =  ( s `  ( ( cod_ `  i
) `  m )
) ) } ) )
481, 47wceq 1623 1  wff  Natural  =  ( i  e.  Cat OLD  ,  t  e.  Cat OLD  |->  ( d  e.  (
Func OLD `  <. i ,  t >. )  |->  { s  e.  ( t  Source  dom  ( id_ `  i ) )  | 
A. m  e.  dom  ( dom_ `  i )
( ( ( dom_ `  t ) `  (
d `  m )
)  =  ( (
cod_ `  t ) `  ( s `  (
( dom_ `  i ) `  m ) ) )  /\  ( ( cod_ `  t ) `  (
d `  m )
)  =  ( (
cod_ `  t ) `  ( s `  (
( cod_ `  i ) `  m ) ) )  /\  ( ( d `
 m ) ( o_ `  t ) ( s `  (
( dom_ `  i ) `  m ) ) )  =  ( s `  ( ( cod_ `  i
) `  m )
) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  isntr  25873
  Copyright terms: Public domain W3C validator