Skip to content

Commit

Permalink
WithGiven* in derivations of *Evaluation
Browse files Browse the repository at this point in the history
  • Loading branch information
Tom Kuhmichel committed Nov 29, 2023
1 parent 1b4122a commit d8e4c21
Show file tree
Hide file tree
Showing 4 changed files with 68 additions and 48 deletions.
29 changes: 18 additions & 11 deletions CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -291,7 +291,7 @@ end : CategoryFilter := IsCartesianClosedCategory );
##
AddDerivationToCAP( CartesianEvaluationForCartesianDualWithGivenDirectProduct,
"CartesianEvaluationForCartesianDualWithGivenDirectProduct using the direct product-exponential adjunction and IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject",
[ [ ExponentialToDirectProductAdjunctionMap, 1 ],
[ [ ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct, 1 ],
[ IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject, 1 ] ],

function( cat, s, a, r )
Expand All @@ -300,8 +300,11 @@ AddDerivationToCAP( CartesianEvaluationForCartesianDualWithGivenDirectProduct,
#
# Adjoint( a^v → Exp(a,1) ) = ( a^v × a → 1 )

return ExponentialToDirectProductAdjunctionMap( cat, a, r,
IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject( cat, a ) );
return ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct( cat,
a,
r,
IsomorphismFromCartesianDualObjectToExponentialIntoTerminalObject( cat, a ),
s );

end : CategoryFilter := IsCartesianClosedCategory );

Expand Down Expand Up @@ -682,34 +685,38 @@ end : CategoryFilter := IsCartesianClosedCategory );
##
AddDerivationToCAP( CartesianEvaluationMorphismWithGivenSource,
"CartesianEvaluationMorphismWithGivenSource using the direct product-exponential adjunction on the identity",
[ [ ExponentialToDirectProductAdjunctionMap, 1 ],
[ [ ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct, 1 ],
[ IdentityMorphism, 1 ],
[ ExponentialOnObjects, 1 ] ],

function( cat, a, b, direct_product_object )

# Adjoint( id_Exp(a,b): Exp(a,b) → Exp(a,b) ) = ( Exp(a,b) × a → b )

return ExponentialToDirectProductAdjunctionMap( cat,
a, b,
IdentityMorphism( cat, ExponentialOnObjects( cat, a, b ) ) );
return ExponentialToDirectProductAdjunctionMapWithGivenDirectProduct( cat,
a,
b,
IdentityMorphism( cat, ExponentialOnObjects( cat, a, b ) ),
direct_product_object );

end : CategoryFilter := IsCartesianClosedCategory );

##
AddDerivationToCAP( CartesianCoevaluationMorphismWithGivenRange,
"CartesianCoevaluationMorphismWithGivenRange using the direct product-exponential adjunction on the identity",
[ [ DirectProductToExponentialAdjunctionMap, 1 ],
[ [ DirectProductToExponentialAdjunctionMapWithGivenExponential, 1 ],
[ IdentityMorphism, 1 ],
[ DirectProduct, 1 ] ],

function( cat, a, b, internal_hom )

# Adjoint( id_(a × b): a × b → a × b ) = ( a → Exp(b, a × b) )

return DirectProductToExponentialAdjunctionMap( cat,
a, b,
IdentityMorphism( cat, BinaryDirectProduct( cat, a, b ) ) );
return DirectProductToExponentialAdjunctionMapWithGivenExponential( cat,
a,
b,
IdentityMorphism( cat, BinaryDirectProduct( cat, a, b ) ),
internal_hom );

end : CategoryFilter := IsCartesianClosedCategory );

Expand Down
29 changes: 16 additions & 13 deletions CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -296,7 +296,7 @@ end : CategoryFilter := IsCocartesianCoclosedCategory );
##
AddDerivationToCAP( CocartesianEvaluationForCocartesianDualWithGivenCoproduct,
"CocartesianEvaluationForCocartesianDualWithGivenCoproduct using the coexponential-coproduct adjunction and IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject",
[ [ CoexponentialToCoproductAdjunctionMap, 1 ],
[ [ CoexponentialToCoproductAdjunctionMapWithGivenCoproduct, 1 ],
[ IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject, 1 ] ],

function( cat, s, a, r )
Expand All @@ -305,10 +305,11 @@ AddDerivationToCAP( CocartesianEvaluationForCocartesianDualWithGivenCoproduct,

# Adjoint( Coexp(1,a) → a_v ) = ( 1 → a_v ⊔ a )

return CoexponentialToCoproductAdjunctionMap( cat,
return CoexponentialToCoproductAdjunctionMapWithGivenCoproduct( cat,
s,
a,
IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject( cat, a ) );
IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject( cat, a ),
r );

end : CategoryFilter := IsCocartesianCoclosedCategory );

Expand Down Expand Up @@ -693,35 +694,37 @@ end : CategoryFilter := IsCocartesianCoclosedCategory );
##
AddDerivationToCAP( CocartesianEvaluationMorphismWithGivenRange,
"CocartesianEvaluationMorphismWithGivenRange using the coexponential-coproduct adjunction on the identity",
[ [ CoexponentialToCoproductAdjunctionMap, 1 ],
[ [ CoexponentialToCoproductAdjunctionMapWithGivenCoproduct, 1 ],
[ IdentityMorphism, 1 ],
[ CoexponentialOnObjects, 1 ] ],

function( cat, a, b, coproduct_object )

# Adjoint( id_Coexp(a,b): Coexp(a,b) → Coexp(a,b) ) = ( a → Coexp(a,b) ⊔ b )

return CoexponentialToCoproductAdjunctionMap( cat,
a, b,
IdentityMorphism( cat, CoexponentialOnObjects( cat, a, b ) )
);
return CoexponentialToCoproductAdjunctionMapWithGivenCoproduct( cat,
a,
b,
IdentityMorphism( cat, CoexponentialOnObjects( cat, a, b ) ),
coproduct_object );

end : CategoryFilter := IsCocartesianCoclosedCategory );

AddDerivationToCAP( CocartesianCoevaluationMorphismWithGivenSource,
"CocartesianCoevaluationMorphismWithGivenSource using the coexponential-coproduct adjunction on the identity",
[ [ CoproductToCoexponentialAdjunctionMap, 1 ],
[ [ CoproductToCoexponentialAdjunctionMapWithGivenCoexponential, 1 ],
[ IdentityMorphism, 1 ],
[ Coproduct, 1 ] ],

function( cat, a, b, internal_cohom )

# Adjoint( id_(a ⊔ b): a ⊔ b → a ⊔ b ) = ( Coexp(a ⊔ b, b) → a )

return CoproductToCoexponentialAdjunctionMap( cat,
a, b,
IdentityMorphism( cat, BinaryCoproduct( cat, a, b ) )
);
return CoproductToCoexponentialAdjunctionMapWithGivenCoexponential( cat,
a,
b,
IdentityMorphism( cat, BinaryCoproduct( cat, a, b ) ),
internal_cohom );

end : CategoryFilter := IsCocartesianCoclosedCategory );

Expand Down
29 changes: 18 additions & 11 deletions MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -288,7 +288,7 @@ end : CategoryFilter := IsSymmetricClosedMonoidalCategory );
##
AddDerivationToCAP( EvaluationForDualWithGivenTensorProduct,
"EvaluationForDualWithGivenTensorProduct using the tensor hom adjunction and IsomorphismFromDualObjectToInternalHomIntoTensorUnit",
[ [ InternalHomToTensorProductAdjunctionMap, 1 ],
[ [ InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct, 1 ],
[ IsomorphismFromDualObjectToInternalHomIntoTensorUnit, 1 ] ],

function( cat, s, a, r )
Expand All @@ -297,8 +297,11 @@ AddDerivationToCAP( EvaluationForDualWithGivenTensorProduct,
#
# Adjoint( a^v → Hom(a,1) ) = ( a^v ⊗ a → 1 )

return InternalHomToTensorProductAdjunctionMap( cat, a, r,
IsomorphismFromDualObjectToInternalHomIntoTensorUnit( cat, a ) );
return InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat,
a,
r,
IsomorphismFromDualObjectToInternalHomIntoTensorUnit( cat, a ),
s );

end : CategoryFilter := IsSymmetricClosedMonoidalCategory );

Expand Down Expand Up @@ -679,34 +682,38 @@ end : CategoryFilter := IsSymmetricClosedMonoidalCategory );
##
AddDerivationToCAP( EvaluationMorphismWithGivenSource,
"EvaluationMorphismWithGivenSource using the tensor hom adjunction on the identity",
[ [ InternalHomToTensorProductAdjunctionMap, 1 ],
[ [ InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct, 1 ],
[ IdentityMorphism, 1 ],
[ InternalHomOnObjects, 1 ] ],

function( cat, a, b, tensor_object )

# Adjoint( id_Hom(a,b): Hom(a,b) → Hom(a,b) ) = ( Hom(a,b) ⊗ a → b )

return InternalHomToTensorProductAdjunctionMap( cat,
a, b,
IdentityMorphism( cat, InternalHomOnObjects( cat, a, b ) ) );
return InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat,
a,
b,
IdentityMorphism( cat, InternalHomOnObjects( cat, a, b ) ),
tensor_object );

end : CategoryFilter := IsSymmetricClosedMonoidalCategory );

##
AddDerivationToCAP( CoevaluationMorphismWithGivenRange,
"CoevaluationMorphismWithGivenRange using the tensor hom adjunction on the identity",
[ [ TensorProductToInternalHomAdjunctionMap, 1 ],
[ [ TensorProductToInternalHomAdjunctionMapWithGivenInternalHom, 1 ],
[ IdentityMorphism, 1 ],
[ TensorProductOnObjects, 1 ] ],

function( cat, a, b, internal_hom )

# Adjoint( id_(a ⊗ b): a ⊗ b → a ⊗ b ) = ( a → Hom(b, a ⊗ b) )

return TensorProductToInternalHomAdjunctionMap( cat,
a, b,
IdentityMorphism( cat, TensorProductOnObjects( cat, a, b ) ) );
return TensorProductToInternalHomAdjunctionMapWithGivenInternalHom( cat,
a,
b,
IdentityMorphism( cat, TensorProductOnObjects( cat, a, b ) ),
internal_hom );

end : CategoryFilter := IsSymmetricClosedMonoidalCategory );

Expand Down
29 changes: 16 additions & 13 deletions MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -293,7 +293,7 @@ end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );
##
AddDerivationToCAP( CoclosedEvaluationForCoDualWithGivenTensorProduct,
"CoclosedEvaluationForCoDualWithGivenTensorProduct using the cohom tensor adjunction and IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject",
[ [ InternalCoHomToTensorProductAdjunctionMap, 1 ],
[ [ InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct, 1 ],
[ IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject, 1 ] ],

function( cat, s, a, r )
Expand All @@ -302,10 +302,11 @@ AddDerivationToCAP( CoclosedEvaluationForCoDualWithGivenTensorProduct,

# Adjoint( Cohom(1,a) → a_v ) = ( 1 → a_v ⊗ a )

return InternalCoHomToTensorProductAdjunctionMap( cat,
return InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat,
s,
a,
IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( cat, a ) );
IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( cat, a ),
r );

end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );

Expand Down Expand Up @@ -690,35 +691,37 @@ end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );
##
AddDerivationToCAP( CoclosedEvaluationMorphismWithGivenRange,
"CoclosedEvaluationMorphismWithGivenRange using the cohom tensor adjunction on the identity",
[ [ InternalCoHomToTensorProductAdjunctionMap, 1 ],
[ [ InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct, 1 ],
[ IdentityMorphism, 1 ],
[ InternalCoHomOnObjects, 1 ] ],

function( cat, a, b, tensor_object )

# Adjoint( id_Cohom(a,b): Cohom(a,b) → Cohom(a,b) ) = ( a → Cohom(a,b) ⊗ b )

return InternalCoHomToTensorProductAdjunctionMap( cat,
a, b,
IdentityMorphism( cat, InternalCoHomOnObjects( cat, a, b ) )
);
return InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct( cat,
a,
b,
IdentityMorphism( cat, InternalCoHomOnObjects( cat, a, b ) ),
tensor_object );

end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );

AddDerivationToCAP( CoclosedCoevaluationMorphismWithGivenSource,
"CoclosedCoevaluationMorphismWithGivenSource using the cohom tensor adjunction on the identity",
[ [ TensorProductToInternalCoHomAdjunctionMap, 1 ],
[ [ TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom, 1 ],
[ IdentityMorphism, 1 ],
[ TensorProductOnObjects, 1 ] ],

function( cat, a, b, internal_cohom )

# Adjoint( id_(a ⊗ b): a ⊗ b → a ⊗ b ) = ( Cohom(a ⊗ b, b) → a )

return TensorProductToInternalCoHomAdjunctionMap( cat,
a, b,
IdentityMorphism( cat, TensorProductOnObjects( cat, a, b ) )
);
return TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom( cat,
a,
b,
IdentityMorphism( cat, TensorProductOnObjects( cat, a, b ) ),
internal_cohom );

end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );

Expand Down

0 comments on commit d8e4c21

Please sign in to comment.