search

homalg-project / CAP_project

CAP project -- Categories, Algorithms, and Programming
https://homalg-project.github.io/docs/CAP_project-based/
24 stars 18 forks source link

(co)closed -> left (co)closed #1571

Closed mohamed-barakat closed 8 months ago

mohamed-barakat commented 8 months ago

I am planning the following renamings to free the way for the "right closed monoidal structure"

(a ⊗ -) ⊣ ℋomᵣ(a,-)

and the "right coclosed monoidal structure"

co-ℋomᵣ(-,a) ⊣ (a ⊗ -)

following @TKuh's master thesis.

If there are no objections or alternative suggestions I will soon make a PR and merge it after the CI passes.

CoDualOnMorphisms -> LeftCoDualOnMorphisms
CoDualOnMorphismsWithGivenCoDuals -> LeftCoDualOnMorphismsWithGivenLeftCoDuals
CoDualOnObjects -> LeftCoDualOnObjects
CoDualityTensorProductCompatibilityMorphism -> LeftCoDualityTensorProductCompatibilityMorphism
CoDualityTensorProductCompatibilityMorphismWithGivenObjects -> LeftCoDualityTensorProductCompatibilityMorphismWithGivenObjects
CoLambdaElimination -> LeftCoclosedMonoidalLambdaElimination
CoLambdaIntroduction -> LeftCoclosedMonoidalLambdaIntroduction
CoclosedCoevaluationForCoDual -> LeftCoclosedMonoidalCoevaluationForLeftCoDual
CoclosedCoevaluationForCoDualWithGivenTensorProduct -> LeftCoclosedMonoidalCoevaluationForLeftCoDualWithGivenTensorProduct
CoclosedCoevaluationMorphism -> LeftCoclosedMonoidalCoevaluationMorphism
CoclosedCoevaluationMorphismWithGivenSource -> LeftCoclosedMonoidalCoevaluationMorphismWithGivenSource
CoclosedEvaluationForCoDual -> LeftCoclosedMonoidalEvaluationForLeftCoDual
CoclosedEvaluationForCoDualWithGivenTensorProduct -> LeftCoclosedMonoidalEvaluationForLeftCoDualWithGivenTensorProduct
CoclosedEvaluationMorphism -> LeftCoclosedMonoidalEvaluationMorphism
CoclosedEvaluationMorphismWithGivenRange -> LeftCoclosedMonoidalEvaluationMorphismWithGivenRange
CoevaluationForDual -> CoevaluationForLeftDual
CoevaluationForDualWithGivenTensorProduct -> CoevaluationForLeftDualWithGivenTensorProduct
CoevaluationMorphism -> LeftClosedMonoidalCoevaluationMorphism
CoevaluationMorphismWithGivenRange -> LeftClosedMonoidalCoevaluationMorphismWithGivenRange
DualOnMorphisms -> LeftDualOnMorphisms
DualOnMorphismsWithGivenDuals -> LeftDualOnMorphismsWithGivenLeftDuals
DualOnObjects -> LeftDualOnObjects
EvaluationForDual -> LeftClosedMonoidalEvaluationForLeftDual
EvaluationForDualWithGivenTensorProduct -> LeftClosedMonoidalEvaluationForLeftDualWithGivenTensorProduct
EvaluationMorphism -> LeftClosedMonoidalEvaluationMorphism
EvaluationMorphismWithGivenSource -> LeftClosedMonoidalEvaluationMorphismWithGivenSource
InternalCoHomOnMorphisms -> LeftInternalCoHomOnMorphisms
InternalCoHomOnMorphismsWithGivenInternalCoHoms -> LeftInternalCoHomOnMorphismsWithGivenLeftInternalCoHoms
InternalCoHomOnObjects -> LeftInternalCoHomOnObjects
InternalCoHomTensorProductCompatibilityMorphism -> LeftInternalCoHomTensorProductCompatibilityMorphism
InternalCoHomTensorProductCompatibilityMorphismInverse -> LeftInternalCoHomTensorProductCompatibilityMorphismInverse
InternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects -> LeftInternalCoHomTensorProductCompatibilityMorphismInverseWithGivenObjects
InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects -> LeftInternalCoHomTensorProductCompatibilityMorphismWithGivenObjects
InternalCoHomToTensorProductAdjunctionMap -> LeftInternalCoHomToTensorProductAdjunctionMap
InternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct -> LeftInternalCoHomToTensorProductAdjunctionMapWithGivenTensorProduct
InternalHomOnMorphisms -> LeftInternalHomOnMorphisms
InternalHomOnMorphismsWithGivenInternalHoms -> LeftInternalHomOnMorphismsWithGivenLeftInternalHoms
InternalHomOnObjects -> LeftInternalHomOnObjects
InternalHomToTensorProductAdjunctionMap -> LeftInternalHomToTensorProductAdjunctionMap
InternalHomToTensorProductAdjunctionMapWithGivenTensorProduct -> LeftInternalHomToTensorProductAdjunctionMapWithGivenTensorProduct
IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit -> IsomorphismFromLeftCoDualObjectToLeftInternalCoHomFromTensorUnit
IsomorphismFromDualObjectToInternalHomIntoTensorUnit -> IsomorphismFromLeftDualObjectToLeftInternalHomIntoTensorUnit
IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject -> IsomorphismFromLeftInternalCoHomFromTensorUnitToLeftCoDualObject
IsomorphismFromInternalCoHomToObject -> IsomorphismFromLeftInternalCoHomToObject
IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom -> IsomorphismFromLeftInternalCoHomToObjectWithGivenLeftInternalCoHom
IsomorphismFromInternalCoHomToTensorProductWithCoDualObject -> IsomorphismFromLeftInternalCoHomToTensorProductWithLeftCoDualObject
IsomorphismFromInternalHomIntoTensorUnitToDualObject -> IsomorphismFromLeftInternalHomIntoTensorUnitToLeftDualObject
IsomorphismFromInternalHomToObject -> IsomorphismFromLeftInternalHomToObject
IsomorphismFromInternalHomToObjectWithGivenInternalHom -> IsomorphismFromLeftInternalHomToObjectWithGivenLeftInternalHom
IsomorphismFromInternalHomToTensorProductWithDualObject -> IsomorphismFromLeftInternalHomToTensorProductWithLeftDualObject
IsomorphismFromObjectToInternalCoHom -> IsomorphismFromObjectToLeftInternalCoHom
IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom -> IsomorphismFromObjectToLeftInternalCoHomWithGivenLeftInternalCoHom
IsomorphismFromObjectToInternalHom -> IsomorphismFromObjectToLeftInternalHom
IsomorphismFromObjectToInternalHomWithGivenInternalHom -> IsomorphismFromObjectToLeftInternalHomWithGivenLeftInternalHom
IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom -> IsomorphismFromTensorProductWithLeftCoDualObjectToLeftInternalCoHom
IsomorphismFromTensorProductWithDualObjectToInternalHom -> IsomorphismFromTensorProductWithLeftDualObjectToLeftInternalHom
LambdaElimination -> LeftClosedMonoidalLambdaElimination
LambdaIntroduction -> LeftClosedMonoidalLambdaIntroduction
MonoidalPostCoComposeMorphism -> LeftCoclosedMonoidalPostCoComposeMorphism
MonoidalPostCoComposeMorphismWithGivenObjects -> LeftCoclosedMonoidalPostCoComposeMorphismWithGivenObjects
MonoidalPostComposeMorphism -> LeftClosedMonoidalPostComposeMorphism
MonoidalPostComposeMorphismWithGivenObjects -> LeftClosedMonoidalPostComposeMorphismWithGivenObjects
MonoidalPreCoComposeMorphism -> LeftCoclosedMonoidalPreCoComposeMorphism
MonoidalPreCoComposeMorphismWithGivenObjects -> LeftCoclosedMonoidalPreCoComposeMorphismWithGivenObjects
MonoidalPreComposeMorphism -> LeftClosedMonoidalPreComposeMorphism
MonoidalPreComposeMorphismWithGivenObjects -> LeftClosedMonoidalPreComposeMorphismWithGivenObjects
MorphismFromBidual -> MorphismFromLeftBidual
MorphismFromBidualWithGivenBidual -> MorphismFromLeftBidualWithGivenLeftBidual
MorphismFromCoBidual -> MorphismFromLeftCoBidual
MorphismFromCoBidualWithGivenCoBidual -> MorphismFromLeftCoBidualWithGivenLeftCoBidual
MorphismFromInternalCoHomToTensorProduct -> MorphismFromLeftInternalCoHomToTensorProduct
MorphismFromInternalCoHomToTensorProductWithGivenObjects -> MorphismFromLeftInternalCoHomToTensorProductWithGivenObjects
MorphismFromInternalHomToTensorProduct -> MorphismFromLeftInternalHomToTensorProduct
MorphismFromInternalHomToTensorProductWithGivenObjects -> MorphismFromLeftInternalHomToTensorProductWithGivenObjects
MorphismFromTensorProductToInternalCoHom -> MorphismFromTensorProductToLeftInternalCoHom
MorphismFromTensorProductToInternalCoHomWithGivenObjects -> MorphismFromTensorProductToLeftInternalCoHomWithGivenObjects
MorphismFromTensorProductToInternalHom -> MorphismFromTensorProductToLeftInternalHom
MorphismFromTensorProductToInternalHomWithGivenObjects -> MorphismFromTensorProductToLeftInternalHomWithGivenObjects
MorphismToBidual -> MorphismToLeftBidual
MorphismToBidualWithGivenBidual -> MorphismToLeftBidualWithGivenLeftBidual
MorphismToCoBidual -> MorphismToLeftCoBidual
MorphismToCoBidualWithGivenCoBidual -> MorphismToLeftCoBidualWithGivenLeftCoBidual
TensorProductDualityCompatibilityMorphism -> TensorProductLeftDualityCompatibilityMorphism
TensorProductDualityCompatibilityMorphismWithGivenObjects -> TensorProductLeftDualityCompatibilityMorphismWithGivenObjects
TensorProductInternalHomCompatibilityMorphism -> TensorProductLeftInternalHomCompatibilityMorphism
TensorProductInternalHomCompatibilityMorphismInverse -> TensorProductLeftInternalHomCompatibilityMorphismInverse
TensorProductInternalHomCompatibilityMorphismInverseWithGivenObjects -> TensorProductLeftInternalHomCompatibilityMorphismInverseWithGivenObjects
TensorProductInternalHomCompatibilityMorphismWithGivenObjects -> TensorProductLeftInternalHomCompatibilityMorphismWithGivenObjects
TensorProductToInternalCoHomAdjunctionMap -> TensorProductToLeftInternalCoHomAdjunctionMap
TensorProductToInternalCoHomAdjunctionMapWithGivenInternalCoHom -> TensorProductToLeftInternalCoHomAdjunctionMapWithGivenLeftInternalCoHom
TensorProductToInternalHomAdjunctionMap -> TensorProductToLeftInternalHomAdjunctionMap
TensorProductToInternalHomAdjunctionMapWithGivenInternalHom -> TensorProductToLeftInternalHomAdjunctionMapWithGivenLeftInternalHom
UniversalPropertyOfCoDual -> UniversalPropertyOfLeftCoDual
UniversalPropertyOfDual -> UniversalPropertyOfLeftDual
mohamed-barakat commented 8 months ago

I will keep the current names as aliases for the left closed monoidal structure. After introducing the right closed monoidal structure I suggest using the current names for it.

mohamed-barakat commented 8 months ago

Since yesterday I made some updates to the above list. Apart from adding the synonyms the PR is now working locally. In this sense, the above list is now stable.

TKuh commented 8 months ago

The names look good to me, but it's admittedly hard to read.

mohamed-barakat commented 8 months ago

The names look good to me, but it's admittedly hard to read.

Do you have alternative suggestions for how to simplify them? Here is the rationale:

  1. The names must distinguish between Left and Right.
  2. Left/Right must sometimes be followed by C(oc)losed to make sense.
  3. C(oc)closed must be followed by Monoidal (a) to make sense and (b) to specialize Monoidal to the name of specific monoidal structures.