The support for building towers of category constructors is one of the main design features of CAP. Many categories that appear in the various applications can be modeled by towers of multiple category constructors. The category constructor ReinterpretationOfCategory (12.6-1) allows adding one last layer on top which allows expressing the desired (re)interpretation of such a modeling tower. In particular, this category constructor allows specifying the name of the category together with customized methods for the operations
ObjectConstructor
MorphismConstructor
ObjectDatum
MorphismDatum
in order to reflect the desired (re)interpretation with a user-interface that is independent of the modeling tower (see below for details). Note that the same tower might have multiple interpretations.
R := ReinterpretationOfCategory( cat_n ) |
cat_n := CategoryConstructor_n( cat_{n-1} ) |
| ... |
cat_1 := CategoryConstructor_1( non_categorical_input ) |
The reinterpretation R is isomorphic to the top category cat_n in the tower. In practice, the word tower
stands more generally for a finite poset with a greatest element.
We will show how one can reinterpret a category with the following guiding example: We reinterpret Opposite( CategoryOfRows( R ) ) as CategoryOfColumns( R ) using ReinterpretationOfCategory (12.6-1) with the options described in the following (see CategoryOfColumns_as_Opposite_CategoryOfRows.gi in FreydCategoriesForCAP for a full implementation).
Set the options category_filter, category_object_filter, and category_morphism_filter to the filters corresponding to the data structure of the desired reinterpretation, e.g. IsCategoryOfColumns, IsCategoryOfColumsObject, and IsCategoryOfColumsMorphism.
Set object_constructor, object_datum, morphism_constructor, and morphism_datum to the functions one would write for ObjectConstructor and so on for a primitive implementation of the desired reinterpretation. In our example, object_constructor takes the reinterpretation R (which lies in IsCategoryOfColumns due to the filter set in the first step) and an integer, and returns a CAP object in the category with attribute RankOfObject set to the integer, just like a primitive implementation of CategoryOfColumns would do.
Set modeling_tower_object_constructor, modeling_tower_object_datum, modeling_tower_morphism_constructor, and modeling_tower_morphism_datum: modeling_tower_object_constructor gets the same input as object_constructor but must return the corresponding object in the tower cat_n. modeling_tower_object_datum has the same output as object_datum but gets the reinterpretation R and an object in the tower cat_n as an input. In our example, modeling_tower_object_constructor gets the reinterpretation R and an integer as in step 2 and wraps the integer as a CategoryOfRowsObject and the result as an object in the opposite category. modeling_tower_object_datum gets the reinterpretation R and an object in Opposite( CategoryOfRows( R ) ) (that is, an integer boxed as a category of rows object boxed as an object in the opposite category) and returns the underlying integer. modeling_tower_morphism_constructor and modeling_tower_morphism_datum are given analogously.
By composing modeling_tower_object_datum with object_constructor and modeling_tower_morphism_datum with morphism_constructor (with suitable source and range), ReinterpretationOfCategory defines a functor "Reinterpretation" from cat_n to R. Similarly, it defines a functor "Model" from R to cat_n by composing object_datum with modeling_tower_object_constructor and morphism_datum with modeling_tower_morphism_constructor (with suitable source and range). "Reinterpretation" should be an isomorphism of categories with inverse "Model". More precisely, one has to take care of the following things:
Since R should just be a reinterpretation of cat_n with a nicer data structure, we certainly want "Reinterpretation" to be an equivalence of categories with pseudo-inverse "Model".
ReinterpretationOfCategory copies all properties from cat_n to R, including properties like IsSkeletalCategory which are not necessarily preserved by mere equivalences.
To fulfill the specification of WithGiven operations, reinterpreting a WithGiven object A in cat_n as an object in R and taking its model again must give an object equal to A. So we require applying "Reinterpretation" and then "Model" to give the identity. Conversely, let B_1 be an object in R. We take its model and reinterpret this again to form an object B_2. By construction of R, B_1 and B_2 are equal if and only if their models are equal. But since applying "Reinterpretation" and then "Model" gives the identity, taking the model of B_2 simply gives an object equal to the model of B_1. Thus, also B_1 and B_2 are equal. Hence, "Reinterpretation" has to be an equivalence which is a bijection on objects, and hence an isomorphism (although "Model" is not necessarily its inverse). Note: Alternatively, one can make sure that WithGiven operations in cat_n are only called via the corresponding non-WithGiven operation in cat_n. This can be achieved by reinterpreting all operations of cat_n (i.e. creating R with only_primitive_operations := false), disabling redirect functions (i.e. creating R with the option overhead := false) and not calling WithGiven operations of R manually.
Operations in ReinterpretationOfCategory are implemented as follows:
Apply object_datum and morphism_datum to the input to get the underlying data.
Apply modeling_tower_object_constructor and modeling_tower_morphism_constructor to the underlying data to get objects and morphisms in the tower cat_n.
Apply the operation of the tower cat_n.
Apply modeling_tower_object_datum or modeling_tower_morphism_datum to the result to get the underlying data.
Apply object_constructor or morphism_constructor to the underlying data to get an object or a morphism in the reinterpretation R.
The first two steps define the functor "Model" and the last two steps define the functor "Reinterpretation". "Reinterpretation" on objects and morphisms is called ReinterpretationOfObject and ReinterpretationOfMorphism in the code. "Model" on objects and morphisms is called ModelingObject and ModelingMorphism in the code.
CompilerForCAPThe operation of the tower cat_n (step 3 above) usually unboxes objects and morphisms, operates on the underlying data, and boxes the result. The unboxing usually cancels with step 2 above, and boxing the result usually cancels with step 4 above. If one now compiles the operations of the reinterpretation R, only the following steps remain:
Apply object_datum and morphism_datum to the input to get the underlying data.
Operate on the underlying data. (previously part of step 3)
Apply object_constructor or morphism_constructor to the underlying data to get an object or a morphism in the reinterpretation R. (previously step 5)
This is exactly what a primitive implementation would look like. Thus, in many cases compiling a reinterpretation immediately gives a primitive implementation with no remaining references to the tower cat_n.
‣ ModelingCategory( R ) | ( attribute ) |
Returns: a category
The tower cat_n modeling the reinterpretation R.
‣ ReinterpretationOfCategory( category, options ) | ( operation ) |
Returns: a category
Reinterprets a category category (the "modeling category") to form a new category R (the "reinterpretation") subject to the options given via options, which is a record with the following keys:
name: the name of the reinterpretation R,
category_filter, category_object_filter, category_morphism_filter, object_datum_type, morphism_datum_type, object_constructor, object_datum, morphism_constructor, morphism_datum: same meaning as for CategoryConstructor (11.2-1), which is used to create the reinterpretation R,
modeling_tower_object_constructor: a function which gets the reinterpretation R and an object datum (in the sense of object_datum) and returns the corresponding modeling object in the modeling category,
modeling_tower_object_datum: a function which gets the reinterpretation R and an object in the modeling category and returns the corresponding object datum (in the sense of object_datum),
modeling_tower_morphism_constructor: a function which gets the reinterpretation R, a source in the modeling category, a morphism datum (in the sense of morphism_datum), and a range in the modeling category and returns the corresponding modeling morphism in the modeling category,
modeling_tower_morphism_datum: a function which gets the reinterpretation R and a morphism in the modeling category and returns the corresponding morphism datum (in the sense of morphism_datum),
only_primitive_operations (optional, default false): whether to only reinterpret primitive operations or all operations.
‣ ReinterpretationFunctor( R ) | ( attribute ) |
Returns: a functor
Returns the functor from the modeling category ModelingCategory(R) to the reinterpretation R which maps each object/morphism to its reinterpretation.
‣ ModelingObject( R, obj ) | ( operation ) |
Returns: a CAP category object
Returns the object in ModelingCategory(R) modeling the object obj in the reinterpretation R.
‣ ReinterpretationOfObject( R, obj ) | ( operation ) |
Returns: a CAP category object
Returns the reinterpretation in R of an object obj in ModelingCategory(R).
‣ ModelingMorphism( R, mor ) | ( operation ) |
Returns: a CAP category morphism
Returns the morphism in ModelingCategory(R) modeling the morphism mor in the reinterpretation R.
‣ ReinterpretationOfMorphism( R, source, obj, range ) | ( operation ) |
Returns: a CAP category morphism
Returns the reinterpretation in R with given source and range of a morphism mor in ModelingCategory(R).
generated by GAPDoc2HTML