-
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
3546f09
commit 1032cff
Showing
5 changed files
with
286 additions
and
1 deletion.
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,80 @@ | ||
#! @Chunk DifferenceCSL | ||
|
||
# the assumption si <= mi leads to fewer meets and joins: | ||
|
||
#! @Example | ||
LoadPackage( "FunctorCategories", false ); | ||
#! true | ||
q := "q(m0,s0,m1,s1,m2,s2,m0_x_s1,s0_u_m1,m1_x_s2,s1_u_m2)\ | ||
[sm0:s0->m0,sm1:s1->m1,sm2:s2->m2,\ | ||
p011:m0_x_s1->s1,\ | ||
i101:m1->s0_u_m1,\ | ||
p122:m1_x_s2->s2,\ | ||
i212:m2->s1_u_m2,\ | ||
mc0:m0_x_s1->s0,jc0:m0->s0_u_m1,\ | ||
mc1:m1_x_s2->s1,jc1:m1->s1_u_m2]";; | ||
q := FinQuiver( q ); | ||
#! FinQuiver( "q(m0,s0,m1,s1,m2,s2,m0_x_s1,s0_u_m1,m1_x_s2,s1_u_m2) | ||
#! [sm0:s0-≻m0,sm1:s1-≻m1,sm2:s2-≻m2, | ||
#! p011:m0_x_s1-≻s1, | ||
#! i101:m1-≻s0_u_m1, | ||
#! p122:m1_x_s2-≻s2, | ||
#! i212:m2-≻s1_u_m2, | ||
#! mc0:m0_x_s1-≻s0,jc0:m0-≻s0_u_m1, | ||
#! mc1:m1_x_s2-≻s1,jc1:m1-≻s1_u_m2]" ) | ||
F := PathCategory( q ); | ||
#! PathCategory( FinQuiver( "q(m0,s0,m1,s1,m2,s2,m0_x_s1,s0_u_m1,m1_x_s2,s1_u_m2) | ||
#! [sm0:s0-≻m0,sm1:s1-≻m1,sm2:s2-≻m2, | ||
#! p011:m0_x_s1-≻s1, | ||
#! i101:m1-≻s0_u_m1, | ||
#! p122:m1_x_s2-≻s2, | ||
#! i212:m2-≻s1_u_m2, | ||
#! mc0:m0_x_s1-≻s0,jc0:m0-≻s0_u_m1, | ||
#! mc1:m1_x_s2-≻s1,jc1:m1-≻s1_u_m2]" ) ) | ||
Size( F ); | ||
#! 35 | ||
HomStructure( F.s0, F.s0_u_m1 ); | ||
#! |1| | ||
HomStructure( F.s1, F.s1_u_m2 ); | ||
#! |1| | ||
HomStructure( F.m0_x_s1, F.m0 ); | ||
#! |1| | ||
HomStructure( F.m1_x_s2, F.m1 ); | ||
#! |1| | ||
C := F / | ||
[ [ F.p011 * F.sm1 * F.i101, F.mc0 * F.sm0 * F.jc0 ], | ||
[ F.p122 * F.sm2 * F.i212, F.mc1 * F.sm1 * F.jc1 ] ]; | ||
#! PathCategory( FinQuiver( "q(m0,s0,m1,s1,m2,s2,m0_x_s1,s0_u_m1,m1_x_s2,s1_u_m2) | ||
#! [sm0:s0-≻m0,sm1:s1-≻m1,sm2:s2-≻m2, | ||
#! p011:m0_x_s1-≻s1, | ||
#! i101:m1-≻s0_u_m1, | ||
#! p122:m1_x_s2-≻s2, | ||
#! i212:m2-≻s1_u_m2, | ||
#! mc0:m0_x_s1-≻s0,jc0:m0-≻s0_u_m1, | ||
#! mc1:m1_x_s2-≻s1,jc1:m1-≻s1_u_m2]" ) ) | ||
#! / [ p011⋅sm1⋅i101 = mc0⋅sm0⋅jc0, p122⋅sm2⋅i212 = mc1⋅sm1⋅jc1 ] | ||
Size( C ); | ||
#! 33 | ||
P := PosetOfCategory( F );; | ||
Size( P ); | ||
#! 33 | ||
digraphF := DigraphOfPoset( P );; | ||
digraphF!.vertexlabels := List( SetOfObjects( F ), String ); | ||
#Splash( DotVertexLabelledDigraph( digraphF ) ); | ||
PSh := PreSheaves( P );; | ||
digraphPSh := DigraphOfPoset( PSh );; | ||
#Splash( DotVertexLabelledDigraph( digraphPSh ) ); | ||
presheaves := SetOfObjects( PSh );; | ||
Y := YonedaEmbeddingOfSourceCategory( PSh ); | ||
digraphP := DigraphOfPoset( P );; | ||
digraphP!.vertexlabels := List( SetOfObjects( P ), o -> String( -1 + SafePosition( presheaves, Y( o ) ) ) ); | ||
#Splash( DotVertexLabelledDigraph( digraphP ) ); | ||
cocones := [ [ P.s0_u_m1, [ P.s0, P.m1 ] ], | ||
[ P.s1_u_m2, [ P.s1, P.m2 ] ] ]; | ||
is_closed := F -> IsClosedPreSheafWRTCoproducts( PSh, F, cocones ); | ||
PShJ := FullSubcategoryByObjectMembershipFunction( PSh, is_closed ); | ||
digraphPShJ := DigraphOfPoset( PShJ );; | ||
digraphPShJ!.vertexlabels := List( SetOfObjects( PShJ ), c -> String( -1 + SafePosition( presheaves, ObjectDatum( c ) ) ) ); | ||
#Splash( DotVertexLabelledDigraph( digraphPShJ ) ); | ||
|
||
#! @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,71 @@ | ||
#! @Chunk FreeBooleanAlgebra | ||
|
||
#! Construct the free boolean algebra on two generators with its $2^(2^2)$ elements | ||
#! in two steps. | ||
|
||
#! @Example | ||
LoadPackage( "FunctorCategories", false ); | ||
#! true | ||
pq := FinQuiver( "quiver(p,q)" ); | ||
#! FinQuiver( "quiver(p,q)[]" ) | ||
F := PathCategory( pq ); | ||
#! PathCategory( FinQuiver( "quiver(p,q)[]" ) ) | ||
P := PosetOfCategory( F ); | ||
#! PosetOfCategory( PathCategory( FinQuiver( "quiver(p,q)[]" ) ) ) | ||
Length( SetOfObjects( P ) ); | ||
#! 2 | ||
Dist := FreeDistributiveCompletion( P ); | ||
#! FreeDistributiveCompletion( | ||
#! PosetOfCategory( PathCategory( FinQuiver( "quiver(p,q)[]" ) ) ) ) | ||
Display( Dist ); | ||
#! A CAP category with name FreeDistributiveCompletion( | ||
#! PosetOfCategory( PathCategory( FinQuiver( "quiver(p,q)[]" ) ) ) ): | ||
#! | ||
#! 54 primitive operations were used to derive 250 operations for this category | ||
#! which algorithmically | ||
#! * IsFiniteCategory | ||
#! * IsEquippedWithHomomorphismStructure | ||
#! * IsDistributiveLattice | ||
#! and not yet algorithmically | ||
#! * IsBiHeytingAlgebra | ||
Length( SetOfObjects( Dist ) ); | ||
#! 6 | ||
digraphDist := DigraphOfPoset( Dist );; | ||
#Splash( DotVertexLabelledDigraph( digraphDist ) ); | ||
DiffbCSL := MeetSemilatticeOfSingleDifferences( Dist ); | ||
#! MeetSemilatticeOfSingleDifferences( FreeDistributiveCompletion( | ||
#! PosetOfCategory( PathCategory( FinQuiver( "quiver(p,q)[]" ) ) ) ) ) | ||
Length( SetOfObjects( DiffbCSL ) ); | ||
#! 13 | ||
digraphDiffbCSL := DigraphOfPoset( DiffbCSL );; | ||
#Splash( DotVertexLabelledDigraph( digraphDiffbCSL ) ); | ||
PSh := PreSheaves( DiffbCSL ); | ||
#! PreSheaves( MeetSemilatticeOfSingleDifferences( FreeDistributiveCompletion( | ||
#! PosetOfCategory( PathCategory( FinQuiver( "quiver(p,q)[]" ) ) ) ) ), | ||
#! IntervalCategory ) | ||
presheaves := SetOfObjects( PSh );; | ||
Length( presheaves ); | ||
#! 85 | ||
#digraphPSh := DigraphOfPoset( PSh );; | ||
#Splash( DotVertexLabelledDigraph( digraphPSh ) ); | ||
cocones := [ [ 0, [ ] ], | ||
[ 3, [ 5, 7 ] ], | ||
[ 2, [ 5, 9 ] ], | ||
[ 6, [ 7, 10 ] ], | ||
[ 8, [ 9, 10 ] ], | ||
[ 12, [ 7, 9 ] ], | ||
[ 4, [ 3, 2, 12 ] ], | ||
[ 11, [ 6, 8, 12 ] ], | ||
[ 1, [ 4, 11 ] ] ];; | ||
is_closed := F -> IsClosedPreSheafWRTCoproductsByIndices( PSh, F, cocones : offset := 1 ); | ||
PShJ := FullSubcategoryByObjectMembershipFunction( PSh, is_closed ); | ||
#! FullSubcategoryByObjectMembershipFunction( PreSheaves( | ||
#! MeetSemilatticeOfSingleDifferences( FreeDistributiveCompletion( | ||
#! PosetOfCategory( PathCategory( FinQuiver( "quiver(p,q)[]" ) ) ) ) ), | ||
#! IntervalCategory ), ObjectMembershipFunction ) | ||
digraphPShJ := DigraphOfPoset( PShJ );; | ||
digraphPShJ!.vertexlabels := List( SetOfObjects( PShJ ), c -> String( -1 + SafePosition( presheaves, ObjectDatum( c ) ) ) ); | ||
Length( SetOfObjects( PShJ ) ); | ||
#! 16 | ||
#Splash( DotVertexLabelledDigraph( digraphPShJ ) ); | ||
#! @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