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 25975
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 25974 . 2  class  Natural
2 vi . . 3  set  i
3 vt . . 3  set  t
4 ccatOLD 25855 . . 3  class  Cat OLD
5 vd . . . 4  set  d
62cv 1631 . . . . . 6  class  i
73cv 1631 . . . . . 6  class  t
86, 7cop 3656 . . . . 5  class  <. i ,  t >.
9 cfuncOLD 25934 . . . . 5  class  Func OLD
108, 9cfv 5271 . . . 4  class  ( Func
OLD `  <. i ,  t >. )
11 vm . . . . . . . . . . 11  set  m
1211cv 1631 . . . . . . . . . 10  class  m
135cv 1631 . . . . . . . . . 10  class  d
1412, 13cfv 5271 . . . . . . . . 9  class  ( d `
 m )
15 cdom_ 25815 . . . . . . . . . 10  class  dom_
167, 15cfv 5271 . . . . . . . . 9  class  ( dom_ `  t )
1714, 16cfv 5271 . . . . . . . 8  class  ( (
dom_ `  t ) `  ( d `  m
) )
186, 15cfv 5271 . . . . . . . . . . 11  class  ( dom_ `  i )
1912, 18cfv 5271 . . . . . . . . . 10  class  ( (
dom_ `  i ) `  m )
20 vs . . . . . . . . . . 11  set  s
2120cv 1631 . . . . . . . . . 10  class  s
2219, 21cfv 5271 . . . . . . . . 9  class  ( s `
 ( ( dom_ `  i ) `  m
) )
23 ccod_ 25816 . . . . . . . . . 10  class  cod_
247, 23cfv 5271 . . . . . . . . 9  class  ( cod_ `  t )
2522, 24cfv 5271 . . . . . . . 8  class  ( (
cod_ `  t ) `  ( s `  (
( dom_ `  i ) `  m ) ) )
2617, 25wceq 1632 . . . . . . 7  wff  ( (
dom_ `  t ) `  ( d `  m
) )  =  ( ( cod_ `  t
) `  ( s `  ( ( dom_ `  i
) `  m )
) )
2714, 24cfv 5271 . . . . . . . 8  class  ( (
cod_ `  t ) `  ( d `  m
) )
286, 23cfv 5271 . . . . . . . . . . 11  class  ( cod_ `  i )
2912, 28cfv 5271 . . . . . . . . . 10  class  ( (
cod_ `  i ) `  m )
3029, 21cfv 5271 . . . . . . . . 9  class  ( s `
 ( ( cod_ `  i ) `  m
) )
3130, 24cfv 5271 . . . . . . . 8  class  ( (
cod_ `  t ) `  ( s `  (
( cod_ `  i ) `  m ) ) )
3227, 31wceq 1632 . . . . . . 7  wff  ( (
cod_ `  t ) `  ( d `  m
) )  =  ( ( cod_ `  t
) `  ( s `  ( ( cod_ `  i
) `  m )
) )
33 co_ 25818 . . . . . . . . . 10  class  o_
347, 33cfv 5271 . . . . . . . . 9  class  ( o_
`  t )
3514, 22, 34co 5874 . . . . . . . 8  class  ( ( d `  m ) ( o_ `  t
) ( s `  ( ( dom_ `  i
) `  m )
) )
3635, 30wceq 1632 . . . . . . 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 4705 . . . . . 6  class  dom  ( dom_ `  i )
3937, 11, 38wral 2556 . . . . 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_ 25817 . . . . . . . 8  class  id_
416, 40cfv 5271 . . . . . . 7  class  ( id_ `  i )
4241cdm 4705 . . . . . 6  class  dom  ( id_ `  i )
43 csrce 25968 . . . . . 6  class  Source
447, 42, 43co 5874 . . . . 5  class  ( t 
Source  dom  ( id_ `  i
) )
4539, 20, 44crab 2560 . . . 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 4093 . . 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 5876 . 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 1632 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  25976
  Copyright terms: Public domain W3C validator