Skip to content

Commit 1ec0f5b

Browse files
committedJun 4, 2023
relocated code
1 parent cffe240 commit 1ec0f5b

File tree

2 files changed

+33
-33
lines changed

2 files changed

+33
-33
lines changed
 

‎Toposes/doc/Doc.autodoc

+4-4
Original file line numberDiff line numberDiff line change
@@ -20,10 +20,6 @@ variations are implemented in the CAP-based package `CartesianCategories`.
2020

2121
@Section Heyting algebra of subobjects
2222

23-
@Section Lawvere-Tierney topologies
24-
25-
@InsertChunk LawvereTierney
26-
2723
@Section Pushout complements
2824

2925
@Subsection Example in FinSets
@@ -36,6 +32,10 @@ variations are implemented in the CAP-based package `CartesianCategories`.
3632

3733
@Section Double-pushout rewriting
3834

35+
@Section Lawvere-Tierney topologies
36+
37+
@InsertChunk LawvereTierney
38+
3939
@Section Add-methods
4040

4141
@Chapter Category of relations

‎Toposes/gap/Topos.gd

+29-29
Original file line numberDiff line numberDiff line change
@@ -546,6 +546,35 @@ DeclareOperation( "EmbeddingOfRelativePseudoComplementSubobject",
546546
DeclareOperation( "EmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication",
547547
[ IsCapCategoryMorphism, IsCapCategoryMorphism, IsCapCategoryObject ] );
548548

549+
###################################
550+
##
551+
#! @Section Pushout complements
552+
##
553+
###################################
554+
555+
#! @Description
556+
#! The arguments are two composable morphisms $l: K \rightarrow L$, $m: L \rightarrow G$.
557+
#! The output is <C>true</C> if there exists a morphism $d: K \rightarrow D$ and a morphism $g: D \rightarrow G$
558+
#! such that the four morphisms $l,d,m,g$ form a pushout diagram, i.e., such that
559+
#! $m$=<C>InjectionOfCofactorOfPushoutWithGivenPushout</C>([$l,d$], 1) and
560+
#! $g$=<C>InjectionOfCofactorOfPushoutWithGivenPushout</C>([$l,d$], 2).
561+
#! Otherwise the output is <C>false</C>.
562+
#! @Returns a boolean
563+
#! @Arguments l, m
564+
DeclareOperation( "HasPushoutComplement",
565+
[ IsCapCategoryMorphism, IsCapCategoryMorphism ] );
566+
567+
#! @Description
568+
#! The arguments are two composable morphisms $l: K \rightarrow L$, $m: L \rightarrow G$.
569+
#! The output is a morphism $d: K \rightarrow D$ such that there exists a morphism $g: D \rightarrow G$
570+
#! turing the four morphisms $l,d,m,g$ into a pushout diagram, i.e., such that
571+
#! $m$=<C>InjectionOfCofactorOfPushoutWithGivenPushout</C>([$l,d$], 1) and
572+
#! $g$=<C>InjectionOfCofactorOfPushoutWithGivenPushout</C>([$l,d$], 2).
573+
#! @Returns a morphism
574+
#! @Arguments l, m
575+
DeclareOperation( "PushoutComplement",
576+
[ IsCapCategoryMorphism, IsCapCategoryMorphism ] );
577+
549578
###################################
550579
##
551580
#! @Section Lawvere-Tierney topologies
@@ -576,32 +605,3 @@ DeclareAttribute( "LawvereTierneySubobjects",
576605
#! @Arguments T
577606
DeclareAttribute( "LawvereTierneyEmbeddingsOfSubobjectClassifiers",
578607
IsCapCategory );
579-
580-
###################################
581-
##
582-
#! @Section Pushout complements
583-
##
584-
###################################
585-
586-
#! @Description
587-
#! The arguments are two composable morphisms $l: K \rightarrow L$, $m: L \rightarrow G$.
588-
#! The output is <C>true</C> if there exists a morphism $d: K \rightarrow D$ and a morphism $g: D \rightarrow G$
589-
#! such that the four morphisms $l,d,m,g$ form a pushout diagram, i.e., such that
590-
#! $m$=<C>InjectionOfCofactorOfPushoutWithGivenPushout</C>([$l,d$], 1) and
591-
#! $g$=<C>InjectionOfCofactorOfPushoutWithGivenPushout</C>([$l,d$], 2).
592-
#! Otherwise the output is <C>false</C>.
593-
#! @Returns a boolean
594-
#! @Arguments l, m
595-
DeclareOperation( "HasPushoutComplement",
596-
[ IsCapCategoryMorphism, IsCapCategoryMorphism ] );
597-
598-
#! @Description
599-
#! The arguments are two composable morphisms $l: K \rightarrow L$, $m: L \rightarrow G$.
600-
#! The output is a morphism $d: K \rightarrow D$ such that there exists a morphism $g: D \rightarrow G$
601-
#! turing the four morphisms $l,d,m,g$ into a pushout diagram, i.e., such that
602-
#! $m$=<C>InjectionOfCofactorOfPushoutWithGivenPushout</C>([$l,d$], 1) and
603-
#! $g$=<C>InjectionOfCofactorOfPushoutWithGivenPushout</C>([$l,d$], 2).
604-
#! @Returns a morphism
605-
#! @Arguments l, m
606-
DeclareOperation( "PushoutComplement",
607-
[ IsCapCategoryMorphism, IsCapCategoryMorphism ] );

0 commit comments

Comments
 (0)
Please sign in to comment.