An elementary topos is a finite complete, cartesian closed category with a subobject classifier. It follows that an elementary topos is also a finitely cocomplete Heyting category.
The doctrines of (co)cartesian (co)closed categories and their variations are implemented in the CAP-based package CartesianCategories.
‣ ExactCoverWithGlobalElements( a ) | ( attribute ) |
Returns: a list of morphisms in \(\mathrm{Hom}( t, a )\)
The argument is an object a of a category \(\mathbf{C}\) which is enriched over itself, i.e., \(\mathbf{C}\) = RangeCategoryOfHomomorphismStructure( \(\mathbf{C}\) ). The output is a list \(D\) of global elements of a (i.e., morphisms from the distinguished object \(t :=\)DistinguishedObjectOfHomomorphismStructure( \(\mathbf{C}\) ) to a), such that UniversalMorphismFromCoproduct(a, \(D\)) is an isomorphism.
‣ IndexOfNonliftableMorphismFromDistinguishedObject( iota ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( t, \mathrm{Target}( \iota ) )\)
The argument is a nonepimorphic monomorphism iota of a category \(\mathbf{C}\) which is enriched over itself, i.e., \(\mathbf{C}\) = RangeCategoryOfHomomorphismStructure( \(\mathbf{C}\) ). The output is a positive integer, namely the position of a morphism \(\tau\) in the list ExactCoverWithGlobalElements( Range( iota ) ) of morphisms from the distinguished object \(t :=\)DistinguishedObjectOfHomomorphismStructure( \(\mathbf{C}\) ) to Range( iota ), such that IsLiftableAlongMonomorphism( iota, \(\tau\) ) = false.
‣ NonliftableMorphismFromDistinguishedObject( iota ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( t, \mathrm{Target}( \iota ) )\)
The argument is a nonepimorphic monomorphism iota of a category \(\mathbf{C}\) which is enriched over itself, i.e., \(\mathbf{C}\) = RangeCategoryOfHomomorphismStructure( \(\mathbf{C}\) ). The output is a morphism \(\tau\) from the distinguished object \(t :=\)DistinguishedObjectOfHomomorphismStructure( \(\mathbf{C}\) ) to Range( iota ), such that IsLiftableAlongMonomorphism( iota, \(\tau\) ) = false.
‣ IsElementaryTopos( C ) | ( property ) |
Returns: true or false
The property of the category C being an elementary topos.
A subobject classifier consists of three parts:
an object \(\Omega\),
a function \(\mathrm{true}\) providing a morphism \(\mathrm{true}: 1 \rightarrow \Omega\),
a function \(\chi\) mapping each monomorphism \(i : A \rightarrow S\) to a morphism \(\chi_i : S \to \Omega\).
The triple \((\Omega,\mathrm{true},\chi)\) is called a subobject classifier if for each monomorphism \(i : A \to S\), the morphism \(\chi_i : S \to \Omega\) is the unique morphism such that \(\chi_i \circ i = \mathrm{true} \circ \ast\) determine a pullback diagram.
‣ SubobjectClassifier( C ) | ( attribute ) |
Returns: an object
The argument is a category \(C\). The output is the subobject classifier object \(\Omega\) of \(C\).
‣ CartesianSquareOfSubobjectClassifier( C ) | ( attribute ) |
Returns: an object
The argument is a category \(C\). The output is the cartesian square of the subobject classifier object \Omega of \(C\).
‣ ClassifyingMorphismOfSubobject( m ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{Target}(m), \mathrm{SubobjectClassifier} )\)
The argument is a monomorphism \(m : A \rightarrow S\). The output is its classifying morphism \(\chi_m : S \rightarrow \mathrm{SubobjectClassifier}\).
‣ ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier( m, omega ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{Target}(m), \mathrm{SubobjectClassifier} )\)
The arguments are a monomorphism \(m : A \rightarrow S\) and the subobject classifier \(\Omega\). The output is the classifying morphism of the monomorphism \(\chi_m : S \rightarrow \mathrm{SubobjectClassifier}\).
‣ SubobjectOfClassifyingMorphism( chi ) | ( attribute ) |
Returns: a monomorphism in \(\mathrm{Hom}( A, S )\)
The argument is a classifying morphism \(\chi : S \rightarrow \Omega\). The output is the subobject monomorphism of the classifying morphism, \(m : A \rightarrow S\).
‣ ListOfSubobjects( A ) | ( attribute ) |
Returns: a list of monomorphisms into \(A\).
The argument is an object A. The output is a list of all subobjects of A.
‣ TruthMorphismOfTrue( C ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{SubobjectClassifier} )\)
The argument is a category \(C\). The output is the truth morphism \(\mathrm{true}: \mathrm{TerminalObject} \rightarrow \mathrm{SubobjectClassifier}\).
‣ TruthMorphismOfTrueWithGivenObjects( T, Omega ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( T, \Omega )\)
The arguments are the terminal object of the category and the subobject classifier. The output is the truth morphism \(\mathrm{true}: T \rightarrow \Omega\).
‣ TruthMorphismOfFalse( C ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{SubobjectClassifier} )\)
The argument is a category \(C\). The output is the truth morphism \(\mathrm{false}: \mathrm{TerminalObject} \rightarrow \mathrm{SubobjectClassifier}\).
‣ TruthMorphismOfFalseWithGivenObjects( T, Omega ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( T, \Omega )\)
The arguments are the terminal object T of the category and the subobject classifier Omega. The output is the truth morphism \(\mathrm{false}: T \rightarrow \Omega\).
‣ TruthMorphismOfNot( C ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{SubobjectClassifier}, \mathrm{SubobjectClassifier} )\)
The argument is a category \(C\). The output is the truth endomorphism \(\mathrm{not}: \mathrm{SubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}\).
‣ TruthMorphismOfNotWithGivenObjects( Omega, Omega ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \Omega, \Omega )\)
The arguments are a subobject classifier Omega as first and as second argument. The output is the truth endomorphism \(\mathrm{not}: \Omega \rightarrow \Omega\).
‣ TruthMorphismOfAnd( C ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{CartesianSquareOfSubobjectClassifier}, \mathrm{SubobjectClassifier} )\)
The argument is a category \(C\). The output is the truth morphism \(\mathrm{and}: \mathrm{CartesianSquareOfSubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}\).
‣ TruthMorphismOfAndWithGivenObjects( Omega2, Omega ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \Omega^{\times 2}, \Omega )\)
The arguments are the cartesian square Omega^{\times 2} of a subobject classifier Omega of the category and the subobject classifier. The output is the truth morphism \(\mathrm{and}: \Omega^{\times 2} \rightarrow \Omega\).
‣ TruthMorphismOfOr( C ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{CartesianSquareOfSubobjectClassifier}, \mathrm{SubobjectClassifier} )\)
The argument is a category \(C\). The output is the truth morphism \(\mathrm{or}: \mathrm{CartesianSquareOfSubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}\).
‣ TruthMorphismOfOrWithGivenObjects( Omega2, Omega ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \Omega^{\times 2}, \Omega )\)
The arguments are the cartesian square Omega^{\times 2} of a subobject classifier Omega of the category and the subobject classifier. The output is the truth morphism \(\mathrm{or}: \Omega^{\times 2} \rightarrow \Omega\).
‣ TruthMorphismOfImplies( C ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{CartesianSquareOfSubobjectClassifier}, \mathrm{SubobjectClassifier} )\)
The argument is a category \(C\). The output is the truth morphism \(\mathrm{implies}: \mathrm{CartesianSquareOfSubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}\).
‣ TruthMorphismOfImpliesWithGivenObjects( Omega2, Omega ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( \Omega^{\times 2}, \Omega )\)
The arguments are the cartesian square Omega^{\times 2} of a subobject classifier Omega of the category and the subobject classifier. The output is the truth morphism \(\mathrm{implies}: \Omega^{\times 2} \rightarrow \Omega\).
‣ PowerObject( a ) | ( attribute ) |
Returns: an object
The argument is an object a. The output is the power object \(P(a)\) of a.
‣ PowerObjectFunctorial( f ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}(b), \mathrm{PowerObject}(a) )\)
The argument is a morphism f\(:a \to b\). The output is the power morphism of \(P(f): P(b) \to P(a)\).
gap> LoadPackage( "FinSetsForCAP" ); true gap> a := FinSet( 3 ); |3| gap> b := FinSet( 4 ); |4| gap> f := MapOfFinSets( a, [ 0, 1, 1 ], b ); |3| → |4| gap> Pf := PowerObjectFunctorial( f ); |16| → |8| gap> Display( Pf ); { 0,..., 15 } ⱶ[ 0, 1, 6, 7, 0, 1, 6, 7, 0, 1, 6, 7, 0, 1, 6, 7 ]→ { 0,..., 7 }
‣ PowerObjectFunctorialWithGivenPowerObjects( Pb, f, Pa ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( Pb, Pa )\)
The arguments are an object Pb, a morphism \(f:a \to b\), and object Pa, such that Pa\(= P(a)\) and Pb\(= P(b)\). The output is the power morphism of \(P(f): Pb \to Pa\).
‣ PowerObjectRightEvaluationMorphism( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( a \times \mathrm{PowerObject}(a), \Omega )\)
The argument is an object a. The output is the power object right evaluation morphism of \(\epsilon_a: a \times P(a) \to \Omega\), where \(\Omega\) is the subobject classifier of CapCategory(a).
‣ PowerObjectRightEvaluationMorphismWithGivenObjects( axPa, a, Omega ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( axPa, Omega )\)
The arguments are three objects Pa_xa, a, and Omega, such that axPa\(= a \times P(a)\) and Omega the subobject classifier of CapCategory(a). The output is the power object right evaluation morphism of \(\epsilon_a:\) axPa \(\to\) Omega.
‣ PowerObjectLeftEvaluationMorphism( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}(a) \times a, \Omega )\)
The argument is an object a. The output is the power object left evaluation morphism of \(\epsilon_a: P(a) \times a \to \Omega\), where \(\Omega\) is the subobject classifier of CapCategory(a).
‣ PowerObjectLeftEvaluationMorphismWithGivenObjects( Pa_xa, a, Omega ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( Pa_xa, Omega )\)
The arguments are three objects Pa_xa, a, and Omega, such that Pa_xa\(= P(a) \times a\) and Omega the subobject classifier of CapCategory(a). The output is the power object left evaluation morphism of \(\epsilon_a:\) Pa_xa \(\to\) Omega.
‣ PRightTransposeMorphism( a, b, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, P(a) )\)
The arguments are two objects a, b, a morphism f: a \(\times\) b \(\to \Omega\), where \(\Omega\) is the subobject classifier of CapCategory(f). The output is the \(P\)-right-transpose morphism b \(\to P(a)\), where \(P(a) =\) PowerObject( a ).
‣ PRightTransposeMorphismWithGivenRange( a, b, f, Pa ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, Pa )\)
The arguments are two objects a, b, a morphism f: a \(\times\) b \(\to \Omega\), and an object Pa, where \(\Omega\) is the subobject classifier of CapCategory(f) and Pa = PowerObject( a ). The output is the \(P\)-right-transpose morphism b \(\to\) Pa.
‣ PLeftTransposeMorphism( a, b, f ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, P(b) )\)
The arguments are two objects a, b, a morphism f: a \(\times\) b \(\to \Omega\), where \(\Omega\) is the subobject classifier of CapCategory(f). The output is the \(P\)-left-transpose morphism a \(\to P(b)\), where \(P(b) =\) PowerObject( b ).
‣ PLeftTransposeMorphismWithGivenRange( a, b, f, Pb ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, Pb )\)
The arguments are two objects a, b, a morphism f: a \(\times\) b \(\to \Omega\), and an object Pb, where \(\Omega\) is the subobject classifier of CapCategory(f) and Pb = PowerObject( b ). The output is the \(P\)-left-transpose morphism a \(\to\) Pb.
‣ UpperSegmentOfRelation( a, b, mu ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, \mathrm{PowerObject}( b ) )\)
The arguments are two objects a, b in a category \(C\) and a monomorphism mu\(: r \hookrightarrow a \times b\) defining a relation on \(a \times b\). The output is the upper segment of the relation which is a morphism \(a \to Pb\) given by the adjunction, where \(Pb\) := PowerObject( b ) is the the power object of b.
‣ UpperSegmentOfRelationWithGivenRange( a, b, mu, Pb ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, Pb )\)
The arguments are two objects a, b in a category \(C\), a monomorphism mu\(: r \hookrightarrow a \times b\) defining a relation on \(a \times b\), and the power object Pb := PowerObject( b ) of b. The output is the upper segment of the relation which is a morphism \(a \to Pb\) given by the adjunction.
‣ LowerSegmentOfRelation( a, b, mu ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, \mathrm{PowerObject}( a ) )\)
The arguments are two objects a, b in a category \(C\) and a monomorphism mu\(:r \hookrightarrow a \times b\) defining a relation on \(a \times b\). The output is the lower segment of the relation which is a morphism \(b \to Pa\) given by the adjunction, where \(Pa\) := PowerObject( a ) is the the power object of a.
‣ LowerSegmentOfRelationWithGivenRange( a, b, mu, Pa ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( b, Pa )\)
The arguments are two objects a, b in a category \(C\), a monomorphism mu\(:r \hookrightarrow a \times b\) defining a relation on \(a \times b\), and the power object Pa := PowerObject( a ) of a. The output is the lower segment of the relation which is a morphism \(b \to Pa\) given by the adjunction.
‣ SingletonMorphism( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( a, \mathrm{PowerObject}(a) )\)
The argument is an object a. The output is the singleton morphism from a to the power object \(\mathrm{PowerObject}(a)\).
gap> LoadPackage( "FinSetsForCAP" ); true gap> sFinSets := SkeletalCategoryOfFiniteSets( : no_precompiled_code := true ); SkeletalFinSets gap> a := BigInt( 3 ) / sFinSets; |3| gap> sa := SingletonMorphism( a ); |3| ↪ |8| gap> Display( sa ); { 0, 1, 2 } ⱶ[ 1, 2, 4 ]→ { 0,..., 7 } gap> sa = UpperSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) ); true gap> sa = LowerSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) ); true
‣ SingletonMorphismWithGivenPowerObject( a, Pa ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( a, Pa )\)
The arguments are an object a and an object Pa which is equal to the power object \(\mathrm{PowerObject}(a)\). The output is the singleton morphism from a to Pa.
‣ IsomorphismOntoCartesianSquareOfPowerObject( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{Exponential}( a, \mathrm{CartesianSquareOfSubobjectClassifier}( C ) ), \mathrm{DirectProduct}( \mathrm{PowerObject}(a), \mathrm{PowerObject}(a) ) )\)
The argument is an object a in a category \(C\). The output is the isomorphism \(\mathrm{Exponential}( a, \mathrm{CartesianSquareOfSubobjectClassifier}( C ) ) \rightarrow \mathrm{DirectProduct}( \mathrm{PowerObject}(a), \mathrm{PowerObject}(a) )\).
gap> LoadPackage( "FinSetsForCAP" ); true gap> a := FinSet( 2 ); |2| gap> ia := IsomorphismOntoCartesianSquareOfPowerObject( a ); |16| ⭇ |16| gap> Display( ia ); { 0,..., 15 }\ ⱶ[ 0, 1, 4, 5, 2, 3, 6, 7, 8, 9, 12, 13, 10, 11, 14, 15 ]→ { 0,..., 15 }
‣ IsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects( Exp_a_Omega2, a, PaxPa ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( Exp\_a\_Omega2, PaxPa )\)
The arguments are an object the exponential Exp_a_Omega2 = Exponential( a, CartesianSquareOfSubobjectClassifier ), an object a in a category \(C\), and the cartesian squre PaxPa of the power object PowerObject( a ). The output is the isomorphism \(Exp\_a\_Omega2 \stackrel{\sim}{\rightarrow} PaxPa\)
‣ IntersectWithPreimagesWithGivenObjects( PAxB, f, PA ) | ( operation ) |
Returns: a morphism \(\mathrm{Hom}( PAxB, PA )\)
The input is the direct product PAxB = PA \(\times B\), a morphism f: \(A \to B\), and the power object PA = PowerObject(\(A\)). The output is the morphism PAxB \(\rightarrow\) PA, \((T, b) \mapsto T \cap f^{-1}(b)\).
‣ EmbeddingOfRelativePowerObject( f ) | ( attribute ) |
Returns: a monomorphism \(\mathrm{Hom}( P_fa, Pa \times b )\)
The input is a morphism f: \(a \to b\). The output is the embedding of the relative power object \(P_fa \hookrightarrow Pa \times b\), where \(Pa\) = PowerObject(\(a\)).
‣ RelativePowerObjectFibrationMorphism( f ) | ( attribute ) |
Returns: a monomorphism \(\mathrm{Hom}( P_fa, b )\)
The input is a morphism f: \(a \to b\). The output is the fibration morphism \(P_f: P_fa \rightarrow \times b\), where is \(P_fa\) the relative power object of f.
‣ RelativePowerObjectLeftEvaluationMorphism( f ) | ( attribute ) |
Returns: a monomorphism \(\mathrm{Hom}( P_fa \times a, \Omega \times b )\)
The input is a morphism f: \(a \to b\). The output is the evaluation morphism \(P_fa \times a \rightarrow \Omega \times b\), where \(P_fa\) is the relative power object of f.
‣ RightFiberMorphism( b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( c \times P(b \times c), P(b) )\)
The arguments are two objects b, c. The output is the morphism c \(\times\) PowerObject(b \times c) \(\to\) PowerObject( b ) that for a given relation \(R \subseteq\) b \(\times\) c and an element \(y\) in the base c computes the fiber over \(y\) as subset of b.
gap> LoadPackage( "FinSetsForCAP", false ); true gap> a := FinSet( 3 ); |3| gap> b := FinSet( 2 ); |2| gap> right := RightFiberMorphism( a, b ); |128| → |8| gap> LoadPackage( "LazyCategories", false ); true gap> L := LazyCategory( SkeletalFinSets : primitive_operations := true ); LazyCategory( SkeletalFinSets ) gap> lazy_right := RightFiberMorphism( a / L, b / L ); <A morphism in LazyCategory( SkeletalFinSets )>
‣ RightFiberMorphismWithGivenObjects( cxPbxc, b, c, Pb ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( cxPbxc, Pb )\)
The arguments are four objects cxPbxc, b, c, Pb, where cxPbxc = \(c \times P(b \times c)\) and Pb = PowerObject( b ). The output is the morphism that for a given relation \(R \subseteq\) b \(\times\) c and an element \(y\) in the base c computes the fiber over \(y\) as subset of b.
‣ LeftFiberMorphism( b, c ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( P(b \times c) \times b, P(c) )\)
The arguments are two objects b, c. The output is the morphism PowerObject(b \times c) \(\times\) b \(\to\) PowerObject( c ) that for a given relation \(R \subseteq\) b \(\times\) c and an element \(x\) in the base b computes the fiber over \(x\) as subset of c.
gap> LoadPackage( "FinSetsForCAP", false ); true gap> a := FinSet( 2 ); |2| gap> b := FinSet( 3 ); |3| gap> left := LeftFiberMorphism( a, b ); |128| → |8| gap> LoadPackage( "LazyCategories", false ); true gap> L := LazyCategory( SkeletalFinSets : primitive_operations := true ); LazyCategory( SkeletalFinSets ) gap> lazy_left := LeftFiberMorphism( a / L, b / L ); <A morphism in LazyCategory( SkeletalFinSets )>
‣ LeftFiberMorphismWithGivenObjects( Pbxc_xb, b, c, Pc ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( Pbxc_xb, Pc )\)
The arguments are four objects Pbxc_xb, b, c, Pc, where Pbxc_xb = \(P(b \times c) \times b\) and Pc = PowerObject( c ). The output is the morphism that for a given relation \(R \subseteq\) b \(\times\) c and an element \(x\) in the base b computes the fiber over \(x\) as subset of c.
‣ SingletonSupportOfRelationsWithGivenObjects( Pbxc, b, c, Pb ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( Pbxc, Pb )\)
Return the morphism that for a given relation \(R \subseteq\) b \(\times\) c computes the subset of b over which \(R\) is a singleton.
‣ RelativeTruthMorphismOfTrue( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{PowerObect}( a ) )\)
The argument is an object a in a category \(C\). The output is the relative truth morphism \(\mathrm{true}: \mathrm{TerminalObject} \rightarrow \mathrm{PowerObject}( a )\).
‣ RelativeTruthMorphismOfTrueWithGivenObjects( T, a, Pa ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( T, Pa )\)
The arguments are the terminal object of the category \(C\), an object a, and the power object Pa of a. The output is the relative truth morphism \(\mathrm{true}: T \rightarrow Pa\).
‣ RelativeTruthMorphismOfFalse( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{PowerObect}( a ) )\)
The argument is an object a in a category \(C\). The output is the relative truth morphism \(\mathrm{false}: \mathrm{TerminalObject} \rightarrow \mathrm{PowerObject}( a )\).
‣ RelativeTruthMorphismOfFalseWithGivenObjects( T, a, Pa ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( T, Pa )\)
The arguments are the terminal object of the category \(C\), an object a, and the power object Pa of a. The output is the relative truth morphism \(\mathrm{false}: T \rightarrow Pa\).
‣ RelativeTruthMorphismOfNot( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}( a ), \mathrm{PowerObect}( a ) )\)
The argument is an object a in a category \(C\). The output is the relative truth endomorphism \(\mathrm{not}: \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a )\).
‣ RelativeTruthMorphismOfNotWithGivenObjects( Pa, a, Pa ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( Pa, Pa )\)
The arguments are the power object Pa of a, the object a, and Pa. The output is the relative truth endomorphism \(\mathrm{not}: Pa \rightarrow Pa\).
‣ RelativeTruthMorphismOfAnd( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ), \mathrm{PowerObject}( a ) )\)
The argument is an object a in a category \(C\). The output is the relative truth morphism \(\mathrm{and}: \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a )\).
‣ RelativeTruthMorphismOfAndWithGivenObjects( PaxPa, a, Pa ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( PaxPa, Pa )\)
The arguments are the cartesian square PaxPa of the power object Pa of a, the object a, and Pa. The output is the relative truth morphism \(\mathrm{and}: PaxPa \rightarrow Pa\).
‣ RelativeTruthMorphismOfOr( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ), \mathrm{PowerObject}( a ) )\)
The argument is an object a in a category \(C\). The output is the relative truth morphism \(\mathrm{or}: \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a )\).
‣ RelativeTruthMorphismOfOrWithGivenObjects( PaxPa, a, Pa ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( PaxPa, Pa )\)
The arguments are the cartesian square PaxPa of the power object Pa of a, the object a, and Pa. The output is the relative truth morphism \(\mathrm{or}: PaxPa \rightarrow Pa\).
‣ RelativeTruthMorphismOfImplies( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ), \mathrm{PowerObject}( a ) )\)
The argument is an object a in a category \(C\). The output is the relative truth morphism \(\mathrm{implies}: \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a )\).
‣ RelativeTruthMorphismOfImpliesWithGivenObjects( PaxPa, a, Pa ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( PaxPa, Pa )\)
The arguments are the cartesian square PaxPa of the power object Pa of a, the object a, and Pa. The output is the relative truth morphism \(\mathrm{implies}: PaxPa \rightarrow Pa\).
gap> LoadPackage( "FinSetsForCAP" ); true gap> sFinSets := SkeletalFinSets; SkeletalFinSets gap> t := TerminalObject( sFinSets ); |1| gap> TruthMorphismOfFalse( sFinSets ) = RelativeTruthMorphismOfFalse( t ); true gap> TruthMorphismOfTrue( sFinSets ) = RelativeTruthMorphismOfTrue( t ); true gap> TruthMorphismOfNot( sFinSets ) = RelativeTruthMorphismOfNot( t ); true gap> TruthMorphismOfAnd( sFinSets ) = RelativeTruthMorphismOfAnd( t ); true gap> TruthMorphismOfOr( sFinSets ) = RelativeTruthMorphismOfOr( t ); true gap> TruthMorphismOfImplies( sFinSets ) = RelativeTruthMorphismOfImplies( t ); true gap> a := FinSet( 2 ); |2| gap> fPa := RelativeTruthMorphismOfFalse( a ); |1| → |4| gap> Display( fPa ); { 0 } ⱶ[ 0 ]→ { 0,..., 3 } gap> tPa := RelativeTruthMorphismOfTrue( a ); |1| → |4| gap> Display( tPa ); { 0 } ⱶ[ 3 ]→ { 0,..., 3 } gap> nPa := RelativeTruthMorphismOfNot( a ); |4| → |4| gap> Display( nPa ); { 0,..., 3 } ⱶ[ 3, 2, 1, 0 ]→ { 0,..., 3 } gap> aPa := RelativeTruthMorphismOfAnd( a ); |16| → |4| gap> Display( aPa ); { 0,..., 15 } ⱶ[ 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 2, 2, 0, 1, 2, 3 ]→ { 0,..., 3 } gap> oPa := RelativeTruthMorphismOfOr( a ); |16| → |4| gap> Display( oPa ); { 0,..., 15 } ⱶ[ 0, 1, 2, 3, 1, 1, 3, 3, 2, 3, 2, 3, 3, 3, 3, 3 ]→ { 0,..., 3 } gap> iPa := RelativeTruthMorphismOfImplies( a ); |16| → |4| gap> Display( iPa ); { 0,..., 15 } ⱶ[ 3, 2, 1, 0, 3, 3, 1, 1, 3, 2, 3, 2, 3, 3, 3, 3 ]→ { 0,..., 3 }
‣ PseudoComplementSubobject( iota ) | ( operation ) |
Returns: an object
The argument is a monomorphism \(\iota: S \hookrightarrow A\). The output is the pseudo-complement of \(S\) in \(A\)
, i.e., the pseudo-complement object of \(\iota\).
‣ EmbeddingOfPseudoComplementSubobject( iota ) | ( operation ) |
Returns: an object
The argument is a monomorphism \(\iota: S \hookrightarrow A\). The output is the embedding PseudoComplementSubobject(\(\iota\)) \(\hookrightarrow A\) of pseudo-complement object of \(\iota\).
‣ EmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement( iota ) | ( operation ) |
Returns: an object
The argument is a monomorphism \(\iota: S \hookrightarrow A\) and an object T with IsEqualForObjects(T, PseudoComplementSubobject(\(\iota\))). The output is the embedding of \(\iota:T \hookrightarrow A\) of pseudo-complement object T of \(\iota\).
‣ IntersectionSubobject( iota1, iota2 ) | ( operation ) |
Returns: an object
The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the intersection of \(S_1\) and \(S_2\)
, which is naturally isomorphic to the pullback of \(\iota_1\) and \(\iota_2\).
‣ EmbeddingOfIntersectionSubobject( iota1, iota2 ) | ( operation ) |
Returns: a monomorphism into \(A\)
The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the embedding IntersectionSubobject(\(\iota\)) \(\hookrightarrow A\) of their intersection subobject.
‣ EmbeddingOfIntersectionSubobjectWithGivenIntersection( iota1, iota2, T ) | ( operation ) |
Returns: a monomorphism in \(\mathrm{Hom}( T, A )\)
The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\) and an object T with IsEqualForObjects(T, IntersectionSubobject(iota1, iota2)). The output is the embedding \(T \hookrightarrow A\) of their intersection subobject T.
‣ UnionSubobject( iota1, iota2 ) | ( operation ) |
Returns: an object
The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the union of \(S_1\) and \(S_2\)
, which is naturally isomorphic to the image object of the coproduct morphism of \(\iota_1\) and \(\iota_2\).
‣ EmbeddingOfUnionSubobject( iota1, iota2 ) | ( operation ) |
Returns: a monomorphism into \(A\)
The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the embedding UnionSubobject(iota1, iota2) \(\hookrightarrow A\) of their union subobject.
‣ EmbeddingOfUnionSubobjectWithGivenUnion( iota1, iota2, U ) | ( operation ) |
Returns: a monomorphism in \(\mathrm{Hom}( U, A )\)
The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\) and an object U with IsEqualForObjects(U, UnionSubobject(iota1, iota2)). The output is the embedding \(U \hookrightarrow A\) of their union subobject U.
‣ RelativePseudoComplementSubobject( iota1, iota2 ) | ( operation ) |
Returns: an object
The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the relative pseudo-complement of \(S_1\) relative to \(S_2\)
.
‣ EmbeddingOfRelativePseudoComplementSubobject( iota1, iota2 ) | ( operation ) |
Returns: a monomorphism into \(A\)
The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the embedding RelativePseudoComplementSubobject(iota1, iota2) \(\hookrightarrow A\) of their relative pseudo-complement into \(A\).
‣ EmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication( iota1, iota2, I ) | ( operation ) |
Returns: a monomorphism in \(\mathrm{Hom}( I, A )\)
The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\) and an object I with IsEqualForObjects(I, RelativePseudoComplementSubobject(iota1, iota2)). The output is the embedding \(I \hookrightarrow A\) of their relative pseudo-complement I into \(A\).
Define two composable monos \(K \stackrel{l}{\hookrightarrow} L \stackrel{m}{\hookrightarrow} G\) in FinSets:
gap> LoadPackage( "FinSetsForCAP" ); true gap> K := FinSet( [ 2, 3, 5 ] );; gap> Display( K ); [ 2, 3, 5 ] gap> L := FinSet( [ 0, 1, 2, 3, 5, 6 ] );; gap> Display( L ); [ 0, 1, 2, 3, 5, 6 ] gap> l := EmbeddingOfFinSets( K, L ); <A monomorphism in FinSets> gap> G := FinSet( [ 0, 1, 2, 3, 4, 5, 6, 10 ] );; gap> Display( G ); [ 0, 1, 2, 3, 4, 5, 6, 10 ] gap> m := EmbeddingOfFinSets( L, G ); <A monomorphism in FinSets>
Now we compute the pushout complement \(D \stackrel{c}{\hookrightarrow} G\) of \(K \stackrel{l}{\hookrightarrow} L \stackrel{m}{\hookrightarrow} G\):
gap> HasPushoutComplement( l, m ); true gap> c := PushoutComplement( l, m ); <A monomorphism in FinSets> gap> D := Source( c );; gap> Display( D ); [ 2, 3, 4, 5, 10 ]
Define two composable monos \(K \stackrel{l}{\hookrightarrow} L \stackrel{m}{\hookrightarrow} G\) in SkeletalFinSets:
gap> LoadPackage( "FinSetsForCAP" ); true gap> K := FinSet( 3 ); |3| gap> L := FinSet( 6 ); |6| gap> l := MapOfFinSets( K, [ 2, 3, 4 ], L );; IsMonomorphism( l );; l; |3| ↪ |6| gap> Display( l ); { 0, 1, 2 } ⱶ[ 2, 3, 4 ]→ { 0,..., 5 } gap> G := FinSet( 8 ); |8| gap> Display( G ); { 0,..., 7 } gap> m := MapOfFinSets( L, [ 0, 1, 2, 3, 5, 6 ], G ); |6| → |8| gap> Display( m ); { 0,..., 5 } ⱶ[ 0, 1, 2, 3, 5, 6 ]→ { 0,..., 7 }
Now we compute the pushout complement \(D \stackrel{c}{\hookrightarrow} G\) of \(K \stackrel{l}{\hookrightarrow} L \stackrel{m}{\hookrightarrow} G\):
gap> HasPushoutComplement( l, m ); true gap> c := PushoutComplement( l, m ); |5| → |8| gap> Display( c ); { 0,..., 4 } ⱶ[ 2, 3, 4, 5, 7 ]→ { 0,..., 7 }
‣ HasPushoutComplement( l, m ) | ( operation ) |
Returns: a boolean
The arguments are two composable morphisms \(l: K \rightarrow L\), \(m: L \rightarrow G\). The output is true if there exists a morphism \(d: K \rightarrow D\) and a morphism \(g: D \rightarrow G\) such that the four morphisms \(l,d,m,g\) form a pushout diagram, i.e., such that \(m\)=InjectionOfCofactorOfPushoutWithGivenPushout([\(l,d\)], 1) and \(g\)=InjectionOfCofactorOfPushoutWithGivenPushout([\(l,d\)], 2). Otherwise the output is false.
‣ PushoutComplement( l, m ) | ( operation ) |
Returns: a morphism
The arguments are two composable morphisms \(l: K \rightarrow L\), \(m: L \rightarrow G\). The output is a morphism \(d: K \rightarrow D\) such that there exists a morphism \(g: D \rightarrow G\) turing the four morphisms \(l,d,m,g\) into a pushout diagram, i.e., such that \(m\)=InjectionOfCofactorOfPushoutWithGivenPushout([\(l,d\)], 1) and \(g\)=InjectionOfCofactorOfPushoutWithGivenPushout([\(l,d\)], 2).
‣ DPO( m, l, r ) | ( operation ) |
Returns: a pair of morhpisms
Compute the double-pushout of m along the rule given by [ l, r ].
We start by defining a linear rewriting rule as a span of two monos \(L \stackrel{l}{\hookleftarrow} K \stackrel{r}{\hookrightarrow} R\) in FinSets:
gap> LoadPackage( "FinSetsForCAP" ); true gap> K := FinSet( [ 2, 3, 5 ] );; gap> Length( K ); 3 gap> Display( K ); [ 2, 3, 5 ] gap> L := FinSet( [ 0, 1, 2, 3, 5, 6 ] );; gap> Length( L ); 6 gap> Display( L ); [ 0, 1, 2, 3, 5, 6 ] gap> R := FinSet( [ 2, 3, 4, 5, 7 ] );; gap> Length( R ); 5 gap> Display( R ); [ 2, 3, 4, 5, 7 ] gap> l := EmbeddingOfFinSets( K, L ); <A monomorphism in FinSets> gap> r := EmbeddingOfFinSets( K, R ); <A monomorphism in FinSets>
Then we define an object within the context of the rule and a matching \(L \stackrel{m}{\hookrightarrow} G\):
gap> G := FinSet( [ 0, 1, 2, 3, 4, 5, 6, 10 ] );; gap> Length( G ); 8 gap> Display( G ); [ 0, 1, 2, 3, 4, 5, 6, 10 ] gap> m := EmbeddingOfFinSets( L, G ); <A monomorphism in FinSets>
The double-pushout rewriting now applies the linear rule \((l,r)\) to the matriching \(m\):
gap> p := DPO( m, l, r );; gap> h := p[1]; <A monomorphism in FinSets> gap> p := p[2]; <A monomorphism in FinSets> gap> H := Target( p );; gap> Length( H ); 7 gap> Display( H ); [ [ [ 1, 2 ], [ 2, 2 ] ],\ [ [ 1, 3 ], [ 2, 3 ] ],\ [ [ 1, 4 ] ],\ [ [ 1, 5 ], [ 2, 5 ] ],\ [ [ 1, 10 ] ],\ [ [ 2, 4 ] ],\ [ [ 2, 7 ] ] ]
This means
\(2, 3, 5\) are in \(K\) and hence in both \(G\) and \(R\);
\(10\) is only in \(G\);
\(7\) are only in \(R\);
\(4\) is in \(G\) but it must be duplicated since it is also in \(R\) but not in \(K\).
Compute the Lawvere-Tierney topologies of SkeletalFinSets:
gap> LoadPackage( "FinSetsForCAP" ); true gap> LTI := LawvereTierneyLocalModalityOperators( SkeletalFinSets );; gap> Perform( LTI, Display ); { 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 } { 0, 1 } ⱶ[ 1, 1 ]→ { 0, 1 } gap> LTS := LawvereTierneySubobjects( SkeletalFinSets );; gap> Perform( LTS, Display ); { 0 } ⱶ[ 1 ]→ { 0, 1 } { 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 } gap> LTC := LawvereTierneyEmbeddingsOfSubobjectClassifiers( SkeletalFinSets );; gap> Perform( LTC, Display ); { 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 } { 0 } ⱶ[ 1 ]→ { 0, 1 }
‣ LawvereTierneyLocalModalityOperators( T ) | ( attribute ) |
Returns: a list of endomorphisms in \(\mathrm{Hom}( \mathrm{SubobjectClassifier}( T ), \mathrm{SubobjectClassifier}( T ) )\)
The input is an elementary topos T. The output is the list of Lawvere-Tierney idempotents of the subobject classifier of the topos T.
‣ LawvereTierneySubobjects( T ) | ( attribute ) |
Returns: a list of monomorphisms into \(\mathrm{SubobjectClassifier}( T )\)
The input is an elementary topos T. The output is the list of Lawvere-Tierney subobjects of the subobject classifier of the topos T.
‣ LawvereTierneyEmbeddingsOfSubobjectClassifiers( T ) | ( attribute ) |
Returns: a list of monomorphisms \(\mathrm{SubobjectClassifier}( T )\)
The input is an elementary topos T. The output is the list of embeddings of the subobject classifiers of full sheaf subtoposes (with respect to the Lawvere-Tierney topologies of the topos T) into the subobject classifier of T.
‣ AddCartesianSquareOfSubobjectClassifier( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianSquareOfSubobjectClassifier. \(F: ( ) \mapsto \mathtt{CartesianSquareOfSubobjectClassifier}()\).
‣ AddClassifyingMorphismOfSubobject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ClassifyingMorphismOfSubobject. \(F: ( alpha ) \mapsto \mathtt{ClassifyingMorphismOfSubobject}(alpha)\).
‣ AddClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier. \(F: ( alpha, Omega ) \mapsto \mathtt{ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier}(alpha, Omega)\).
‣ AddCoproductComplement( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoproductComplement. \(F: ( iota ) \mapsto \mathtt{CoproductComplement}(iota)\).
‣ AddDirectProductComplement( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductComplement. \(F: ( pi ) \mapsto \mathtt{DirectProductComplement}(pi)\).
‣ AddEmbeddingOfIntersectionSubobject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfIntersectionSubobject. \(F: ( iota1, iota2 ) \mapsto \mathtt{EmbeddingOfIntersectionSubobject}(iota1, iota2)\).
‣ AddEmbeddingOfIntersectionSubobjectWithGivenIntersection( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfIntersectionSubobjectWithGivenIntersection. \(F: ( iota1, iota2, intersection ) \mapsto \mathtt{EmbeddingOfIntersectionSubobjectWithGivenIntersection}(iota1, iota2, intersection)\).
‣ AddEmbeddingOfPseudoComplementSubobject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfPseudoComplementSubobject. \(F: ( iota ) \mapsto \mathtt{EmbeddingOfPseudoComplementSubobject}(iota)\).
‣ AddEmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement. \(F: ( iota, complement ) \mapsto \mathtt{EmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement}(iota, complement)\).
‣ AddEmbeddingOfRelativePseudoComplementSubobject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfRelativePseudoComplementSubobject. \(F: ( iota1, iota2 ) \mapsto \mathtt{EmbeddingOfRelativePseudoComplementSubobject}(iota1, iota2)\).
‣ AddEmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication. \(F: ( iota1, iota2, implication ) \mapsto \mathtt{EmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication}(iota1, iota2, implication)\).
‣ AddEmbeddingOfUnionSubobject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfUnionSubobject. \(F: ( iota1, iota2 ) \mapsto \mathtt{EmbeddingOfUnionSubobject}(iota1, iota2)\).
‣ AddEmbeddingOfUnionSubobjectWithGivenUnion( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfUnionSubobjectWithGivenUnion. \(F: ( iota1, iota2, union ) \mapsto \mathtt{EmbeddingOfUnionSubobjectWithGivenUnion}(iota1, iota2, union)\).
‣ AddExactCoverWithGlobalElements( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExactCoverWithGlobalElements. \(F: ( arg2 ) \mapsto \mathtt{ExactCoverWithGlobalElements}(arg2)\).
‣ AddHasPushoutComplement( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation HasPushoutComplement. \(F: ( arg2, arg3 ) \mapsto \mathtt{HasPushoutComplement}(arg2, arg3)\).
‣ AddIndexOfNonliftableMorphismFromDistinguishedObject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IndexOfNonliftableMorphismFromDistinguishedObject. \(F: ( iota ) \mapsto \mathtt{IndexOfNonliftableMorphismFromDistinguishedObject}(iota)\).
‣ AddInjectionOfCoproductComplement( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InjectionOfCoproductComplement. \(F: ( iota ) \mapsto \mathtt{InjectionOfCoproductComplement}(iota)\).
‣ AddInjectionOfCoproductComplementWithGivenCoproductComplement( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InjectionOfCoproductComplementWithGivenCoproductComplement. \(F: ( iota, complement ) \mapsto \mathtt{InjectionOfCoproductComplementWithGivenCoproductComplement}(iota, complement)\).
‣ AddIntersectionSubobject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IntersectionSubobject. \(F: ( arg2, arg3 ) \mapsto \mathtt{IntersectionSubobject}(arg2, arg3)\).
‣ AddIsomorphismOntoCartesianSquareOfPowerObject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismOntoCartesianSquareOfPowerObject. \(F: ( a ) \mapsto \mathtt{IsomorphismOntoCartesianSquareOfPowerObject}(a)\).
‣ AddIsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects. \(F: ( ExpaOmega2, a, PaxPa ) \mapsto \mathtt{IsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects}(ExpaOmega2, a, PaxPa)\).
‣ AddLawvereTierneyEmbeddingsOfSubobjectClassifiers( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LawvereTierneyEmbeddingsOfSubobjectClassifiers. \(F: ( ) \mapsto \mathtt{LawvereTierneyEmbeddingsOfSubobjectClassifiers}()\).
‣ AddLawvereTierneyLocalModalityOperators( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LawvereTierneyLocalModalityOperators. \(F: ( ) \mapsto \mathtt{LawvereTierneyLocalModalityOperators}()\).
‣ AddLawvereTierneySubobjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LawvereTierneySubobjects. \(F: ( ) \mapsto \mathtt{LawvereTierneySubobjects}()\).
‣ AddLeftFiberMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftFiberMorphism. \(F: ( b, c ) \mapsto \mathtt{LeftFiberMorphism}(b, c)\).
‣ AddLeftFiberMorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftFiberMorphismWithGivenObjects. \(F: ( Pbxc_b, b, c, Pc ) \mapsto \mathtt{LeftFiberMorphismWithGivenObjects}(Pbxc_b, b, c, Pc)\).
‣ AddListOfSubobjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ListOfSubobjects. \(F: ( arg2 ) \mapsto \mathtt{ListOfSubobjects}(arg2)\).
‣ AddLowerSegmentOfRelation( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LowerSegmentOfRelation. \(F: ( a, b, mu ) \mapsto \mathtt{LowerSegmentOfRelation}(a, b, mu)\).
‣ AddLowerSegmentOfRelationWithGivenRange( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LowerSegmentOfRelationWithGivenRange. \(F: ( a, b, mu, Pa ) \mapsto \mathtt{LowerSegmentOfRelationWithGivenRange}(a, b, mu, Pa)\).
‣ AddNonliftableMorphismFromDistinguishedObject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation NonliftableMorphismFromDistinguishedObject. \(F: ( iota ) \mapsto \mathtt{NonliftableMorphismFromDistinguishedObject}(iota)\).
‣ AddPLeftTransposeMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PLeftTransposeMorphism. \(F: ( a, b, f ) \mapsto \mathtt{PLeftTransposeMorphism}(a, b, f)\).
‣ AddPLeftTransposeMorphismWithGivenRange( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PLeftTransposeMorphismWithGivenRange. \(F: ( a, b, f, Pb ) \mapsto \mathtt{PLeftTransposeMorphismWithGivenRange}(a, b, f, Pb)\).
‣ AddPRightTransposeMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PRightTransposeMorphism. \(F: ( a, b, f ) \mapsto \mathtt{PRightTransposeMorphism}(a, b, f)\).
‣ AddPRightTransposeMorphismWithGivenRange( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PRightTransposeMorphismWithGivenRange. \(F: ( a, b, f, Pa ) \mapsto \mathtt{PRightTransposeMorphismWithGivenRange}(a, b, f, Pa)\).
‣ AddPowerObject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObject. \(F: ( arg2 ) \mapsto \mathtt{PowerObject}(arg2)\).
‣ AddPowerObjectFunctorial( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectFunctorial. \(F: ( f ) \mapsto \mathtt{PowerObjectFunctorial}(f)\).
‣ AddPowerObjectFunctorialWithGivenPowerObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectFunctorialWithGivenPowerObjects. \(F: ( Pb, f, Pa ) \mapsto \mathtt{PowerObjectFunctorialWithGivenPowerObjects}(Pb, f, Pa)\).
‣ AddPowerObjectLeftEvaluationMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectLeftEvaluationMorphism. \(F: ( a ) \mapsto \mathtt{PowerObjectLeftEvaluationMorphism}(a)\).
‣ AddPowerObjectLeftEvaluationMorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectLeftEvaluationMorphismWithGivenObjects. \(F: ( Pa_xa, a, Omega ) \mapsto \mathtt{PowerObjectLeftEvaluationMorphismWithGivenObjects}(Pa_xa, a, Omega)\).
‣ AddPowerObjectRightEvaluationMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectRightEvaluationMorphism. \(F: ( a ) \mapsto \mathtt{PowerObjectRightEvaluationMorphism}(a)\).
‣ AddPowerObjectRightEvaluationMorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectRightEvaluationMorphismWithGivenObjects. \(F: ( axPa, a, Omega ) \mapsto \mathtt{PowerObjectRightEvaluationMorphismWithGivenObjects}(axPa, a, Omega)\).
‣ AddProjectionInDirectProductComplement( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ProjectionInDirectProductComplement. \(F: ( pi ) \mapsto \mathtt{ProjectionInDirectProductComplement}(pi)\).
‣ AddProjectionInDirectProductComplementWithGivenDirectProductComplement( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ProjectionInDirectProductComplementWithGivenDirectProductComplement. \(F: ( pi, complement ) \mapsto \mathtt{ProjectionInDirectProductComplementWithGivenDirectProductComplement}(pi, complement)\).
‣ AddPseudoComplementSubobject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PseudoComplementSubobject. \(F: ( arg2 ) \mapsto \mathtt{PseudoComplementSubobject}(arg2)\).
‣ AddPushoutComplement( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PushoutComplement. \(F: ( l, m ) \mapsto \mathtt{PushoutComplement}(l, m)\).
‣ AddRelativePseudoComplementSubobject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativePseudoComplementSubobject. \(F: ( arg2, arg3 ) \mapsto \mathtt{RelativePseudoComplementSubobject}(arg2, arg3)\).
‣ AddRelativeTruthMorphismOfAnd( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfAnd. \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfAnd}(a)\).
‣ AddRelativeTruthMorphismOfAndWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfAndWithGivenObjects. \(F: ( PaxPa, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfAndWithGivenObjects}(PaxPa, a, Pa)\).
‣ AddRelativeTruthMorphismOfFalse( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfFalse. \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfFalse}(a)\).
‣ AddRelativeTruthMorphismOfFalseWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfFalseWithGivenObjects. \(F: ( T, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfFalseWithGivenObjects}(T, a, Pa)\).
‣ AddRelativeTruthMorphismOfImplies( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfImplies. \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfImplies}(a)\).
‣ AddRelativeTruthMorphismOfImpliesWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfImpliesWithGivenObjects. \(F: ( PaxPa, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfImpliesWithGivenObjects}(PaxPa, a, Pa)\).
‣ AddRelativeTruthMorphismOfNot( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfNot. \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfNot}(a)\).
‣ AddRelativeTruthMorphismOfNotWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfNotWithGivenObjects. \(F: ( Pa, a, Pa1 ) \mapsto \mathtt{RelativeTruthMorphismOfNotWithGivenObjects}(Pa, a, Pa1)\).
‣ AddRelativeTruthMorphismOfOr( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfOr. \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfOr}(a)\).
‣ AddRelativeTruthMorphismOfOrWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfOrWithGivenObjects. \(F: ( PaxPa, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfOrWithGivenObjects}(PaxPa, a, Pa)\).
‣ AddRelativeTruthMorphismOfTrue( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfTrue. \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfTrue}(a)\).
‣ AddRelativeTruthMorphismOfTrueWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfTrueWithGivenObjects. \(F: ( T, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfTrueWithGivenObjects}(T, a, Pa)\).
‣ AddRightFiberMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightFiberMorphism. \(F: ( b, c ) \mapsto \mathtt{RightFiberMorphism}(b, c)\).
‣ AddRightFiberMorphismWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightFiberMorphismWithGivenObjects. \(F: ( cxPbxc, b, c, Pb ) \mapsto \mathtt{RightFiberMorphismWithGivenObjects}(cxPbxc, b, c, Pb)\).
‣ AddSingletonMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation SingletonMorphism. \(F: ( a ) \mapsto \mathtt{SingletonMorphism}(a)\).
‣ AddSingletonMorphismWithGivenPowerObject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation SingletonMorphismWithGivenPowerObject. \(F: ( a, Pa ) \mapsto \mathtt{SingletonMorphismWithGivenPowerObject}(a, Pa)\).
‣ AddSubobjectClassifier( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation SubobjectClassifier. \(F: ( ) \mapsto \mathtt{SubobjectClassifier}()\).
‣ AddSubobjectOfClassifyingMorphism( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation SubobjectOfClassifyingMorphism. \(F: ( alpha ) \mapsto \mathtt{SubobjectOfClassifyingMorphism}(alpha)\).
‣ AddTruthMorphismOfAnd( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfAnd. \(F: ( ) \mapsto \mathtt{TruthMorphismOfAnd}()\).
‣ AddTruthMorphismOfAndWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfAndWithGivenObjects. \(F: ( Omega2, Omega ) \mapsto \mathtt{TruthMorphismOfAndWithGivenObjects}(Omega2, Omega)\).
‣ AddTruthMorphismOfFalse( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfFalse. \(F: ( ) \mapsto \mathtt{TruthMorphismOfFalse}()\).
‣ AddTruthMorphismOfFalseWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfFalseWithGivenObjects. \(F: ( T, Omega ) \mapsto \mathtt{TruthMorphismOfFalseWithGivenObjects}(T, Omega)\).
‣ AddTruthMorphismOfImplies( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfImplies. \(F: ( ) \mapsto \mathtt{TruthMorphismOfImplies}()\).
‣ AddTruthMorphismOfImpliesWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfImpliesWithGivenObjects. \(F: ( Omega2, Omega ) \mapsto \mathtt{TruthMorphismOfImpliesWithGivenObjects}(Omega2, Omega)\).
‣ AddTruthMorphismOfNot( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfNot. \(F: ( ) \mapsto \mathtt{TruthMorphismOfNot}()\).
‣ AddTruthMorphismOfNotWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfNotWithGivenObjects. \(F: ( Omega, Omega1 ) \mapsto \mathtt{TruthMorphismOfNotWithGivenObjects}(Omega, Omega1)\).
‣ AddTruthMorphismOfOr( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfOr. \(F: ( ) \mapsto \mathtt{TruthMorphismOfOr}()\).
‣ AddTruthMorphismOfOrWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfOrWithGivenObjects. \(F: ( Omega2, Omega ) \mapsto \mathtt{TruthMorphismOfOrWithGivenObjects}(Omega2, Omega)\).
‣ AddTruthMorphismOfTrue( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfTrue. \(F: ( ) \mapsto \mathtt{TruthMorphismOfTrue}()\).
‣ AddTruthMorphismOfTrueWithGivenObjects( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfTrueWithGivenObjects. \(F: ( T, Omega ) \mapsto \mathtt{TruthMorphismOfTrueWithGivenObjects}(T, Omega)\).
‣ AddUnionSubobject( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation UnionSubobject. \(F: ( arg2, arg3 ) \mapsto \mathtt{UnionSubobject}(arg2, arg3)\).
‣ AddUpperSegmentOfRelation( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation UpperSegmentOfRelation. \(F: ( a, b, mu ) \mapsto \mathtt{UpperSegmentOfRelation}(a, b, mu)\).
‣ AddUpperSegmentOfRelationWithGivenRange( C, F ) | ( operation ) |
Returns: nothing
The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation UpperSegmentOfRelationWithGivenRange. \(F: ( a, b, mu, Pb ) \mapsto \mathtt{UpperSegmentOfRelationWithGivenRange}(a, b, mu, Pb)\).
‣ CoproductComplement( iota ) | ( attribute ) |
Returns: an object
The argument is a morphism iota\(: S \to T\) which is a coproduct injection of some binary coproduct. The output is an object \(C\) such that \(S \sqcup C \cong T\).
‣ InjectionOfCoproductComplement( iota ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( C, \mathrm{Target}( \iota ) )\)
The argument is a morphism iota\(: S \to T\) which is a coproduct injection of some binary coproduct. The output is a coproduct injection \(\iota_2: C \to T\) such that UniversalMorphismFromCoproduct( iota, \(\iota_2\) )\(: S \sqcup C \to T\) is an isomorphism.
‣ InjectionOfCoproductComplementWithGivenCoproductComplement( iota, C ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( C, \mathrm{Target}( \iota ) )\)
The argument is a morphism iota\(: S \to T\) which is a coproduct injection of some binary coproduct and a coproduct complement C. The output is a coproduct injection \(\iota_2:\) C \(\to T\) such that UniversalMorphismFromCoproduct( iota, \(\iota_2\) )\(: S \sqcup C \to T\) is an isomorphism.
‣ DirectProductComplement( pi ) | ( attribute ) |
Returns: an object
The argument is a morphism pi\(: S \to T\) which is a product projection of some binary direct product. The output is an object \(C\) such that \(S \times C \cong T\).
‣ ProjectionInDirectProductComplement( pi ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}( C, \mathrm{Target}( \pi ) )\)
The argument is a morphism pi\(: S \to T\) which is a direct product projection of some binary direct product. The output is a direct product projection \(\pi_2: C \to T\) such that UniversalMorphismIntoDirectProduct( pi, \(\pi_2\) )\(: T \to S \times C\) is an isomorphism.
‣ ProjectionInDirectProductComplementWithGivenDirectProductComplement( pi, C ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}( C, \mathrm{Target}( \pi ) )\)
The argument is a morphism pi\(: S \to T\) which is a direct product projection of some binary direct product and a coproduct complement C. The output is a direct product projection \(\pi_2:\) C \(\to T\) such that UniversalMorphismIntoDirectProduct( pi, \(\pi_2\) )\(: T \to S \times C\) is an isomorphism.
generated by GAPDoc2HTML