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.
CompilerForCAP
The 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