Goto Chapter: Top 1 2 3 4 5 6 Ind
 [Top of Book]  [Contents]   [Next Chapter] 

CartesianCategories

Cartesian and cocartesian categories and various subdoctrines

2024.09-04

19 September 2024

Mohamed Barakat
Email: mohamed.barakat@uni-siegen.de
Homepage: https://mohamed-barakat.github.io
Address:
Walter-Flex-Str. 3
57068 Siegen
Germany

Fabian Zickgraf
Email: fabian.zickgraf@uni-siegen.de
Homepage: https://github.com/zickgraf/
Address:
Walter-Flex-Str. 3
57068 Siegen
Germany

Tom Kuhmichel
Email: tom.kuhmichel@student.uni-siegen.de
Homepage: https://github.com/TKuh
Address:
Walter-Flex-Str. 3
57068 Siegen
Germany

Contents

1 Cartesian Categories
 1.2 Cartesian Closed Categories

  1.2-1 ExponentialOnObjects

  1.2-2 ExponentialOnMorphisms

  1.2-3 ExponentialOnMorphismsWithGivenExponentials

  1.2-4 CartesianRightEvaluationMorphism

  1.2-5 CartesianRightEvaluationMorphismWithGivenSource

  1.2-6 CartesianRightCoevaluationMorphism

  1.2-7 CartesianRightCoevaluationMorphismWithGivenRange

  1.2-8 DirectProductToExponentialRightAdjunctMorphism

  1.2-9 DirectProductToExponentialRightAdjunctMorphismWithGivenExponential

  1.2-10 DirectProductToExponentialRightAdjunctionIsomorphism

  1.2-11 DirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects

  1.2-12 ExponentialToDirectProductRightAdjunctMorphism

  1.2-13 ExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct

  1.2-14 ExponentialToDirectProductRightAdjunctionIsomorphism

  1.2-15 ExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects

  1.2-16 CartesianLeftEvaluationMorphism

  1.2-17 CartesianLeftEvaluationMorphismWithGivenSource

  1.2-18 CartesianLeftCoevaluationMorphism

  1.2-19 CartesianLeftCoevaluationMorphismWithGivenRange

  1.2-20 DirectProductToExponentialLeftAdjunctMorphism

  1.2-21 DirectProductToExponentialLeftAdjunctMorphismWithGivenExponential

  1.2-22 DirectProductToExponentialLeftAdjunctionIsomorphism

  1.2-23 DirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects

  1.2-24 ExponentialToDirectProductLeftAdjunctMorphism

  1.2-25 ExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct

  1.2-26 ExponentialToDirectProductLeftAdjunctionIsomorphism

  1.2-27 ExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects

  1.2-28 CartesianPreComposeMorphism

  1.2-29 CartesianPreComposeMorphismWithGivenObjects

  1.2-30 CartesianPostComposeMorphism

  1.2-31 CartesianPostComposeMorphismWithGivenObjects

  1.2-32 CartesianDualOnObjects

  1.2-33 CartesianDualOnMorphisms

  1.2-34 CartesianDualOnMorphismsWithGivenCartesianDuals

  1.2-35 CartesianEvaluationForCartesianDual

  1.2-36 CartesianEvaluationForCartesianDualWithGivenDirectProduct

  1.2-37 MorphismToCartesianBidual

  1.2-38 MorphismToCartesianBidualWithGivenCartesianBidual

  1.2-39 DirectProductExponentialCompatibilityMorphism

  1.2-40 DirectProductExponentialCompatibilityMorphismWithGivenObjects

  1.2-41 DirectProductCartesianDualityCompatibilityMorphism

  1.2-42 DirectProductCartesianDualityCompatibilityMorphismWithGivenObjects

  1.2-43 MorphismFromDirectProductToExponential

  1.2-44 MorphismFromDirectProductToExponentialWithGivenObjects

  1.2-45 IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject

  1.2-46 IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject

  1.2-47 UniversalPropertyOfCartesianDual

  1.2-48 CartesianLambdaIntroduction

  1.2-49 CartesianLambdaElimination

  1.2-50 IsomorphismFromObjectToExponential

  1.2-51 IsomorphismFromObjectToExponentialWithGivenExponential

  1.2-52 IsomorphismFromExponentialToObject

  1.2-53 IsomorphismFromExponentialToObjectWithGivenExponential
 1.4 Add-methods

  1.4-1 AddCartesianBraiding

  1.4-2 AddCartesianBraidingInverse

  1.4-3 AddCartesianBraidingInverseWithGivenDirectProducts

  1.4-4 AddCartesianBraidingWithGivenDirectProducts

  1.4-5 AddCartesianAssociatorLeftToRight

  1.4-6 AddCartesianAssociatorLeftToRightWithGivenDirectProducts

  1.4-7 AddCartesianAssociatorRightToLeft

  1.4-8 AddCartesianAssociatorRightToLeftWithGivenDirectProducts

  1.4-9 AddCartesianDiagonal

  1.4-10 AddCartesianDiagonalWithGivenCartesianPower

  1.4-11 AddCartesianLeftUnitor

  1.4-12 AddCartesianLeftUnitorInverse

  1.4-13 AddCartesianLeftUnitorInverseWithGivenDirectProduct

  1.4-14 AddCartesianLeftUnitorWithGivenDirectProduct

  1.4-15 AddCartesianRightUnitor

  1.4-16 AddCartesianRightUnitorInverse

  1.4-17 AddCartesianRightUnitorInverseWithGivenDirectProduct

  1.4-18 AddCartesianRightUnitorWithGivenDirectProduct

  1.4-19 AddDirectProductOnMorphisms

  1.4-20 AddDirectProductOnMorphismsWithGivenDirectProducts

  1.4-21 AddCartesianDualOnMorphisms

  1.4-22 AddCartesianDualOnMorphismsWithGivenCartesianDuals

  1.4-23 AddCartesianDualOnObjects

  1.4-24 AddCartesianEvaluationForCartesianDual

  1.4-25 AddCartesianEvaluationForCartesianDualWithGivenDirectProduct

  1.4-26 AddCartesianLambdaElimination

  1.4-27 AddCartesianLambdaIntroduction

  1.4-28 AddCartesianLeftCoevaluationMorphism

  1.4-29 AddCartesianLeftCoevaluationMorphismWithGivenRange

  1.4-30 AddCartesianLeftEvaluationMorphism

  1.4-31 AddCartesianLeftEvaluationMorphismWithGivenSource

  1.4-32 AddCartesianPostComposeMorphism

  1.4-33 AddCartesianPostComposeMorphismWithGivenObjects

  1.4-34 AddCartesianPreComposeMorphism

  1.4-35 AddCartesianPreComposeMorphismWithGivenObjects

  1.4-36 AddCartesianRightCoevaluationMorphism

  1.4-37 AddCartesianRightCoevaluationMorphismWithGivenRange

  1.4-38 AddCartesianRightEvaluationMorphism

  1.4-39 AddCartesianRightEvaluationMorphismWithGivenSource

  1.4-40 AddDirectProductCartesianDualityCompatibilityMorphism

  1.4-41 AddDirectProductCartesianDualityCompatibilityMorphismWithGivenObjects

  1.4-42 AddDirectProductExponentialCompatibilityMorphism

  1.4-43 AddDirectProductExponentialCompatibilityMorphismWithGivenObjects

  1.4-44 AddDirectProductToExponentialLeftAdjunctMorphism

  1.4-45 AddDirectProductToExponentialLeftAdjunctMorphismWithGivenExponential

  1.4-46 AddDirectProductToExponentialLeftAdjunctionIsomorphism

  1.4-47 AddDirectProductToExponentialLeftAdjunctionIsomorphismWithGivenObjects

  1.4-48 AddDirectProductToExponentialRightAdjunctMorphism

  1.4-49 AddDirectProductToExponentialRightAdjunctMorphismWithGivenExponential

  1.4-50 AddDirectProductToExponentialRightAdjunctionIsomorphism

  1.4-51 AddDirectProductToExponentialRightAdjunctionIsomorphismWithGivenObjects

  1.4-52 AddExponentialOnMorphisms

  1.4-53 AddExponentialOnMorphismsWithGivenExponentials

  1.4-54 AddExponentialOnObjects

  1.4-55 AddExponentialToDirectProductLeftAdjunctMorphism

  1.4-56 AddExponentialToDirectProductLeftAdjunctMorphismWithGivenDirectProduct

  1.4-57 AddExponentialToDirectProductLeftAdjunctionIsomorphism

  1.4-58 AddExponentialToDirectProductLeftAdjunctionIsomorphismWithGivenObjects

  1.4-59 AddExponentialToDirectProductRightAdjunctMorphism

  1.4-60 AddExponentialToDirectProductRightAdjunctMorphismWithGivenDirectProduct

  1.4-61 AddExponentialToDirectProductRightAdjunctionIsomorphism

  1.4-62 AddExponentialToDirectProductRightAdjunctionIsomorphismWithGivenObjects

  1.4-63 AddIsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject

  1.4-64 AddIsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject

  1.4-65 AddIsomorphismFromExponentialToObject

  1.4-66 AddIsomorphismFromExponentialToObjectWithGivenExponential

  1.4-67 AddIsomorphismFromObjectToExponential

  1.4-68 AddIsomorphismFromObjectToExponentialWithGivenExponential

  1.4-69 AddMorphismFromDirectProductToExponential

  1.4-70 AddMorphismFromDirectProductToExponentialWithGivenObjects

  1.4-71 AddMorphismToCartesianBidual

  1.4-72 AddMorphismToCartesianBidualWithGivenCartesianBidual

  1.4-73 AddUniversalPropertyOfCartesianDual

  1.4-74 AddLeftCartesianDistributivityExpanding

  1.4-75 AddLeftCartesianDistributivityExpandingWithGivenObjects

  1.4-76 AddLeftCartesianDistributivityFactoring

  1.4-77 AddLeftCartesianDistributivityFactoringWithGivenObjects

  1.4-78 AddRightCartesianDistributivityExpanding

  1.4-79 AddRightCartesianDistributivityExpandingWithGivenObjects

  1.4-80 AddRightCartesianDistributivityFactoring

  1.4-81 AddRightCartesianDistributivityFactoringWithGivenObjects
