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 . 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 be a diagram, a source indexed by the objects of is said to be natural for the diagram provided that each morphism of 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
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-natur
StepHypRef Expression
1 cntrl 25974 . 2
2 vi . . 3
3 vt . . 3
4 ccatOLD 25855 . . 3
5 vd . . . 4
62cv 1631 . . . . . 6
73cv 1631 . . . . . 6
86, 7cop 3656 . . . . 5
9 cfuncOLD 25934 . . . . 5
108, 9cfv 5271 . . . 4
11 vm . . . . . . . . . . 11
1211cv 1631 . . . . . . . . . 10
135cv 1631 . . . . . . . . . 10
1412, 13cfv 5271 . . . . . . . . 9
15 cdom_ 25815 . . . . . . . . . 10
167, 15cfv 5271 . . . . . . . . 9
1714, 16cfv 5271 . . . . . . . 8
186, 15cfv 5271 . . . . . . . . . . 11
1912, 18cfv 5271 . . . . . . . . . 10
20 vs . . . . . . . . . . 11
2120cv 1631 . . . . . . . . . 10
2219, 21cfv 5271 . . . . . . . . 9
23 ccod_ 25816 . . . . . . . . . 10
247, 23cfv 5271 . . . . . . . . 9
2522, 24cfv 5271 . . . . . . . 8
2617, 25wceq 1632 . . . . . . 7
2714, 24cfv 5271 . . . . . . . 8
286, 23cfv 5271 . . . . . . . . . . 11
2912, 28cfv 5271 . . . . . . . . . 10
3029, 21cfv 5271 . . . . . . . . 9
3130, 24cfv 5271 . . . . . . . 8
3227, 31wceq 1632 . . . . . . 7
33 co_ 25818 . . . . . . . . . 10
347, 33cfv 5271 . . . . . . . . 9
3514, 22, 34co 5874 . . . . . . . 8
3635, 30wceq 1632 . . . . . . 7
3726, 32, 36w3a 934 . . . . . 6
3818cdm 4705 . . . . . 6
3937, 11, 38wral 2556 . . . . 5
40 cid_ 25817 . . . . . . . 8
416, 40cfv 5271 . . . . . . 7
4241cdm 4705 . . . . . 6
43 csrce 25968 . . . . . 6
447, 42, 43co 5874 . . . . 5
4539, 20, 44crab 2560 . . . 4
465, 10, 45cmpt 4093 . . 3
472, 3, 4, 4, 46cmpt2 5876 . 2
481, 47wceq 1632 1
 Colors of variables: wff set class This definition is referenced by:  isntr  25976
 Copyright terms: Public domain W3C validator