diff --git a/Algebroids/PackageInfo.g b/Algebroids/PackageInfo.g index aba1d8b2d..cfbb3403c 100644 --- a/Algebroids/PackageInfo.g +++ b/Algebroids/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "Algebroids", Subtitle := "Algebroids and bialgebroids as preadditive categories generated by enhanced quivers", -Version := "2024.09-03", +Version := "2024.09-04", Date := ~.Version{[ 1 .. 10 ]}, Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ), License := "GPL-2.0-or-later", @@ -137,7 +137,7 @@ Dependencies := rec( [ "CartesianCategories", ">= 2024.02-01" ], [ "Toposes", ">= 2023.03-05" ], [ "FinSetsForCAP", ">= 2024.02-02" ], - [ "FpCategories", ">= 2024.09-04" ], + [ "FpCategories", ">= 2024.09-06" ], [ "QPA", ">= 2.0" ], [ "MatricesForHomalg", ">= 2021.12-01" ], [ "FreydCategoriesForCAP", ">= 2024.07-05" ], diff --git a/Algebroids/doc/Doc.autodoc b/Algebroids/doc/Doc.autodoc index a27a9bab1..4c61858ae 100644 --- a/Algebroids/doc/Doc.autodoc +++ b/Algebroids/doc/Doc.autodoc @@ -9,9 +9,6 @@ @Section A f.p. category @InsertChunk FpCategory -@Section The full subcategory of the simplicial category truncated in degree 2 -@InsertChunk Delta2 - @Section Algebroids @InsertChunk Algebroid @@ -103,5 +100,4 @@ @InsertChunk PrecompileAdditiveClosureOfAlgebroid @InsertChunk PrecompileAdditiveClosureOfAlgebroidFromDataTables @InsertChunk PrecompileAdelmanCategoryOfAdditiveClosureOfAlgebroid -@InsertChunk PrecompileCategoryFromNerveData @InsertChunk PrecompileCategoryFromDataTables diff --git a/Algebroids/examples/CategoryFromDataTables.g b/Algebroids/examples/CategoryFromDataTables.g index 52629e48b..a5c564f44 100644 --- a/Algebroids/examples/CategoryFromDataTables.g +++ b/Algebroids/examples/CategoryFromDataTables.g @@ -4,20 +4,20 @@ LoadPackage( "Algebroids", false ); #! true Delta1 := SimplicialCategoryTruncatedInDegree( 1 ); -#! FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] +#! PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] Size( Delta1 ); #! 7 mors := SetOfMorphisms( Delta1 ); -#! [ (C0)-[(C0)]->(C0), (C1)-[(id)]->(C0), (C0)-[(s)]->(C1), (C0)-[(t)]->(C1), -#! (C1)-[(C1)]->(C1), (C1)-[(id*s)]->(C1), (C1)-[(id*t)]->(C1) ] +#! [ [id(C0)]:(C0) -≻ (C0), [id]:(C1) -≻ (C0), [s]:(C0) -≻ (C1), [t]:(C0) -≻ (C1), +#! [id(C1)]:(C1) -≻ (C1), [id⋅s]:(C1) -≻ (C1), [id⋅t]:(C1) -≻ (C1) ] List( mors, DecompositionOfMorphismInCategory ); -#! [ [ ], [ (C1)-[(id)]->(C0) ], [ (C0)-[(s)]->(C1) ], [ (C0)-[(t)]->(C1) ], -#! [ ], [ (C1)-[(id)]->(C0), (C0)-[(s)]->(C1) ], -#! [ (C1)-[(id)]->(C0), (C0)-[(t)]->(C1) ] ] +#! [ [ ], [ [id]:(C1) -≻ (C0) ], [ [s]:(C0) -≻ (C1) ], [ [t]:(C0) -≻ (C1) ], +#! [ ], [ [id]:(C1) -≻ (C0), [s]:(C0) -≻ (C1) ], +#! [ [id]:(C1) -≻ (C0), [t]:(C0) -≻ (C1) ] ] C := CategoryFromDataTables( Delta1 ); -#! FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] +#! PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] Size( C ); #! 7 morsC := SetOfMorphisms( C ); @@ -35,8 +35,8 @@ SetOfGeneratingMorphisms( C ); #! [ (C1)-[(id)]->(C0), (C0)-[(s)]->(C1), (C0)-[(t)]->(C1) ] Display( C ); #! A CAP category with name -#! FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ]: +#! PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ]: #! #! 19 primitive operations were used to derive 55 operations for this category #! which algorithmically @@ -161,8 +161,8 @@ List( mors, DecompositionOfMorphismInCategory ); #! [ (C1)-[(id)]->(C0), (C0)-[(t)]->(C1) ] ] C_op := OppositeCategoryFromDataTables( C ); #! Opposite( -#! FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] ) +#! PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] ) IsIdenticalObj( OppositeCategoryFromDataTables( C_op ), C ); #! true IndicesOfGeneratingMorphisms( C_op ); diff --git a/Algebroids/examples/doc/Delta2.g b/Algebroids/examples/doc/Delta2.g deleted file mode 100644 index 55150cb6a..000000000 --- a/Algebroids/examples/doc/Delta2.g +++ /dev/null @@ -1,31 +0,0 @@ -#! @BeginChunk Delta2 - -#! The full subcategory of the simplicial category $\Delta$ on the objects $[0], [1], [2]$ - -#! @Example -LoadPackage( "Algebroids" ); -#! true -Delta2 := SimplicialCategoryTruncatedInDegree( 2 ); -#! FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations -RelationsOfFpCategory( Delta2 ); -#! [ [ (s*id), (C0) ], [ (t*id), (C0) ], -#! [ (ps*is), (C1) ], [ (pt*it), (C1) ], -#! [ (is*id), (it*id) ], [ (pt*is), (id*t) ], -#! [ (ps*it), (id*s) ], [ (s*pt), (t*ps) ], -#! [ (s*mu), (s*ps) ], [ (t*mu), (t*pt) ], -#! [ (mu*is), (C1) ], [ (mu*it), (C1) ] ] -Size( Delta2 ); -#! 31 -Delta2_op := OppositeFiniteCategory( Delta2 ); -#! Opposite( FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations ) -IsIdenticalObj( OppositeFiniteCategory( Delta2_op ), Delta2 ); -#! true -#! @EndExample - -#! @EndChunk diff --git a/Algebroids/examples/doc/NerveTruncatedInDegree2AsFunctor.g b/Algebroids/examples/doc/NerveTruncatedInDegree2AsFunctor.g deleted file mode 100644 index fbda60e5f..000000000 --- a/Algebroids/examples/doc/NerveTruncatedInDegree2AsFunctor.g +++ /dev/null @@ -1,50 +0,0 @@ -#! @BeginChunk NerveTruncatedInDegree2AsFunctor - -LoadPackage( "Algebroids" ); - -#! We compute the nerve of the full subcategory of the simplicial category $\Delta$ on the objects $[0], [1], [2]$. - -#! @Example -Delta2 := SimplicialCategoryTruncatedInDegree( 2 ); -#! FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations -RelationsOfFpCategory( Delta2 ); -#! [ [ (s*id), (C0) ], [ (t*id), (C0) ], -#! [ (ps*is), (C1) ], [ (pt*it), (C1) ], -#! [ (is*id), (it*id) ], [ (pt*is), (id*t) ], -#! [ (ps*it), (id*s) ], [ (s*pt), (t*ps) ], -#! [ (s*mu), (s*ps) ], [ (t*mu), (t*pt) ], -#! [ (mu*is), (C1) ], [ (mu*it), (C1) ] ] -Size( Delta2 ); -#! 31 -N := NerveTruncatedInDegree2AsFunctor( Delta2 ); -#! Functor from FreeCategory( RightQuiver( -#! "Delta_op(C0,C1,C2)[id:C0->C1,s:C1->C0,t:C1->C0, -#! is:C1->C2,it:C1->C2, -#! ps:C2->C1,pt:C2->C1,mu:C2->C1]" ) ) / relations -#! -> SkeletalFinSets -Delta2op := SourceOfFunctor( N ); -#! FreeCategory( RightQuiver( -#! "Delta_op(C0,C1,C2)[id:C0->C1,s:C1->C0,t:C1->C0, -#! is:C1->C2,it:C1->C2, -#! ps:C2->C1,pt:C2->C1,mu:C2->C1]" ) ) / relations -N( Delta2op.C0 ); -#! |3| -Display( N( Delta2op.C0 ) ); -#! { 0, 1, 2 } -N( Delta2op.C1 ); -#! |31| -Display( N( Delta2op.C1 ) ); -#! { 0,..., 30 } -N( Delta2op.C2 ); -#! |393| -Display( N( Delta2op.C2 ) ); -#! { 0,..., 392 } -N( Delta2op.id ); -#! |3| → |31| -Display( N( Delta2op.id ) ); -#! { 0, 1, 2 } ⱶ[ 0, 5, 21 ]→ { 0,..., 30 } -#! @EndExample -#! @EndChunk diff --git a/Algebroids/examples/doc/YonedaCompositionAsNaturalEpimorphism.g b/Algebroids/examples/doc/YonedaCompositionAsNaturalEpimorphism.g deleted file mode 100644 index 421dff927..000000000 --- a/Algebroids/examples/doc/YonedaCompositionAsNaturalEpimorphism.g +++ /dev/null @@ -1,63 +0,0 @@ -#! @BeginChunk YonedaCompositionAsNaturalEpimorphism - -LoadPackage( "Algebroids" ); - -#! We compute the Yoneda composition natural epimorphism of the full subcategory -#! of the simplicial category $\Delta$ on the objects $[0], [1], [2]$. - -#! @Example -Delta2 := SimplicialCategoryTruncatedInDegree( 2 ); -#! FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations -RelationsOfFpCategory( Delta2 ); -#! [ [ (s*id), (C0) ], [ (t*id), (C0) ], -#! [ (ps*is), (C1) ], [ (pt*it), (C1) ], -#! [ (is*id), (it*id) ], [ (pt*is), (id*t) ], -#! [ (ps*it), (id*s) ], [ (s*pt), (t*ps) ], -#! [ (s*mu), (s*ps) ], [ (t*mu), (t*pt) ], -#! [ (mu*is), (C1) ], [ (mu*it), (C1) ] ] -Size( Delta2 ); -#! 31 -Ymu := YonedaCompositionAsNaturalEpimorphism( Delta2 ); -#! Natural transformation from -#! Functor from FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations -> -#! SkeletalFinSets -#! -> -#! Functor from FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations -> -#! SkeletalFinSets -Ymu := YonedaProjectionAsNaturalEpimorphism( Delta2 ); -#! Natural transformation from -#! Functor from FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations -> -#! SkeletalFinSets -#! -> -#! Functor from FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations -> -#! SkeletalFinSets -Ys := YonedaFibrationAsNaturalTransformation( Delta2 ); -#! Natural transformation from -#! Functor from FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations -> -#! SkeletalFinSets -#! -> -#! Functor from FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations -> -#! SkeletalFinSets -#! @EndExample -#! @EndChunk diff --git a/Algebroids/gap/Algebroids.gd b/Algebroids/gap/Algebroids.gd index 1ba6aec58..5cddd2b27 100644 --- a/Algebroids/gap/Algebroids.gd +++ b/Algebroids/gap/Algebroids.gd @@ -463,20 +463,6 @@ DeclareOperation( "CapFunctor", DeclareOperation( "CapFunctor", [ IsAlgebroid, IsCapCategoryObject ] ); -#! @Description -#! Construct, using the record (or list) of images eta, a natural transformation -#! from the functor F to the parallel functor G. -#! @Arguments eta, F, G -#! @Returns a &CAP; natural transformation -#! @Group NaturalTransformation -DeclareOperation( "NaturalTransformation", - [ IsRecord, IsCapFunctor, IsCapFunctor ] ); - -#! @Arguments F, eta, G -#! @Group NaturalTransformation -DeclareOperation( "NaturalTransformation", - [ IsCapFunctor, IsList, IsCapFunctor ] ); - #! @Description #! The constructor of objects in an algebroid A given a vertex V #! in the underlying quiver. diff --git a/Algebroids/gap/Algebroids.gi b/Algebroids/gap/Algebroids.gi index d9a9c542e..0042dde45 100644 --- a/Algebroids/gap/Algebroids.gi +++ b/Algebroids/gap/Algebroids.gi @@ -2161,38 +2161,6 @@ InstallMethod( IsCommutative, return true; end ); -## -InstallMethod( NaturalTransformation, - "for a list and two CAP functors", - [ IsCapFunctor, IsList, IsCapFunctor ], - - function( F, images, G ) - local eta, vertices; - - eta := NaturalTransformation( Concatenation( "Natural transformation from ", Name( F ), " -> ", Name( G ) ), F, G ); - - eta!.ValuesOnAllObjects := images; - - vertices := Vertices( QuiverOfAlgebra( UnderlyingQuiverAlgebra( AsCapCategory( Source( F ) ) ) ) ); - - AddNaturalTransformationFunction( eta, - function( source, obj, range ) - local pos; - - pos := SafePosition( vertices, UnderlyingVertex( obj ) ); - - if not IsInt( pos ) then - Error( "vertex UnderlyingVertex( obj ) = ", UnderlyingVertex( obj ), " not found in the list ", vertices, " of vertices\n" ); - fi; - - return images[pos]; - - end ); - - return eta; - -end ); - ## InstallMethod( NaturalTransformation, "for a record and two CAP functors", diff --git a/Algebroids/gap/CategoryFromDataTables.gd b/Algebroids/gap/CategoryFromDataTables.gd index 8987328e3..12e5d3260 100644 --- a/Algebroids/gap/CategoryFromDataTables.gd +++ b/Algebroids/gap/CategoryFromDataTables.gd @@ -173,6 +173,14 @@ DeclareAttribute( "CategoryFromDataTables", DeclareAttribute( "CategoryFromDataTables", IsFpCategory ); +#! @Arguments C +DeclareAttribute( "CategoryFromDataTables", + IsPathCategory ); + +#! @Arguments C +DeclareAttribute( "CategoryFromDataTables", + IsQuotientOfPathCategory ); + #! @Arguments C DeclareAttribute( "CategoryFromDataTables", IsCategoryFromNerveData ); diff --git a/Algebroids/gap/CategoryFromDataTables.gi b/Algebroids/gap/CategoryFromDataTables.gi index 04982d799..110d8f58b 100644 --- a/Algebroids/gap/CategoryFromDataTables.gi +++ b/Algebroids/gap/CategoryFromDataTables.gi @@ -356,6 +356,45 @@ InstallMethod( CategoryFromDataTables, end ); +## +InstallMethod( CategoryFromDataTables, + "for a path category", + [ IsPathCategory ], + + function( C ) + + return CategoryFromDataTables( + rec( name := Name( C ), + range_of_HomStructure := RangeCategoryOfHomomorphismStructure( C ), + data_tables := DataTablesOfCategory( C ), + indices_of_generating_morphisms := IndicesOfGeneratingMorphismsFromHomStructure( C ), + decomposition_of_all_morphisms := DecompositionIndicesOfAllMorphismsFromHomStructure( C ), + relations := RelationsAmongGeneratingMorphisms( C ), + labels := [ List( SetOfObjects( C ), ObjectLabel ), List( SetOfGeneratingMorphisms( C ), MorphismLabel ) ], + properties := ListKnownCategoricalProperties( C ) ) ); + +end ); + +## +InstallMethod( CategoryFromDataTables, + "for a quotient of a path category", + [ IsQuotientOfPathCategory ], + + function( C ) + + return CategoryFromDataTables( + rec( name := Name( C ), + range_of_HomStructure := RangeCategoryOfHomomorphismStructure( C ), + data_tables := DataTablesOfCategory( C ), + indices_of_generating_morphisms := IndicesOfGeneratingMorphismsFromHomStructure( C ), + decomposition_of_all_morphisms := DecompositionIndicesOfAllMorphismsFromHomStructure( C ), + relations := RelationsAmongGeneratingMorphisms( C ), + labels := [ List( SetOfObjects( C ), o -> ObjectLabel( UnderlyingCell( o ) ) ), + List( SetOfGeneratingMorphisms( C ), m -> MorphismLabel( CanonicalRepresentative( m ) ) ) ], + properties := ListKnownCategoricalProperties( C ) ) ); + +end ); + ## InstallMethod( CategoryFromDataTables, "for a category from nerve data", @@ -499,6 +538,24 @@ InstallMethod( \., end ); +## +InstallOtherMethod( CategoryFromNerveData, + "for a category from data tables", + [ IsCategoryFromDataTables ], + + function( C ) + + return CategoryFromNerveData( + rec( name := Name( C ), + nerve_data := NerveTruncatedInDegree2Data( C ), + indices_of_generating_morphisms := IndicesOfGeneratingMorphismsFromHomStructure( C ), + decomposition_of_all_morphisms := DecompositionIndicesOfAllMorphisms( C ), + relations := RelationsAmongGeneratingMorphisms( C ), + labels := C!.labels, + properties := ListKnownCategoricalProperties( C ) ) ); + +end ); + ## InstallMethod( OppositeCategoryFromDataTables, "for a category from data tables", diff --git a/Algebroids/gap/FpCategories.gd b/Algebroids/gap/FpCategories.gd index 3215f236d..144236649 100644 --- a/Algebroids/gap/FpCategories.gd +++ b/Algebroids/gap/FpCategories.gd @@ -276,60 +276,13 @@ DeclareAttribute( "DecompositionIndicesOfMorphism", DeclareAttribute( "DecompositionOfMorphismInCategory", IsMorphismInFpCategory ); -DeclareAttribute( "DecompositionIndicesOfAllMorphismsFromHomStructure", - IsFpCategory ); - DeclareAttribute( "DecompositionIndicesOfAllMorphisms", IsFpCategory ); -#! @Description -#! The input is a finitely presented category C equipped with a homomorphism structure -#! with values in the skeletal category SkeletalFinSets of finite sets. -#! The output is the nerve of B truncated in degree $2$, -#! as a presheaf on SimplicialCategoryTruncatedInDegree($2$) -#! with values in SkeletalFinSets. #! @Arguments C -#! @Returns a &CAP; functor -DeclareAttribute( "NerveTruncatedInDegree2AsFunctor", - IsCapCategory ); -#! @InsertChunk NerveTruncatedInDegree2AsFunctor - -DeclareAttribute( "YonedaNaturalEpimorphisms", IsCapCategory ); - -#! @Description -#! The input is a finitely presented category B. The output is a natural morphism. -#! Its source is the functor $B \to H, c \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,c), -#! \psi \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,\psi)$. -#! Its targe is the constant functor of $0$-cells -#! $B \to H, c \mapsto B_0, \psi \mapsto \mathrm{id}_{B_0}$. -#! @Arguments B -#! @Returns a &CAP; natural transformation -DeclareAttribute( "YonedaFibrationAsNaturalTransformation", IsCapCategory ); - -#! @Description -#! The input is a finitely presented category B. The output is a natural epimorphism. -#! Its source is the functor -#! $B \to H, c \mapsto \sqcup_{a,b\in B} \mathrm{Hom}(a,b) \times \mathrm{Hom}(b,c), -#! \psi \mapsto \sqcup_{a,b\in B} \mathrm{Hom}(1_a,1_b) \times \mathrm{Hom}(b,\psi)$. -#! Its target is the functor $B \to H, c \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,c), -#! \psi \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,\psi)$. -#! @Arguments B -#! @Returns a &CAP; natural transformation -DeclareAttribute( "YonedaProjectionAsNaturalEpimorphism", IsCapCategory ); - -#! @Description -#! The input is a finitely presented category B. The output is a natural epimorphism. -#! Its source is the functor -#! $B \to H, c \mapsto \sqcup_{a,b\in B} \mathrm{Hom}(a,b) \times \mathrm{Hom}(b,c), -#! \psi \mapsto \sqcup_{a,b\in B} \mathrm{Hom}(1_a,1_b) \times \mathrm{Hom}(b,\psi)$. -#! Its target is the functor $B \to H, c \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,c), -#! \psi \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,\psi)$. -#! @Arguments B -#! @Returns a &CAP; natural transformation -DeclareAttribute( "YonedaCompositionAsNaturalEpimorphism", IsCapCategory ); -#! @InsertChunk YonedaCompositionAsNaturalEpimorphism +DeclareAttribute( "CategoryFromNerveData", + IsFpCategory ); -DeclareAttribute( "TruthMorphismOfTrueToSieveFunctorAndEmbedding", IsCapCategory ); DeclareAttribute( "EmbeddingOfSieveFunctor", IsFpCategory ); #! @Description diff --git a/Algebroids/gap/FpCategories.gi b/Algebroids/gap/FpCategories.gi index d8f82efec..798e60600 100644 --- a/Algebroids/gap/FpCategories.gi +++ b/Algebroids/gap/FpCategories.gi @@ -1616,777 +1616,20 @@ InstallMethod( OppositeFpCategory, end ); ## -InstallMethodForCompilerForCAP( NerveTruncatedInDegree2Data, - [ IsCapCategory and IsFiniteCategory ], - - function ( B ) - local A, sFinSets, B0, N0, D00, N0N0, p21, p22, B1, N1, N1_elements, d, id, pi2, s, t, - D000, N0N0N0, p31, p32, p33, B2, N2, N2_elements, T, ds, is, dt, it, - p312, p323, p313, pi3, pi312, pi323, pi313, ps, pt, mus, mus1, mus2, mus3, mu; - - sFinSets := RangeCategoryOfHomomorphismStructure( B ); - - ## sFinSets must be the category skeletal finite sets - #% CAP_JIT_DROP_NEXT_STATEMENT - Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); - - B0 := SetOfObjects( B ); - N0 := ObjectConstructor( sFinSets, Length( B0 ) ); - - ## N0 × N0 - D00 := [ N0, N0 ]; - N0N0 := DirectProduct( sFinSets, D00 ); - - ## N0 × N0 -> N0 - p21 := ProjectionInFactorOfDirectProductWithGivenDirectProduct( sFinSets, D00, 1, N0N0 ); - p22 := ProjectionInFactorOfDirectProductWithGivenDirectProduct( sFinSets, D00, 2, N0N0 ); - - B1 := List( N0N0, i -> - HomomorphismStructureOnObjects( B, - B0[1 + AsList( p21 )[1 + i]], - B0[1 + AsList( p22 )[1 + i]] ) ); - - N1 := Coproduct( sFinSets, B1 ); - - N1_elements := ExactCoverWithGlobalElements( N1 ); - - ## N0 -> N0 × N0 - d := EmbeddingOfEqualizerWithGivenEqualizer( sFinSets, - N0N0, - [ p21, p22 ], - N0 ); - - #% CAP_JIT_DROP_NEXT_STATEMENT - Assert( 0, d = UniversalMorphismIntoDirectProduct( sFinSets, D00, N0, [ IdentityMorphism( sFinSets, N0 ), IdentityMorphism( sFinSets, N0 ) ] ) ); - - ## N0 -> N1 - id := MorphismConstructor( sFinSets, - N0, - List( N0, i -> - AsList( - PreCompose( sFinSets, - InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( B, - IdentityMorphism( B, - B0[1 + i] ) ), - InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, - B1, - 1 + AsList( d )[1 + i], - N1 ) ) )[1 + 0] ), - N1 ); - - ## N1 -> N0 × N0 - ## this morphism is mixing two levels and is not a CAP operation: - ## the coproduct N1 in SkeletalFinSets is taken over the index set N0N0 (here also realized as an object in SkeletalFinSets), - ## so this morphism is a fibration of a coproduct over its "index set" which are both assumed to be objects in the same category: - pi2 := MorphismConstructor( sFinSets, - N1, - Concatenation( List( N0N0, i -> ListWithIdenticalEntries( Length( B1[1 + i] ), i ) ) ), - N0N0 ); - - ## N1 -> N0 × N0 -> N0 - s := PreCompose( sFinSets, pi2, p21 ); - - ## N1 -> N0 × N0 -> N0 - t := PreCompose( sFinSets, pi2, p22 ); - - ## N0 × N0 × N0 - D000 := [ N0, N0, N0 ]; - N0N0N0 := DirectProduct( sFinSets, D000 ); - - ## N0 × N0 × N0 -> N0 - p31 := ProjectionInFactorOfDirectProductWithGivenDirectProduct( sFinSets, D000, 1, N0N0N0 ); - p32 := ProjectionInFactorOfDirectProductWithGivenDirectProduct( sFinSets, D000, 2, N0N0N0 ); - p33 := ProjectionInFactorOfDirectProductWithGivenDirectProduct( sFinSets, D000, 3, N0N0N0 ); - - B2 := List( N0N0N0, i -> - DirectProduct( sFinSets, - [ HomomorphismStructureOnObjects( B, - B0[1 + AsList( p31 )[1 + i]], - B0[1 + AsList( p32 )[1 + i]] ), - HomomorphismStructureOnObjects( B, - B0[1 + AsList( p32 )[1 + i]], - B0[1 + AsList( p33 )[1 + i]] ) ] ) ); - - N2 := Coproduct( sFinSets, B2 ); - - N2_elements := ExactCoverWithGlobalElements( N2 ); - - T := TerminalObject( sFinSets ); - - ## N1 -> N0 × N0 -> N0 × N0 × N0 - ## this is elegant but needs a justification: - ds := PreCompose( sFinSets, - pi2, - EmbeddingOfEqualizerWithGivenEqualizer( sFinSets, - N0N0N0, - [ p32, p33 ], - N0N0 ) ); - - ## N1 -> N2 - is := MorphismConstructor( sFinSets, - N1, - List( N1, i -> - AsList( - PreCompose( sFinSets, - DirectProductFunctorial( sFinSets, - [ LiftAlongMonomorphism( sFinSets, - InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, - B1, - 1 + AsList( pi2 )[1 + i], - N1 ), - N1_elements[1 + i] ), - InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( B, - IdentityMorphism( B, - B0[1 + AsList( t )[1 + i]] ) ) ] ), - InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, - B2, - 1 + AsList( ds )[1 + i], - N2 ) ) )[1 + 0] ), - N2 ); - - ## N1 -> N0 × N0 -> N0 × N0 × N0 - ## this is elegant but needs a justification: - dt := PreCompose( sFinSets, - pi2, - EmbeddingOfEqualizerWithGivenEqualizer( sFinSets, - N0N0N0, - [ p31, p32 ], - N0N0 ) ); - - ## N1 -> N2 - it := MorphismConstructor( sFinSets, - N1, - List( N1, i -> - AsList( - PreCompose( sFinSets, - DirectProductFunctorial( sFinSets, - [ InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( B, - IdentityMorphism( B, - B0[1 + AsList( s )[1 + i]] ) ), - LiftAlongMonomorphism( sFinSets, - InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, - B1, - 1 + AsList( pi2 )[1 + i], - N1 ), - N1_elements[1 + i] ) ] ), - InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, - B2, - 1 + AsList( dt )[1 + i], - N2 ) ) )[1 + 0] ), - N2 ); - - ## N0 × N0 × N0 -> N0 × N0 - p312 := UniversalMorphismIntoDirectProduct( sFinSets, D00, N0N0N0, [ p31, p32 ] ); - p323 := UniversalMorphismIntoDirectProduct( sFinSets, D00, N0N0N0, [ p32, p33 ] ); - p313 := UniversalMorphismIntoDirectProduct( sFinSets, D00, N0N0N0, [ p31, p33 ] ); - - #% CAP_JIT_DROP_NEXT_STATEMENT - Assert( 0, p312 = ProjectionInFactorOfDirectProduct( sFinSets, [ N0N0, N0 ], 1 ) ); - - #% CAP_JIT_DROP_NEXT_STATEMENT - Assert( 0, p323 = ProjectionInFactorOfDirectProduct( sFinSets, [ N0, N0N0 ], 2 ) ); - - ## N2 -> N0 × N0 × N0 - ## this morphism is mixing two levels and is not a CAP operation: - ## the coproduct N2 in SkeletalFinSets is taken over the index set N0N0N0 (here also realized as an object in SkeletalFinSets), - ## so this morphism is a fibration of a coproduct over its "index set" which are both assumed to objects in the same category: - pi3 := MorphismConstructor( sFinSets, - N2, - Concatenation( List( N0N0N0, i -> ListWithIdenticalEntries( Length( B2[1 + i] ), i ) ) ), - N0N0N0 ); - - ## N2 -> N0 × N0 × N0 -> N0 × N0 - pi312 := PreCompose( sFinSets, pi3, p312 ); - pi323 := PreCompose( sFinSets, pi3, p323 ); - pi313 := PreCompose( sFinSets, pi3, p313 ); - - ## N2 -> N1 - ps := MorphismConstructor( sFinSets, - N2, - List( N2, i -> - AsList( - PreComposeList( sFinSets, - T, - [ LiftAlongMonomorphism( sFinSets, - InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, - B2, - 1 + AsList( pi3 )[1 + i], - N2 ), - N2_elements[1 + i] ), - ProjectionInFactorOfDirectProduct( sFinSets, - [ B1[1 + AsList( pi312 )[1 + i]], - B1[1 + AsList( pi323 )[1 + i]] ], - 1 ), - InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, - B1, - 1 + AsList( pi312 )[1 + i], - N1 ) ], - N1 ) )[1 + 0] ), - N1 ); - - ## N2 -> N1 - pt := MorphismConstructor( sFinSets, - N2, - List( N2, i -> - AsList( - PreComposeList( sFinSets, - T, - [ LiftAlongMonomorphism( sFinSets, - InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, - B2, - 1 + AsList( pi3 )[ 1 + i], - N2 ), - N2_elements[1 + i] ), - ProjectionInFactorOfDirectProduct( sFinSets, - [ B1[1 + AsList( pi312 )[1 + i]], - B1[1 + AsList( pi323 )[1 + i]] ], - 2 ), - InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, - B1, - 1 + AsList( pi323 )[1 + i], - N1 ) ], - N1 ) )[1 + 0] ), - N1 ); - - mus := List( N0N0N0, i -> - List( B2[1 + i], j -> - [ MorphismConstructor( sFinSets, - T, - [ AsList( - ProjectionInFactorOfDirectProduct( sFinSets, - [ B1[1 + AsList( p312 )[1 + i]], - B1[1 + AsList( p323 )[1 + i]] ], - 1 ) )[1 + j] ], - B1[1 + AsList( p312 )[1 + i]] ), - MorphismConstructor( sFinSets, - T, - [ AsList( - ProjectionInFactorOfDirectProduct( sFinSets, - [ B1[1 + AsList( p312 )[1 + i]], - B1[1 + AsList( p323 )[1 + i]] ], - 2 ) )[1 + j] ], - B1[1 + AsList( p323 )[1 + i]] ) ] ) ); - - #% CAP_JIT_DROP_NEXT_STATEMENT - Assert( 0, Length( Concatenation( mus ) ) = Length( N2 ) ); - - #% CAP_JIT_DROP_NEXT_STATEMENT - Assert( 0, ForAll( mus, mu -> ForAll( mu, m -> IsWellDefined( m[1] ) and IsWellDefined( m[2] ) ) ) ); - - mus1 := List( N0N0N0, i -> - List( B2[1 + i], j -> - PreCompose( B, - InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( B, - B0[1 + AsList( p31 )[1 + i]], - B0[1 + AsList( p32 )[1 + i]], - mus[1 + i][1 + j][1] ), - InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( B, - B0[1 + AsList( p32 )[1 + i]], - B0[1 + AsList( p33 )[1 + i]], - mus[1 + i][1 + j][2] ) ) ) ); - - mus2 := List( N0N0N0, i -> - List( B2[1 + i], j -> - InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( B, - mus1[1 + i][1 + j] ) ) ); - - mus3 := List( N0N0N0, i -> - UniversalMorphismFromCoproductWithGivenCoproduct( sFinSets, - List( mus2[1 + i], Source ), - B1[1 + AsList( p313 )[1 + i]], - mus2[1 + i], - B2[1 + i] ) ); - - #% CAP_JIT_DROP_NEXT_STATEMENT - Assert( 0, ForAll( [ 1 .. Length( N0N0N0 ) ], i -> Source( mus3[i] ) = B2[i] ) ); - - ## N2 -> N1 - mu := MorphismConstructor( sFinSets, - N2, - List( N2, i -> - AsList( - PreComposeList( sFinSets, - T, - [ LiftAlongMonomorphism( sFinSets, - InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, - B2, - 1 + AsList( pi3 )[1 + i], - N2 ), - N2_elements[1 + i] ), - mus3[1 + AsList( pi3 )[1 + i]], - InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, - B1, - 1 + AsList( pi313 )[1 + i], - N1 ) ], - N1 ) )[1 + 0] ), - N1 ); - - return Pair( Triple( N0, N1, N2 ), - NTuple( 8, id, s, t, is, it, ps, pt, mu ) ); - -end ); - -## -InstallMethod( NerveTruncatedInDegree2AsFunctor, - [ IsCapCategory and IsFiniteCategory ], - - function ( B ) - local nerve, nerve_ValuesOnAllObjects, nerve_ValuesOnAllGeneratingMorphisms, name, Delta2, Delta2op; - - nerve := NerveTruncatedInDegree2Data( B ); - - nerve_ValuesOnAllObjects := rec( C0 := nerve[1][1], C1 := nerve[1][2], C2 := nerve[1][3] ); - - nerve_ValuesOnAllGeneratingMorphisms := - rec( - id := nerve[2][1], - s := nerve[2][2], - t := nerve[2][3], - is := nerve[2][4], - it := nerve[2][5], - ps := nerve[2][6], - pt := nerve[2][7], - mu := nerve[2][8] ); - - name := Concatenation( "Nerve of ", Name( B ) ); - - ## Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1,is:C2->C1,it:C2->C1,ps:C1->C2,pt:C1->C2,mu:C1->C2] - Delta2 := SimplicialCategoryTruncatedInDegree( 2 ); - - ## Delta_op(C0,C1,C2)[id:C0->C1,s:C1->C0,t:C1->C0,is:C1->C2,it:C1->C2,ps:C2->C1,pt:C2->C1,mu:C2->C1] - Delta2op := OppositeFpCategory( Delta2 ); - - return CapFunctor( Delta2op, nerve_ValuesOnAllObjects, nerve_ValuesOnAllGeneratingMorphisms ); - -end ); - -## -InstallMethodForCompilerForCAP( YonedaNaturalEpimorphisms, - [ IsCapCategory and IsFiniteCategory ], - - function ( B ) - local sFinSets, objs, mors, o, m, Hom2, hom3, Hom3, tum2, emb2, sum2, iso2, - B0, N0, N1, N2, D, precompose, pt, mu, s; - - sFinSets := RangeCategoryOfHomomorphismStructure( B ); - - ## sFinSets must be the category skeletal finite sets - #% CAP_JIT_DROP_NEXT_STATEMENT - Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); - - objs := SetOfObjects( B ); - mors := SetOfGeneratingMorphisms( B ); - - o := Length( objs ); - m := Length( mors ); - - ## [ [ Hom(a, c) ]_{a ∈ B} ]_{c ∈ B}: - Hom2 := List( objs, c -> - List( objs, a -> - HomomorphismStructureOnObjects( B, a, c ) ) ); - - ## [ [ [ ( Hom(a, b), Hom(b, c) ) ]_{b ∈ B} ]_{a ∈ B} ]_{c ∈ B}: - hom3 := List( [ 1 .. o ], c -> - List( [ 1 .. o ], a -> - List( [ 1 .. o ], b -> - [ Hom2[b][a], Hom2[c][b] ] ) ) ); - - ## [ [ [ Hom(a, b) × Hom(b, c) ]_{b ∈ B} ]_{a ∈ B} ]_{c ∈ B}: - Hom3 := List( [ 1 .. o ], c -> - List( [ 1 .. o ], a -> - List( [ 1 .. o ], b -> - DirectProduct( sFinSets, hom3[c][a][b] ) ) ) ); - - ## [ [ Hom(a, b) × Hom(b, c) ]_{a, b ∈ B} ]_{c ∈ B}: - ## tum2 := List( Hom3, L -> Concatenation( TransposedMat( L ) ) ); - tum2 := List( [ 1 .. o ], c -> - Concatenation( - List( [ 1 .. o ], b -> - List( [ 1 .. o ], a -> - Hom3[c][a][b] ) ) ) ); - - ## The embeddings into the double coproducts - ## [ [ Hom(a, b) × Hom(b, c) ↪ ⊔_{a' ∈ B} ⊔_{b' ∈ B} Hom(a', b') × Hom(b', c) ]_{a ∈ B, b ∈ B} ]_{c ∈ B}: - emb2 := List( [ 1 .. o ], c -> - Concatenation( - List( [ 1 .. o ], a -> - List( [ 1 .. o ], b -> - InjectionOfCofactorOfCoproduct( sFinSets, - tum2[c], o * ( b - 1 ) + a ) ) ) ) ); - - ## [ [ Hom(a, b) × Hom(b, c) ]_{b, a ∈ B} ]_{c ∈ B}: - sum2 := List( Hom3, L -> Concatenation( L ) ); - - ## The isomorphisms - ## [ ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c) → ⊔_{b ∈ B} ⊔_{a ∈ B} Hom(a, b) × Hom(b, c) ]_{c ∈ B}: - iso2 := List( [ 1 .. o ], c -> - UniversalMorphismFromCoproduct( sFinSets, - sum2[c], - Coproduct( sFinSets, - tum2[c] ), - emb2[c] ) ); - - ## The constant functor of 0-cells B → sFinSets, c ↦ B_0, ψ ↦ id_{B_0} - B0 := ObjectConstructor( sFinSets, o ); - - N0 := Pair( ListWithIdenticalEntries( o, B0 ), - ListWithIdenticalEntries( m, IdentityMorphism( sFinSets, B0 ) ) ); - - ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ), where - ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c), - ## Hom(-, ψ) := ⊔_{a ∈ B} Hom(id_a, ψ): - N1 := Pair( - List( [ 1 .. o ], c -> - ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c): - Coproduct( sFinSets, Hom2[c] ) ), - List( mors, psi -> - ## Hom(-, ψ) := ⊔_{a ∈ B} Hom(id_a, ψ): - CoproductFunctorial( sFinSets, - List( objs, a -> - HomomorphismStructureOnMorphisms( B, - IdentityMorphism( B, a ), psi ) ) ) ) ); - - ## The 2-Yoneda functor B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ), where - ## Hom(-, -) × Hom(-, c) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c), - ## Hom(-, -) × Hom(-, ψ) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(id_a, id_b) × Hom(id_b, ψ): - N2 := Pair( - List( [ 1 .. o ], c -> - ## Hom(-, -) × Hom(-, c) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c): - Coproduct( sFinSets, - Concatenation( Hom3[c] ) ) ), - List( mors, psi -> - ## Hom(-, -) × Hom(-, ψ) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(id_a, id_b) × Hom(id_b, ψ): - CoproductFunctorial( sFinSets, - Concatenation( - List( objs, a -> - List( objs, b -> - ## Hom(id_a, id_b) × Hom(id_b, ψ): - DirectProductFunctorial( sFinSets, - [ HomomorphismStructureOnMorphisms( B, - IdentityMorphism( B, a ), IdentityMorphism( B, b ) ), - HomomorphismStructureOnMorphisms( B, - IdentityMorphism( B, b ), psi ) ] ) ) ) ) ) ) ); - - D := DistinguishedObjectOfHomomorphismStructure( B ); - - ## mu_{a,b,c}: Hom(a, b) × Hom(b, c) ↠ Hom(a, c): - precompose := - function ( a, b, c ) - return - MorphismConstructor( sFinSets, - Hom3[c][a][b], # = Hom(a, b) × Hom(b, c) - List( Hom3[c][a][b], - function ( i ) - local d, d_ab, d_bc, m_ab, m_bc, m; - - ## D → Hom(a, b) × Hom(b, c): - d := MorphismConstructor( sFinSets, D, [ i ], Hom3[c][a][b] ); - - ## D → Hom(a, b) × Hom(b, c) → Hom(a, b): - d_ab := PreCompose( sFinSets, d, ProjectionInFactorOfDirectProduct( sFinSets, hom3[c][a][b], 1 ) ); - - ## D → Hom(a, b) × Hom(b, c) → Hom(b, c): - d_bc := PreCompose( sFinSets, d, ProjectionInFactorOfDirectProduct( sFinSets, hom3[c][a][b], 2 ) ); - - ## the map a → b corresponding to d_ab: - m_ab := InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( B, objs[a], objs[b], d_ab ); - - ## the map b → c corresponding to d_bc: - m_bc := InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( B, objs[b], objs[c], d_bc ); - - ## the composition a → b → c: - m := PreCompose( B, m_ab, m_bc ); - - ## reinterpret the composition m as a morphism D → Hom(a, c), - ## then get its number as an element in Hom(a, c): - return AsList( InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( B, m ) )[1 + 0]; - - end ), - Hom2[c][a] ); # = Hom(a, c) - end; - - ## The Yoneda projection is a natrual epimorphism from the 2-Yoneda functor to the Yoneda functor - ## B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ) - pt := List( [ 1 .. o ], c -> - ## ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c) ↠ ⊔_{b ∈ B} Hom(b, c): - PreCompose( sFinSets, - ## ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c) → ⊔_{b ∈ B} ⊔_{a ∈ B} Hom(a, b) × Hom(b, c): - iso2[c], - ## ⊔_{b ∈ B} ⊔_{a ∈ B} Hom(a, b) × Hom(b, c) ↠ ⊔_{b ∈ B} Hom(b, c): - CoproductFunctorial( sFinSets, - List( [ 1 .. o ], b -> - ## ⊔_{a ∈ B} Hom(a, b) × Hom(b, c) ↠ Hom(b, c): - UniversalMorphismFromCoproduct( sFinSets, - List( [ 1 .. o ], a -> Hom3[c][a][b] ), - Hom2[c][b], - List( [ 1 .. o ], a -> - ## Hom(a, b) × Hom(b, c) ↠ Hom(b, c): - ProjectionInFactorOfDirectProduct( sFinSets, - hom3[c][a][b], 2 ) ) ) ) ) ) ); - - ## The Yoneda composition is a natrual epimorphism from the 2-Yoneda functor to the Yoneda functor - ## Hom(-, -) × Hom(-, c) ↠ Hom(-, c): - mu := List( [ 1 .. o ], c -> - ## ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c) ↠ ⊔_{a ∈ B} Hom(a, c): - CoproductFunctorial( sFinSets, - List( [ 1 .. o ], a -> - ## ⊔_{b ∈ B} Hom(a, b) × Hom(b, c) ↠ Hom(a, c): - UniversalMorphismFromCoproduct( sFinSets, - List( [ 1 .. o ], b -> Hom3[c][a][b] ), - Hom2[c][a], - List( [ 1 .. o ], b -> - ## Hom(a, b) × Hom(b, c) ↠ Hom(a, c): - precompose( a, b, c ) ) ) ) ) ); - - ## The source fibration is a natrual morphism from the Yoneda functor to the constant functor of 0-cells - ## Hom(-, c) → B_0: - s := List( [ 1 .. o ], c -> - ## ⊔_{a ∈ B} Hom(a, c) → B_0, ϕ ↦ Source(ϕ) - CoproductFunctorial( sFinSets, - List( [ 1 .. o ], a -> - ## Hom(a, c) → {a}, ϕ ↦ a - UniversalMorphismIntoTerminalObject( sFinSets, - Hom2[c][a] ) ) ) ); - - return NTuple( 6, N0, N1, N2, pt, mu, s ); - -end ); - -## -InstallMethod( YonedaProjectionAsNaturalEpimorphism, - [ IsFpCategory and HasRangeCategoryOfHomomorphismStructure ], - - function ( B ) - local Yepis, sFinSets, N1, N2, pt; - - Yepis := YonedaNaturalEpimorphisms( B ); - - sFinSets := RangeCategoryOfHomomorphismStructure( B ); - - ## sFinSets must be the category skeletal finite sets - Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); - - ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ), where - ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c), - ## Hom(-, ψ) := ⊔_{a ∈ B} Hom(id_a, ψ): - N1 := CapFunctor( B, Yepis[2][1], Yepis[2][2], sFinSets ); - - ## The 2-Yoneda functor B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ), where - ## Hom(-, -) × Hom(-, c) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c), - ## Hom(-, -) × Hom(-, ψ) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(id_a, id_b) × Hom(id_b, ψ): - N2 := CapFunctor( B, Yepis[3][1], Yepis[3][2], sFinSets ); - - ## The Yoneda projection is a natrual epimorphism from the 2-Yoneda functor to the Yoneda functor - ## B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ) - pt := NaturalTransformation( - N2, ## The 2-Yoneda functor: B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ) - Yepis[4], - N1 ); ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ) - - #% CAP_JIT_DROP_NEXT_STATEMENT - SetIsEpimorphism( pt, true ); - - return pt; - -end ); - -## -InstallMethod( YonedaCompositionAsNaturalEpimorphism, - [ IsFpCategory and HasRangeCategoryOfHomomorphismStructure ], - - function ( B ) - local Yepis, sFinSets, N1, N2, mu; - - Yepis := YonedaNaturalEpimorphisms( B ); - - sFinSets := RangeCategoryOfHomomorphismStructure( B ); - - ## sFinSets must be the category skeletal finite sets - Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); - - ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ), where - ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c), - ## Hom(-, ψ) := ⊔_{a ∈ B} Hom(id_a, ψ): - N1 := CapFunctor( B, Yepis[2][1], Yepis[2][2], sFinSets ); - - ## The 2-Yoneda functor B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ), where - ## Hom(-, -) × Hom(-, c) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c), - ## Hom(-, -) × Hom(-, ψ) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(id_a, id_b) × Hom(id_b, ψ): - N2 := CapFunctor( B, Yepis[3][1], Yepis[3][2], sFinSets ); - - ## The Yoneda composition is a natrual epimorphism from the 2-Yoneda functor to the Yoneda functor - ## Hom(-, -) × Hom(-, c) ↠ Hom(-, c): - mu := NaturalTransformation( - N2, ## The 2-Yoneda functor: B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ) - Yepis[5], - N1 ); ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ) - - #% CAP_JIT_DROP_NEXT_STATEMENT - SetIsEpimorphism( mu, true ); - - return mu; - -end ); - -## -InstallMethod( YonedaFibrationAsNaturalTransformation, - [ IsFpCategory and HasRangeCategoryOfHomomorphismStructure ], - - function ( B ) - local Yepis, sFinSets, N0, N1; - - Yepis := YonedaNaturalEpimorphisms( B ); - - sFinSets := RangeCategoryOfHomomorphismStructure( B ); - - ## sFinSets must be the category skeletal finite sets - Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); - - ## The constant functor of 0-cells B → sFinSets, c ↦ B_0, ψ ↦ id_{B_0} - N0 := CapFunctor( B, Yepis[1][1], Yepis[1][2], sFinSets ); - - ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ), where - ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c), - ## Hom(-, ψ) := ⊔_{a ∈ B} Hom(id_a, ψ): - N1 := CapFunctor( B, Yepis[2][1], Yepis[2][2], sFinSets ); - - ## The source fibration is a natrual morphism from the Yoneda functor to the constant functor of 0-cells - ## Hom(-, c) → B_0: - return NaturalTransformation( - N1, ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ) - Yepis[6], - N0 ); ## The constant functor of 0-cells - -end ); - -## -InstallMethodForCompilerForCAP( TruthMorphismOfTrueToSieveFunctorAndEmbedding, - [ IsCapCategory and IsFiniteCategory ], - - function ( B ) - local sFinSets, D, Omega, Yepis, Ymu, Ypt, sieves, defining_triple, lobjs, lmors, arrows, id, N1, - Sieves, Sieves_emb, Sieves_maximal, - HomHomOmega_objects, HomHomOmega_morphisms, Sieves_objects, Sieves_morphisms, - Constant_functor, Sieves_functor, HomHomOmega_functor; - - sFinSets := RangeCategoryOfHomomorphismStructure( B ); - - ## sFinSets must be the category skeletal finite sets - #% CAP_JIT_DROP_NEXT_STATEMENT - Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); - - D := DistinguishedObjectOfHomomorphismStructure( B ); - - Omega := SubobjectClassifier( sFinSets ); - - Yepis := YonedaNaturalEpimorphisms( B ); - - Ypt := Yepis[4]; # YonedaProjectionAsNaturalEpimorphism( B ); - Ymu := Yepis[5]; # YonedaCompositionAsNaturalEpimorphism( B ); - - sieves := - function ( c ) - local pt_c, mu_c, hom_c, power, action, maximal, emb; - - ## Hom(-, -) × Hom(-, c) ↠ Hom(-, c) - pt_c := Ypt[c]; - - ## Hom(-, -) × Hom(-, c) ↠ Hom(-, c) - mu_c := Ymu[c]; - - ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c) - hom_c := Target( mu_c ); - - ## Hom(Hom(-, c), Ω) := Hom(⊔_{a ∈ B} Hom(a, c), Ω) - power := HomomorphismStructureOnObjects( sFinSets, hom_c, Omega ); - - ## define the action as an endomorphism on Hom(Hom(-, c), Ω) - action := - MorphismConstructor( sFinSets, - power, ## Hom(Hom(-, c), Ω) - List( power, i -> - ## interpreted as an "element" D → Hom(Hom(-, c), Ω) - AsList( InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( sFinSets, - ## interpreted as a classifying morphism χ_{s'}: Hom(-, c) → Ω - ClassifyingMorphismOfSubobject( sFinSets, - ## s' ↪ Hom(-, c) - ImageEmbedding( sFinSets, - ## Hom(-, -) × s → Hom(-, c) - PreCompose( sFinSets, - ## Hom(-, -) × s ↪ Hom(-, -) × Hom(-, c) - ProjectionInFactorOfFiberProduct( sFinSets, - [ pt_c, - ## interpreted as a subobject s ↪ Hom(-, c) - SubobjectOfClassifyingMorphism( sFinSets, - ## interpreted as a classifying morphism χ_s: Hom(-, c) → Ω - InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( sFinSets, - hom_c, - Omega, - ## an "element" D → Hom(Hom(-, c), Ω) - MorphismConstructor( sFinSets, D, [ i ], power ) ) ) - ], 1 ), - ## μ_c: Hom(-, -) × Hom(-, c) ↠ Hom(-, c) - mu_c ) ) ) ) )[1 + 0] ), - power ); ## Hom(Hom(-, c), Ω) - - ## The sieves on c are the fixed points of the above action on Hom(Hom(-, c), Ω), - ## resulting in the embedding Sieves(c) ↪ Hom(Hom(-, c), Ω): - emb := EmbeddingOfEqualizer( sFinSets, power, [ action, IdentityMorphism( sFinSets, power ) ] ); - - ## the "element" D → Sieves(c) corresponding to the maximal sieve: - maximal := LiftAlongMonomorphism( sFinSets, - ## Sieves(c) ↪ Hom(Hom(-, c), Ω): - emb, - ## interpreted as an "element" D → Hom(Hom(-, c), Ω) - InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( sFinSets, - ## the corresponding classifying morphism χ: Hom(-, c) → Ω - ClassifyingMorphismOfSubobject( sFinSets, - ## id: Hom(-, c) → Hom(-, c) - IdentityMorphism( sFinSets, hom_c ) ) ) ); - - return Pair( emb, maximal ); +InstallMethod( CategoryFromNerveData, + "for a f.p. category", + [ IsFpCategory ], - end; - - defining_triple := DefiningTripleOfUnderlyingQuiver( B ); - - lobjs := defining_triple[1]; - lmors := defining_triple[2]; - - arrows := defining_triple[3]; - - id := IdentityMorphism( sFinSets, Omega ); - - N1 := Yepis[2]; # Target( Ypt ); - - Sieves := List( [ 1 .. lobjs ], o -> sieves( o ) ); - Sieves_emb := List( Sieves, s -> s[1] ); - Sieves_maximal := List( Sieves, s -> s[2] ); - - ## Hom(Hom(-, c), Ω) - HomHomOmega_objects := List( Sieves_emb, Range ); - HomHomOmega_morphisms := List( [ 1 .. lmors ], m -> - HomomorphismStructureOnMorphisms( sFinSets, - N1[2][m], # N1( m ) - id ) ); - - Sieves_objects := List( Sieves_emb, Source ); - Sieves_morphisms := List( [ 1 .. lmors ], m -> - LiftAlongMonomorphism( sFinSets, - Sieves_emb[1 + arrows[m][1]], # Source( m ) - PreCompose( sFinSets, - Sieves_emb[1 + arrows[m][2]], # Target( m ) - HomHomOmega_morphisms[m] ) ) ); + function( C ) - return NTuple( 5, - Pair( Sieves_objects, - Sieves_morphisms ), - Pair( ListWithIdenticalEntries( lobjs, D ), - ListWithIdenticalEntries( lmors, IdentityMorphism( sFinSets, D ) ) ), - Pair( HomHomOmega_objects, - HomHomOmega_morphisms ), - Sieves_maximal, - Sieves_emb ); + return CategoryFromNerveData( + rec( name := Name( C ), + nerve_data := NerveTruncatedInDegree2Data( C ), + indices_of_generating_morphisms := IndicesOfGeneratingMorphismsFromHomStructure( C ), + decomposition_of_all_morphisms := DecompositionIndicesOfAllMorphismsFromHomStructure( C ), + relations := RelationsAmongGeneratingMorphisms( C ), + labels := [ List( SetOfObjects( C ), Label ), List( SetOfGeneratingMorphisms( C ), Label ) ], + properties := ListKnownCategoricalProperties( C ) ) ); end ); diff --git a/Algebroids/gap/SimplicialCategory.gi b/Algebroids/gap/SimplicialCategory.gi deleted file mode 100644 index 548570289..000000000 --- a/Algebroids/gap/SimplicialCategory.gi +++ /dev/null @@ -1,45 +0,0 @@ -# SPDX-License-Identifier: GPL-2.0-or-later -# Algebroids: Algebroids and bialgebroids as preadditive categories generated by enhanced quivers -# -# Implementations -# - -#################################### -# -# global variables: -# -#################################### - -## -InstallGlobalFunction( SimplicialCategoryTruncatedInDegree, - function( n ) - local F; - - if n = 0 then - F := FreeCategory( RightQuiver( "Delta(C0)[]" ) ); - return F; - elif n = 1 then - F := FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ); - return F / - [ [ PreCompose( F.s, F.id ), IdentityMorphism( F.C0 ) ], - [ PreCompose( F.t, F.id ), IdentityMorphism( F.C0 ) ] ]; - elif n = 2 then - F := FreeCategory( RightQuiver( "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1,is:C2->C1,it:C2->C1,ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ); - return F / - [ [ PreCompose( F.s, F.id ), IdentityMorphism( F.C0 ) ], - [ PreCompose( F.t, F.id ), IdentityMorphism( F.C0 ) ], - [ PreCompose( F.ps, F.is ), IdentityMorphism( F.C1 ) ], - [ PreCompose( F.pt, F.it ), IdentityMorphism( F.C1 ) ], - [ PreCompose( F.is, F.id ), PreCompose( F.it, F.id ) ], ## s(1_M) = M = t(1_M) - [ PreCompose( F.pt, F.is ), PreCompose( F.id, F.t ) ], - [ PreCompose( F.ps, F.it ), PreCompose( F.id, F.s ) ], - [ PreCompose( F.s, F.pt ), PreCompose( F.t, F.ps ) ], - [ PreCompose( F.s, F.mu ), PreCompose( F.s, F.ps ) ], - [ PreCompose( F.t, F.mu ), PreCompose( F.t, F.pt ) ], - [ PreCompose( F.mu, F.is ), IdentityMorphism( F.C1 ) ], - [ PreCompose( F.mu, F.it ), IdentityMorphism( F.C1 ) ] ]; - fi; - - Error( "the case n > 2 is not implemented yet\n" ); - -end ); diff --git a/Algebroids/gap/Tools.gd b/Algebroids/gap/Tools.gd index 2a756b416..9b56075ea 100644 --- a/Algebroids/gap/Tools.gd +++ b/Algebroids/gap/Tools.gd @@ -42,27 +42,6 @@ DeclareAttribute( "DefiningTripleOfAQuiver", # #################################### -#! @Description -#! The nerve data of the category C. -#! @Arguments C -#! @Returns a pair consisting of a triple and an 8-tuple -DeclareAttribute( "NerveTruncatedInDegree2Data", - IsCapCategory ); - -#! @Description -#! The normalized indices of the generating morphisms of the finite category C. -#! @Arguments C -#! @Returns a list of integers -DeclareAttribute( "IndicesOfGeneratingMorphismsFromHomStructure", - IsCapCategory ); - -#! @Description -#! The opposite category of a finite category C. -#! @Arguments C -#! @Returns a &CAP; category -DeclareAttribute( "OppositeFiniteCategory", - IsCapCategory ); - DeclareGlobalFunction( "DefiningTripleOfUnderlyingQuiverAsString" ); DeclareGlobalFunction( "DefiningTripleOfUnderlyingQuiverAsENHANCED_SYNTAX_TREE" ); diff --git a/Algebroids/gap/Tools.gi b/Algebroids/gap/Tools.gi index f0c4b3225..185792021 100644 --- a/Algebroids/gap/Tools.gi +++ b/Algebroids/gap/Tools.gi @@ -36,72 +36,6 @@ InstallMethod( DefiningTripleOfAQuiver, end ); -## -InstallMethod( IndicesOfGeneratingMorphismsFromHomStructure, - "for a finite category", - [ IsCapCategory and IsFiniteCategory ], - - function( C ) - local sFinSets, C0, N0, D00, N0N0, p21, p22, C1, T, st, mors; - - sFinSets := RangeCategoryOfHomomorphismStructure( C ); - - ## sFinSets must be the category skeletal finite sets - Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); - - C0 := SetOfObjects( C ); - N0 := ObjectConstructor( sFinSets, Length( C0 ) ); - - D00 := [ N0, N0 ]; - - ## N0 × N0 -> N0 - p21 := ProjectionInFactorOfDirectProduct( sFinSets, D00, 1 ); - p22 := ProjectionInFactorOfDirectProduct( sFinSets, D00, 2 ); - - C1 := List( DirectProduct( sFinSets, D00 ), i -> - HomomorphismStructureOnObjects( C, - C0[1 + AsList( p21 )[1 + i]], - C0[1 + AsList( p22 )[1 + i]] ) ); - - T := DistinguishedObjectOfHomomorphismStructure( C ); - - st := List( DefiningTripleOfUnderlyingQuiver( C )[3], pair -> - UniversalMorphismIntoDirectProduct( sFinSets, - D00, - T, - [ MorphismConstructor( sFinSets, T, [ pair[1] ], N0 ), - MorphismConstructor( sFinSets, T, [ pair[2] ], N0 ) ] ) ); - - mors := SetOfGeneratingMorphisms( C ); - - return List( [ 1 .. Length( st ) ], i -> - Sum( C1{[ 1 .. AsList( st[i] )[1 + 0] ]}, Length ) + - AsList( InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( C, mors[i] ) )[1 + 0] ); - -end ); - -## -InstallMethod( OppositeFiniteCategory, - "for a finite category", - [ IsCapCategory and IsFiniteCategory ], - - function( C ) - local C_op, defining_triple; - - C_op := Opposite( C ); - - defining_triple := DefiningTripleOfUnderlyingQuiver( C ); - - defining_triple := Triple( defining_triple[1], - defining_triple[2], - List( defining_triple[3], a -> Pair( a[2], a[1] ) ) ); - - SetDefiningTripleOfUnderlyingQuiver( C_op, defining_triple ); - - return C_op; - -end ); - ## InstallGlobalFunction( DefiningTripleOfUnderlyingQuiverAsString, function( defining_triple_of_underlying_quiver ) diff --git a/Algebroids/init.g b/Algebroids/init.g index 1c6388a2f..4b96e2c81 100644 --- a/Algebroids/init.g +++ b/Algebroids/init.g @@ -9,13 +9,11 @@ ReadPackage( "Algebroids", "gap/QuiverRows.gd" ); ReadPackage( "Algebroids", "gap/FpCategories.gd"); ReadPackage( "Algebroids", "gap/Algebroids.gd"); ReadPackage( "Algebroids", "gap/Functors.gd"); -ReadPackage( "Algebroids", "gap/CategoryFromNerveData.gd"); ReadPackage( "Algebroids", "gap/CategoryFromDataTables.gd"); ReadPackage( "Algebroids", "gap/LinearClosuresOfPathCategoriesAndTheirQuotients.gd"); ReadPackage( "Algebroids", "gap/AlgebroidFromDataTables.gd"); ReadPackage( "Algebroids", "gap/CategoryOfAlgebroids.gd"); ReadPackage( "Algebroids", "gap/Bialgebroids.gd"); -ReadPackage( "Algebroids", "gap/SimplicialCategory.gd"); ReadPackage( "Algebroids", "gap/Tools.gd"); if IsPackageMarkedForLoading( "JuliaInterface", ">= 0.2" ) then diff --git a/Algebroids/read.g b/Algebroids/read.g index 068705c9c..8b6a2cf95 100644 --- a/Algebroids/read.g +++ b/Algebroids/read.g @@ -6,9 +6,6 @@ ReadPackage( "Algebroids", "gap/QuiverRows.gi" ); -ReadPackage( "Algebroids", "gap/precompiled_categories/CategoryFromNerveDataPrecompiled.gi" ); -ReadPackage( "Algebroids", "gap/precompiled_categories/CategoryFromNerveDataHomStructureOnMorphismsPrecompiled.gi" ); - ReadPackage( "Algebroids", "gap/precompiled_categories/CategoryFromDataTablesPrecompiled.gi" ); ReadPackage( "Algebroids", "gap/precompiled_categories/AdditiveClosureOfAlgebroidOfFiniteDimensionalQuiverAlgebraOfRightQuiverOverFieldPrecompiled.gi" ); @@ -22,13 +19,11 @@ ReadPackage( "Algebroids", "gap/FpCategories.gi"); ReadPackage( "Algebroids", "gap/Algebroids.gi"); ReadPackage( "Algebroids", "gap/QPA2.gi"); ReadPackage( "Algebroids", "gap/Functors.gi"); -ReadPackage( "Algebroids", "gap/CategoryFromNerveData.gi"); ReadPackage( "Algebroids", "gap/CategoryFromDataTables.gi"); ReadPackage( "Algebroids", "gap/LinearClosuresOfPathCategoriesAndTheirQuotients.gi" ); ReadPackage( "Algebroids", "gap/AlgebroidFromDataTables.gi"); ReadPackage( "Algebroids", "gap/CategoryOfAlgebroids.gi"); ReadPackage( "Algebroids", "gap/Bialgebroids.gi"); -ReadPackage( "Algebroids", "gap/SimplicialCategory.gi"); ReadPackage( "Algebroids", "gap/Tools.gi"); ReadPackage( "Algebroids", "gap/GroebnerBasesForLinearClosuresOfPathCategories.gi" ); ReadPackage( "Algebroids", "gap/QuotientsOfLinearClosuresOfPathCategories.gi" ); diff --git a/FiniteCocompletions/PackageInfo.g b/FiniteCocompletions/PackageInfo.g index 5fa3fc6f7..74ae77228 100644 --- a/FiniteCocompletions/PackageInfo.g +++ b/FiniteCocompletions/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "FiniteCocompletions", Subtitle := "Finite (co)product/(co)limit (co)completions", -Version := "2024.09-04", +Version := "2024.09-05", Date := ~.Version{[ 1 .. 10 ]}, Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ), License := "GPL-2.0-or-later", @@ -80,8 +80,8 @@ Dependencies := rec( [ "FinSetsForCAP", ">= 2024.03-01" ], [ "Locales", ">= 2024.03-04" ], [ "QuotientCategories", ">= 2024.02-01" ], - [ "FpCategories", ">= 2024.02-11" ], - [ "Algebroids", ">= 2024.02-02" ], + [ "FpCategories", ">= 2024.09-06" ], + [ "Algebroids", ">= 2024.09-04" ], [ "PreSheaves", ">= 2024.02-02" ], ], SuggestedOtherPackages := [ ], diff --git a/FiniteCocompletions/examples/CategoryOfColimitQuivers.g b/FiniteCocompletions/examples/CategoryOfColimitQuivers.g index c3794fdef..77cad6033 100644 --- a/FiniteCocompletions/examples/CategoryOfColimitQuivers.g +++ b/FiniteCocompletions/examples/CategoryOfColimitQuivers.g @@ -1,56 +1,56 @@ #! @BeginChunk CategoryOfColimitQuivers #! @Example -LoadPackage( "FunctorCategories", ">= 2024.03-18", false ); +LoadPackage( "FunctorCategories", ">= 2024.09-09", false ); #! true FinBouquets; #! FinBouquets Chat := ModelingCategory( FinBouquets ); -#! FiniteCocompletion( FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) +#! FiniteCocompletion( PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) ColimitQuiversC := CategoryOfColimitQuivers( UnderlyingCategory( FinBouquets ) ); #! CategoryOfColimitQuivers( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) P := ColimitQuiversC.P; #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> Display( P ); #! [ [ <(P)> ], [ ] ] #! #! An object in CategoryOfColimitQuivers( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data L := ColimitQuiversC.L; #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> Display( L ); #! [ [ <(L)> ], [ ] ] #! #! An object in CategoryOfColimitQuivers( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data b := ColimitQuiversC.b; #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> Display( b ); #! Source: [ [ <(P)> ], [ ] ] #! #! An object in CategoryOfColimitQuivers( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Datum: [ [ [ 0 ], [ (P)-[(b)]->(L) ] ], [ ] ] #! #! Range: [ [ <(L)> ], [ ] ] #! #! An object in CategoryOfColimitQuivers( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! A morphism in CategoryOfColimitQuivers( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data F := CreateBouquet( 3, [ 0, 0, 0, 2 ] ); #! Display( F ); #! ( { 0, 1, 2 }, { 0 ↦ 0, 1 ↦ 0, 2 ↦ 0, 3 ↦ 2 } ) F_as_presheaf := ModelingObject( Chat, ModelingObject( FinBouquets, F ) ); -#! L]" ) ), +#! Display( F_as_presheaf ); #! Image of <(P)>: @@ -62,18 +62,18 @@ Display( F_as_presheaf ); #! Image of (P)-[(b)]->(L): #! { 0,..., 3 } ⱶ[ 0, 0, 0, 2 ]→ { 0, 1, 2 } #! -#! An object in PreSheaves( FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ), +#! An object in PreSheaves( PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ), #! SkeletalFinSets ) given by the above data F_as_coequalizer_object := CoYonedaLemmaOnObjects( F_as_presheaf ); #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> ColimitCompletionC := CapCategory( F_as_coequalizer_object ); #! FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) Display( ColimitCompletionC ); #! A CAP category with name #! FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ): +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ): #! #! 22 primitive operations were used to derive 64 operations for this category #! which algorithmically @@ -84,50 +84,50 @@ Display( F_as_coequalizer_object ); #! Image of <(V)>: #! [ 7, [ <(P)>, <(P)>, <(P)>, <(L)>, <(L)>, <(L)>, <(L)> ] ] #! -#! An object in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! An object in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of <(A)>: #! [ 4, [ <(P)>, <(P)>, <(P)>, <(P)> ] ] #! -#! An object in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! An object in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(s)]->(A): #! { 0,..., 3 } ⱶ[ 0, 0, 0, 2 ]→ { 0,..., 6 } #! #! [ (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P) ] #! -#! A morphism in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! A morphism in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(t)]->(A): #! { 0,..., 3 } ⱶ[ 3, 4, 5, 6 ]→ { 0,..., 6 } #! #! [ (P)-[(b)]->(L), (P)-[(b)]->(L), (P)-[(b)]->(L), (P)-[(b)]->(L) ] #! -#! A morphism in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! A morphism in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! -#! An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), +#! An object in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), #! FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) ) given by the above data #! #! An object in FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data F_as_presheaf = Coequalizer( AssociatedCoequalizerPairInPreSheaves( F_as_coequalizer_object )[2] ); #! true F_as_colimit_quiver := AssociatedColimitQuiver( F_as_coequalizer_object ); #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> Display( F_as_colimit_quiver ); #! [ [ <(P)>, <(P)>, <(P)>, <(L)>, <(L)>, <(L)>, <(L)> ], #! [ [ 0, (P)-[(b)]->(L), 3 ], [ 0, (P)-[(b)]->(L), 4 ], #! [ 0, (P)-[(b)]->(L), 5 ], [ 2, (P)-[(b)]->(L), 6 ] ] ] #! #! An object in CategoryOfColimitQuivers( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data F_as_presheaf = Coequalizer( AssociatedCoequalizerPairInPreSheaves( F_as_colimit_quiver )[2] ); #! true diff --git a/FiniteCocompletions/examples/CharacteristicMatrix.g b/FiniteCocompletions/examples/CharacteristicMatrix.g index 854f6209a..582444aba 100644 --- a/FiniteCocompletions/examples/CharacteristicMatrix.g +++ b/FiniteCocompletions/examples/CharacteristicMatrix.g @@ -106,7 +106,7 @@ Display( Mphi_as_coequqlizer_pair ); #! [3,1]: (o)-[{ 0 }]->(o) #! [3,2]: (o)-[{ 0 }]->(o) #! [3,3]: (o)-[{ 1*(x) }]->(o) -#! An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), +#! An object in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), #! AdditiveClosure( Algebra( Q, FreeCategory( RightQuiver( "q(o)[x:o->o]" ) ) ) / #! relations ) ) given by the above data #! diff --git a/FiniteCocompletions/examples/CoequalizerCompletion.g b/FiniteCocompletions/examples/CoequalizerCompletion.g index d91de2c9a..4005b76f3 100644 --- a/FiniteCocompletions/examples/CoequalizerCompletion.g +++ b/FiniteCocompletions/examples/CoequalizerCompletion.g @@ -140,7 +140,7 @@ Display( coeq ); #! [3,2]: (VS)-[{ 0 }]->(VS) #! [4,1]: (VS)-[{ 1*(m3) }]->(VT) #! [4,2]: (VS)-[{ 0 }]->(VS) -#! An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), +#! An object in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), #! AdditiveClosure( Algebroid( Q, FreeCategory( RightQuiver( "q(VS,AS,VT,AT) #! [sS:AS->VS,tS:AS->VS,sT:AT->VT,tT:AT->VT, #! m1:VS->VT,w1:AS->AT,m2:VS->VT,w2:AS->AT,m3:VS->VT,w3:AS->AT]" ) ) ) / relations ) ) @@ -189,7 +189,7 @@ Display( proj ); #! [1,2]: (AT)-[{ 0 }]->(VS) #! [1,3]: (AT)-[{ 0 }]->(VS) #! [1,4]: (AT)-[{ 0 }]->(VS) -#! A morphism in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), +#! A morphism in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), #! AdditiveClosure( Algebroid( Q, FreeCategory( RightQuiver( "q(VS,AS,VT,AT) #! [sS:AS->VS,tS:AS->VS,sT:AT->VT,tT:AT->VT, #! m1:VS->VT,w1:AS->AT,m2:VS->VT,w2:AS->AT,m3:VS->VT,w3:AS->AT]" ) ) ) diff --git a/FiniteCocompletions/examples/FinBouquetsAsFiniteColimitCompletion.g b/FiniteCocompletions/examples/FinBouquetsAsFiniteColimitCompletion.g index ce6babcb7..335426455 100644 --- a/FiniteCocompletions/examples/FinBouquetsAsFiniteColimitCompletion.g +++ b/FiniteCocompletions/examples/FinBouquetsAsFiniteColimitCompletion.g @@ -1,12 +1,12 @@ #! @BeginChunk FinBouquetsAsFiniteColimitCompletion #! @Example -LoadPackage( "FunctorCategories", ">= 2023.11-07", false ); +LoadPackage( "FunctorCategories", ">= 2024.09-09", false ); #! true FinBouquets; #! FinBouquets Chat := ModelingCategory( FinBouquets ); -#! FiniteCocompletion( FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) +#! FiniteCocompletion( PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) source_bouquet := CreateBouquet( 3, [ 0, 0, 1 ] ); #! Display( source_bouquet ); @@ -14,47 +14,47 @@ Display( source_bouquet ); source_presheaf := ModelingObject( Chat, ModelingObject( FinBouquets, source_bouquet ) ); #! L]" ) ), SkeletalFinSets )> +#! PreSheaves( PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ), SkeletalFinSets )> source_coeq_pair := CoYonedaLemmaOnObjects( source_presheaf ); #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> IsWellDefined( source_coeq_pair ); #! true Display( source_coeq_pair ); #! Image of <(V)>: #! [ 6, [ <(P)>, <(P)>, <(P)>, <(L)>, <(L)>, <(L)> ] ] #! -#! An object in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! An object in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of <(A)>: #! [ 3, [ <(P)>, <(P)>, <(P)> ] ] #! -#! An object in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! An object in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(s)]->(A): #! { 0, 1, 2 } ⱶ[ 0, 0, 1 ]→ { 0,..., 5 } #! #! [ (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P) ] #! -#! A morphism in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! A morphism in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(t)]->(A): #! { 0, 1, 2 } ⱶ[ 3, 4, 5 ]→ { 0,..., 5 } #! #! [ (P)-[(b)]->(L), (P)-[(b)]->(L), (P)-[(b)]->(L) ] #! -#! A morphism in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! A morphism in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! -#! An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), +#! An object in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), #! FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) ) given by the above data #! #! An object in FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data target_bouquet := CreateBouquet( 2, [ 0, 0, 0, 0, 1 ] ); #! Display( target_bouquet ); @@ -62,45 +62,45 @@ Display( target_bouquet ); target_presheaf := ModelingObject( Chat, ModelingObject( FinBouquets, target_bouquet ) ); #! L]" ) ), SkeletalFinSets )> +#! PreSheaves( PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ), SkeletalFinSets )> target_coeq_pair := CoYonedaLemmaOnObjects( target_presheaf ); #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> Display( target_coeq_pair ); #! Image of <(V)>: #! [ 7, [ <(P)>, <(P)>, <(L)>, <(L)>, <(L)>, <(L)>, <(L)> ] ] #! -#! An object in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! An object in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of <(A)>: #! [ 5, [ <(P)>, <(P)>, <(P)>, <(P)>, <(P)> ] ] #! -#! An object in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! An object in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(s)]->(A): #! { 0,..., 4 } ⱶ[ 0, 0, 0, 0, 1 ]→ { 0,..., 6 } #! #! [ (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P) ] #! -#! A morphism in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! A morphism in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(t)]->(A): #! { 0,..., 4 } ⱶ[ 2, 3, 4, 5, 6 ]→ { 0,..., 6 } #! #! [ (P)-[(b)]->(L), (P)-[(b)]->(L), (P)-[(b)]->(L), (P)-[(b)]->(L), (P)-[(b)]->(L) ] #! -#! A morphism in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! A morphism in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! -#! An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), +#! An object in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), #! FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) ) given by the above data #! #! An object in FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data bouquet_morphism := CreateBouquetMorphism( source_bouquet, [ 0, 1, 1 ], [ 1, 3, 4 ], @@ -111,10 +111,10 @@ IsWellDefined( bouquet_morphism ); presheaf_morphism := ModelingMorphism( Chat, ModelingMorphism( FinBouquets, bouquet_morphism ) ); #! L]" ) ), SkeletalFinSets )> +#! PreSheaves( PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ), SkeletalFinSets )> coeq_pair_morphism := CoYonedaLemmaOnMorphisms( presheaf_morphism ); #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> IsWellDefined( coeq_pair_morphism ); #! true Display( coeq_pair_morphism ); @@ -124,22 +124,22 @@ Display( coeq_pair_morphism ); #! [ (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P), #! (L)-[(L)]->(L), (L)-[(L)]->(L), (L)-[(L)]->(L) ] #! -#! A morphism in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! A morphism in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of <(A)>: #! { 0, 1, 2 } ⱶ[ 1, 3, 4 ]→ { 0,..., 4 } #! #! [ (P)-[(P)]->(P), (P)-[(P)]->(P), (P)-[(P)]->(P) ] #! -#! A morphism in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! A morphism in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! -#! A morphism in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), +#! A morphism in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), #! FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) ) given by the above data #! #! A morphism in FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! @EndExample #! @EndChunk diff --git a/FiniteCocompletions/examples/FinReflexiveQuiversAsFiniteColimitCompletion.g b/FiniteCocompletions/examples/FinReflexiveQuiversAsFiniteColimitCompletion.g index 707edbe34..aebb7f23a 100644 --- a/FiniteCocompletions/examples/FinReflexiveQuiversAsFiniteColimitCompletion.g +++ b/FiniteCocompletions/examples/FinReflexiveQuiversAsFiniteColimitCompletion.g @@ -4,119 +4,127 @@ LoadPackage( "FunctorCategories", ">= 2023.11-07", false ); #! true Delta1 := SimplicialCategoryTruncatedInDegree( 1 ); -#! FreeCategory( RightQuiver( -#! "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ] +#! PathCategory( FinQuiver( +#! "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] Size( Delta1 ); #! 7 PSh := PreSheaves( Delta1 ); -#! PreSheaves( FreeCategory( RightQuiver( -#! "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ], +#! PreSheaves( PathCategory( FinQuiver( +#! "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ], #! SkeletalFinSets ) Display( PSh.C1 ); -#! Image of <(C0)>: +#! Image of (C0): #! { 0, 1 } #! -#! Image of <(C1)>: +#! Image of (C1): #! { 0, 1, 2 } #! -#! Image of (C1)-[(id)]->(C0): +#! Image of [id]:(C1) -≻ (C0): #! { 0, 1 } ⱶ[ 1, 2 ]→ { 0, 1, 2 } #! -#! Image of (C0)-[(s)]->(C1): +#! Image of [s]:(C0) -≻ (C1): #! { 0, 1, 2 } ⱶ[ 0, 0, 1 ]→ { 0, 1 } #! -#! Image of (C0)-[(t)]->(C1): +#! Image of [t]:(C0) -≻ (C1): #! { 0, 1, 2 } ⱶ[ 1, 0, 1 ]→ { 0, 1 } #! -#! An object in PreSheaves( FreeCategory( RightQuiver( -#! "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ], +#! An object in PreSheaves( PathCategory( FinQuiver( +#! "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ], #! SkeletalFinSets ) given by the above data coeq_pair := CoYonedaLemmaOnObjects( PSh.C1 ); #! C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] )> +#! PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] )> Display( coeq_pair ); #! Image of <(V)>: -#! [ 5, [ <(C0)>, <(C0)>, <(C1)>, <(C1)>, <(C1)> ] ] +#! [ 5, [ (C0), (C0), (C1), (C1), (C1) ] ] #! -#! An object in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] ) given by the above data +#! An object in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] ) given by the above data #! #! Image of <(A)>: -#! [ 8, [ <(C1)>, <(C1)>, <(C0)>, <(C0)>, <(C0)>, <(C0)>, <(C0)>, <(C0)> ] ] +#! [ 8, [ (C1), (C1), (C0), (C0), (C0), (C0), (C0), (C0) ] ] #! -#! An object in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] ) given by the above data +#! An object in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] ) given by the above data #! #! Image of (V)-[(s)]->(A): #! { 0,..., 7 } ⱶ[ 3, 4, 0, 0, 1, 1, 0, 1 ]→ { 0,..., 4 } #! -#! [ (C1)-[(C1)]->(C1), (C1)-[(C1)]->(C1), (C0)-[(C0)]->(C0), (C0)-[(C0)]->(C0), -#! (C0)-[(C0)]->(C0), (C0)-[(C0)]->(C0), (C0)-[(C0)]->(C0), (C0)-[(C0)]->(C0) ] +#! [ [id(C1)]:(C1) -≻ (C1), [id(C1)]:(C1) -≻ (C1), [id(C0)]:(C0) -≻ (C0), +#! [id(C0)]:(C0) -≻ (C0), [id(C0)]:(C0) -≻ (C0), [id(C0)]:(C0) -≻ (C0), +#! [id(C0)]:(C0) -≻ (C0), [id(C0)]:(C0) -≻ (C0) ] #! -#! A morphism in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] ) given by the above data +#! A morphism in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] ) given by the above data #! #! Image of (V)-[(t)]->(A): #! { 0,..., 7 } ⱶ[ 0, 1, 2, 3, 4, 2, 3, 4 ]→ { 0,..., 4 } #! -#! [ (C1)-[(id)]->(C0), (C1)-[(id)]->(C0), (C0)-[(s)]->(C1), (C0)-[(s)]->(C1), -#! (C0)-[(s)]->(C1), (C0)-[(t)]->(C1), (C0)-[(t)]->(C1), (C0)-[(t)]->(C1) ] +#! [ [id]:(C1) -≻ (C0), [id]:(C1) -≻ (C0), [s]:(C0) -≻ (C1), [s]:(C0) -≻ (C1), +#! [s]:(C0) -≻ (C1), [t]:(C0) -≻ (C1), [t]:(C0) -≻ (C1), [t]:(C0) -≻ (C1) ] #! -#! A morphism in FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] ) given by the above data +#! A morphism in FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] ) given by the above data #! -#! An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), -#! FiniteStrictCoproductCompletion( FreeCategory( -#! RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] ) ) given by the above data +#! An object in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), +#! FiniteStrictCoproductCompletion( PathCategory( +#! FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] ) ) given by the above data #! #! An object in FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] ) given by the above data +#! PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] ) given by the above data IsWellDefined( coeq_pair ); #! true coeq_pair_in_presheaves := CoYonedaLemmaCoequalizerPair( PSh.C1 );; coeq := Coequalizer( coeq_pair_in_presheaves[2] ); -#! C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ], +#! Display( coeq ); -#! Image of <(C0)>: +#! Image of (C0): #! { 0, 1 } #! -#! Image of <(C1)>: +#! Image of (C1): #! { 0, 1, 2 } #! -#! Image of (C1)-[(id)]->(C0): +#! Image of [id]:(C1) -≻ (C0): #! { 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1, 2 } #! -#! Image of (C0)-[(s)]->(C1): +#! Image of [s]:(C0) -≻ (C1): #! { 0, 1, 2 } ⱶ[ 0, 1, 0 ]→ { 0, 1 } #! -#! Image of (C0)-[(t)]->(C1): +#! Image of [t]:(C0) -≻ (C1): #! { 0, 1, 2 } ⱶ[ 0, 1, 1 ]→ { 0, 1 } #! -#! An object in PreSheaves( FreeCategory( RightQuiver( -#! "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ], +#! An object in PreSheaves( PathCategory( FinQuiver( +#! "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ], #! SkeletalFinSets ) given by the above data iso := Filtered( MorphismsOfExternalHom( PSh.C1, coeq ), IsIsomorphism )[1]; -#! C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ], +#! Display( iso ); -#! Image of <(C0)>: +#! Image of (C0): #! { 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 } #! -#! Image of <(C1)>: +#! Image of (C1): #! { 0, 1, 2 } ⱶ[ 2, 0, 1 ]→ { 0, 1, 2 } #! -#! A morphism in PreSheaves( FreeCategory( RightQuiver( -#! "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) / [ s*id = C0, t*id = C0 ], +#! A morphism in PreSheaves( PathCategory( FinQuiver( +#! "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ], #! SkeletalFinSets ) given by the above data #! @EndExample #! @EndChunk diff --git a/FiniteCocompletions/examples/FiniteColimitCompletionWithStrictCoproducts.g b/FiniteCocompletions/examples/FiniteColimitCompletionWithStrictCoproducts.g index f45e10331..3365fdcdb 100644 --- a/FiniteCocompletions/examples/FiniteColimitCompletionWithStrictCoproducts.g +++ b/FiniteCocompletions/examples/FiniteColimitCompletionWithStrictCoproducts.g @@ -15,17 +15,17 @@ Display( FinBouquets ); #! * IsEquippedWithHomomorphismStructure #! * IsElementaryTopos C := UnderlyingCategory( FinBouquets ); -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) C_hat := FiniteColimitCompletionWithStrictCoproducts( C ); #! FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) ModelingCategory( C_hat ); #! CoequalizerCompletion( FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) ) Display( C_hat ); #! A CAP category with name #! FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ): +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ): #! #! 22 primitive operations were used to derive 64 operations for this category #! which algorithmically @@ -36,13 +36,13 @@ MissingOperationsForConstructivenessOfCategory( C_hat, "IsFiniteCocompleteCatego #! [ "UniversalMorphismFromCoequalizerWithGivenCoequalizer" ] P := C_hat.P; #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> L := C_hat.L; #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> b := C_hat.b; #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> Source( b ) = P; #! true Target( b ) = L; @@ -52,13 +52,13 @@ Display( P ); #! [ 1, [ <(P)> ] ] #! #! An object in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of <(A)>: #! [ 0, [ ] ] #! #! An object in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(s)]->(A): #! ∅ ⱶ[ ]→ { 0 } @@ -66,7 +66,7 @@ Display( P ); #! [ ] #! #! A morphism in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(t)]->(A): #! ∅ ⱶ[ ]→ { 0 } @@ -74,26 +74,26 @@ Display( P ); #! [ ] #! #! A morphism in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! -#! An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), +#! An object in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), #! FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) ) given by the above data #! #! An object in FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data Display( L ); #! Image of <(V)>: #! [ 1, [ <(L)> ] ] #! #! An object in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of <(A)>: #! [ 0, [ ] ] #! #! An object in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(s)]->(A): #! ∅ ⱶ[ ]→ { 0 } @@ -101,7 +101,7 @@ Display( L ); #! [ ] #! #! A morphism in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(t)]->(A): #! ∅ ⱶ[ ]→ { 0 } @@ -109,14 +109,14 @@ Display( L ); #! [ ] #! #! A morphism in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! -#! An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), +#! An object in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), #! FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) ) given by the above data #! #! An object in FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data Display( b ); #! Image of <(V)>: #! { 0 } ⱶ[ 0 ]→ { 0 } @@ -124,7 +124,7 @@ Display( b ); #! [ (P)-[(b)]->(L) ] #! #! A morphism in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of <(A)>: #! ∅ ⱶ[ ]→ ∅ @@ -132,36 +132,36 @@ Display( b ); #! [ ] #! #! A morphism in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! -#! A morphism in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), +#! A morphism in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), #! FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) ) given by the above data #! #! A morphism in FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data inj := InjectionOfCofactorOfPushout( [ b, b ], 1 ); #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> IsWellDefined( inj ); #! true Source( inj ) = L; #! true pushout := Target( inj ); #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> Display( pushout ); #! Image of <(V)>: #! [ 3, [ <(L)>, <(L)>, <(P)> ] ] #! #! An object in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of <(A)>: #! [ 2, [ <(P)>, <(P)> ] ] #! #! An object in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(s)]->(A): #! { 0, 1 } ⱶ[ 2, 2 ]→ { 0, 1, 2 } @@ -169,7 +169,7 @@ Display( pushout ); #! [ (P)-[(P)]->(P), (P)-[(P)]->(P) ] #! #! A morphism in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! #! Image of (V)-[(t)]->(A): #! { 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1, 2 } @@ -177,13 +177,13 @@ Display( pushout ); #! [ (P)-[(b)]->(L), (P)-[(b)]->(L) ] #! #! A morphism in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! -#! An object in PreSheaves( FreeCategory( RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ), +#! An object in PreSheaves( PathCategory( FinQuiver( "q(V,A)[s:V-≻A,t:V-≻A]" ) ), #! FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) ) given by the above data #! #! An object in FiniteColimitCompletionWithStrictCoproducts( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data #! @EndExample #! @EndChunk diff --git a/FiniteCocompletions/examples/FiniteStrictCoproductCompletion.g b/FiniteCocompletions/examples/FiniteStrictCoproductCompletion.g index b2216ad0e..f047df4e8 100644 --- a/FiniteCocompletions/examples/FiniteStrictCoproductCompletion.g +++ b/FiniteCocompletions/examples/FiniteStrictCoproductCompletion.g @@ -1,49 +1,49 @@ #! @BeginChunk FiniteStrictCoproductCompletion #! @Example -LoadPackage( "FunctorCategories", ">= 2023.10-04" ); +LoadPackage( "FunctorCategories", ">= 2024.09-09", false ); #! true FinBouquets; #! FinBouquets Chat := ModelingCategory( FinBouquets ); -#! FiniteCocompletion( FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) +#! FiniteCocompletion( PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) UC := FiniteStrictCoproductCompletion( UnderlyingCategory( FinBouquets ) ); #! FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) P := UC.P; #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> Display( P ); #! [ 1, [ <(P)> ] ] #! #! An object in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data L := UC.L; #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> Display( L ); #! [ 1, [ <(L)> ] ] #! #! An object in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data b := UC.b; #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> Display( b ); #! { 0 } ⱶ[ 0 ]→ { 0 } #! #! [ (P)-[(b)]->(L) ] #! #! A morphism in FiniteStrictCoproductCompletion( -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) ) given by the above data +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) ) given by the above data HomStructure( UC ); #! |1| HomStructure( P, L ); #! |1| homPL := MorphismsOfExternalHom( P, L ); #! [ L]" ) ) )> ] +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> ] List( homPL, m -> HomStructure( P, L, HomStructure( m ) ) = m ); #! [ true ] HomStructure( b, b ); @@ -54,10 +54,10 @@ HomStructure( P, b ); #! |1| → |1| M := Coproduct( P, L, P ); #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> N := Coproduct( L, P, L ); #! L]" ) ) )> +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) )> HomStructure( M, N ); #! |18| HomStructure( P, L ); diff --git a/FiniteCocompletions/gap/PairOfParallelArrowsCategory.gi b/FiniteCocompletions/gap/PairOfParallelArrowsCategory.gi index d1702053e..4c326f7c7 100644 --- a/FiniteCocompletions/gap/PairOfParallelArrowsCategory.gi +++ b/FiniteCocompletions/gap/PairOfParallelArrowsCategory.gi @@ -6,7 +6,7 @@ ## BindGlobal( "QuiverOfCategoryOfQuivers", - RightQuiver( "q(V,A)[s:V->A,t:V->A]" ) ); + FinQuiver( "q(V,A)[s:V->A,t:V->A]" ) ); ## InstallMethod( PairOfParallelArrowsCategory, @@ -64,7 +64,7 @@ InstallMethod( PairOfParallelArrowsCategory, morphism_datum := { ParallelPairs, m } -> DefiningPairOfMorphismBetweenParallelPairs( m ); ## building the categorical tower: - F := FreeCategory( QuiverOfCategoryOfQuivers : range_of_HomStructure := SkeletalFinSets, FinalizeCategory := true ); + F := PathCategory( QuiverOfCategoryOfQuivers : range_of_HomStructure := SkeletalFinSets, FinalizeCategory := true ); F := CategoryFromDataTables( F : set_category_attribute_resolving_functions := true, FinalizeCategory := true ); diff --git a/FpCategories/PackageInfo.g b/FpCategories/PackageInfo.g index a2ac9924c..17db21564 100644 --- a/FpCategories/PackageInfo.g +++ b/FpCategories/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "FpCategories", Subtitle := "Finitely presented categories by generating quivers and relations", -Version := "2024.09-05", +Version := "2024.09-06", Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ), License := "GPL-2.0-or-later", diff --git a/FpCategories/doc/Doc.autodoc b/FpCategories/doc/Doc.autodoc index 4f2a156fb..3d9a32e85 100644 --- a/FpCategories/doc/Doc.autodoc +++ b/FpCategories/doc/Doc.autodoc @@ -1,18 +1,20 @@ @Chapter Quivers -@Section GAP categories @Section Constructors @Section Attributes +@Section GAP categories -@Chapter Path Categories +@Chapter Path categories -@Section GAP categories @Section Constructors @Section Attributes -@Section Operations -@Section Quotients of path categories +@Section GAP categories @Chapter Tools @Section Properties +@Section Attributes @Section Operations + +@Chapter Precompilation +@InsertChunk PrecompileCategoryFromNerveData diff --git a/Algebroids/examples/CategoryFromNerveData.g b/FpCategories/examples/CategoryFromNerveData.g similarity index 78% rename from Algebroids/examples/CategoryFromNerveData.g rename to FpCategories/examples/CategoryFromNerveData.g index 396f2ee27..37d27b2ef 100644 --- a/Algebroids/examples/CategoryFromNerveData.g +++ b/FpCategories/examples/CategoryFromNerveData.g @@ -4,13 +4,13 @@ LoadPackage( "Algebroids" ); #! true Delta1 := SimplicialCategoryTruncatedInDegree( 1 ); -#! FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] +#! PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] Size( Delta1 ); #! 7 C := CategoryFromNerveData( Delta1 ); -#! FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] +#! PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] Size( C ); #! 7 NerveTruncatedInDegree2Data( C ) = NerveTruncatedInDegree2Data( Delta1 ); @@ -18,11 +18,11 @@ NerveTruncatedInDegree2Data( C ) = NerveTruncatedInDegree2Data( Delta1 ); IndicesOfGeneratingMorphisms( C ); #! [ 1, 2, 3 ] SetOfGeneratingMorphisms( C ); -#! [ (C1)-[(id)]->(C0), (C0)-[(s)]->(C1), (C0)-[(t)]->(C1) ] +#! [ (C1)-[(id)]-≻(C0), (C0)-[(s)]-≻(C1), (C0)-[(t)]-≻(C1) ] Display( C ); #! A CAP category with name -#! FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ]: +#! PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ]: #! #! 19 primitive operations were used to derive 55 operations for this category #! which algorithmically @@ -41,29 +41,29 @@ IsWellDefined( C1 ); IsWellDefined( 2 / C ); #! false idC0 := CreateMorphism( C0, 0, C0 ); -#! (C0)-[(C0)]->(C0) +#! (C0)-[(C0)]-≻(C0) CreateMorphism( C, 0 ) = idC0; #! true IsOne( idC0 ); #! true id := CreateMorphism( C, 1 ); -#! (C1)-[(id)]->(C0) +#! (C1)-[(id)]-≻(C0) s := CreateMorphism( C, 2 ); -#! (C0)-[(s)]->(C1) +#! (C0)-[(s)]-≻(C1) t := CreateMorphism( C, 3 ); -#! (C0)-[(t)]->(C1) +#! (C0)-[(t)]-≻(C1) idC1 := CreateMorphism( C, 4 ); -#! (C1)-[(C1)]->(C1) +#! (C1)-[(C1)]-≻(C1) IsOne( idC1 ); #! true sigma := CreateMorphism( C, 5 ); -#! (C1)-[(id*s)]->(C1) +#! (C1)-[(id⋅s)]-≻(C1) IsEndomorphism( sigma ); #! true IsOne( sigma ); #! false tau := CreateMorphism( C, 6 ); -#! (C1)-[(id*t)]->(C1) +#! (C1)-[(id⋅t)]-≻(C1) IsEndomorphism( tau ); #! true IsOne( tau ); @@ -116,8 +116,8 @@ Display( HomStructure( idC1, idC1 ) ); #! { 0, 1, 2 } ⱶ[ 0, 1, 2 ]→ { 0, 1, 2 } C_op := OppositeCategoryFromNerveData( C ); #! Opposite( -#! FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] ) +#! PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] ) NerveData( C_op ) = NerveTruncatedInDegree2Data( C_op ); #! true IsIdenticalObj( OppositeCategoryFromNerveData( C_op ), C ); @@ -125,6 +125,6 @@ IsIdenticalObj( OppositeCategoryFromNerveData( C_op ), C ); IndicesOfGeneratingMorphisms( C_op ); #! [ 3, 1, 2 ] SetOfGeneratingMorphisms( C_op ); -#! [ (C0)-[(id)]->(C1), (C1)-[(s)]->(C0), (C1)-[(t)]->(C0) ] +#! [ (C0)-[(id)]-≻(C1), (C1)-[(s)]-≻(C0), (C1)-[(t)]-≻(C0) ] #! @EndExample #! @EndChunk diff --git a/FpCategories/examples/Delta2.g b/FpCategories/examples/Delta2.g new file mode 100644 index 000000000..59ca74685 --- /dev/null +++ b/FpCategories/examples/Delta2.g @@ -0,0 +1,39 @@ +#! @BeginChunk Delta2 + +#! The full subcategory of the simplicial category $\Delta$ on the objects $[0], [1], [2]$ + +#! @Example +LoadPackage( "Algebroids" ); +#! true +Delta2 := SimplicialCategoryTruncatedInDegree( 2 ); +#! PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] +DefiningRelations( Delta2 ); +#! [ [ s⋅id:(C0) -≻ (C0), id(C0):(C0) -≻ (C0) ], +#! [ t⋅id:(C0) -≻ (C0), id(C0):(C0) -≻ (C0) ], +#! [ ps⋅is:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ pt⋅it:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ is⋅id:(C2) -≻ (C0), it⋅id:(C2) -≻ (C0) ], +#! [ pt⋅is:(C1) -≻ (C1), id⋅t:(C1) -≻ (C1) ], +#! [ ps⋅it:(C1) -≻ (C1), id⋅s:(C1) -≻ (C1) ], +#! [ s⋅pt:(C0) -≻ (C2), t⋅ps:(C0) -≻ (C2) ], +#! [ s⋅mu:(C0) -≻ (C2), s⋅ps:(C0) -≻ (C2) ], +#! [ t⋅mu:(C0) -≻ (C2), t⋅pt:(C0) -≻ (C2) ], +#! [ mu⋅is:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ mu⋅it:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ] ] +Size( Delta2 ); +#! 31 +Delta2_op := OppositeFiniteCategory( Delta2 ); +#! Opposite( PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) / +#! [ s⋅id = id(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] ) +IsIdenticalObj( OppositeFiniteCategory( Delta2_op ), Delta2 ); +#! true +#! @EndExample + +#! @EndChunk diff --git a/FpCategories/examples/NerveTruncatedInDegree2AsFunctor.g b/FpCategories/examples/NerveTruncatedInDegree2AsFunctor.g new file mode 100644 index 000000000..dd8d2efe8 --- /dev/null +++ b/FpCategories/examples/NerveTruncatedInDegree2AsFunctor.g @@ -0,0 +1,70 @@ +#! @BeginChunk NerveTruncatedInDegree2AsFunctor + +#! We compute the nerve of the full subcategory of the simplicial category $\Delta$ on the objects $[0], [1], [2]$. + +#! @Example +LoadPackage( "FpCategories", false ); +#! true +Delta2 := SimplicialCategoryTruncatedInDegree( 2 ); +#! PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1,ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] +DefiningRelations( Delta2 ); +#! [ [ s⋅id:(C0) -≻ (C0), id(C0):(C0) -≻ (C0) ], +#! [ t⋅id:(C0) -≻ (C0), id(C0):(C0) -≻ (C0) ], +#! [ ps⋅is:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ pt⋅it:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ is⋅id:(C2) -≻ (C0), it⋅id:(C2) -≻ (C0) ], +#! [ pt⋅is:(C1) -≻ (C1), id⋅t:(C1) -≻ (C1) ], +#! [ ps⋅it:(C1) -≻ (C1), id⋅s:(C1) -≻ (C1) ], +#! [ s⋅pt:(C0) -≻ (C2), t⋅ps:(C0) -≻ (C2) ], +#! [ s⋅mu:(C0) -≻ (C2), s⋅ps:(C0) -≻ (C2) ], +#! [ t⋅mu:(C0) -≻ (C2), t⋅pt:(C0) -≻ (C2) ], +#! [ mu⋅is:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ mu⋅it:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ] ] +Size( Delta2 ); +#! 31 +N := NerveTruncatedInDegree2AsFunctor( Delta2 ); +#! Functor from PathCategory( FinQuiver( +#! "Delta_op(C0,C1,C2)[id:C0-≻C1,s:C1-≻C0,t:C1-≻C0, +#! is:C1-≻C2,it:C1-≻C2,ps:C2-≻C1,pt:C2-≻C1,mu:C2-≻C1]" ) ) +#! / [ id⋅s = id(C0), id⋅t = id(C0), is⋅ps = id(C1), ... ] -> SkeletalFinSets +Delta2op := SourceOfFunctor( N ); +#! PathCategory( FinQuiver( +#! "Delta_op(C0,C1,C2)[id:C0-≻C1,s:C1-≻C0,t:C1-≻C0, +#! is:C1-≻C2,it:C1-≻C2,ps:C2-≻C1,pt:C2-≻C1,mu:C2-≻C1]" ) ) +#! / [ id⋅s = id(C0), id⋅t = id(C0), is⋅ps = id(C1), ... ] +N( Delta2op.C0 ); +#! |3| +Display( N( Delta2op.C0 ) ); +#! { 0, 1, 2 } +N( Delta2op.C1 ); +#! |31| +Display( N( Delta2op.C1 ) ); +#! { 0,..., 30 } +N( Delta2op.C2 ); +#! |393| +Display( N( Delta2op.C2 ) ); +#! { 0,..., 392 } +N( Delta2op.id ); +#! |3| → |31| +Display( N( Delta2op.id ) ); +#! { 0, 1, 2 } ⱶ[ 0, 5, 21 ]→ { 0,..., 30 } +LoadPackage( "FunctorCategories", false ); +#! true +N := NerveTruncatedInDegree2( Delta2 ); +#! +IntCat := CategoryOfInternalCategories( + RangeCategoryOfHomomorphismStructure( Delta2 ) ); +#! FullSubcategoryByObjectMembershipFunction( +#! PreSheaves( PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1,ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ], SkeletalFinSets ), +#! ObjectMembershipFunction ) +#! @EndExample +#! @EndChunk diff --git a/FpCategories/examples/PathCategory.g b/FpCategories/examples/PathCategory.g index a84ba72e6..a6e2e2656 100644 --- a/FpCategories/examples/PathCategory.g +++ b/FpCategories/examples/PathCategory.g @@ -32,7 +32,7 @@ Display( C ); #! #! 17 primitive operations were used to derive 32 operations for this category #! which algorithmically -#! * IsObjectFiniteCategory +#! * IsFinitelyPresentedCategory SetOfObjects( C ); #! [ (0), (1), (2), (3), (4), (5) ] SetOfGeneratingMorphisms( C ); diff --git a/Algebroids/examples/PrecompileCategoryFromNerveData.g b/FpCategories/examples/PrecompileCategoryFromNerveData.g similarity index 83% rename from Algebroids/examples/PrecompileCategoryFromNerveData.g rename to FpCategories/examples/PrecompileCategoryFromNerveData.g index b090f9eaa..fca277913 100644 --- a/Algebroids/examples/PrecompileCategoryFromNerveData.g +++ b/FpCategories/examples/PrecompileCategoryFromNerveData.g @@ -15,9 +15,9 @@ ReadPackageOnce( "FinSetsForCAP", "gap/CompilerLogic.gi" ); category_constructor := function( quiver ) - local sFinSets; sFinSets := SkeletalCategoryOfFiniteSets( : FinalizeCategory := true ); return CategoryFromNerveData( FreeCategory( quiver : range_of_HomStructure := sFinSets, FinalizeCategory := true ) ); end;; + local sFinSets; sFinSets := SkeletalCategoryOfFiniteSets( : FinalizeCategory := true ); return CategoryFromNerveData( PathCategory( quiver : range_of_HomStructure := sFinSets, FinalizeCategory := true ) ); end;; -given_arguments := [ RightQuiver( "q(a,b)[m:a->b]" ) ];; +given_arguments := [ FinQuiver( "q(a,b)[m:a->b]" ) ];; compiled_category_name := "CategoryFromNerveDataPrecompiled";; package_name := "Algebroids";; @@ -30,9 +30,9 @@ CapJitPrecompileCategoryAndCompareResult( [ "HomomorphismStructureOnMorphismsWithGivenObjects" ] ) );; CategoryFromNerveDataPrecompiled( given_arguments[1] ); -#! FreeCategory( RightQuiver( "q(a,b)[m:a->b]" ) ) +#! PathCategory( FinQuiver( "q(a,b)[m:a-≻b]" ) ) -CategoryFromNerveData( FreeCategory( given_arguments[1] ) )!.precompiled_functions_added; +CategoryFromNerveData( PathCategory( given_arguments[1] ) )!.precompiled_functions_added; #! true #! #@fi diff --git a/Algebroids/examples/PrecompileCategoryFromNerveDataHomStructureOnMorphisms.g b/FpCategories/examples/PrecompileCategoryFromNerveDataHomStructureOnMorphisms.g similarity index 81% rename from Algebroids/examples/PrecompileCategoryFromNerveDataHomStructureOnMorphisms.g rename to FpCategories/examples/PrecompileCategoryFromNerveDataHomStructureOnMorphisms.g index b04a678be..2b4b44303 100644 --- a/Algebroids/examples/PrecompileCategoryFromNerveDataHomStructureOnMorphisms.g +++ b/FpCategories/examples/PrecompileCategoryFromNerveDataHomStructureOnMorphisms.g @@ -15,9 +15,9 @@ ReadPackageOnce( "FinSetsForCAP", "gap/CompilerLogic.gi" ); category_constructor := function( quiver ) - local sFinSets; sFinSets := SkeletalCategoryOfFiniteSets( : FinalizeCategory := true ); return CategoryFromNerveData( FreeCategory( quiver : range_of_HomStructure := sFinSets, FinalizeCategory := true ) ); end;; + local sFinSets; sFinSets := SkeletalCategoryOfFiniteSets( : FinalizeCategory := true ); return CategoryFromNerveData( PathCategory( quiver : range_of_HomStructure := sFinSets, FinalizeCategory := true ) ); end;; -given_arguments := [ RightQuiver( "q(a,b)[m:a->b]" ) ];; +given_arguments := [ FinQuiver( "q(a,b)[m:a->b]" ) ];; compiled_category_name := "CategoryFromNerveDataHomStructureOnMorphismsPrecompiled";; package_name := "Algebroids";; @@ -30,9 +30,9 @@ CapJitPrecompileCategoryAndCompareResult( );; CategoryFromNerveDataHomStructureOnMorphismsPrecompiled( given_arguments[1] ); -#! FreeCategory( RightQuiver( "q(a,b)[m:a->b]" ) ) +#! PathCategory( FinQuiver( "q(a,b)[m:a->b]" ) ) -CategoryFromNerveData( FreeCategory( given_arguments[1] ) )!.precompiled_functions_added; +CategoryFromNerveData( PathCategory( given_arguments[1] ) )!.precompiled_functions_added; #! true #! #@fi diff --git a/FpCategories/examples/YonedaCompositionAsNaturalEpimorphism.g b/FpCategories/examples/YonedaCompositionAsNaturalEpimorphism.g new file mode 100644 index 000000000..111560c16 --- /dev/null +++ b/FpCategories/examples/YonedaCompositionAsNaturalEpimorphism.g @@ -0,0 +1,70 @@ +#! @BeginChunk YonedaCompositionAsNaturalEpimorphism + +LoadPackage( "Algebroids" ); + +#! We compute the Yoneda composition natural epimorphism of the full subcategory +#! of the simplicial category $\Delta$ on the objects $[0], [1], [2]$. + +#! @Example +Delta2 := SimplicialCategoryTruncatedInDegree( 2 ); +#! PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] +DefiningRelations( Delta2 ); +#! [ [ s⋅id:(C0) -≻ (C0), id(C0):(C0) -≻ (C0) ], +#! [ t⋅id:(C0) -≻ (C0), id(C0):(C0) -≻ (C0) ], +#! [ ps⋅is:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ pt⋅it:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ is⋅id:(C2) -≻ (C0), it⋅id:(C2) -≻ (C0) ], +#! [ pt⋅is:(C1) -≻ (C1), id⋅t:(C1) -≻ (C1) ], +#! [ ps⋅it:(C1) -≻ (C1), id⋅s:(C1) -≻ (C1) ], +#! [ s⋅pt:(C0) -≻ (C2), t⋅ps:(C0) -≻ (C2) ], +#! [ s⋅mu:(C0) -≻ (C2), s⋅ps:(C0) -≻ (C2) ], +#! [ t⋅mu:(C0) -≻ (C2), t⋅pt:(C0) -≻ (C2) ], +#! [ mu⋅is:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ mu⋅it:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ] ] +Size( Delta2 ); +#! 31 +Ymu := YonedaCompositionAsNaturalEpimorphism( Delta2 ); +#! Natural transformation from +#! Functor from PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = i d(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] -> SkeletalFinSets +#! -> +#! Functor from PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = i d(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] -> SkeletalFinSets +Ymu := YonedaProjectionAsNaturalEpimorphism( Delta2 ); +#! Natural transformation from +#! Functor from PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = i d(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] -> SkeletalFinSets +#! -> +#! Functor from PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = i d(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] -> SkeletalFinSets +Ys := YonedaFibrationAsNaturalTransformation( Delta2 ); +#! Natural transformation from +#! Functor from PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = i d(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] -> SkeletalFinSets +#! -> +#! Functor from PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = i d(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] -> SkeletalFinSets +#! @EndExample +#! @EndChunk diff --git a/Algebroids/gap/CategoryFromNerveData.gd b/FpCategories/gap/CategoryFromNerveData.gd similarity index 97% rename from Algebroids/gap/CategoryFromNerveData.gd rename to FpCategories/gap/CategoryFromNerveData.gd index 5e895e4d5..f25f501f1 100644 --- a/Algebroids/gap/CategoryFromNerveData.gd +++ b/FpCategories/gap/CategoryFromNerveData.gd @@ -1,5 +1,5 @@ # SPDX-License-Identifier: GPL-2.0-or-later -# Algebroids: Algebroids and bialgebroids as preadditive categories generated by enhanced quivers +# FpCategories: Finitely presented categories by generating quivers and relations # # Declarations # @@ -159,6 +159,9 @@ DeclareAttribute( "OppositeNerveData", DeclareAttribute( "OppositeCategoryFromNerveData", IsCategoryFromNerveData ); +DeclareAttribute( "DecompositionIndicesOfAllMorphismsFromHomStructure", + IsCapCategory ); + #################################### # #! @Section Constructors @@ -181,10 +184,6 @@ DeclareAttribute( "CategoryFromNerveData", IsRecord ); #! @InsertChunk CategoryFromNerveData -#! @Arguments C -DeclareAttribute( "CategoryFromNerveData", - IsFpCategory ); - if false then #! @Arguments C DeclareAttribute( "CategoryFromNerveData", diff --git a/Algebroids/gap/CategoryFromNerveData.gi b/FpCategories/gap/CategoryFromNerveData.gi similarity index 94% rename from Algebroids/gap/CategoryFromNerveData.gi rename to FpCategories/gap/CategoryFromNerveData.gi index 85cef62a7..55bcd87aa 100644 --- a/Algebroids/gap/CategoryFromNerveData.gi +++ b/FpCategories/gap/CategoryFromNerveData.gi @@ -1,5 +1,5 @@ # SPDX-License-Identifier: GPL-2.0-or-later -# Algebroids: Algebroids and bialgebroids as preadditive categories generated by enhanced quivers +# FpCategories: Finitely presented categories by generating quivers and relations # # Implementations # @@ -545,42 +545,6 @@ InstallMethod( CategoryFromNerveData, end ); -## -InstallMethod( CategoryFromNerveData, - "for a f.p. category", - [ IsFpCategory ], - - function( C ) - - return CategoryFromNerveData( - rec( name := Name( C ), - nerve_data := NerveTruncatedInDegree2Data( C ), - indices_of_generating_morphisms := IndicesOfGeneratingMorphismsFromHomStructure( C ), - decomposition_of_all_morphisms := DecompositionIndicesOfAllMorphismsFromHomStructure( C ), - relations := RelationsAmongGeneratingMorphisms( C ), - labels := [ List( SetOfObjects( C ), Label ), List( SetOfGeneratingMorphisms( C ), Label ) ], - properties := ListKnownCategoricalProperties( C ) ) ); - -end ); - -## -InstallOtherMethod( CategoryFromNerveData, - "for a category from data tables", - [ IsCategoryFromDataTables ], - - function( C ) - - return CategoryFromNerveData( - rec( name := Name( C ), - nerve_data := NerveTruncatedInDegree2Data( C ), - indices_of_generating_morphisms := IndicesOfGeneratingMorphismsFromHomStructure( C ), - decomposition_of_all_morphisms := DecompositionIndicesOfAllMorphisms( C ), - relations := RelationsAmongGeneratingMorphisms( C ), - labels := C!.labels, - properties := ListKnownCategoricalProperties( C ) ) ); - -end ); - ## InstallMethodForCompilerForCAP( SetOfObjects, "for a category from nerve data", @@ -1027,13 +991,13 @@ InstallMethod( ViewString, else pos := JoinStringsWithSeparator( List( DecompositionIndicesOfAllMorphisms( C )[1+t, 1+s][1 + HomStructure( mor )(0)], i -> labels[2][1 + i] ), - "*" ); + "⋅" ); fi; fi; return Concatenation( "(", labels[1][1 + s], ")", - "-[(", pos, ")]->", + "-[(", pos, ")]-≻", "(", labels[1][1 + t], ")" ); end ); diff --git a/FpCategories/gap/PathCategories.gd b/FpCategories/gap/PathCategories.gd index 720aa08a8..f80b35782 100644 --- a/FpCategories/gap/PathCategories.gd +++ b/FpCategories/gap/PathCategories.gd @@ -83,6 +83,15 @@ DeclareOperation( "AssignSetOfGeneratingMorphisms", [ IsPathCategory, IsString ] # #################################### +#! @Description +#! Returns the opposite category of the path category C. +#! @Arguments C +#! @Returns a path category +DeclareAttribute( "OppositePathCategory", IsPathCategory ); + +#! @Arguments C +DeclareAttribute( "CategoryFromNerveData", IsPathCategory ); + #! @Description #! Returns the defining quiver of the path category C. #! @Arguments C @@ -140,6 +149,12 @@ CapJitAddTypeSignature( "MorphismIndices", [ IsPathCategoryMorphism ], CapJitDat #! @Returns a positive integer DeclareAttribute( "MorphismLabel", IsPathCategoryMorphism ); +DeclareAttribute( "DecompositionIndicesOfMorphism", + IsPathCategoryMorphism ); + +DeclareAttribute( "DecompositionOfMorphismInCategory", + IsPathCategoryMorphism ); + #! @Description #! Returns whether C can be enriched over the category of finite sets. #! @Arguments C @@ -167,6 +182,9 @@ KeyDependentOperation( "ExternalHomsWithGivenLengthData", IsPathCategory, IsInt, KeyDependentOperation( "ExternalHomsWithGivenLength", IsCapCategory, IsInt, ReturnTrue ); DeclareAttribute( "ExternalHoms", IsPathCategory ); +DeclareAttribute( "RelationsAmongGeneratingMorphisms", + IsPathCategory ); + #################################### # #! @Section Operations diff --git a/FpCategories/gap/PathCategories.gi b/FpCategories/gap/PathCategories.gi index 81dc625c8..8f14686ce 100644 --- a/FpCategories/gap/PathCategories.gi +++ b/FpCategories/gap/PathCategories.gi @@ -9,7 +9,7 @@ InstallMethod( PathCategory, [ IsFinQuiver ], function ( q ) - local admissible_order, name, C; + local admissible_order, name, C, range_of_HomStructure; admissible_order := ValueOption( "admissible_order" ); @@ -42,7 +42,7 @@ InstallMethod( PathCategory, C!.admissible_order := admissible_order; - SetIsObjectFiniteCategory( C, true ); + SetIsFinitelyPresentedCategory( C, true ); SetUnderlyingQuiver( C, q ); @@ -266,7 +266,15 @@ InstallMethod( PathCategory, SetIsFiniteCategory( C, true ); - SET_RANGE_CATEGORY_Of_HOMOMORPHISM_STRUCTURE( C, SkeletalFinSets ); + range_of_HomStructure := ValueOption( "range_of_HomStructure" ); + + if not IsSkeletalCategoryOfFiniteSets( range_of_HomStructure ) then + range_of_HomStructure := SkeletalFinSets; + fi; + + SET_RANGE_CATEGORY_Of_HOMOMORPHISM_STRUCTURE( C, range_of_HomStructure ); + + Assert( 0, IsIdenticalObj( RangeCategoryOfHomomorphismStructure( C ), range_of_HomStructure ) ); AddMorphismsOfExternalHom( C, function ( C, obj_1, obj_2 ) @@ -309,6 +317,37 @@ InstallMethodForCompilerForCAP( SetOfGeneratingMorphisms, end ); +## +InstallOtherMethod( DecompositionIndicesOfMorphism, + "for a path category and a morphism therein", + [ IsPathCategory, IsPathCategoryMorphism ], + + function( C, mor ) + + return -1 + MorphismDatum( C, mor )[2]; + +end ); + +## +InstallMethod( DecompositionOfMorphismInCategory, + "for a morphism in a path category", + [ IsPathCategoryMorphism ], + + function( mor ) + local C, dec; + + C := CapCategory( mor ); + + dec := SetOfGeneratingMorphisms( C ){1 + DecompositionIndicesOfMorphism( C, mor )}; + + if ForAny( dec, IsEqualToIdentityMorphism ) then + Error( "one of the generating morphisms is an identity morphism\n" ); + fi; + + return dec; + +end ); + ## InstallMethod( ExternalHomsWithGivenLengthDataOp, [ IsPathCategory, IsInt ], @@ -756,6 +795,56 @@ InstallMethod( \., end ); +## +InstallMethod( OppositePathCategory, + "for a path category", + [ IsPathCategory ], + + function( C ) + local quiver_op, range_category, C_op; + + quiver_op := OppositeQuiver( UnderlyingQuiver( C ) ); + + if HasRangeCategoryOfHomomorphismStructure( C ) then + C_op := PathCategory( quiver_op : range_of_HomStructure := RangeCategoryOfHomomorphismStructure( C ) ); + else + C_op := PathCategory( quiver_op ); + fi; + + SetOppositePathCategory( C_op, C ); + + return C_op; + +end ); + +## +InstallOtherMethod( CapFunctor, + "for a path category, two lists, and a category", + [ IsPathCategory, IsList, IsList, IsCapCategory ], + + function( C, imgs_of_objs, imgs_of_gmors, D ) + local F; + + F := CapFunctor( Concatenation( "Functor from ", Name( C ), " -> ", Name( D ) ), C, D ); + + AddObjectFunction( F, + function ( obj ) + + return imgs_of_objs[ObjectIndex( obj )]; + + end ); + + AddMorphismFunction( F, + function ( F_s, mor, F_t ) + + return PreComposeList( D, F_s, imgs_of_gmors{MorphismIndices( mor )}, F_t ); + + end ); + + return F; + +end ); + ################### # # Orders @@ -1173,6 +1262,62 @@ InstallMethodForCompilerForCAP( ExtendFunctorToFpCategoryData, end ); +## +InstallMethod( DecompositionIndicesOfAllMorphismsFromHomStructure, + "for a path category", + [ IsPathCategory and IsFinite ], + + function( C ) + local objs; + + objs := SetOfObjects( C ); + + return List( objs, t -> + List( objs, s -> + List( MorphismsOfExternalHom( C, s, t ), mor -> List( MorphismIndices( mor ), i -> -1 + i ) ) ) ); + +end ); + +## +InstallMethod( RelationsAmongGeneratingMorphisms, + "for a path category", + [ IsPathCategory ], + + function( C ) + + return [ ]; + +end ); + +## +InstallMethod( CategoryFromNerveData, + "for a path category", + [ IsPathCategory and IsFinite ], + + function( C ) + + return CategoryFromNerveData( + rec( name := Name( C ), + nerve_data := NerveTruncatedInDegree2Data( C ), + indices_of_generating_morphisms := IndicesOfGeneratingMorphismsFromHomStructure( C ), + decomposition_of_all_morphisms := DecompositionIndicesOfAllMorphismsFromHomStructure( C ), + relations := RelationsAmongGeneratingMorphisms( C ), + labels := [ List( SetOfObjects( C ), ObjectLabel ), List( SetOfGeneratingMorphisms( C ), MorphismLabel ) ], + properties := ListKnownCategoricalProperties( C ) ) ); + +end ); + +## +InstallMethod( DataTablesOfCategory, + "for a path category", + [ IsPathCategory ], + + function( C ) + + return DataTablesOfCategory( CategoryFromNerveData( C : FinalizeCategory := true ) ); + +end ); + ################### # # View Methods diff --git a/FpCategories/gap/QuotientsOfPathCategories.gd b/FpCategories/gap/QuotientsOfPathCategories.gd index 2f657587f..6c234f9ae 100644 --- a/FpCategories/gap/QuotientsOfPathCategories.gd +++ b/FpCategories/gap/QuotientsOfPathCategories.gd @@ -4,11 +4,11 @@ # Declarations # -#! @Chapter Path Categories +#! @Chapter Path categories #################################### # -#! @Section Quotients of path categories +#! @Section GAP categories # #################################### @@ -27,13 +27,20 @@ DeclareCategory( "IsQuotientOfPathCategoryObject", DeclareCategory( "IsQuotientOfPathCategoryMorphism", IsQuotientCapCategoryMorphism ); -if false then +#################################### +# +#! @Section Attributes +# +#################################### + #! @Description -#! Returns the quotient category of C by the two-sided ideal of morphisms generated by rels. -#! @Arguments C, rels -#! @Returns a &CAP; category -DeclareOperation( "QuotientCategory", [ IsPathCategory, IsDenseList ] ); -fi; +#! Returns the opposite category of a quotient qC of a path category $C$. +#! @Arguments qC +#! @Returns a quotient of a path category +DeclareAttribute( "OppositeQuotientOfPathCategory", IsQuotientOfPathCategory ); + +#! @Arguments C +DeclareAttribute( "CategoryFromNerveData", IsQuotientOfPathCategory ); #! @Description #! Returns the generators of the underlying two-sided ideal of morphisms. @@ -41,6 +48,9 @@ fi; #! @Returns a dense list DeclareAttribute( "DefiningRelations", IsQuotientOfPathCategory ); +DeclareAttribute( "RelationsAmongGeneratingMorphisms", + IsQuotientOfPathCategory ); + #! @Description #! Returns the reduced Groebner basis of the underlying two-sided ideal of morphisms. #! @Arguments qC @@ -61,5 +71,24 @@ DeclareAttribute( "ObjectIndex", IsQuotientOfPathCategoryObject ); #! @Returns a &CAP; morphism DeclareAttribute( "CanonicalRepresentative", IsQuotientOfPathCategoryMorphism ); -#! @InsertChunk PathCategories +DeclareAttribute( "DecompositionIndicesOfMorphism", + IsQuotientOfPathCategoryMorphism ); +DeclareAttribute( "DecompositionOfMorphismInCategory", + IsQuotientOfPathCategoryMorphism ); + +#################################### +# +#! @Section Constructors +# +#################################### + +if false then +#! @Description +#! Returns the quotient category of C by the two-sided ideal of morphisms generated by rels. +#! @Arguments C, rels +#! @Returns a &CAP; category +DeclareOperation( "QuotientCategory", [ IsPathCategory, IsDenseList ] ); +fi; + +#! @InsertChunk PathCategories diff --git a/FpCategories/gap/QuotientsOfPathCategories.gi b/FpCategories/gap/QuotientsOfPathCategories.gi index 269583231..61b46f0c8 100644 --- a/FpCategories/gap/QuotientsOfPathCategories.gi +++ b/FpCategories/gap/QuotientsOfPathCategories.gi @@ -9,7 +9,7 @@ InstallOtherMethod( QuotientCategory, [ IsPathCategory, IsDenseList ], function ( C, relations ) - local reduced_gb, congruence_function, name, quo_C, q, leading_monomials, hom_quo_C; + local reduced_gb, congruence_function, name, quo_C, q, leading_monomials, hom_quo_C, range_of_HomStructure; reduced_gb := ReducedGroebnerBasis( C, relations ); @@ -36,6 +36,8 @@ InstallOtherMethod( QuotientCategory, congruence_function := congruence_function, underlying_category := C ) : FinalizeCategory := false, overhead := false ); + SetIsFinitelyPresentedCategory( quo_C, true ); + ## AddSetOfGeneratingMorphismsOfCategory( quo_C, function( quo_C ) @@ -78,7 +80,15 @@ InstallOtherMethod( QuotientCategory, m, SetOfObjects( quo_C )[t] ) ) ) ) ); - SET_RANGE_CATEGORY_Of_HOMOMORPHISM_STRUCTURE( quo_C, SkeletalFinSets ); + range_of_HomStructure := ValueOption( "range_of_HomStructure" ); + + if not IsSkeletalCategoryOfFiniteSets( range_of_HomStructure ) then + range_of_HomStructure := SkeletalFinSets; + fi; + + SET_RANGE_CATEGORY_Of_HOMOMORPHISM_STRUCTURE( quo_C, range_of_HomStructure ); + + Assert( 0, IsIdenticalObj( RangeCategoryOfHomomorphismStructure( quo_C ), range_of_HomStructure ) ); ## AddMorphismsOfExternalHom( quo_C, @@ -156,6 +166,192 @@ InstallMethod( ExternalHomsWithGivenLengthOp, end ); +## +InstallMethod( OppositeQuotientOfPathCategory, + "for a quotient of a path category", + [ IsQuotientOfPathCategory ], + + function( quo_C ) + local C, C_op, relations_op, quo_C_op; + + C := UnderlyingCategory( quo_C ); + + C_op := OppositePathCategory( C ); + + relations_op := List( DefiningRelations( quo_C ), pair -> + Pair( MorphismConstructor( C_op, + SetOfObjects( C_op )[ObjectIndex( Target( pair[1] ) )], + Pair( MorphismLength( pair[1] ), Reversed( MorphismIndices( pair[1] ) ) ), + SetOfObjects( C_op )[ObjectIndex( Source( pair[1] ) )] ), + MorphismConstructor( C_op, + SetOfObjects( C_op )[ObjectIndex( Target( pair[2] ) )], + Pair( MorphismLength( pair[2] ), Reversed( MorphismIndices( pair[2] ) ) ), + SetOfObjects( C_op )[ObjectIndex( Source( pair[2] ) )] ) ) ); + + quo_C_op := QuotientCategory( C_op, relations_op ); + + SetOppositeQuotientOfPathCategory( quo_C_op, quo_C ); + + return quo_C_op; + +end ); + +## +InstallOtherMethod( CapFunctor, + "for a quotient of a path category, two lists, and a category", + [ IsQuotientOfPathCategory, IsList, IsList, IsCapCategory ], + + function( C, imgs_of_objs, imgs_of_gmors, D ) + local F; + + F := CapFunctor( Concatenation( "Functor from ", Name( C ), " -> ", Name( D ) ), C, D ); + + AddObjectFunction( F, + function ( obj ) + + return imgs_of_objs[ObjectIndex( ObjectDatum( obj ) )]; + + end ); + + AddMorphismFunction( F, + function ( F_s, mor, F_t ) + + return PreComposeList( D, F_s, imgs_of_gmors{MorphismIndices( MorphismDatum( mor ) )}, F_t ); + + end ); + + return F; + +end ); + +## +InstallOtherMethod( CapFunctor, + "for a quotient of a path category, two records, and a category", + [ IsQuotientOfPathCategory, IsRecord, IsRecord, IsCapCategory ], + + function( C, imgs_of_objs, imgs_of_gmors, D ) + local F; + + F := CapFunctor( Concatenation( "Functor from ", Name( C ), " -> ", Name( D ) ), C, D ); + + AddObjectFunction( F, + function ( obj ) + + return imgs_of_objs.(ObjectLabel( ObjectDatum( obj ) )); + + end ); + + AddMorphismFunction( F, + function ( F_s, mor, F_t ) + + return PreComposeList( D, + F_s, + List( MorphismSupport( MorphismDatum( mor ) ), m -> + imgs_of_gmors.(MorphismLabel( m )) ), + F_t ); + + end ); + + return F; + +end ); + +## +InstallOtherMethod( DecompositionIndicesOfMorphism, + "for a quotient of a path category and a morphism therein", + [ IsQuotientOfPathCategory, IsQuotientOfPathCategoryMorphism ], + + function( C, mor ) + + return DecompositionIndicesOfMorphism( UnderlyingCategory( C ), MorphismDatum( C, mor ) ); + +end ); + +## +InstallMethod( DecompositionOfMorphismInCategory, + "for a morphism in a quotient of a path category", + [ IsQuotientOfPathCategoryMorphism ], + + function( mor ) + local C, dec; + + C := CapCategory( mor ); + + dec := SetOfGeneratingMorphisms( C ){1 + DecompositionIndicesOfMorphism( C, mor )}; + + if ForAny( dec, IsEqualToIdentityMorphism ) then + Error( "one of the generating morphisms is an identity morphism\n" ); + fi; + + return dec; + +end ); + +## +InstallMethod( DecompositionIndicesOfAllMorphismsFromHomStructure, + "for a quotient of a path category", + [ IsQuotientOfPathCategory and IsFinite ], + + function( C ) + local objs; + + objs := SetOfObjects( C ); + + return List( objs, t -> + List( objs, s -> + List( MorphismsOfExternalHom( C, s, t ), mor -> List( MorphismIndices( CanonicalRepresentative( mor ) ), i -> -1 + i ) ) ) ); + +end ); + +## +InstallMethod( RelationsAmongGeneratingMorphisms, + "for a quotient of a path category", + [ IsQuotientOfPathCategory ], + + function( C ) + + return List( DefiningRelations( C ), pair -> + Pair( List( MorphismIndices( pair[1] ), i -> -1 + i ), + List( MorphismIndices( pair[2] ), i -> -1 + i ) ) ); + +end ); + +## +InstallMethod( CategoryFromNerveData, + "for a quotient of a path category", + [ IsQuotientOfPathCategory and IsFinite ], + + function( C ) + + return CategoryFromNerveData( + rec( name := Name( C ), + nerve_data := NerveTruncatedInDegree2Data( C ), + indices_of_generating_morphisms := IndicesOfGeneratingMorphismsFromHomStructure( C ), + decomposition_of_all_morphisms := DecompositionIndicesOfAllMorphismsFromHomStructure( C ), + relations := RelationsAmongGeneratingMorphisms( C ), + labels := [ List( SetOfObjects( C ), o -> ObjectLabel( UnderlyingCell( o ) ) ), + List( SetOfGeneratingMorphisms( C ), m -> MorphismLabel( CanonicalRepresentative( m ) ) ) ], + properties := ListKnownCategoricalProperties( C ) ) ); + +end ); + +## +InstallMethod( DataTablesOfCategory, + "for a quotient of a path category", + [ IsQuotientOfPathCategory ], + + function( C ) + + return DataTablesOfCategory( CategoryFromNerveData( C : FinalizeCategory := true ) ); + +end ); + +################### +# +# View Methods +# +################### + ## InstallMethod( DisplayString, [ IsQuotientOfPathCategoryObject ], diff --git a/Algebroids/gap/SimplicialCategory.gd b/FpCategories/gap/SimplicialCategory.gd similarity index 81% rename from Algebroids/gap/SimplicialCategory.gd rename to FpCategories/gap/SimplicialCategory.gd index 69b9843c7..ac8b547bd 100644 --- a/Algebroids/gap/SimplicialCategory.gd +++ b/FpCategories/gap/SimplicialCategory.gd @@ -1,5 +1,5 @@ # SPDX-License-Identifier: GPL-2.0-or-later -# Algebroids: Algebroids and bialgebroids as preadditive categories generated by enhanced quivers +# FpCategories: Finitely presented categories by generating quivers and relations # # Declarations # @@ -17,3 +17,4 @@ #! @Arguments n #! @Returns a &CAP; category DeclareGlobalFunction( "SimplicialCategoryTruncatedInDegree" ); +#! @InsertChunk Delta2 diff --git a/FpCategories/gap/SimplicialCategory.gi b/FpCategories/gap/SimplicialCategory.gi new file mode 100644 index 000000000..3a8ae32c3 --- /dev/null +++ b/FpCategories/gap/SimplicialCategory.gi @@ -0,0 +1,59 @@ +# SPDX-License-Identifier: GPL-2.0-or-later +# FpCategories: Finitely presented categories by generating quivers and relations +# +# Implementations +# + +#################################### +# +# global variables: +# +#################################### + +## +InstallGlobalFunction( SimplicialCategoryTruncatedInDegree, + function( n ) + local F, Delta; + + if n = 0 then + + F := PathCategory( FinQuiver( "Delta(C0)[]" ) ); + Delta := F; + + elif n = 1 then + + F := PathCategory( FinQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ); + Delta := F / + [ [ PreCompose( F.s, F.id ), IdentityMorphism( F.C0 ) ], + [ PreCompose( F.t, F.id ), IdentityMorphism( F.C0 ) ] ]; + + elif n = 2 then + + F := PathCategory( FinQuiver( "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1,is:C2->C1,it:C2->C1,ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ); + Delta := F / + [ [ PreCompose( F.s, F.id ), IdentityMorphism( F.C0 ) ], + [ PreCompose( F.t, F.id ), IdentityMorphism( F.C0 ) ], + [ PreCompose( F.ps, F.is ), IdentityMorphism( F.C1 ) ], + [ PreCompose( F.pt, F.it ), IdentityMorphism( F.C1 ) ], + [ PreCompose( F.is, F.id ), PreCompose( F.it, F.id ) ], ## s(1_M) = M = t(1_M) + [ PreCompose( F.pt, F.is ), PreCompose( F.id, F.t ) ], + [ PreCompose( F.ps, F.it ), PreCompose( F.id, F.s ) ], + [ PreCompose( F.s, F.pt ), PreCompose( F.t, F.ps ) ], + [ PreCompose( F.s, F.mu ), PreCompose( F.s, F.ps ) ], + [ PreCompose( F.t, F.mu ), PreCompose( F.t, F.pt ) ], + [ PreCompose( F.mu, F.is ), IdentityMorphism( F.C1 ) ], + [ PreCompose( F.mu, F.it ), IdentityMorphism( F.C1 ) ] ]; + + else + + Error( "the case n > 2 is not implemented yet\n" ); + + fi; + + return Delta; + +end ); + +## +BindGlobal( "SimplicialCategoryTruncatedInDegree2", + SimplicialCategoryTruncatedInDegree( 2 ) ); diff --git a/FpCategories/gap/Tools.gd b/FpCategories/gap/Tools.gd index a5fb22f2e..23d4969bc 100644 --- a/FpCategories/gap/Tools.gd +++ b/FpCategories/gap/Tools.gd @@ -62,6 +62,21 @@ CapJitAddTypeSignature( "SetOfGeneratingMorphismsAsUnresolvableAttribute", [ IsC end ); +#################################### +# +#! @Section Attributes +# +#################################### + +if false then +#! @Description +#! Return the number of morphisms in the finite category C. +#! @Arguments C +#! @Returns a nonnegative integer +DeclareAttribute( "Size", + IsCapCategory ); +fi; + #################################### # #! @Section Operations @@ -95,6 +110,92 @@ end ); DeclareAttribute( "DataTablesOfCategory", IsCapCategory ); +#! @Description +#! The nerve data of the category C. +#! @Arguments C +#! @Returns a pair consisting of a triple and an 8-tuple +DeclareAttribute( "NerveTruncatedInDegree2Data", + IsCapCategory ); + +#! @Description +#! The input is a finitely presented category C equipped with a homomorphism structure +#! with values in the skeletal category SkeletalFinSets of finite sets. +#! The output is the nerve of B truncated in degree $2$, +#! as a presheaf on SimplicialCategoryTruncatedInDegree($2$) +#! with values in SkeletalFinSets. +#! @Arguments C +#! @Returns a &CAP; functor +DeclareAttribute( "NerveTruncatedInDegree2AsFunctor", + IsCapCategory ); +#! @InsertChunk NerveTruncatedInDegree2AsFunctor + +#! @Description +#! The normalized indices of the generating morphisms of the finite category C. +#! @Arguments C +#! @Returns a list of integers +DeclareAttribute( "IndicesOfGeneratingMorphismsFromHomStructure", + IsCapCategory ); + +#! @Description +#! The opposite category of a finite category C. +#! @Arguments C +#! @Returns a &CAP; category +DeclareAttribute( "OppositeFiniteCategory", + IsCapCategory ); + +DeclareAttribute( "YonedaNaturalEpimorphisms", + IsCapCategory ); + +#! @Description +#! The input is a finitely presented category B. The output is a natural morphism. +#! Its source is the functor $B \to H, c \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,c), +#! \psi \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,\psi)$. +#! Its targe is the constant functor of $0$-cells +#! $B \to H, c \mapsto B_0, \psi \mapsto \mathrm{id}_{B_0}$. +#! @Arguments B +#! @Returns a &CAP; natural transformation +DeclareAttribute( "YonedaFibrationAsNaturalTransformation", IsCapCategory ); + +#! @Description +#! The input is a finitely presented category B. The output is a natural epimorphism. +#! Its source is the functor +#! $B \to H, c \mapsto \sqcup_{a,b\in B} \mathrm{Hom}(a,b) \times \mathrm{Hom}(b,c), +#! \psi \mapsto \sqcup_{a,b\in B} \mathrm{Hom}(1_a,1_b) \times \mathrm{Hom}(b,\psi)$. +#! Its target is the functor $B \to H, c \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,c), +#! \psi \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,\psi)$. +#! @Arguments B +#! @Returns a &CAP; natural transformation +DeclareAttribute( "YonedaProjectionAsNaturalEpimorphism", IsCapCategory ); + +#! @Description +#! The input is a finitely presented category B. The output is a natural epimorphism. +#! Its source is the functor +#! $B \to H, c \mapsto \sqcup_{a,b\in B} \mathrm{Hom}(a,b) \times \mathrm{Hom}(b,c), +#! \psi \mapsto \sqcup_{a,b\in B} \mathrm{Hom}(1_a,1_b) \times \mathrm{Hom}(b,\psi)$. +#! Its target is the functor $B \to H, c \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,c), +#! \psi \mapsto \sqcup_{a\in B} \mathrm{Hom}(a,\psi)$. +#! @Arguments B +#! @Returns a &CAP; natural transformation +DeclareAttribute( "YonedaCompositionAsNaturalEpimorphism", IsCapCategory ); +#! @InsertChunk YonedaCompositionAsNaturalEpimorphism + +DeclareAttribute( "TruthMorphismOfTrueToSieveFunctorAndEmbedding", + IsCapCategory ); + +#! @Description +#! Construct, using the record (or list) of images eta, a natural transformation +#! from the functor F to the parallel functor G. +#! @Arguments eta, F, G +#! @Returns a &CAP; natural transformation +#! @Group NaturalTransformation +DeclareOperation( "NaturalTransformation", + [ IsRecord, IsCapFunctor, IsCapFunctor ] ); + +#! @Arguments F, eta, G +#! @Group NaturalTransformation +DeclareOperation( "NaturalTransformation", + [ IsCapFunctor, IsList, IsCapFunctor ] ); + if IsPackageMarkedForLoading( "Digraphs", ">= 1.3.1" ) then #! @Description diff --git a/FpCategories/gap/Tools.gi b/FpCategories/gap/Tools.gi index 6439313e8..fd1e6b6d0 100644 --- a/FpCategories/gap/Tools.gi +++ b/FpCategories/gap/Tools.gi @@ -4,6 +4,7 @@ # Implementations # + ## InstallTrueMethod( IsObjectFiniteCategory, IsFinitelyPresentedCategory ); InstallTrueMethod( IsFinitelyPresentedCategory, IsFiniteCategory ); @@ -221,6 +222,879 @@ InstallMethodForCompilerForCAP( CoYonedaEmbeddingData, end ); +## +InstallMethodForCompilerForCAP( NerveTruncatedInDegree2Data, + [ IsCapCategory and IsFiniteCategory ], + + function ( B ) + local A, sFinSets, B0, N0, D00, N0N0, p21, p22, B1, N1, N1_elements, d, id, pi2, s, t, + D000, N0N0N0, p31, p32, p33, B2, N2, N2_elements, T, ds, is, dt, it, + p312, p323, p313, pi3, pi312, pi323, pi313, ps, pt, mus, mus1, mus2, mus3, mu; + + sFinSets := RangeCategoryOfHomomorphismStructure( B ); + + ## sFinSets must be the category skeletal finite sets + #% CAP_JIT_DROP_NEXT_STATEMENT + Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); + + B0 := SetOfObjects( B ); + N0 := ObjectConstructor( sFinSets, Length( B0 ) ); + + ## N0 × N0 + D00 := [ N0, N0 ]; + N0N0 := DirectProduct( sFinSets, D00 ); + + ## N0 × N0 -> N0 + p21 := ProjectionInFactorOfDirectProductWithGivenDirectProduct( sFinSets, D00, 1, N0N0 ); + p22 := ProjectionInFactorOfDirectProductWithGivenDirectProduct( sFinSets, D00, 2, N0N0 ); + + B1 := List( N0N0, i -> + HomomorphismStructureOnObjects( B, + B0[1 + AsList( p21 )[1 + i]], + B0[1 + AsList( p22 )[1 + i]] ) ); + + N1 := Coproduct( sFinSets, B1 ); + + N1_elements := ExactCoverWithGlobalElements( N1 ); + + ## N0 -> N0 × N0 + d := EmbeddingOfEqualizerWithGivenEqualizer( sFinSets, + N0N0, + [ p21, p22 ], + N0 ); + + #% CAP_JIT_DROP_NEXT_STATEMENT + Assert( 0, d = UniversalMorphismIntoDirectProduct( sFinSets, D00, N0, [ IdentityMorphism( sFinSets, N0 ), IdentityMorphism( sFinSets, N0 ) ] ) ); + + ## N0 -> N1 + id := MorphismConstructor( sFinSets, + N0, + List( N0, i -> + AsList( + PreCompose( sFinSets, + InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( B, + IdentityMorphism( B, + B0[1 + i] ) ), + InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, + B1, + 1 + AsList( d )[1 + i], + N1 ) ) )[1 + 0] ), + N1 ); + + ## N1 -> N0 × N0 + ## this morphism is mixing two levels and is not a CAP operation: + ## the coproduct N1 in SkeletalFinSets is taken over the index set N0N0 (here also realized as an object in SkeletalFinSets), + ## so this morphism is a fibration of a coproduct over its "index set" which are both assumed to be objects in the same category: + pi2 := MorphismConstructor( sFinSets, + N1, + Concatenation( List( N0N0, i -> ListWithIdenticalEntries( Length( B1[1 + i] ), i ) ) ), + N0N0 ); + + ## N1 -> N0 × N0 -> N0 + s := PreCompose( sFinSets, pi2, p21 ); + + ## N1 -> N0 × N0 -> N0 + t := PreCompose( sFinSets, pi2, p22 ); + + ## N0 × N0 × N0 + D000 := [ N0, N0, N0 ]; + N0N0N0 := DirectProduct( sFinSets, D000 ); + + ## N0 × N0 × N0 -> N0 + p31 := ProjectionInFactorOfDirectProductWithGivenDirectProduct( sFinSets, D000, 1, N0N0N0 ); + p32 := ProjectionInFactorOfDirectProductWithGivenDirectProduct( sFinSets, D000, 2, N0N0N0 ); + p33 := ProjectionInFactorOfDirectProductWithGivenDirectProduct( sFinSets, D000, 3, N0N0N0 ); + + B2 := List( N0N0N0, i -> + DirectProduct( sFinSets, + [ HomomorphismStructureOnObjects( B, + B0[1 + AsList( p31 )[1 + i]], + B0[1 + AsList( p32 )[1 + i]] ), + HomomorphismStructureOnObjects( B, + B0[1 + AsList( p32 )[1 + i]], + B0[1 + AsList( p33 )[1 + i]] ) ] ) ); + + N2 := Coproduct( sFinSets, B2 ); + + N2_elements := ExactCoverWithGlobalElements( N2 ); + + T := TerminalObject( sFinSets ); + + ## N1 -> N0 × N0 -> N0 × N0 × N0 + ## this is elegant but needs a justification: + ds := PreCompose( sFinSets, + pi2, + EmbeddingOfEqualizerWithGivenEqualizer( sFinSets, + N0N0N0, + [ p32, p33 ], + N0N0 ) ); + + ## N1 -> N2 + is := MorphismConstructor( sFinSets, + N1, + List( N1, i -> + AsList( + PreCompose( sFinSets, + DirectProductFunctorial( sFinSets, + [ LiftAlongMonomorphism( sFinSets, + InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, + B1, + 1 + AsList( pi2 )[1 + i], + N1 ), + N1_elements[1 + i] ), + InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( B, + IdentityMorphism( B, + B0[1 + AsList( t )[1 + i]] ) ) ] ), + InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, + B2, + 1 + AsList( ds )[1 + i], + N2 ) ) )[1 + 0] ), + N2 ); + + ## N1 -> N0 × N0 -> N0 × N0 × N0 + ## this is elegant but needs a justification: + dt := PreCompose( sFinSets, + pi2, + EmbeddingOfEqualizerWithGivenEqualizer( sFinSets, + N0N0N0, + [ p31, p32 ], + N0N0 ) ); + + ## N1 -> N2 + it := MorphismConstructor( sFinSets, + N1, + List( N1, i -> + AsList( + PreCompose( sFinSets, + DirectProductFunctorial( sFinSets, + [ InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( B, + IdentityMorphism( B, + B0[1 + AsList( s )[1 + i]] ) ), + LiftAlongMonomorphism( sFinSets, + InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, + B1, + 1 + AsList( pi2 )[1 + i], + N1 ), + N1_elements[1 + i] ) ] ), + InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, + B2, + 1 + AsList( dt )[1 + i], + N2 ) ) )[1 + 0] ), + N2 ); + + ## N0 × N0 × N0 -> N0 × N0 + p312 := UniversalMorphismIntoDirectProduct( sFinSets, D00, N0N0N0, [ p31, p32 ] ); + p323 := UniversalMorphismIntoDirectProduct( sFinSets, D00, N0N0N0, [ p32, p33 ] ); + p313 := UniversalMorphismIntoDirectProduct( sFinSets, D00, N0N0N0, [ p31, p33 ] ); + + #% CAP_JIT_DROP_NEXT_STATEMENT + Assert( 0, p312 = ProjectionInFactorOfDirectProduct( sFinSets, [ N0N0, N0 ], 1 ) ); + + #% CAP_JIT_DROP_NEXT_STATEMENT + Assert( 0, p323 = ProjectionInFactorOfDirectProduct( sFinSets, [ N0, N0N0 ], 2 ) ); + + ## N2 -> N0 × N0 × N0 + ## this morphism is mixing two levels and is not a CAP operation: + ## the coproduct N2 in SkeletalFinSets is taken over the index set N0N0N0 (here also realized as an object in SkeletalFinSets), + ## so this morphism is a fibration of a coproduct over its "index set" which are both assumed to objects in the same category: + pi3 := MorphismConstructor( sFinSets, + N2, + Concatenation( List( N0N0N0, i -> ListWithIdenticalEntries( Length( B2[1 + i] ), i ) ) ), + N0N0N0 ); + + ## N2 -> N0 × N0 × N0 -> N0 × N0 + pi312 := PreCompose( sFinSets, pi3, p312 ); + pi323 := PreCompose( sFinSets, pi3, p323 ); + pi313 := PreCompose( sFinSets, pi3, p313 ); + + ## N2 -> N1 + ps := MorphismConstructor( sFinSets, + N2, + List( N2, i -> + AsList( + PreComposeList( sFinSets, + T, + [ LiftAlongMonomorphism( sFinSets, + InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, + B2, + 1 + AsList( pi3 )[1 + i], + N2 ), + N2_elements[1 + i] ), + ProjectionInFactorOfDirectProduct( sFinSets, + [ B1[1 + AsList( pi312 )[1 + i]], + B1[1 + AsList( pi323 )[1 + i]] ], + 1 ), + InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, + B1, + 1 + AsList( pi312 )[1 + i], + N1 ) ], + N1 ) )[1 + 0] ), + N1 ); + + ## N2 -> N1 + pt := MorphismConstructor( sFinSets, + N2, + List( N2, i -> + AsList( + PreComposeList( sFinSets, + T, + [ LiftAlongMonomorphism( sFinSets, + InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, + B2, + 1 + AsList( pi3 )[ 1 + i], + N2 ), + N2_elements[1 + i] ), + ProjectionInFactorOfDirectProduct( sFinSets, + [ B1[1 + AsList( pi312 )[1 + i]], + B1[1 + AsList( pi323 )[1 + i]] ], + 2 ), + InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, + B1, + 1 + AsList( pi323 )[1 + i], + N1 ) ], + N1 ) )[1 + 0] ), + N1 ); + + mus := List( N0N0N0, i -> + List( B2[1 + i], j -> + [ MorphismConstructor( sFinSets, + T, + [ AsList( + ProjectionInFactorOfDirectProduct( sFinSets, + [ B1[1 + AsList( p312 )[1 + i]], + B1[1 + AsList( p323 )[1 + i]] ], + 1 ) )[1 + j] ], + B1[1 + AsList( p312 )[1 + i]] ), + MorphismConstructor( sFinSets, + T, + [ AsList( + ProjectionInFactorOfDirectProduct( sFinSets, + [ B1[1 + AsList( p312 )[1 + i]], + B1[1 + AsList( p323 )[1 + i]] ], + 2 ) )[1 + j] ], + B1[1 + AsList( p323 )[1 + i]] ) ] ) ); + + #% CAP_JIT_DROP_NEXT_STATEMENT + Assert( 0, Length( Concatenation( mus ) ) = Length( N2 ) ); + + #% CAP_JIT_DROP_NEXT_STATEMENT + Assert( 0, ForAll( mus, mu -> ForAll( mu, m -> IsWellDefined( m[1] ) and IsWellDefined( m[2] ) ) ) ); + + mus1 := List( N0N0N0, i -> + List( B2[1 + i], j -> + PreCompose( B, + InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( B, + B0[1 + AsList( p31 )[1 + i]], + B0[1 + AsList( p32 )[1 + i]], + mus[1 + i][1 + j][1] ), + InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( B, + B0[1 + AsList( p32 )[1 + i]], + B0[1 + AsList( p33 )[1 + i]], + mus[1 + i][1 + j][2] ) ) ) ); + + mus2 := List( N0N0N0, i -> + List( B2[1 + i], j -> + InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( B, + mus1[1 + i][1 + j] ) ) ); + + mus3 := List( N0N0N0, i -> + UniversalMorphismFromCoproductWithGivenCoproduct( sFinSets, + List( mus2[1 + i], Source ), + B1[1 + AsList( p313 )[1 + i]], + mus2[1 + i], + B2[1 + i] ) ); + + #% CAP_JIT_DROP_NEXT_STATEMENT + Assert( 0, ForAll( [ 1 .. Length( N0N0N0 ) ], i -> Source( mus3[i] ) = B2[i] ) ); + + ## N2 -> N1 + mu := MorphismConstructor( sFinSets, + N2, + List( N2, i -> + AsList( + PreComposeList( sFinSets, + T, + [ LiftAlongMonomorphism( sFinSets, + InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, + B2, + 1 + AsList( pi3 )[1 + i], + N2 ), + N2_elements[1 + i] ), + mus3[1 + AsList( pi3 )[1 + i]], + InjectionOfCofactorOfCoproductWithGivenCoproduct( sFinSets, + B1, + 1 + AsList( pi313 )[1 + i], + N1 ) ], + N1 ) )[1 + 0] ), + N1 ); + + return Pair( Triple( N0, N1, N2 ), + NTuple( 8, id, s, t, is, it, ps, pt, mu ) ); + +end ); + +## +InstallMethod( NerveTruncatedInDegree2AsFunctor, + [ IsCapCategory and IsFiniteCategory ], + + function ( C ) + local nerve, nerve_ValuesOnAllObjects, nerve_ValuesOnAllGeneratingMorphisms, name, Delta2, Delta2op; + + nerve := NerveTruncatedInDegree2Data( C ); + + nerve_ValuesOnAllObjects := rec( C0 := nerve[1][1], C1 := nerve[1][2], C2 := nerve[1][3] ); + + nerve_ValuesOnAllGeneratingMorphisms := + rec( + id := nerve[2][1], + s := nerve[2][2], + t := nerve[2][3], + is := nerve[2][4], + it := nerve[2][5], + ps := nerve[2][6], + pt := nerve[2][7], + mu := nerve[2][8] ); + + name := Concatenation( "Nerve of ", Name( C ) ); + + ## Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1,is:C2->C1,it:C2->C1,ps:C1->C2,pt:C1->C2,mu:C1->C2] + Delta2 := ValueGlobal( "SimplicialCategoryTruncatedInDegree2" ); + + ## Delta_op(C0,C1,C2)[id:C0->C1,s:C1->C0,t:C1->C0,is:C1->C2,it:C1->C2,ps:C2->C1,pt:C2->C1,mu:C2->C1] + Delta2op := OppositeQuotientOfPathCategory( Delta2 ); + + return CapFunctor( Delta2op, nerve_ValuesOnAllObjects, nerve_ValuesOnAllGeneratingMorphisms, RangeCategoryOfHomomorphismStructure( C ) ); + +end ); + +## +InstallMethod( IndicesOfGeneratingMorphismsFromHomStructure, + "for a finite category", + [ IsCapCategory and IsFiniteCategory ], + + function( C ) + local sFinSets, C0, N0, D00, N0N0, p21, p22, C1, T, st, mors; + + sFinSets := RangeCategoryOfHomomorphismStructure( C ); + + ## sFinSets must be the category skeletal finite sets + Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); + + C0 := SetOfObjects( C ); + N0 := ObjectConstructor( sFinSets, Length( C0 ) ); + + D00 := [ N0, N0 ]; + + ## N0 × N0 -> N0 + p21 := ProjectionInFactorOfDirectProduct( sFinSets, D00, 1 ); + p22 := ProjectionInFactorOfDirectProduct( sFinSets, D00, 2 ); + + C1 := List( DirectProduct( sFinSets, D00 ), i -> + HomomorphismStructureOnObjects( C, + C0[1 + AsList( p21 )[1 + i]], + C0[1 + AsList( p22 )[1 + i]] ) ); + + T := DistinguishedObjectOfHomomorphismStructure( C ); + + st := List( DefiningTripleOfUnderlyingQuiver( C )[3], pair -> + UniversalMorphismIntoDirectProduct( sFinSets, + D00, + T, + [ MorphismConstructor( sFinSets, T, [ pair[1] ], N0 ), + MorphismConstructor( sFinSets, T, [ pair[2] ], N0 ) ] ) ); + + mors := SetOfGeneratingMorphisms( C ); + + return List( [ 1 .. Length( st ) ], i -> + Sum( C1{[ 1 .. AsList( st[i] )[1 + 0] ]}, Length ) + + AsList( InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( C, mors[i] ) )[1 + 0] ); + +end ); + +## +InstallMethod( OppositeFiniteCategory, + "for a finite category", + [ IsCapCategory and IsFiniteCategory ], + + function( C ) + local C_op, defining_triple; + + C_op := Opposite( C ); + + defining_triple := DefiningTripleOfUnderlyingQuiver( C ); + + defining_triple := Triple( defining_triple[1], + defining_triple[2], + List( defining_triple[3], a -> Pair( a[2], a[1] ) ) ); + + SetDefiningTripleOfUnderlyingQuiver( C_op, defining_triple ); + + return C_op; + +end ); + +## +InstallMethodForCompilerForCAP( YonedaNaturalEpimorphisms, + [ IsCapCategory and IsFiniteCategory ], + + function ( B ) + local sFinSets, objs, mors, o, m, Hom2, hom3, Hom3, tum2, emb2, sum2, iso2, + B0, N0, N1, N2, D, precompose, pt, mu, s; + + sFinSets := RangeCategoryOfHomomorphismStructure( B ); + + ## sFinSets must be the category skeletal finite sets + #% CAP_JIT_DROP_NEXT_STATEMENT + Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); + + objs := SetOfObjects( B ); + mors := SetOfGeneratingMorphisms( B ); + + o := Length( objs ); + m := Length( mors ); + + ## [ [ Hom(a, c) ]_{a ∈ B} ]_{c ∈ B}: + Hom2 := List( objs, c -> + List( objs, a -> + HomomorphismStructureOnObjects( B, a, c ) ) ); + + ## [ [ [ ( Hom(a, b), Hom(b, c) ) ]_{b ∈ B} ]_{a ∈ B} ]_{c ∈ B}: + hom3 := List( [ 1 .. o ], c -> + List( [ 1 .. o ], a -> + List( [ 1 .. o ], b -> + [ Hom2[b][a], Hom2[c][b] ] ) ) ); + + ## [ [ [ Hom(a, b) × Hom(b, c) ]_{b ∈ B} ]_{a ∈ B} ]_{c ∈ B}: + Hom3 := List( [ 1 .. o ], c -> + List( [ 1 .. o ], a -> + List( [ 1 .. o ], b -> + DirectProduct( sFinSets, hom3[c][a][b] ) ) ) ); + + ## [ [ Hom(a, b) × Hom(b, c) ]_{a, b ∈ B} ]_{c ∈ B}: + ## tum2 := List( Hom3, L -> Concatenation( TransposedMat( L ) ) ); + tum2 := List( [ 1 .. o ], c -> + Concatenation( + List( [ 1 .. o ], b -> + List( [ 1 .. o ], a -> + Hom3[c][a][b] ) ) ) ); + + ## The embeddings into the double coproducts + ## [ [ Hom(a, b) × Hom(b, c) ↪ ⊔_{a' ∈ B} ⊔_{b' ∈ B} Hom(a', b') × Hom(b', c) ]_{a ∈ B, b ∈ B} ]_{c ∈ B}: + emb2 := List( [ 1 .. o ], c -> + Concatenation( + List( [ 1 .. o ], a -> + List( [ 1 .. o ], b -> + InjectionOfCofactorOfCoproduct( sFinSets, + tum2[c], o * ( b - 1 ) + a ) ) ) ) ); + + ## [ [ Hom(a, b) × Hom(b, c) ]_{b, a ∈ B} ]_{c ∈ B}: + sum2 := List( Hom3, L -> Concatenation( L ) ); + + ## The isomorphisms + ## [ ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c) → ⊔_{b ∈ B} ⊔_{a ∈ B} Hom(a, b) × Hom(b, c) ]_{c ∈ B}: + iso2 := List( [ 1 .. o ], c -> + UniversalMorphismFromCoproduct( sFinSets, + sum2[c], + Coproduct( sFinSets, + tum2[c] ), + emb2[c] ) ); + + ## The constant functor of 0-cells B → sFinSets, c ↦ B_0, ψ ↦ id_{B_0} + B0 := ObjectConstructor( sFinSets, o ); + + N0 := Pair( ListWithIdenticalEntries( o, B0 ), + ListWithIdenticalEntries( m, IdentityMorphism( sFinSets, B0 ) ) ); + + ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ), where + ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c), + ## Hom(-, ψ) := ⊔_{a ∈ B} Hom(id_a, ψ): + N1 := Pair( + List( [ 1 .. o ], c -> + ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c): + Coproduct( sFinSets, Hom2[c] ) ), + List( mors, psi -> + ## Hom(-, ψ) := ⊔_{a ∈ B} Hom(id_a, ψ): + CoproductFunctorial( sFinSets, + List( objs, a -> + HomomorphismStructureOnMorphisms( B, + IdentityMorphism( B, a ), psi ) ) ) ) ); + + ## The 2-Yoneda functor B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ), where + ## Hom(-, -) × Hom(-, c) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c), + ## Hom(-, -) × Hom(-, ψ) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(id_a, id_b) × Hom(id_b, ψ): + N2 := Pair( + List( [ 1 .. o ], c -> + ## Hom(-, -) × Hom(-, c) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c): + Coproduct( sFinSets, + Concatenation( Hom3[c] ) ) ), + List( mors, psi -> + ## Hom(-, -) × Hom(-, ψ) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(id_a, id_b) × Hom(id_b, ψ): + CoproductFunctorial( sFinSets, + Concatenation( + List( objs, a -> + List( objs, b -> + ## Hom(id_a, id_b) × Hom(id_b, ψ): + DirectProductFunctorial( sFinSets, + [ HomomorphismStructureOnMorphisms( B, + IdentityMorphism( B, a ), IdentityMorphism( B, b ) ), + HomomorphismStructureOnMorphisms( B, + IdentityMorphism( B, b ), psi ) ] ) ) ) ) ) ) ); + + D := DistinguishedObjectOfHomomorphismStructure( B ); + + ## mu_{a,b,c}: Hom(a, b) × Hom(b, c) ↠ Hom(a, c): + precompose := + function ( a, b, c ) + return + MorphismConstructor( sFinSets, + Hom3[c][a][b], # = Hom(a, b) × Hom(b, c) + List( Hom3[c][a][b], + function ( i ) + local d, d_ab, d_bc, m_ab, m_bc, m; + + ## D → Hom(a, b) × Hom(b, c): + d := MorphismConstructor( sFinSets, D, [ i ], Hom3[c][a][b] ); + + ## D → Hom(a, b) × Hom(b, c) → Hom(a, b): + d_ab := PreCompose( sFinSets, d, ProjectionInFactorOfDirectProduct( sFinSets, hom3[c][a][b], 1 ) ); + + ## D → Hom(a, b) × Hom(b, c) → Hom(b, c): + d_bc := PreCompose( sFinSets, d, ProjectionInFactorOfDirectProduct( sFinSets, hom3[c][a][b], 2 ) ); + + ## the map a → b corresponding to d_ab: + m_ab := InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( B, objs[a], objs[b], d_ab ); + + ## the map b → c corresponding to d_bc: + m_bc := InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( B, objs[b], objs[c], d_bc ); + + ## the composition a → b → c: + m := PreCompose( B, m_ab, m_bc ); + + ## reinterpret the composition m as a morphism D → Hom(a, c), + ## then get its number as an element in Hom(a, c): + return AsList( InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( B, m ) )[1 + 0]; + + end ), + Hom2[c][a] ); # = Hom(a, c) + end; + + ## The Yoneda projection is a natrual epimorphism from the 2-Yoneda functor to the Yoneda functor + ## B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ) + pt := List( [ 1 .. o ], c -> + ## ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c) ↠ ⊔_{b ∈ B} Hom(b, c): + PreCompose( sFinSets, + ## ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c) → ⊔_{b ∈ B} ⊔_{a ∈ B} Hom(a, b) × Hom(b, c): + iso2[c], + ## ⊔_{b ∈ B} ⊔_{a ∈ B} Hom(a, b) × Hom(b, c) ↠ ⊔_{b ∈ B} Hom(b, c): + CoproductFunctorial( sFinSets, + List( [ 1 .. o ], b -> + ## ⊔_{a ∈ B} Hom(a, b) × Hom(b, c) ↠ Hom(b, c): + UniversalMorphismFromCoproduct( sFinSets, + List( [ 1 .. o ], a -> Hom3[c][a][b] ), + Hom2[c][b], + List( [ 1 .. o ], a -> + ## Hom(a, b) × Hom(b, c) ↠ Hom(b, c): + ProjectionInFactorOfDirectProduct( sFinSets, + hom3[c][a][b], 2 ) ) ) ) ) ) ); + + ## The Yoneda composition is a natrual epimorphism from the 2-Yoneda functor to the Yoneda functor + ## Hom(-, -) × Hom(-, c) ↠ Hom(-, c): + mu := List( [ 1 .. o ], c -> + ## ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c) ↠ ⊔_{a ∈ B} Hom(a, c): + CoproductFunctorial( sFinSets, + List( [ 1 .. o ], a -> + ## ⊔_{b ∈ B} Hom(a, b) × Hom(b, c) ↠ Hom(a, c): + UniversalMorphismFromCoproduct( sFinSets, + List( [ 1 .. o ], b -> Hom3[c][a][b] ), + Hom2[c][a], + List( [ 1 .. o ], b -> + ## Hom(a, b) × Hom(b, c) ↠ Hom(a, c): + precompose( a, b, c ) ) ) ) ) ); + + ## The source fibration is a natrual morphism from the Yoneda functor to the constant functor of 0-cells + ## Hom(-, c) → B_0: + s := List( [ 1 .. o ], c -> + ## ⊔_{a ∈ B} Hom(a, c) → B_0, ϕ ↦ Source(ϕ) + CoproductFunctorial( sFinSets, + List( [ 1 .. o ], a -> + ## Hom(a, c) → {a}, ϕ ↦ a + UniversalMorphismIntoTerminalObject( sFinSets, + Hom2[c][a] ) ) ) ); + + return NTuple( 6, N0, N1, N2, pt, mu, s ); + +end ); + +## +InstallMethod( YonedaProjectionAsNaturalEpimorphism, + [ IsCapCategory and IsFiniteCategory and HasRangeCategoryOfHomomorphismStructure ], + + function ( B ) + local Yepis, sFinSets, N1, N2, pt; + + Yepis := YonedaNaturalEpimorphisms( B ); + + sFinSets := RangeCategoryOfHomomorphismStructure( B ); + + ## sFinSets must be the category skeletal finite sets + Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); + + ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ), where + ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c), + ## Hom(-, ψ) := ⊔_{a ∈ B} Hom(id_a, ψ): + N1 := CapFunctor( B, Yepis[2][1], Yepis[2][2], sFinSets ); + + ## The 2-Yoneda functor B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ), where + ## Hom(-, -) × Hom(-, c) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c), + ## Hom(-, -) × Hom(-, ψ) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(id_a, id_b) × Hom(id_b, ψ): + N2 := CapFunctor( B, Yepis[3][1], Yepis[3][2], sFinSets ); + + ## The Yoneda projection is a natrual epimorphism from the 2-Yoneda functor to the Yoneda functor + ## B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ) + pt := NaturalTransformation( + N2, ## The 2-Yoneda functor: B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ) + Yepis[4], + N1 ); ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ) + + #% CAP_JIT_DROP_NEXT_STATEMENT + SetIsEpimorphism( pt, true ); + + return pt; + +end ); + +## +InstallMethod( YonedaCompositionAsNaturalEpimorphism, + [ IsCapCategory and IsFiniteCategory and HasRangeCategoryOfHomomorphismStructure ], + + function ( B ) + local Yepis, sFinSets, N1, N2, mu; + + Yepis := YonedaNaturalEpimorphisms( B ); + + sFinSets := RangeCategoryOfHomomorphismStructure( B ); + + ## sFinSets must be the category skeletal finite sets + Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); + + ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ), where + ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c), + ## Hom(-, ψ) := ⊔_{a ∈ B} Hom(id_a, ψ): + N1 := CapFunctor( B, Yepis[2][1], Yepis[2][2], sFinSets ); + + ## The 2-Yoneda functor B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ), where + ## Hom(-, -) × Hom(-, c) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(a, b) × Hom(b, c), + ## Hom(-, -) × Hom(-, ψ) := ⊔_{a ∈ B} ⊔_{b ∈ B} Hom(id_a, id_b) × Hom(id_b, ψ): + N2 := CapFunctor( B, Yepis[3][1], Yepis[3][2], sFinSets ); + + ## The Yoneda composition is a natrual epimorphism from the 2-Yoneda functor to the Yoneda functor + ## Hom(-, -) × Hom(-, c) ↠ Hom(-, c): + mu := NaturalTransformation( + N2, ## The 2-Yoneda functor: B → sFinSets, c ↦ Hom(-, -) × Hom(-, c) and ψ ↦ Hom(-, -) × Hom(-, ψ) + Yepis[5], + N1 ); ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ) + + #% CAP_JIT_DROP_NEXT_STATEMENT + SetIsEpimorphism( mu, true ); + + return mu; + +end ); + +## +InstallMethod( YonedaFibrationAsNaturalTransformation, + [ IsCapCategory and IsFiniteCategory and HasRangeCategoryOfHomomorphismStructure ], + + function ( B ) + local Yepis, sFinSets, N0, N1; + + Yepis := YonedaNaturalEpimorphisms( B ); + + sFinSets := RangeCategoryOfHomomorphismStructure( B ); + + ## sFinSets must be the category skeletal finite sets + Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); + + ## The constant functor of 0-cells B → sFinSets, c ↦ B_0, ψ ↦ id_{B_0} + N0 := CapFunctor( B, Yepis[1][1], Yepis[1][2], sFinSets ); + + ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ), where + ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c), + ## Hom(-, ψ) := ⊔_{a ∈ B} Hom(id_a, ψ): + N1 := CapFunctor( B, Yepis[2][1], Yepis[2][2], sFinSets ); + + ## The source fibration is a natrual morphism from the Yoneda functor to the constant functor of 0-cells + ## Hom(-, c) → B_0: + return NaturalTransformation( + N1, ## The Yoneda functor B → sFinSets, c ↦ Hom(-, c), ψ ↦ Hom(-, ψ) + Yepis[6], + N0 ); ## The constant functor of 0-cells + +end ); + +## +InstallMethodForCompilerForCAP( TruthMorphismOfTrueToSieveFunctorAndEmbedding, + [ IsCapCategory and IsFiniteCategory ], + + function ( B ) + local sFinSets, D, Omega, Yepis, Ymu, Ypt, sieves, defining_triple, lobjs, lmors, arrows, id, N1, + Sieves, Sieves_emb, Sieves_maximal, + HomHomOmega_objects, HomHomOmega_morphisms, Sieves_objects, Sieves_morphisms, + Constant_functor, Sieves_functor, HomHomOmega_functor; + + sFinSets := RangeCategoryOfHomomorphismStructure( B ); + + ## sFinSets must be the category skeletal finite sets + #% CAP_JIT_DROP_NEXT_STATEMENT + Assert( 0, IsSkeletalCategoryOfFiniteSets( sFinSets ) ); + + D := DistinguishedObjectOfHomomorphismStructure( B ); + + Omega := SubobjectClassifier( sFinSets ); + + Yepis := YonedaNaturalEpimorphisms( B ); + + Ypt := Yepis[4]; # YonedaProjectionAsNaturalEpimorphism( B ); + Ymu := Yepis[5]; # YonedaCompositionAsNaturalEpimorphism( B ); + + sieves := + function ( c ) + local pt_c, mu_c, hom_c, power, action, maximal, emb; + + ## Hom(-, -) × Hom(-, c) ↠ Hom(-, c) + pt_c := Ypt[c]; + + ## Hom(-, -) × Hom(-, c) ↠ Hom(-, c) + mu_c := Ymu[c]; + + ## Hom(-, c) := ⊔_{a ∈ B} Hom(a, c) + hom_c := Target( mu_c ); + + ## Hom(Hom(-, c), Ω) := Hom(⊔_{a ∈ B} Hom(a, c), Ω) + power := HomomorphismStructureOnObjects( sFinSets, hom_c, Omega ); + + ## define the action as an endomorphism on Hom(Hom(-, c), Ω) + action := + MorphismConstructor( sFinSets, + power, ## Hom(Hom(-, c), Ω) + List( power, i -> + ## interpreted as an "element" D → Hom(Hom(-, c), Ω) + AsList( InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( sFinSets, + ## interpreted as a classifying morphism χ_{s'}: Hom(-, c) → Ω + ClassifyingMorphismOfSubobject( sFinSets, + ## s' ↪ Hom(-, c) + ImageEmbedding( sFinSets, + ## Hom(-, -) × s → Hom(-, c) + PreCompose( sFinSets, + ## Hom(-, -) × s ↪ Hom(-, -) × Hom(-, c) + ProjectionInFactorOfFiberProduct( sFinSets, + [ pt_c, + ## interpreted as a subobject s ↪ Hom(-, c) + SubobjectOfClassifyingMorphism( sFinSets, + ## interpreted as a classifying morphism χ_s: Hom(-, c) → Ω + InterpretMorphismFromDistinguishedObjectToHomomorphismStructureAsMorphism( sFinSets, + hom_c, + Omega, + ## an "element" D → Hom(Hom(-, c), Ω) + MorphismConstructor( sFinSets, D, [ i ], power ) ) ) + ], 1 ), + ## μ_c: Hom(-, -) × Hom(-, c) ↠ Hom(-, c) + mu_c ) ) ) ) )[1 + 0] ), + power ); ## Hom(Hom(-, c), Ω) + + ## The sieves on c are the fixed points of the above action on Hom(Hom(-, c), Ω), + ## resulting in the embedding Sieves(c) ↪ Hom(Hom(-, c), Ω): + emb := EmbeddingOfEqualizer( sFinSets, power, [ action, IdentityMorphism( sFinSets, power ) ] ); + + ## the "element" D → Sieves(c) corresponding to the maximal sieve: + maximal := LiftAlongMonomorphism( sFinSets, + ## Sieves(c) ↪ Hom(Hom(-, c), Ω): + emb, + ## interpreted as an "element" D → Hom(Hom(-, c), Ω) + InterpretMorphismAsMorphismFromDistinguishedObjectToHomomorphismStructure( sFinSets, + ## the corresponding classifying morphism χ: Hom(-, c) → Ω + ClassifyingMorphismOfSubobject( sFinSets, + ## id: Hom(-, c) → Hom(-, c) + IdentityMorphism( sFinSets, hom_c ) ) ) ); + + return Pair( emb, maximal ); + + end; + + defining_triple := DefiningTripleOfUnderlyingQuiver( B ); + + lobjs := defining_triple[1]; + lmors := defining_triple[2]; + + arrows := defining_triple[3]; + + id := IdentityMorphism( sFinSets, Omega ); + + N1 := Yepis[2]; # Target( Ypt ); + + Sieves := List( [ 1 .. lobjs ], o -> sieves( o ) ); + Sieves_emb := List( Sieves, s -> s[1] ); + Sieves_maximal := List( Sieves, s -> s[2] ); + + ## Hom(Hom(-, c), Ω) + HomHomOmega_objects := List( Sieves_emb, Range ); + HomHomOmega_morphisms := List( [ 1 .. lmors ], m -> + HomomorphismStructureOnMorphisms( sFinSets, + N1[2][m], # N1( m ) + id ) ); + + Sieves_objects := List( Sieves_emb, Source ); + Sieves_morphisms := List( [ 1 .. lmors ], m -> + LiftAlongMonomorphism( sFinSets, + Sieves_emb[1 + arrows[m][1]], # Source( m ) + PreCompose( sFinSets, + Sieves_emb[1 + arrows[m][2]], # Target( m ) + HomHomOmega_morphisms[m] ) ) ); + + return NTuple( 5, + Pair( Sieves_objects, + Sieves_morphisms ), + Pair( ListWithIdenticalEntries( lobjs, D ), + ListWithIdenticalEntries( lmors, IdentityMorphism( sFinSets, D ) ) ), + Pair( HomHomOmega_objects, + HomHomOmega_morphisms ), + Sieves_maximal, + Sieves_emb ); + +end ); + +## +InstallMethod( NaturalTransformation, + "for a list and two CAP functors", + [ IsCapFunctor, IsList, IsCapFunctor ], + + function( F, images, G ) + local eta, vertices; + + eta := NaturalTransformation( Concatenation( "Natural transformation from ", Name( F ), " -> ", Name( G ) ), F, G ); + + eta!.ValuesOnAllObjects := images; + + vertices := SetOfObjects( SourceOfFunctor( F ) ); + + AddNaturalTransformationFunction( eta, + function( source, obj, range ) + local pos; + + pos := SafePosition( vertices, obj ); + + if not IsInt( pos ) then + Error( "vertex obj = ", obj, " not found in the list ", vertices, " of vertices\n" ); + fi; + + return images[pos]; + + end ); + + return eta; + +end ); + if IsPackageMarkedForLoading( "Digraphs", ">= 1.3.1" ) then ## diff --git a/Algebroids/gap/precompiled_categories/CategoryFromNerveDataHomStructureOnMorphismsPrecompiled.gi b/FpCategories/gap/precompiled_categories/CategoryFromNerveDataHomStructureOnMorphismsPrecompiled.gi similarity index 99% rename from Algebroids/gap/precompiled_categories/CategoryFromNerveDataHomStructureOnMorphismsPrecompiled.gi rename to FpCategories/gap/precompiled_categories/CategoryFromNerveDataHomStructureOnMorphismsPrecompiled.gi index 22ab30ff7..520b8a7d7 100644 --- a/Algebroids/gap/precompiled_categories/CategoryFromNerveDataHomStructureOnMorphismsPrecompiled.gi +++ b/FpCategories/gap/precompiled_categories/CategoryFromNerveDataHomStructureOnMorphismsPrecompiled.gi @@ -170,7 +170,7 @@ BindGlobal( "CategoryFromNerveDataHomStructureOnMorphismsPrecompiled", function function ( quiver ) local sFinSets; sFinSets := SkeletalCategoryOfFiniteSets( : FinalizeCategory := true ); - return CategoryFromNerveData( FreeCategory( quiver : range_of_HomStructure := sFinSets, + return CategoryFromNerveData( PathCategory( quiver : range_of_HomStructure := sFinSets, FinalizeCategory := true ) ); end; diff --git a/Algebroids/gap/precompiled_categories/CategoryFromNerveDataPrecompiled.gi b/FpCategories/gap/precompiled_categories/CategoryFromNerveDataPrecompiled.gi similarity index 99% rename from Algebroids/gap/precompiled_categories/CategoryFromNerveDataPrecompiled.gi rename to FpCategories/gap/precompiled_categories/CategoryFromNerveDataPrecompiled.gi index 9490c7a31..9d51cfe89 100644 --- a/Algebroids/gap/precompiled_categories/CategoryFromNerveDataPrecompiled.gi +++ b/FpCategories/gap/precompiled_categories/CategoryFromNerveDataPrecompiled.gi @@ -452,7 +452,7 @@ BindGlobal( "CategoryFromNerveDataPrecompiled", function ( quiver ) function ( quiver ) local sFinSets; sFinSets := SkeletalCategoryOfFiniteSets( : FinalizeCategory := true ); - return CategoryFromNerveData( FreeCategory( quiver : range_of_HomStructure := sFinSets, + return CategoryFromNerveData( PathCategory( quiver : range_of_HomStructure := sFinSets, FinalizeCategory := true ) ); end; diff --git a/FpCategories/init.g b/FpCategories/init.g index 5f4d23a3c..b0da8a595 100644 --- a/FpCategories/init.g +++ b/FpCategories/init.g @@ -8,8 +8,10 @@ ReadPackage( "FpCategories", "gap/Quivers.gd"); ReadPackage( "FpCategories", "gap/PathCategories.gd"); ReadPackage( "FpCategories", "gap/GroebnerBasesForPathCategories.gd"); ReadPackage( "FpCategories", "gap/QuotientsOfPathCategories.gd"); +ReadPackage( "FpCategories", "gap/CategoryFromNerveData.gd"); ReadPackage( "FpCategories", "gap/Tools.gd"); ReadPackage( "FpCategories", "gap/ToolsMethodRecordDeclarations.autogen.gd"); +ReadPackage( "FpCategories", "gap/SimplicialCategory.gd"); if IsPackageMarkedForLoading( "JuliaInterface", ">= 0.2" ) then ReadPackage( "FpCategories", "gap/Julia.gi" ); diff --git a/FpCategories/makedoc.g b/FpCategories/makedoc.g index 296340d10..0c1ac9338 100644 --- a/FpCategories/makedoc.g +++ b/FpCategories/makedoc.g @@ -22,6 +22,10 @@ AutoDoc( rec( LateExtraPreamble := """ \usepackage{mathtools} \usepackage{tikz-cd} + \DeclareUnicodeCharacter{2C76}{\ensuremath{\vdash}\!\!} + \DeclareUnicodeCharacter{2192}{\ensuremath{\!\!\rightarrow\!}} + \DeclareUnicodeCharacter{21AA}{\ensuremath{\!\!\hookrightarrow\!}} + \DeclareUnicodeCharacter{21A0}{\ensuremath{\!\!\twoheadrightarrow\!}} \DeclareUnicodeCharacter{2B47}{\ensuremath{\!\!\xrightarrow{\sim}\!}} \DeclareUnicodeCharacter{227B}{\ensuremath{\succ}} \DeclareUnicodeCharacter{22C5}{\ensuremath{\cdot}} diff --git a/FpCategories/makedoc_with_overfull_hbox_warnings.g b/FpCategories/makedoc_with_overfull_hbox_warnings.g index 964ef8e28..db4bb8584 100644 --- a/FpCategories/makedoc_with_overfull_hbox_warnings.g +++ b/FpCategories/makedoc_with_overfull_hbox_warnings.g @@ -20,6 +20,10 @@ AutoDoc( rec( LateExtraPreamble := """ \usepackage{mathtools} \usepackage{tikz-cd} + \DeclareUnicodeCharacter{2C76}{\ensuremath{\vdash}\!\!} + \DeclareUnicodeCharacter{2192}{\ensuremath{\!\!\rightarrow\!}} + \DeclareUnicodeCharacter{21AA}{\ensuremath{\!\!\hookrightarrow\!}} + \DeclareUnicodeCharacter{21A0}{\ensuremath{\!\!\twoheadrightarrow\!}} \DeclareUnicodeCharacter{2B47}{\ensuremath{\!\!\xrightarrow{\sim}\!}} \DeclareUnicodeCharacter{227B}{\ensuremath{\succ}} \DeclareUnicodeCharacter{22C5}{\ensuremath{\cdot}} diff --git a/FpCategories/read.g b/FpCategories/read.g index bfe57a7e6..e99e27807 100644 --- a/FpCategories/read.g +++ b/FpCategories/read.g @@ -4,11 +4,16 @@ # Reading the implementation part of the package. # +ReadPackage( "FpCategories", "gap/precompiled_categories/CategoryFromNerveDataPrecompiled.gi" ); +ReadPackage( "FpCategories", "gap/precompiled_categories/CategoryFromNerveDataHomStructureOnMorphismsPrecompiled.gi" ); + ReadPackage( "FpCategories", "gap/Quivers.gi"); ReadPackage( "FpCategories", "gap/PathCategories.gi"); ReadPackage( "FpCategories", "gap/GroebnerBasesForPathCategories.gi"); ReadPackage( "FpCategories", "gap/QuotientsOfPathCategories.gi"); +ReadPackage( "FpCategories", "gap/CategoryFromNerveData.gi"); ReadPackage( "FpCategories", "gap/Tools.gi"); ReadPackage( "FpCategories", "gap/ToolsMethodRecord.gi"); ReadPackage( "FpCategories", "gap/ToolsMethodRecordInstallations.autogen.gi"); ReadPackage( "FpCategories", "gap/ToolsDerivedMethods.gi"); +ReadPackage( "FpCategories", "gap/SimplicialCategory.gi"); diff --git a/FunctorCategories/PackageInfo.g b/FunctorCategories/PackageInfo.g index 4e0661664..f8477a8c6 100644 --- a/FunctorCategories/PackageInfo.g +++ b/FunctorCategories/PackageInfo.g @@ -10,7 +10,7 @@ SetPackageInfo( rec( PackageName := "FunctorCategories", Subtitle := "Categories of functors", -Version := "2024.09-08", +Version := "2024.09-09", Date := ~.Version{[ 1 .. 10 ]}, Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ), @@ -93,8 +93,8 @@ Dependencies := rec( [ "MonoidalCategories", ">= 2024.06-02" ], [ "CartesianCategories", ">= 2024.06-03" ], [ "ToolsForCategoricalTowers", ">= 2024.03-02" ], - [ "FpCategories", ">= 2024.09-04" ], - [ "Algebroids", ">= 2024.03-01" ], + [ "FpCategories", ">= 2024.09-06" ], + [ "Algebroids", ">= 2024.09-04" ], [ "FiniteCocompletions", ">= 2024.03-12" ], [ "PreSheaves", ">= 2024.02-02" ], [ "RingsForHomalg", ">= 2020.02.04" ], diff --git a/FunctorCategories/examples/CategoryFromDataTables.g b/FunctorCategories/examples/CategoryFromDataTables.g index 83ed8875d..c7a5d855c 100644 --- a/FunctorCategories/examples/CategoryFromDataTables.g +++ b/FunctorCategories/examples/CategoryFromDataTables.g @@ -6,13 +6,14 @@ LoadPackage( "FunctorCategories", false ); #! true Delta1 := UnderlyingCategory( FinReflexiveQuivers ); -#! FreeCategory( RightQuiver( "Delta(C0,C1)[id:C1->C0,s:C0->C1,t:C0->C1]" ) ) -#! / [ s*id = C0, t*id = C0 ] +#! PathCategory( FinQuiver( "Delta(C0,C1)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0) ] N := NerveTruncatedInDegree2( Delta1 ); -#! C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations, +#! IsWellDefined( N ); #! true @@ -37,18 +38,19 @@ Display( N.is ); Display( N.it ); #! { 0,..., 6 } ⱶ[ 0, 4, 7, 8, 17, 20, 23 ]→ { 0,..., 25 } Delta2 := Source( N ); -#! FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations +#! PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] N( Delta2.it ) = N.it; #! true L := [ Delta2.it, Delta2.id, Delta2.t ]; #! [ (C2)-[(it)]->(C1), (C1)-[(id)]->(C0), (C0)-[(t)]->(C1) ] mor := PreComposeList( L ); -#! (C2)-[(is*id*t)]->(C1) +#! (C2)-[(it*pt*is)]->(C1) DecompositionOfMorphismInCategory( mor ); -#! [ (C2)-[(is)]->(C1), (C1)-[(id)]->(C0), (C0)-[(t)]->(C1) ] +#! [ (C2)-[(it)]->(C1), (C1)-[(pt)]->(C2), (C2)-[(is)]->(C1) ] NL := N( mor ); #! |7| → |26| Display( NL ); diff --git a/FunctorCategories/examples/CategoryFromNerveData.g b/FunctorCategories/examples/CategoryFromNerveData.g index 0168d9c08..fa8ec616c 100644 --- a/FunctorCategories/examples/CategoryFromNerveData.g +++ b/FunctorCategories/examples/CategoryFromNerveData.g @@ -6,15 +6,17 @@ LoadPackage( "FunctorCategories" ); #! @Example Delta2 := CategoryFromNerveData( SimplicialCategoryTruncatedInDegree( 2 ) ); -#! FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations +#! PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] N := NerveTruncatedInDegree2( Delta2 ); -#! C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations, +#! IsWellDefined( N ); #! true diff --git a/FunctorCategories/examples/FinBouquets.g b/FunctorCategories/examples/FinBouquets.g index 38a558e29..844bcb4ec 100644 --- a/FunctorCategories/examples/FinBouquets.g +++ b/FunctorCategories/examples/FinBouquets.g @@ -8,7 +8,7 @@ LoadPackage( "FunctorCategories" ); FinBouquets; #! FinBouquets C := UnderlyingCategory( FinBouquets ); -#! FreeCategory( RightQuiver( "q(P,L)[b:P->L]" ) ) +#! PathCategory( FinQuiver( "q(P,L)[b:P-≻L]" ) ) P := FinBouquets.P; #! Display( P ); diff --git a/FunctorCategories/examples/NerveTruncatedInDegree2.g b/FunctorCategories/examples/NerveTruncatedInDegree2.g index da05d3930..0624c651e 100644 --- a/FunctorCategories/examples/NerveTruncatedInDegree2.g +++ b/FunctorCategories/examples/NerveTruncatedInDegree2.g @@ -1,29 +1,37 @@ #! @BeginChunk NerveTruncatedInDegree2 -LoadPackage( "FunctorCategories" ); +LoadPackage( "FunctorCategories", false ); #! We compute the nerve of the full subcategory of the simplicial category $\Delta$ on the objects $[0], [1], [2]$. #! @Example Delta2 := SimplicialCategoryTruncatedInDegree( 2 ); -#! FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations -RelationsOfFpCategory( Delta2 ); -#! [ [ (s*id), (C0) ], [ (t*id), (C0) ], -#! [ (ps*is), (C1) ], [ (pt*it), (C1) ], -#! [ (is*id), (it*id) ], [ (pt*is), (id*t) ], -#! [ (ps*it), (id*s) ], [ (s*pt), (t*ps) ], -#! [ (s*mu), (s*ps) ], [ (t*mu), (t*pt) ], -#! [ (mu*is), (C1) ], [ (mu*it), (C1) ] ] +#! PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] +DefiningRelations( Delta2 ); +#! [ [ s⋅id:(C0) -≻ (C0), id(C0):(C0) -≻ (C0) ], +#! [ t⋅id:(C0) -≻ (C0), id(C0):(C0) -≻ (C0) ], +#! [ ps⋅is:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ pt⋅it:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ is⋅id:(C2) -≻ (C0), it⋅id:(C2) -≻ (C0) ], +#! [ pt⋅is:(C1) -≻ (C1), id⋅t:(C1) -≻ (C1) ], +#! [ ps⋅it:(C1) -≻ (C1), id⋅s:(C1) -≻ (C1) ], +#! [ s⋅pt:(C0) -≻ (C2), t⋅ps:(C0) -≻ (C2) ], +#! [ s⋅mu:(C0) -≻ (C2), s⋅ps:(C0) -≻ (C2) ], +#! [ t⋅mu:(C0) -≻ (C2), t⋅pt:(C0) -≻ (C2) ], +#! [ mu⋅is:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ mu⋅it:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ] ] Size( Delta2 ); #! 31 N := NerveTruncatedInDegree2( Delta2 ); -#! C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations, +#! IsWellDefined( N ); #! true @@ -46,10 +54,11 @@ Display( N.id ); IntCat := CategoryOfInternalCategories( RangeCategoryOfHomomorphismStructure( Delta2 ) ); #! FullSubcategoryByObjectMembershipFunction( -#! PreSheaves( FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations, +#! PreSheaves( PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ], #! SkeletalFinSets ), ObjectMembershipFunction ) IsWellDefined( N / IntCat ); #! true diff --git a/FunctorCategories/examples/YonedaComposition.g b/FunctorCategories/examples/YonedaComposition.g index 408a32702..4180b821c 100644 --- a/FunctorCategories/examples/YonedaComposition.g +++ b/FunctorCategories/examples/YonedaComposition.g @@ -6,58 +6,69 @@ LoadPackage( "FunctorCategories" ); #! @Example Delta2 := SimplicialCategoryTruncatedInDegree( 2 ); -#! FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations -RelationsOfFpCategory( Delta2 ); -#! [ [ (s*id), (C0) ], [ (t*id), (C0) ], -#! [ (ps*is), (C1) ], [ (pt*it), (C1) ], -#! [ (is*id), (it*id) ], [ (pt*is), (id*t) ], -#! [ (ps*it), (id*s) ], [ (s*pt), (t*ps) ], -#! [ (s*mu), (s*ps) ], [ (t*mu), (t*pt) ], -#! [ (mu*is), (C1) ], [ (mu*it), (C1) ] ] +#! PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ] +DefiningRelations( Delta2 ); +#! [ [ s⋅id:(C0) -≻ (C0), id(C0):(C0) -≻ (C0) ], +#! [ t⋅id:(C0) -≻ (C0), id(C0):(C0) -≻ (C0) ], +#! [ ps⋅is:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ pt⋅it:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ is⋅id:(C2) -≻ (C0), it⋅id:(C2) -≻ (C0) ], +#! [ pt⋅is:(C1) -≻ (C1), id⋅t:(C1) -≻ (C1) ], +#! [ ps⋅it:(C1) -≻ (C1), id⋅s:(C1) -≻ (C1) ], +#! [ s⋅pt:(C0) -≻ (C2), t⋅ps:(C0) -≻ (C2) ], +#! [ s⋅mu:(C0) -≻ (C2), s⋅ps:(C0) -≻ (C2) ], +#! [ t⋅mu:(C0) -≻ (C2), t⋅pt:(C0) -≻ (C2) ], +#! [ mu⋅is:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ], +#! [ mu⋅it:(C1) -≻ (C1), id(C1):(C1) -≻ (C1) ] ] Size( Delta2 ); #! 31 Ypt := YonedaProjection( Delta2 ); -#! C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations, +#! IsWellDefined( Ypt ); #! true Ymu := YonedaComposition( Delta2 ); -#! C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations, +#! IsWellDefined( Ymu ); #! true Ys := YonedaFibration( Delta2 ); -#! C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations, +#! IsWellDefined( Ys ); #! true Display( Ys ); -#! Image of <(C0)>: +#! Image of (C0): #! { 0, 1, 2 } ⱶ[ 0, 1, 2 ]→ { 0, 1, 2 } #! -#! Image of <(C1)>: +#! Image of (C1): #! { 0,..., 8 } ⱶ[ 0, 0, 1, 1, 1, 2, 2, 2, 2 ]→ { 0, 1, 2 } #! -#! Image of <(C2)>: +#! Image of (C2): #! { 0,..., 18 } ⱶ[ 0, 0, 0, 1, 1, 1, 1, 1, 1, #! 2, 2, 2, 2, 2, 2, 2, 2, 2, 2 ]→ { 0, 1, 2 } #! -#! A morphism in FunctorCategory( FreeCategory( RightQuiver( -#! "Delta(C0,C1,C2)[id:C1->C0,s:C0->C1,t:C0->C1, -#! is:C2->C1,it:C2->C1, -#! ps:C1->C2,pt:C1->C2,mu:C1->C2]" ) ) / relations, +#! A morphism in FunctorCategory( PathCategory( FinQuiver( +#! "Delta(C0,C1,C2)[id:C1-≻C0,s:C0-≻C1,t:C0-≻C1, +#! is:C2-≻C1,it:C2-≻C1, +#! ps:C1-≻C2,pt:C1-≻C2,mu:C1-≻C2]" ) ) +#! / [ s⋅id = id(C0), t⋅id = id(C0), ps⋅is = id(C1), ... ], #! SkeletalFinSets ) given by the above data #! @EndExample #! @EndChunk diff --git a/FunctorCategories/examples/notebooks/DPO_Quivers.ipynb b/FunctorCategories/examples/notebooks/DPO_Quivers.ipynb index de96088ce..ace771469 100644 --- a/FunctorCategories/examples/notebooks/DPO_Quivers.ipynb +++ b/FunctorCategories/examples/notebooks/DPO_Quivers.ipynb @@ -68,7 +68,7 @@ { "data": { "text/plain": [ - "GAP: FiniteCocompletion( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ) )" + "GAP: FiniteCocompletion( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ) )" ] }, "execution_count": 4, @@ -89,7 +89,7 @@ { "data": { "text/plain": [ - "GAP: PreSheaves( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ), SkeletalFinSets )" + "GAP: PreSheaves( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ), SkeletalFinSets )" ] }, "execution_count": 5, diff --git a/FunctorCategories/examples/notebooks/FinBouquets.ipynb b/FunctorCategories/examples/notebooks/FinBouquets.ipynb index f8cb44b5f..0de00a278 100644 --- a/FunctorCategories/examples/notebooks/FinBouquets.ipynb +++ b/FunctorCategories/examples/notebooks/FinBouquets.ipynb @@ -100,7 +100,7 @@ { "data": { "text/plain": [ - "GAP: FreeCategory( RightQuiver( \"q(P,L)[b:P->L]\" ) )" + "GAP: PathCategory( FinQuiver( \"q(P,L)[b:P-≻L]\" ) )" ] }, "execution_count": 5, @@ -121,7 +121,7 @@ { "data": { "text/plain": [ - "GAP: FiniteCocompletion( FreeCategory( RightQuiver( \"q(P,L)[b:P->L]\" ) ) )" + "GAP: FiniteCocompletion( PathCategory( FinQuiver( \"q(P,L)[b:P-≻L]\" ) ) )" ] }, "execution_count": 6, @@ -142,7 +142,7 @@ { "data": { "text/plain": [ - "GAP: PreSheaves( FreeCategory( RightQuiver( \"q(P,L)[b:P->L]\" ) ), SkeletalFinSets )" + "GAP: PreSheaves( PathCategory( FinQuiver( \"q(P,L)[b:P-≻L]\" ) ), SkeletalFinSets )" ] }, "execution_count": 7, diff --git a/FunctorCategories/examples/notebooks/LogicInToposOfFinQuivers.ipynb b/FunctorCategories/examples/notebooks/LogicInToposOfFinQuivers.ipynb index cf9f7c686..07163adbc 100644 --- a/FunctorCategories/examples/notebooks/LogicInToposOfFinQuivers.ipynb +++ b/FunctorCategories/examples/notebooks/LogicInToposOfFinQuivers.ipynb @@ -125,7 +125,7 @@ { "data": { "text/plain": [ - "GAP: FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) )" + "GAP: PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) )" ] }, "execution_count": 5, @@ -146,7 +146,7 @@ { "data": { "text/plain": [ - "GAP: FiniteCocompletion( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ) )" + "GAP: FiniteCocompletion( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ) )" ] }, "execution_count": 6, @@ -177,7 +177,7 @@ { "data": { "text/plain": [ - "GAP: PreSheaves( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ), SkeletalFinSets )" + "GAP: PreSheaves( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ), SkeletalFinSets )" ] }, "execution_count": 7, @@ -693,9 +693,9 @@ "Image of (V)-[(t)]->(A):\n", "∅ ⱶ[ ]→ { 0 }\n", "\n", - "An object in PreSheaves( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ), SkeletalFinSets ) given by the above data\n", + "An object in PreSheaves( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ), SkeletalFinSets ) given by the above data\n", "\n", - "An object in FiniteCocompletion( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ) ) given by the above data\n" + "An object in FiniteCocompletion( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ) ) given by the above data\n" ] } ], @@ -725,9 +725,9 @@ "Image of (V)-[(t)]->(A):\n", "{ 0 } ⱶ[ 1 ]→ { 0, 1 }\n", "\n", - "An object in PreSheaves( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ), SkeletalFinSets ) given by the above data\n", + "An object in PreSheaves( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ), SkeletalFinSets ) given by the above data\n", "\n", - "An object in FiniteCocompletion( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ) ) given by the above data\n" + "An object in FiniteCocompletion( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ) ) given by the above data\n" ] } ], @@ -760,9 +760,9 @@ "Image of <(A)>:\n", "∅ ⱶ[ ]→ { 0 }\n", "\n", - "A morphism in PreSheaves( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ), SkeletalFinSets ) given by the above data\n", + "A morphism in PreSheaves( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ), SkeletalFinSets ) given by the above data\n", "\n", - "A morphism in FiniteCocompletion( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ) ) given by the above data\n" + "A morphism in FiniteCocompletion( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ) ) given by the above data\n" ] } ], @@ -786,9 +786,9 @@ "Image of <(A)>:\n", "∅ ⱶ[ ]→ { 0 }\n", "\n", - "A morphism in PreSheaves( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ), SkeletalFinSets ) given by the above data\n", + "A morphism in PreSheaves( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ), SkeletalFinSets ) given by the above data\n", "\n", - "A morphism in FiniteCocompletion( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ) ) given by the above data\n" + "A morphism in FiniteCocompletion( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ) ) given by the above data\n" ] } ], @@ -1554,9 +1554,9 @@ "Image of (V)-[(t)]->(A):\n", "{ 0,..., 8 } ⱶ[ 1, 2, 3, 0, 5, 5, 7, 4, 7 ]→ { 0,..., 7 }\n", "\n", - "An object in PreSheaves( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ), SkeletalFinSets ) given by the above data\n", + "An object in PreSheaves( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ), SkeletalFinSets ) given by the above data\n", "\n", - "An object in FiniteCocompletion( FreeCategory( RightQuiver( \"q(V,A)[s:V->A,t:V->A]\" ) ) ) given by the above data\n" + "An object in FiniteCocompletion( PathCategory( FinQuiver( \"q(V,A)[s:V-≻A,t:V-≻A]\" ) ) ) given by the above data\n" ] } ], diff --git a/FunctorCategories/gap/CategoryOfBouquets.gi b/FunctorCategories/gap/CategoryOfBouquets.gi index b432413e2..44d7e8f79 100644 --- a/FunctorCategories/gap/CategoryOfBouquets.gi +++ b/FunctorCategories/gap/CategoryOfBouquets.gi @@ -6,7 +6,7 @@ ## BindGlobal( "QuiverOfCategoryOfBouquets", - RightQuiver( "q(P,L)[b:P->L]" ) ); + FinQuiver( "q(P,L)[b:P->L]" ) ); ## InstallOtherMethodForCompilerForCAP( CreateBouquet, @@ -99,7 +99,7 @@ InstallMethod( CategoryOfBouquetsEnrichedOver, morphism_datum := { Bouquets, m } -> DefiningPairOfBouquetMorphismEnrichedOverSkeletalFinSets( m ); ## building the categorical tower: - F := FreeCategory( QuiverOfCategoryOfBouquets : range_of_HomStructure := category_of_skeletal_finsets, FinalizeCategory := true ); + F := PathCategory( QuiverOfCategoryOfBouquets : range_of_HomStructure := category_of_skeletal_finsets, FinalizeCategory := true ); F := CategoryFromDataTables( F : set_category_attribute_resolving_functions := true, FinalizeCategory := true ); diff --git a/FunctorCategories/gap/CategoryOfQuivers.gi b/FunctorCategories/gap/CategoryOfQuivers.gi index 3e834b80a..16b346586 100644 --- a/FunctorCategories/gap/CategoryOfQuivers.gi +++ b/FunctorCategories/gap/CategoryOfQuivers.gi @@ -106,7 +106,7 @@ InstallMethod( CategoryOfQuiversEnrichedOver, morphism_datum := { Quivers, m } -> DefiningPairOfQuiverMorphismEnrichedOverSkeletalFinSets( m ); ## building the categorical tower: - F := FreeCategory( QuiverOfCategoryOfQuivers : range_of_HomStructure := category_of_skeletal_finsets, FinalizeCategory := true ); + F := PathCategory( QuiverOfCategoryOfQuivers : range_of_HomStructure := category_of_skeletal_finsets, FinalizeCategory := true ); F := CategoryFromDataTables( F : set_category_attribute_resolving_functions := true, FinalizeCategory := true ); diff --git a/FunctorCategories/gap/FunctorCategories.gi b/FunctorCategories/gap/FunctorCategories.gi index 25b4b83d8..f259074f5 100644 --- a/FunctorCategories/gap/FunctorCategories.gi +++ b/FunctorCategories/gap/FunctorCategories.gi @@ -453,6 +453,10 @@ InstallMethodWithCache( FunctorCategory, if IsFpCategory( B ) then B_op := OppositeFpCategory( B : FinalizeCategory := true ); + elif IsPathCategory( B ) then + B_op := OppositePathCategory( B : FinalizeCategory := true ); + elif IsQuotientOfPathCategory( B ) then + B_op := OppositeQuotientOfPathCategory( B : FinalizeCategory := true ); elif IsCategoryFromNerveData( B ) then B_op := OppositeCategoryFromNerveData( B : FinalizeCategory := true ); elif IsCategoryFromDataTables( B ) then @@ -907,7 +911,7 @@ end ); ## InstallMethodForCompilerForCAP( YonedaProjection, - [ IsFpCategory and HasRangeCategoryOfHomomorphismStructure ], + [ IsCapCategory and IsFiniteCategory ], function ( B ) local Hom, Yepis, N1, N2, pt; @@ -942,7 +946,7 @@ end ); ## InstallMethodForCompilerForCAP( YonedaComposition, - [ IsFpCategory and HasRangeCategoryOfHomomorphismStructure ], + [ IsCapCategory and IsFiniteCategory ], function ( B ) local Hom, Yepis, H, N1, N2, mu; diff --git a/FunctorCategories/gap/PreSheaves.gi b/FunctorCategories/gap/PreSheaves.gi index 92ce0c197..d33ac94d4 100644 --- a/FunctorCategories/gap/PreSheaves.gi +++ b/FunctorCategories/gap/PreSheaves.gi @@ -322,6 +322,11 @@ InstallMethodWithCache( PreSheavesOfFpEnrichedCategory, A := PathAlgebra( A ); fi; relations := List( relations, a -> List( a, ai -> PathAsAlgebraElement( A, ai ) ) ); + elif IsPathCategory( B ) then + B_op := OppositePathCategory( B : FinalizeCategory := true ); + elif IsQuotientOfPathCategory( B ) then + B_op := OppositeQuotientOfPathCategory( B : FinalizeCategory := true ); + relations := DefiningRelations( B_op ); elif IsCategoryFromNerveData( B ) then B_op := OppositeCategoryFromNerveData( B : FinalizeCategory := true ); elif IsCategoryFromDataTables( B ) then @@ -921,6 +926,8 @@ InstallMethodWithCache( PreSheavesOfFpEnrichedCategory, fi; if ( IsFpCategory( B ) and HasIsFinitelyPresentedCategory( B ) and IsFinitelyPresentedCategory( B ) ) or + IsPathCategory( B ) or + IsQuotientOfPathCategory( B ) or IsCategoryFromNerveData( B ) or IsCategoryFromDataTables( B ) or (HasIsFiniteCategory and IsFiniteCategory)( B ) or @@ -987,6 +994,62 @@ InstallMethodWithCache( PreSheavesOfFpEnrichedCategory, end ); + elif IsPathCategory( B ) then + + AddIsWellDefinedForObjects( PSh, + function ( PSh, F ) + local B, D, objects, generating_morphisms; + + B := Source( PSh ); + D := Target( PSh ); + + objects := SetOfObjects( B ); + generating_morphisms := SetOfGeneratingMorphisms( B ); + + if not ForAll( objects, o -> IsWellDefinedForObjects( D, F( o ) ) ) then + return false; + elif not ForAll( generating_morphisms, m -> IsWellDefinedForMorphisms( D, F( m ) ) ) then + return false; + elif not ForAll( generating_morphisms, m -> IsEqualForObjects( D, F( Target( m ) ), Source( F( m ) ) ) ) then + return false; + elif not ForAll( generating_morphisms, m -> IsEqualForObjects( D, F( Source( m ) ), Target( F( m ) ) ) ) then + return false; + fi; + + return true; + + end ); + + elif IsQuotientOfPathCategory( B ) then + + AddIsWellDefinedForObjects( PSh, + function ( PSh, F ) + local B, D, objects, generating_morphisms; + + B := Source( PSh ); + D := Target( PSh ); + + objects := SetOfObjects( B ); + generating_morphisms := SetOfGeneratingMorphisms( B ); + + if not ForAll( objects, o -> IsWellDefinedForObjects( D, F( o ) ) ) then + return false; + elif not ForAll( generating_morphisms, m -> IsWellDefinedForMorphisms( D, F( m ) ) ) then + return false; + elif not ForAll( generating_morphisms, m -> IsEqualForObjects( D, F( Target( m ) ), Source( F( m ) ) ) ) then + return false; + elif not ForAll( generating_morphisms, m -> IsEqualForObjects( D, F( Source( m ) ), Target( F( m ) ) ) ) then + return false; + fi; + + F := ValuesOfPreSheaf( F ); + + F := CapFunctor( UnderlyingCategory( OppositeOfSource( PSh ) ), F[1], F[2], Target( PSh ) ); + + return ForAll( relations, m -> IsCongruentForMorphisms( D, F( m[1] ), F( m[2] ) ) ); + + end ); + elif IsAlgebroid( B ) then AddIsWellDefinedForObjects( PSh, @@ -2526,7 +2589,7 @@ InstallMethod( CategoryOfInternalCategories, function ( H ) local Delta2, sH, membership_function; - Delta2 := SimplicialCategoryTruncatedInDegree( 2 : FinalizeCategory := true ); + Delta2 := SimplicialCategoryTruncatedInDegree2; sH := PreSheaves( Delta2, H ); @@ -4465,7 +4528,7 @@ InstallMethodForCompilerForCAP( NerveTruncatedInDegree2, function ( B ) - return CreatePreSheafByValues( PreSheaves( SimplicialCategoryTruncatedInDegree( 2 ) ), NerveTruncatedInDegree2Data( B ) ); + return CreatePreSheafByValues( PreSheaves( SimplicialCategoryTruncatedInDegree2 ), NerveTruncatedInDegree2Data( B ) ); end ); @@ -4475,7 +4538,7 @@ InstallMethodForCompilerForCAP( NerveTruncatedInDegree2, function ( B ) - return CreatePreSheafByValues( PreSheaves( CategoryFromNerveData( SimplicialCategoryTruncatedInDegree( 2 ) ) ), NerveTruncatedInDegree2Data( B ) ); + return CreatePreSheafByValues( PreSheaves( CategoryFromNerveData( SimplicialCategoryTruncatedInDegree2 ) ), NerveTruncatedInDegree2Data( B ) ); end ); @@ -4485,7 +4548,27 @@ InstallMethodForCompilerForCAP( NerveTruncatedInDegree2, function ( B ) - return CreatePreSheafByValues( PreSheaves( CategoryFromDataTables( SimplicialCategoryTruncatedInDegree( 2 ) ) ), NerveTruncatedInDegree2Data( B ) ); + return CreatePreSheafByValues( PreSheaves( CategoryFromDataTables( SimplicialCategoryTruncatedInDegree2 ) ), NerveTruncatedInDegree2Data( B ) ); + +end ); + +## +InstallMethodForCompilerForCAP( NerveTruncatedInDegree2, + [ IsPathCategory ], + + function ( B ) + + return CreatePreSheafByValues( PreSheaves( SimplicialCategoryTruncatedInDegree2 ), NerveTruncatedInDegree2Data( B ) ); + +end ); + +## +InstallMethodForCompilerForCAP( NerveTruncatedInDegree2, + [ IsQuotientOfPathCategory ], + + function ( B ) + + return CreatePreSheafByValues( PreSheaves( SimplicialCategoryTruncatedInDegree2 ), NerveTruncatedInDegree2Data( B ) ); end );