-
Notifications
You must be signed in to change notification settings - Fork 4
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
d&i IsClosedPreSheafWRTCoproductCocones
- Loading branch information
1 parent
7641847
commit 24d7531
Showing
34 changed files
with
2,617 additions
and
26 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
#! @Chunk ColimitingCocone | ||
|
||
#! @Example | ||
LoadPackage( "FunctorCategories", false ); | ||
#! true | ||
q := "q(a,l,m,r,i,i1,i2,c,b)[ac:a->c,lc:l->c,mi:m->i,ic:i->c,ri1:r->i1,i1i2:i1->i2,i2c:i2->c,cb:c->b]";; | ||
q := RightQuiver( q ); | ||
#! RightQuiver( "" ); | ||
F := FreeCategory( q ); | ||
#F := PathCategory( q ); | ||
#! FreeCategory( | ||
#! RightQuiver( "" ) ); | ||
Size( F ); | ||
#! 7 | ||
PSh := PreSheaves( F ); | ||
#! PreSheaves( FreeCategory( | ||
#! RightQuiver( "" ) ) ); | ||
#! SkeletalFinSets ) | ||
Y := YonedaEmbeddingOfSourceCategory( PSh ); | ||
#! Yoneda embedding functor | ||
coprd_cocone := [ F.c, [ F.lc, F.mi * F.ic, F.ri1 * F.i1i2 * F.i2c ] ]; | ||
#coprd_cocone := [ F.c, [ F.ac, F.lc ] ]; | ||
is_closed := G -> IsClosedPreSheafWRTCoproductCocones( PSh, G, [ coprd_cocone ] ); | ||
#! function( G ) ... end | ||
G := Coproduct( [ PSh.a, PSh.a, PSh.l, PSh.m, PSh.r, PSh.r, PSh.c, PSh.b ] ); | ||
#G := Coproduct( [ PSh.a, PSh.l, PSh.l ] ); | ||
#! <An object in PreSheaves( FreeCategory( | ||
#! RightQuiver( "" ) ), | ||
#! SkeletalFinSets )> | ||
emb := EmbeddingIntoClosureOfPreSheafWRTCoproductCocones( G, [ coprd_cocone ] ); | ||
Assert( 0, IsWellDefined( emb ) ); | ||
Assert( 0, IsMonomorphism( emb ) ); | ||
Assert( 0, Source( emb ) = G ); | ||
Assert( 0, is_closed( Target( emb ) ) ); | ||
#! @EndExample |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
#! @Chunk JoinCocone | ||
|
||
#! @Example | ||
LoadPackage( "FunctorCategories", false ); | ||
#! true | ||
q := FinQuiver( "q(a,l,r,i,c,b)[ac:a->c,lc:l->c,ri:r->i,ic:i->c,cb:c->b]" ); | ||
#! FinQuiver( "q(a,l,r,i,c,b)[ac:a-≻c,lc:l-≻c,ri:r-≻i,ic:i-≻c,cb:c-≻b]" ) | ||
F := PathCategory( q ); | ||
#! PathCategory( | ||
#! FinQuiver( "q(a,l,r,i,c,b)[ac:a-≻c,lc:l-≻c,ri:r-≻i,ic:i-≻c,cb:c-≻b]" ) ) | ||
Size( F ); | ||
#! 16 | ||
P := PosetOfCategory( F ); | ||
#! PosetOfCategory( PathCategory( | ||
#! FinQuiver( "q(a,l,r,i,c,b)[ac:a-≻c,lc:l-≻c,ri:r-≻i,ic:i-≻c,cb:c-≻b]" ) ) ) | ||
Size( P ); | ||
#! 16 | ||
digraphF := DigraphOfPoset( P );; | ||
digraphF!.vertexlabels := List( SetOfObjects( F ), String ); | ||
#Splash( DotVertexLabelledDigraph( digraphF ) ); | ||
#Splash( DotVertexLabelledDigraph( DigraphOfPoset( P ) ) ); | ||
PSh := PreSheaves( P ); | ||
#! PreSheaves( PosetOfCategory( PathCategory( | ||
#! FinQuiver( "q(a,l,r,i,c,b)[ac:a-≻c,lc:l-≻c,ri:r-≻i,ic:i-≻c,cb:c-≻b]" ) ) ), | ||
#! IntervalCategory ) | ||
Y := YonedaEmbeddingOfSourceCategory( PSh ); | ||
#! Yoneda embedding functor | ||
coproducts := [ [ P.c, [ P.l, P.r ] ] ];; | ||
#! [ [ An object in the poset given by: (c), | ||
#! [ An object in the poset given by: (l), | ||
#! An object in the poset given by: (r) ] ] ] | ||
PSh_J := ClosedPreSheavesWRTCoproducts( P, coproducts );; | ||
closed := SetOfObjects( PSh_J );; | ||
Assert( 0, Length( closed ) = 10 ); | ||
psh_J := ModelingCategory( ModelingCategory( PSh_J ) );; | ||
Assert( 0, Length( SetOfObjects( psh_J ) ) = Length( SetOfObjects( PSh_J ) ) ); | ||
is_closed := psh_J!.ObjectMembershipFunction; | ||
Assert( 0, ForAll( closed, obj -> is_closed( ObjectDatum( ModelingObject( PSh_J, obj ) ) ) ) ); | ||
#Splash( DotVertexLabelledDigraph( PSh, [ Y, psh_J ], [ "grey", "blue", "red" ] : offset := 0 ) ); | ||
#! @EndExample |
127 changes: 127 additions & 0 deletions
127
FunctorCategories/gap/ClosedCoPreSheavesWRTLimitingCones.gd
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,127 @@ | ||
# SPDX-License-Identifier: GPL-2.0-or-later | ||
# FunctorCategories: Categories of functors | ||
# | ||
# Declarations | ||
# | ||
|
||
#! @Chapter Category of closed copresheaves with respect to limiting cones | ||
|
||
#################################### | ||
# | ||
#! @Section GAP categories | ||
# | ||
#################################### | ||
|
||
#! @Description | ||
#! The &GAP; category of closed copresheaves with respect to limiting cones. | ||
DeclareCategory( "IsClosedCoPreSheavesWRTLimitingCones", | ||
IsCapCategory ); | ||
|
||
#! @Description | ||
#! The &GAP; category of cells in the category of closed copresheaves with respect to limiting cones. | ||
DeclareCategory( "IsCellInClosedCoPreSheavesWRTLimitingCones", | ||
IsCapCategoryCell ); | ||
|
||
#! @Description | ||
#! The &GAP; category of objects in the category of closed copresheaves with respect to limiting cones. | ||
DeclareCategory( "IsObjectInClosedCoPreSheavesWRTLimitingCones", | ||
IsCellInClosedCoPreSheavesWRTLimitingCones and IsCapCategoryObject ); | ||
|
||
#! @Description | ||
#! The &GAP; category of morphisms in the category of closed copresheaves with respect to limiting cones. | ||
DeclareCategory( "IsMorphismInClosedCoPreSheavesWRTLimitingCones", | ||
IsCellInClosedCoPreSheavesWRTLimitingCones and IsCapCategoryMorphism ); | ||
|
||
#################################### | ||
# | ||
#! @Section Constructors | ||
# | ||
#################################### | ||
|
||
#! @Description | ||
#! The input is category <A>C</A> and a list <A>product_cones</A> of product cones in <A>C</A>. | ||
#! The output is the category of of closed copresheaves with respect to <A>product_cones</A>. | ||
#! @Arguments C, product_cones | ||
DeclareOperation( "ClosedCoPreSheavesWRTProductCones", | ||
[ IsCapCategory, IsList ] ); | ||
|
||
#CapJitAddTypeSignature( "ClosedCoPreSheavesWRTProductCones", [ IsCapCategory, IsList ], function ( input_types ) | ||
# | ||
# return CapJitDataTypeOfCategory( ClosedCoPreSheavesWRTProductCones( input_types[1].category ) ); | ||
# | ||
#end ); | ||
|
||
#! @Description | ||
#! The input is category <A>C</A> and a list <A>lists_of_product_cofactors</A> of lists of product cofactors in <A>C</A>. | ||
#! The output is the category of of closed copresheaves with respect to <A>lists_of_product_cofactors</A>. | ||
#! @Arguments C, lists_of_product_cofactors | ||
DeclareOperation( "ClosedCoPreSheavesWRTProducts", | ||
[ IsCapCategory, IsList ] ); | ||
|
||
#CapJitAddTypeSignature( "ClosedCoPreSheavesWRTProducts", [ IsCapCategory, IsList ], function ( input_types ) | ||
# | ||
# return CapJitDataTypeOfCategory( ClosedCoPreSheavesWRTProducts( input_types[1].category ) ); | ||
# | ||
#end ); | ||
|
||
#! @Description | ||
#! The input is category <A>C</A> and a list <A>lists_of_product_cofactors</A> of lists of product cofactors in <A>C</A>. | ||
#! The output is the category of of closed copresheaves with respect to <A>lists_of_product_cofactors</A>. | ||
#! @Arguments C, lists_of_product_cofactors | ||
DeclareOperation( "ClosedCoPreSheavesWRTProductsByIndices", | ||
[ IsCapCategory, IsList ] ); | ||
|
||
#CapJitAddTypeSignature( "ClosedCoPreSheavesWRTProductsByIndices", [ IsCapCategory, IsList ], function ( input_types ) | ||
# | ||
# return CapJitDataTypeOfCategory( ClosedCoPreSheavesWRTProductsByIndices( input_types[1].category ) ); | ||
# | ||
#end ); | ||
|
||
#################################### | ||
# | ||
#! @Section Attributes | ||
# | ||
#################################### | ||
|
||
#! @Description | ||
#! The input is the category of closed copresheaves on a category $C$ with respect to a list $L$ of limiting cones in $C$. | ||
#! The output is the list $L$. | ||
#! @Arguments coPSh_J | ||
DeclareAttribute( "UnderlyingLimitingCones", | ||
IsClosedCoPreSheavesWRTLimitingCones ); | ||
|
||
#! @Description | ||
#! The input is the category of closed copresheaves on a category $C$ with respect to limiting cones in $C$. | ||
#! The output is the category $C$. | ||
#! @Arguments coPSh_J | ||
DeclareAttribute( "Source", | ||
IsClosedCoPreSheavesWRTLimitingCones ); | ||
|
||
CapJitAddTypeSignature( "Source", [ IsClosedCoPreSheavesWRTLimitingCones ], | ||
function ( input_types ) | ||
|
||
return CapJitDataTypeOfCategory( Source( input_types[1].category ) ); | ||
|
||
end ); | ||
|
||
#! @Description | ||
#! The input is the category of closed copresheaves on a category $C$ with respect to limiting cones in $C$. | ||
#! The output is the target category. | ||
#! @Arguments coPSh_J | ||
DeclareAttribute( "Target", | ||
IsClosedCoPreSheavesWRTLimitingCones ); | ||
|
||
CapJitAddTypeSignature( "Target", [ IsClosedCoPreSheavesWRTLimitingCones ], | ||
function ( input_types ) | ||
|
||
return CapJitDataTypeOfCategory( Target( input_types[1].category ) ); | ||
|
||
end ); | ||
|
||
DeclareAttribute( "CoYonedaEmbeddingDataOfSourceCategory", | ||
IsClosedCoPreSheavesWRTLimitingCones ); | ||
|
||
#! @Arguments coPSh_J | ||
#! @Returns a &CAP; functor | ||
DeclareAttribute( "CoYonedaEmbeddingOfSourceCategory", | ||
IsClosedCoPreSheavesWRTLimitingCones ); |
Oops, something went wrong.