|
3 | 3 | # |
4 | 4 | # Implementations |
5 | 5 | # |
6 | | -InstallValue( CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD, rec( |
| 6 | +InstallValue( CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD, rec( ) ); |
7 | 7 |
|
8 | | -EveryCategory := [ |
9 | | - "PreCompose", "IdentityMorphism", "IsEqualForObjects", "IsEqualForMorphisms", "IsCongruentForMorphisms" ], |
| 8 | +CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.EveryCategory := [ |
| 9 | + "PreCompose", |
| 10 | + "IdentityMorphism", |
| 11 | + "IsEqualForObjects", |
| 12 | + "IsEqualForMorphisms", |
| 13 | + "IsCongruentForMorphisms", |
| 14 | +]; |
10 | 15 |
|
11 | | -IsEquippedWithHomomorphismStructure := Concatenation( [ |
12 | | - "DistinguishedObjectOfHomomorphismStructure", |
13 | | - "HomomorphismStructureOnObjects", |
14 | | - "HomomorphismStructureOnMorphisms", |
15 | | - "InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure", |
16 | | - "InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism" ], ~.EveryCategory ), |
17 | 16 |
|
18 | | -IsEnrichedOverCommutativeRegularSemigroup := Concatenation( |
19 | | - [ "AdditionForMorphisms" ], ~.EveryCategory ), |
| 17 | +CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsEquippedWithHomomorphismStructure := Concatenation( |
| 18 | + CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.EveryCategory, |
| 19 | + [ |
| 20 | + "DistinguishedObjectOfHomomorphismStructure", |
| 21 | + "HomomorphismStructureOnObjects", |
| 22 | + "HomomorphismStructureOnMorphisms", |
| 23 | + "InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure", |
| 24 | + "InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism", |
| 25 | + ] |
| 26 | +); |
20 | 27 |
|
21 | | -IsAbCategory := Concatenation( [ |
22 | | - "ZeroMorphism", |
23 | | - "IsZeroForMorphisms", |
24 | | - "SubtractionForMorphisms", |
25 | | - "AdditiveInverseForMorphisms" ], ~.IsEnrichedOverCommutativeRegularSemigroup ), |
| 28 | +CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsEnrichedOverCommutativeRegularSemigroup := Concatenation( |
| 29 | + CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.EveryCategory, |
| 30 | + [ |
| 31 | + "AdditionForMorphisms", |
| 32 | + ] |
| 33 | +); |
26 | 34 |
|
27 | | -IsLinearCategoryOverCommutativeRing := Concatenation( [ |
28 | | - "MultiplyWithElementOfCommutativeRingForMorphisms" ], ~.IsAbCategory ), |
| 35 | +CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbCategory := Concatenation( |
| 36 | + CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsEnrichedOverCommutativeRegularSemigroup, |
| 37 | + [ |
| 38 | + "ZeroMorphism", |
| 39 | + "IsZeroForMorphisms", |
| 40 | + "SubtractionForMorphisms", |
| 41 | + "AdditiveInverseForMorphisms", |
| 42 | + ] |
| 43 | +); |
29 | 44 |
|
30 | | -IsAdditiveCategory := Concatenation( [ |
31 | | - "ZeroObject", |
32 | | - "UniversalMorphismFromZeroObject", |
33 | | - "UniversalMorphismIntoZeroObject", |
34 | | - "DirectSum", |
35 | | - "ProjectionInFactorOfDirectSum", |
36 | | - "InjectionOfCofactorOfDirectSum", |
37 | | - "UniversalMorphismIntoDirectSum", |
38 | | - "UniversalMorphismFromDirectSum" ], ~.IsAbCategory ), |
| 45 | +CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsLinearCategoryOverCommutativeRing := Concatenation( |
| 46 | + CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbCategory, |
| 47 | + [ |
| 48 | + "MultiplyWithElementOfCommutativeRingForMorphisms", |
| 49 | + ] |
| 50 | +); |
39 | 51 |
|
40 | | -IsPreAbelianCategory := Concatenation( [ |
41 | | -"KernelObject", |
42 | | -"KernelEmbedding", |
43 | | -"KernelLift", |
44 | | -"CokernelObject", |
45 | | -"CokernelProjection", |
46 | | -"CokernelColift" |
47 | | -], ~.IsAdditiveCategory ), |
| 52 | +CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAdditiveCategory := Concatenation( |
| 53 | + CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbCategory, |
| 54 | + [ |
| 55 | + "ZeroObject", |
| 56 | + "UniversalMorphismFromZeroObject", |
| 57 | + "UniversalMorphismIntoZeroObject", |
| 58 | + "DirectSum", |
| 59 | + "ProjectionInFactorOfDirectSum", |
| 60 | + "InjectionOfCofactorOfDirectSum", |
| 61 | + "UniversalMorphismIntoDirectSum", |
| 62 | + "UniversalMorphismFromDirectSum", |
| 63 | + ] |
| 64 | +); |
48 | 65 |
|
49 | | -IsAbelianCategory := Concatenation( [ |
50 | | -"LiftAlongMonomorphism", |
51 | | -"ColiftAlongEpimorphism" ], ~.IsPreAbelianCategory ), |
| 66 | +CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsPreAbelianCategory := Concatenation( |
| 67 | + CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAdditiveCategory, |
| 68 | + [ |
| 69 | + "KernelObject", |
| 70 | + "KernelEmbedding", |
| 71 | + "KernelLift", |
| 72 | + "CokernelObject", |
| 73 | + "CokernelProjection", |
| 74 | + "CokernelColift", |
| 75 | + ] |
| 76 | +); |
52 | 77 |
|
53 | | -IsAbelianCategoryWithEnoughProjectives := Concatenation( [ |
54 | | -"EpimorphismFromSomeProjectiveObject", |
55 | | -"ProjectiveLift" |
56 | | -], ~.IsAbelianCategory ), |
| 78 | +CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory := Concatenation( |
| 79 | + CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsPreAbelianCategory, |
| 80 | + [ |
| 81 | + "LiftAlongMonomorphism", |
| 82 | + "ColiftAlongEpimorphism", |
| 83 | + ] |
| 84 | +); |
57 | 85 |
|
58 | | -IsAbelianCategoryWithEnoughInjectives := Concatenation( [ |
59 | | -"MonomorphismIntoSomeInjectiveObject", |
60 | | -"InjectiveColift" |
61 | | -], ~.IsAbelianCategory ) |
62 | | - |
63 | | -) ); |
| 86 | +CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategoryWithEnoughProjectives := Concatenation( |
| 87 | + CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory, |
| 88 | + [ |
| 89 | + "EpimorphismFromSomeProjectiveObject", |
| 90 | + "ProjectiveLift", |
| 91 | + ] |
| 92 | +); |
64 | 93 |
|
| 94 | +CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategoryWithEnoughInjectives := Concatenation( |
| 95 | + CAP_INTERNAL_CONSTRUCTIVE_CATEGORIES_RECORD.IsAbelianCategory, |
| 96 | + [ |
| 97 | + "MonomorphismIntoSomeInjectiveObject", |
| 98 | + "InjectiveColift", |
| 99 | + ] |
| 100 | +); |
0 commit comments