2 Cocartesian Categories
 2.2 Cocartesian Coclosed Categories

  2.2-1 CoexponentialOnObjects

  2.2-2 CoexponentialOnMorphisms

  2.2-3 CoexponentialOnMorphismsWithGivenCoexponentials

  2.2-4 CocartesianRightEvaluationMorphism

  2.2-5 CocartesianRightEvaluationMorphismWithGivenRange

  2.2-6 CocartesianRightCoevaluationMorphism

  2.2-7 CocartesianRightCoevaluationMorphismWithGivenSource

  2.2-8 CoproductToCoexponentialRightAdjunctMorphism

  2.2-9 CoproductToCoexponentialRightAdjunctMorphismWithGivenCoexponential

  2.2-10 CoexponentialToCoproductRightAdjunctMorphism

  2.2-11 CoexponentialToCoproductRightAdjunctMorphismWithGivenCoproduct

  2.2-12 CocartesianLeftEvaluationMorphism

  2.2-13 CocartesianLeftEvaluationMorphismWithGivenRange

  2.2-14 CocartesianLeftCoevaluationMorphism

  2.2-15 CocartesianLeftCoevaluationMorphismWithGivenSource

  2.2-16 CoproductToCoexponentialLeftAdjunctMorphism

  2.2-17 CoproductToCoexponentialLeftAdjunctMorphismWithGivenCoexponential

  2.2-18 CoexponentialToCoproductLeftAdjunctMorphism

  2.2-19 CoexponentialToCoproductLeftAdjunctMorphismWithGivenCoproduct

  2.2-20 CocartesianPreCoComposeMorphism

  2.2-21 CocartesianPreCoComposeMorphismWithGivenObjects

  2.2-22 CocartesianPostCoComposeMorphism

  2.2-23 CocartesianPostCoComposeMorphismWithGivenObjects

  2.2-24 CocartesianDualOnObjects

  2.2-25 CocartesianDualOnMorphisms

  2.2-26 CocartesianDualOnMorphismsWithGivenCocartesianDuals

  2.2-27 CocartesianEvaluationForCocartesianDual

  2.2-28 CocartesianEvaluationForCocartesianDualWithGivenCoproduct

  2.2-29 MorphismFromCocartesianBidual

  2.2-30 MorphismFromCocartesianBidualWithGivenCocartesianBidual

  2.2-31 CoexponentialCoproductCompatibilityMorphism

  2.2-32 CoexponentialCoproductCompatibilityMorphismWithGivenObjects

  2.2-33 CocartesianDualityCoproductCompatibilityMorphism

  2.2-34 CocartesianDualityCoproductCompatibilityMorphismWithGivenObjects

  2.2-35 MorphismFromCoexponentialToCoproduct

  2.2-36 MorphismFromCoexponentialToCoproductWithGivenObjects

  2.2-37 IsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject

  2.2-38 IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject

  2.2-39 UniversalPropertyOfCocartesianDual

  2.2-40 CocartesianLambdaIntroduction

  2.2-41 CocartesianLambdaElimination

  2.2-42 IsomorphismFromObjectToCoexponential

  2.2-43 IsomorphismFromObjectToCoexponentialWithGivenCoexponential

  2.2-44 IsomorphismFromCoexponentialToObject

  2.2-45 IsomorphismFromCoexponentialToObjectWithGivenCoexponential
 2.4 Add-methods

  2.4-1 AddCocartesianBraiding

  2.4-2 AddCocartesianBraidingInverse

  2.4-3 AddCocartesianBraidingInverseWithGivenCoproducts

  2.4-4 AddCocartesianBraidingWithGivenCoproducts

  2.4-5 AddCocartesianAssociatorLeftToRight

  2.4-6 AddCocartesianAssociatorLeftToRightWithGivenCoproducts

  2.4-7 AddCocartesianAssociatorRightToLeft

  2.4-8 AddCocartesianAssociatorRightToLeftWithGivenCoproducts

  2.4-9 AddCocartesianCodiagonal

  2.4-10 AddCocartesianCodiagonalWithGivenCocartesianMultiple

  2.4-11 AddCocartesianLeftUnitor

  2.4-12 AddCocartesianLeftUnitorInverse

  2.4-13 AddCocartesianLeftUnitorInverseWithGivenCoproduct

  2.4-14 AddCocartesianLeftUnitorWithGivenCoproduct

  2.4-15 AddCocartesianRightUnitor

  2.4-16 AddCocartesianRightUnitorInverse

  2.4-17 AddCocartesianRightUnitorInverseWithGivenCoproduct

  2.4-18 AddCocartesianRightUnitorWithGivenCoproduct

  2.4-19 AddCoproductOnMorphisms

  2.4-20 AddCoproductOnMorphismsWithGivenCoproducts

  2.4-21 AddCocartesianDualOnMorphisms

  2.4-22 AddCocartesianDualOnMorphismsWithGivenCocartesianDuals

  2.4-23 AddCocartesianDualOnObjects

  2.4-24 AddCocartesianDualityCoproductCompatibilityMorphism

  2.4-25 AddCocartesianDualityCoproductCompatibilityMorphismWithGivenObjects

  2.4-26 AddCocartesianEvaluationForCocartesianDual

  2.4-27 AddCocartesianEvaluationForCocartesianDualWithGivenCoproduct

  2.4-28 AddCocartesianLambdaElimination

  2.4-29 AddCocartesianLambdaIntroduction

  2.4-30 AddCocartesianLeftCoevaluationMorphism

  2.4-31 AddCocartesianLeftCoevaluationMorphismWithGivenSource

  2.4-32 AddCocartesianLeftEvaluationMorphism

  2.4-33 AddCocartesianLeftEvaluationMorphismWithGivenRange

  2.4-34 AddCocartesianPostCoComposeMorphism

  2.4-35 AddCocartesianPostCoComposeMorphismWithGivenObjects

  2.4-36 AddCocartesianPreCoComposeMorphism

  2.4-37 AddCocartesianPreCoComposeMorphismWithGivenObjects

  2.4-38 AddCocartesianRightCoevaluationMorphism

  2.4-39 AddCocartesianRightCoevaluationMorphismWithGivenSource

  2.4-40 AddCocartesianRightEvaluationMorphism

  2.4-41 AddCocartesianRightEvaluationMorphismWithGivenRange

  2.4-42 AddCoexponentialCoproductCompatibilityMorphism

  2.4-43 AddCoexponentialCoproductCompatibilityMorphismWithGivenObjects

  2.4-44 AddCoexponentialOnMorphisms

  2.4-45 AddCoexponentialOnMorphismsWithGivenCoexponentials

  2.4-46 AddCoexponentialOnObjects

  2.4-47 AddCoexponentialToCoproductLeftAdjunctMorphism

  2.4-48 AddCoexponentialToCoproductLeftAdjunctMorphismWithGivenCoproduct

  2.4-49 AddCoexponentialToCoproductRightAdjunctMorphism

  2.4-50 AddCoexponentialToCoproductRightAdjunctMorphismWithGivenCoproduct

  2.4-51 AddCoproductToCoexponentialLeftAdjunctMorphism

  2.4-52 AddCoproductToCoexponentialLeftAdjunctMorphismWithGivenCoexponential

  2.4-53 AddCoproductToCoexponentialRightAdjunctMorphism

  2.4-54 AddCoproductToCoexponentialRightAdjunctMorphismWithGivenCoexponential

  2.4-55 AddIsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject

  2.4-56 AddIsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject

  2.4-57 AddIsomorphismFromCoexponentialToObject

  2.4-58 AddIsomorphismFromCoexponentialToObjectWithGivenCoexponential

  2.4-59 AddIsomorphismFromObjectToCoexponential

  2.4-60 AddIsomorphismFromObjectToCoexponentialWithGivenCoexponential

  2.4-61 AddMorphismFromCocartesianBidual

  2.4-62 AddMorphismFromCocartesianBidualWithGivenCocartesianBidual

  2.4-63 AddMorphismFromCoexponentialToCoproduct

  2.4-64 AddMorphismFromCoexponentialToCoproductWithGivenObjects

  2.4-65 AddUniversalPropertyOfCocartesianDual

  2.4-66 AddLeftCocartesianCodistributivityExpanding

  2.4-67 AddLeftCocartesianCodistributivityExpandingWithGivenObjects

  2.4-68 AddLeftCocartesianCodistributivityFactoring

  2.4-69 AddLeftCocartesianCodistributivityFactoringWithGivenObjects

  2.4-70 AddRightCocartesianCodistributivityExpanding

  2.4-71 AddRightCocartesianCodistributivityExpandingWithGivenObjects

  2.4-72 AddRightCocartesianCodistributivityFactoring

  2.4-73 AddRightCocartesianCodistributivityFactoringWithGivenObjects
3 Examples and Tests
4 The initial category
5 Legacy Operations and Synonyms
 5.2 Synonyms for legacy operations

  5.2-1 CartesianEvaluationMorphism

  5.2-2 CartesianEvaluationMorphismWithGivenSource

  5.2-3 CoexponentialToCoproductAdjunctionMap

  5.2-4 CoexponentialToCoproductAdjunctionMapWithGivenCoproduct

  5.2-5 ExponentialToDirectProductAdjunctionMap

  5.2-6 ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct

  5.2-7 CoproductToCoexponentialAdjunctionMap

  5.2-8 CoproductToCoexponentialAdjunctionMapWithGivenCoexponential

  5.2-9 DirectProductToExponentialAdjunctionMap

  5.2-10 DirectProductToExponentialAdjunctionMapWithGivenExponential

  5.2-11 AddCartesianEvaluationMorphism

  5.2-12 AddCartesianEvaluationMorphismWithGivenSource

  5.2-13 AddCoexponentialToCoproductAdjunctionMap

  5.2-14 AddCoexponentialToCoproductAdjunctionMapWithGivenCoproduct

  5.2-15 AddExponentialToDirectProductAdjunctionMap

  5.2-16 AddExponentialToDirectProductAdjunctionMapWithGivenDirectProduct

  5.2-17 AddCoproductToCoexponentialAdjunctionMap

  5.2-18 AddCoproductToCoexponentialAdjunctionMapWithGivenCoexponential

  5.2-19 AddDirectProductToExponentialAdjunctionMap

  5.2-20 AddDirectProductToExponentialAdjunctionMapWithGivenExponential

  5.2-21 CoexponentialToCoproductLeftAdjunctionMap

  5.2-22 CoexponentialToCoproductLeftAdjunctionMapWithGivenCoproduct

  5.2-23 ExponentialToDirectProductLeftAdjunctionMap

  5.2-24 ExponentialToDirectProductLeftAdjunctionMapWithGivenDirectProduct

  5.2-25 CoproductToCoexponentialLeftAdjunctionMap

  5.2-26 CoproductToCoexponentialLeftAdjunctionMapWithGivenCoexponential

  5.2-27 DirectProductToExponentialLeftAdjunctionMap

  5.2-28 DirectProductToExponentialLeftAdjunctionMapWithGivenExponential

  5.2-29 AddCoexponentialToCoproductLeftAdjunctionMap

  5.2-30 AddCoexponentialToCoproductLeftAdjunctionMapWithGivenCoproduct

  5.2-31 AddExponentialToDirectProductLeftAdjunctionMap

  5.2-32 AddExponentialToDirectProductLeftAdjunctionMapWithGivenDirectProduct

  5.2-33 AddCoproductToCoexponentialLeftAdjunctionMap

  5.2-34 AddCoproductToCoexponentialLeftAdjunctionMapWithGivenCoexponential

  5.2-35 AddDirectProductToExponentialLeftAdjunctionMap

  5.2-36 AddDirectProductToExponentialLeftAdjunctionMapWithGivenExponential
6 CartesianCategories automatic generated documentation
Index

 [Top of Book]  [Contents]   [Next Chapter] 
Goto Chapter: Top 1 2 3 4 5 6 Ind

generated by GAPDoc2HTML