|
# SPDX-License-Identifier: GPL-2.0-or-later
# MonoidalCategories: Monoidal and monoidal (co)closed categories
#
# Implementations
#
InstallGlobalFunction( "ClosedMonoidalCategoriesTest",
function( cat, opposite, a, b, c, d, alpha, beta, gamma, delta, epsilon, zeta )
local verbose,
a_op, c_op,
b_op, d_op,
id_a_tensor_b, id_b_tensor_a,
hom_ab, cohom_ab_op, id_hom_ab,
hom_ba, cohom_ba_op, id_hom_ba,
alpha_op, hom_alpha_beta, cohom_alpha_beta_op,
beta_op, hom_beta_alpha, cohom_beta_alpha_op,
ev_ab, coev_ab, cocl_ev_ab_op, cocl_coev_ab_op,
ev_ba, coev_ba, cocl_ev_ba_op, cocl_coev_ba_op,
raiso, laiso, H_ab_ba_c,
alpha_tensor_beta, alpha_tensor_beta_op,
beta_tensor_alpha, beta_tensor_alpha_op,
hom_to_tensor_adjunction_on_id_hom_ab, tensor_to_hom_adjunction_on_id_a_tensor_b,
hom_to_tensor_adjunction_on_id_hom_ba, tensor_to_hom_adjunction_on_id_b_tensor_a,
tensor_to_hom_adjunction_on_alpha_tensor_beta, tensor_to_cohom_adjunction_on_alpha_tensor_beta_op,
tensor_to_hom_adjunction_on_beta_tensor_alpha, tensor_to_cohom_adjunction_on_beta_tensor_alpha_op,
hom_to_tensor_adjunction_on_hom_alpha_beta, cohom_to_tensor_adjunction_on_cohom_alpha_beta_op,
hom_to_tensor_adjunction_on_hom_beta_alpha, cohom_to_tensor_adjunction_on_cohom_beta_alpha_op,
precompose_abc, precocompose_abc_op, postcompose_abc, postcocompose_abc_op,
precompose_cba, precocompose_cba_op, postcompose_cba, postcocompose_cba_op,
a_dual, a_codual_op, dual_alpha, codual_alpha_op,
b_dual, b_codual_op, dual_beta, codual_beta_op,
ev_for_dual_a, cocl_ev_for_codual_a_op,
ev_for_dual_b, cocl_ev_for_codual_b_op,
morphism_to_bidual_a, morphism_from_cobidual_a_op,
morphism_to_bidual_b, morphism_from_cobidual_b_op,
tensor_to_hom_compatibility_abcd, cohom_to_tensor_compatibility_abcd_op,
tensor_to_hom_compatibility_cadb, cohom_to_tensor_compatibility_bdac_op,
tensor_product_duality_compatibility_ab, coduality_tensor_product_compatibility_ab_op,
tensor_product_duality_compatibility_ba, coduality_tensor_product_compatibility_ba_op,
morphism_from_tensor_product_to_hom_ab, morphism_from_cohom_to_tensor_product_ab_op,
morphism_from_tensor_product_to_hom_ba, morphism_from_cohom_to_tensor_product_ba_op,
isomorphism_from_dual_to_hom_a, isomorphism_from_hom_to_dual_a,
isomorphism_from_dual_to_hom_b, isomorphism_from_hom_to_dual_b,
isomorphism_from_codual_to_cohom_a_op, isomorphism_from_cohom_to_codual_a_op,
isomorphism_from_codual_to_cohom_b_op, isomorphism_from_cohom_to_codual_b_op,
gamma_op, universal_property_of_dual_gamma, universal_property_of_codual_gamma_op,
delta_op, universal_property_of_dual_delta, universal_property_of_codual_delta_op,
lambda_intro_alpha, colambda_intro_alpha_op,
lambda_intro_beta, colambda_intro_beta_op,
epsilon_op, lambda_elim_epsilon, colambda_elim_epsilon_op,
zeta_op, lambda_elim_zeta, colambda_elim_zeta_op,
isomorphism_from_a_to_hom, isomorphism_from_hom_to_a, isomorphism_from_a_to_cohom_op, isomorphism_from_cohom_to_a_op,
isomorphism_from_b_to_hom, isomorphism_from_hom_to_b, isomorphism_from_b_to_cohom_op, isomorphism_from_cohom_to_b_op;
a_op := Opposite( opposite, a );
b_op := Opposite( opposite, b );
c_op := Opposite( opposite, c );
d_op := Opposite( opposite, d );
alpha_op := Opposite( opposite, alpha );
beta_op := Opposite( opposite, beta );
verbose := ValueOption( "verbose" ) = true;
if CanCompute( cat, "InternalHomOnObjects" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'InternalHomOnObjects' ..." );
fi;
hom_ab := InternalHomOnObjects( a, b );
hom_ba := InternalHomOnObjects( b, a );
cohom_ab_op := InternalCoHomOnObjects( a_op, b_op );
cohom_ba_op := InternalCoHomOnObjects( b_op, a_op );
Assert( 0, IsEqualForObjects( cohom_ab_op, Opposite( opposite, hom_ba ) ) );
Assert( 0, IsEqualForObjects( cohom_ba_op, Opposite( opposite, hom_ab ) ) );
# Opposite must be self-inverse
Assert( 0, IsEqualForObjects( hom_ab, Opposite( cohom_ba_op ) ) );
Assert( 0, IsEqualForObjects( hom_ba, Opposite( cohom_ab_op ) ) );
# Convenience methods in the opposite category
Assert( 0, IsEqualForObjects( cohom_ab_op, InternalCoHom( a_op, b_op ) ) );
Assert( 0, IsEqualForObjects( cohom_ba_op, InternalCoHom( b_op, a_op ) ) );
fi;
if CanCompute( cat, "InternalHomOnMorphisms" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'InternalHomOnMorphisms' ..." );
fi;
hom_alpha_beta := InternalHomOnMorphisms( alpha, beta );
hom_beta_alpha := InternalHomOnMorphisms( beta, alpha );
cohom_alpha_beta_op := InternalCoHomOnMorphisms( alpha_op, beta_op );
cohom_beta_alpha_op := InternalCoHomOnMorphisms( beta_op, alpha_op );
Assert( 0, IsCongruentForMorphisms( cohom_alpha_beta_op, Opposite( opposite, hom_beta_alpha ) ) );
Assert( 0, IsCongruentForMorphisms( cohom_beta_alpha_op, Opposite( opposite, hom_alpha_beta ) ) );
# Opposite must be self-inverse
Assert( 0, IsCongruentForMorphisms( hom_alpha_beta, Opposite( cohom_beta_alpha_op ) ) );
Assert( 0, IsCongruentForMorphisms( hom_beta_alpha, Opposite( cohom_alpha_beta_op ) ) );
# Convenience methods in the opposite category
Assert( 0, IsCongruentForMorphisms( cohom_alpha_beta_op, InternalCoHom( alpha_op, beta_op ) ) );
Assert( 0, IsCongruentForMorphisms( cohom_beta_alpha_op, InternalCoHom( beta_op, alpha_op ) ) );
fi;
if CanCompute( cat, "ClosedMonoidalRightEvaluationMorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'ClosedMonoidalRightEvaluationMorphism' ..." );
fi;
ev_ab := ClosedMonoidalRightEvaluationMorphism( a, b );
ev_ba := ClosedMonoidalRightEvaluationMorphism( b, a );
cocl_ev_ab_op := CoclosedMonoidalRightEvaluationMorphism( a_op, b_op );
cocl_ev_ba_op := CoclosedMonoidalRightEvaluationMorphism( b_op, a_op );
# Arguments must be reversed for evaluations
Assert( 0, IsCongruentForMorphisms( cocl_ev_ab_op, Opposite( opposite, ev_ab ) ) );
Assert( 0, IsCongruentForMorphisms( cocl_ev_ba_op, Opposite( opposite, ev_ba ) ) );
fi;
if CanCompute( cat, "ClosedMonoidalRightCoevaluationMorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'ClosedMonoidalRightEvaluationMorphism' ..." );
fi;
coev_ab := ClosedMonoidalRightCoevaluationMorphism( a, b );
coev_ba := ClosedMonoidalRightCoevaluationMorphism( b, a );
cocl_coev_ab_op := CoclosedMonoidalRightCoevaluationMorphism( a_op, b_op );
cocl_coev_ba_op := CoclosedMonoidalRightCoevaluationMorphism( b_op, a_op );
Assert( 0, IsCongruentForMorphisms( cocl_coev_ab_op, Opposite( opposite, coev_ab ) ) );
Assert( 0, IsCongruentForMorphisms( cocl_coev_ba_op, Opposite( opposite, coev_ba ) ) );
fi;
if CanCompute( cat, "ClosedMonoidalLeftEvaluationMorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'ClosedMonoidalLeftEvaluationMorphism' ..." );
fi;
ev_ab := ClosedMonoidalLeftEvaluationMorphism( a, b );
ev_ba := ClosedMonoidalLeftEvaluationMorphism( b, a );
cocl_ev_ab_op := CoclosedMonoidalLeftEvaluationMorphism( a_op, b_op );
cocl_ev_ba_op := CoclosedMonoidalLeftEvaluationMorphism( b_op, a_op );
# Arguments must be reversed for evaluations
Assert( 0, IsCongruentForMorphisms( cocl_ev_ab_op, Opposite( opposite, ev_ab ) ) );
Assert( 0, IsCongruentForMorphisms( cocl_ev_ba_op, Opposite( opposite, ev_ba ) ) );
fi;
if CanCompute( cat, "ClosedMonoidalLeftCoevaluationMorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'ClosedMonoidalLeftEvaluationMorphism' ..." );
fi;
coev_ab := ClosedMonoidalLeftCoevaluationMorphism( a, b );
coev_ba := ClosedMonoidalLeftCoevaluationMorphism( b, a );
cocl_coev_ab_op := CoclosedMonoidalLeftCoevaluationMorphism( a_op, b_op );
cocl_coev_ba_op := CoclosedMonoidalLeftCoevaluationMorphism( b_op, a_op );
Assert( 0, IsCongruentForMorphisms( cocl_coev_ab_op, Opposite( opposite, coev_ab ) ) );
Assert( 0, IsCongruentForMorphisms( cocl_coev_ba_op, Opposite( opposite, coev_ba ) ) );
fi;
if CanCompute( cat, "TensorProductToInternalHomRightAdjunctionIsomorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'TensorProductToInternalHomRightAdjunctionIsomorphism' ..." );
fi;
raiso := TensorProductToInternalHomRightAdjunctionIsomorphism( a, b, c );
Assert( 0, IsIsomorphism( raiso ) );
if CanCompute( cat, "TensorProductToInternalHomLeftAdjunctionIsomorphism" ) then
laiso := TensorProductToInternalHomLeftAdjunctionIsomorphism( b, a, c );
Assert( 0, IsIsomorphism( laiso ) );
if CanCompute( cat, "Braiding" ) then
H_ab_ba_c := HomStructure( Braiding( a, b ), c );
Assert( 0, IsIsomorphism( H_ab_ba_c ) );
Assert( 0, IsEqualForMorphisms( laiso, PreCompose( H_ab_ba_c, raiso ) ) );
fi;
fi;
fi;
if CanCompute( cat, "InternalHomToTensorProductRightAdjunctionIsomorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'InternalHomToTensorProductRightAdjunctionIsomorphism' ..." );
fi;
raiso := InternalHomToTensorProductRightAdjunctionIsomorphism( a, b, c );
Assert( 0, IsIsomorphism( raiso ) );
if CanCompute( cat, "InternalHomToTensorProductLeftAdjunctionIsomorphism" ) then
laiso := InternalHomToTensorProductLeftAdjunctionIsomorphism( b, a, c );
Assert( 0, IsIsomorphism( laiso ) );
if CanCompute( cat, "Braiding" ) then
H_ab_ba_c := HomStructure( Braiding( a, b ), c );
Assert( 0, IsIsomorphism( H_ab_ba_c ) );
Assert( 0, IsEqualForMorphisms( raiso, PreCompose( H_ab_ba_c, laiso ) ) );
fi;
fi;
fi;
if CanCompute( cat, "TensorProductToInternalHomLeftAdjunctMorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'TensorProductToInternalHomLeftAdjunctMorphism' ..." );
fi;
######################################
#
# alpha: a → b
# beta: c → d
#
# alpha_tensor_beta: a ⊗ c → b ⊗ d
# beta_tensor_alpha: c ⊗ a → d ⊗ b
#
######################################
#
# alpha_op: b → a
# beta_op: d → c
#
# alpha_tensor_beta_op: b ⊗ d → a ⊗ c
# beta_tensor_alpha_op: d ⊗ b → c ⊗ a
#
######################################
alpha_tensor_beta := TensorProductOnMorphisms( alpha, beta );
beta_tensor_alpha := TensorProductOnMorphisms( beta, alpha );
alpha_tensor_beta_op := TensorProductOnMorphisms( opposite, alpha_op, beta_op );
beta_tensor_alpha_op := TensorProductOnMorphisms( opposite, beta_op, alpha_op );
# Adjoint( a ⊗ c → b ⊗ d ) == a → Hom( c, b ⊗ d )
tensor_to_hom_adjunction_on_alpha_tensor_beta := TensorProductToInternalHomLeftAdjunctMorphism( a, c, alpha_tensor_beta );
# Adjoint( c ⊗ a → d ⊗ b ) == c → Hom( a, d ⊗ b )
tensor_to_hom_adjunction_on_beta_tensor_alpha := TensorProductToInternalHomLeftAdjunctMorphism( c, a, beta_tensor_alpha );
# Adjoint( b ⊗ d → a ⊗ c ) == Cohom( b ⊗ d, c ) → a
tensor_to_cohom_adjunction_on_alpha_tensor_beta_op := TensorProductToInternalCoHomLeftAdjunctMorphism( a_op, c_op, alpha_tensor_beta_op );
# Adjoint( d ⊗ b → c ⊗ a ) == Cohom( d ⊗ b, a ) → c
tensor_to_cohom_adjunction_on_beta_tensor_alpha_op := TensorProductToInternalCoHomLeftAdjunctMorphism( c_op, a_op, beta_tensor_alpha_op );
# coHom( b ⊗ d, c ) → a == op( a → Hom( c, b ⊗ d ) )
Assert( 0, IsCongruentForMorphisms( tensor_to_cohom_adjunction_on_alpha_tensor_beta_op, Opposite( opposite, tensor_to_hom_adjunction_on_alpha_tensor_beta ) ) );
# coHom( d ⊗ b, a ) → c == op( c → Hom( a, d ⊗ b ) )
Assert( 0, IsCongruentForMorphisms( tensor_to_cohom_adjunction_on_beta_tensor_alpha_op, Opposite( opposite, tensor_to_hom_adjunction_on_beta_tensor_alpha ) ) );
fi;
if CanCompute( cat, "InternalHomToTensorProductLeftAdjunctMorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'InternalHomToTensorProductLeftAdjunctMorphism' ..." );
fi;
#####################################################
#
# hom_alpha_beta: Hom( b, c ) → Hom( a, d )
# hom_beta_alpha: Hom( d, a ) → Hom( c, b )
#
#####################################################
#
# cohom_alpha_beta: coHom( a, d ) → coHom( b, c )
# cohom_beta_alpha: coHom( c, b ) → coHom( d, a )
#
# cohom_alpha_beta_op: coHom( b, c ) → coHom( a, d )
# cohom_beta_alpha_op: coHom( d, a ) → coHom( c, b )
#
#####################################################
# Adjoint( Hom( b, c ) → Hom( a, d ) ) == Hom( b, c ) ⊗ a → d
hom_to_tensor_adjunction_on_hom_alpha_beta := InternalHomToTensorProductLeftAdjunctMorphism( a, d, hom_alpha_beta );
# Adjoint( Hom( d, a ) → Hom( c, b ) ) == Hom( d, a ) ⊗ c → b
hom_to_tensor_adjunction_on_hom_beta_alpha := InternalHomToTensorProductLeftAdjunctMorphism( c, b, hom_beta_alpha );
# Adjoint( Cohom( b, c ) → Cohom( a, d ) ) == b → Cohom( a, d ) ⊗ c
cohom_to_tensor_adjunction_on_cohom_alpha_beta_op := InternalCoHomToTensorProductLeftAdjunctMorphism( b_op, c_op, cohom_alpha_beta_op );
# Adjoint( Cohom( d, a ) → Cohom( c, b ) ) == d → Cohom( c, b ) ⊗ a
cohom_to_tensor_adjunction_on_cohom_beta_alpha_op := InternalCoHomToTensorProductLeftAdjunctMorphism( d_op, a_op, cohom_beta_alpha_op );
# b → coHom( a, d ) ⊗ c == op( Hom( d, a ) ⊗ c → b )
Assert( 0, IsCongruentForMorphisms( cohom_to_tensor_adjunction_on_cohom_alpha_beta_op, Opposite( opposite, hom_to_tensor_adjunction_on_hom_beta_alpha ) ) );
# d → coHom( c, b ) ⊗ a == op( Hom( b, c ) ⊗ a → d )
Assert( 0, IsCongruentForMorphisms( cohom_to_tensor_adjunction_on_cohom_beta_alpha_op, Opposite( opposite, hom_to_tensor_adjunction_on_hom_alpha_beta ) ) );
fi;
if CanCompute( cat, "MonoidalPreComposeMorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'MonoidalPreComposeMorphism' ..." );
fi;
precompose_abc := MonoidalPreComposeMorphism( a, b, c );
precompose_cba := MonoidalPreComposeMorphism( c, b, a );
precocompose_abc_op := MonoidalPreCoComposeMorphism( a_op, b_op, c_op );
precocompose_cba_op := MonoidalPreCoComposeMorphism( c_op, b_op, a_op );
Assert( 0, IsCongruentForMorphisms( precocompose_abc_op, Opposite( opposite, precompose_cba ) ) );
Assert( 0, IsCongruentForMorphisms( precocompose_cba_op, Opposite( opposite, precompose_abc ) ) );
fi;
if CanCompute( cat, "MonoidalPostComposeMorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'MonoidalPostComposeMorphism' ..." );
fi;
postcompose_abc := MonoidalPostComposeMorphism( a, b, c );
postcompose_cba := MonoidalPostComposeMorphism( c, b, a );
postcocompose_abc_op := MonoidalPostCoComposeMorphism( a_op, b_op, c_op );
postcocompose_cba_op := MonoidalPostCoComposeMorphism( c_op, b_op, a_op );
Assert( 0, IsCongruentForMorphisms( postcocompose_abc_op, Opposite( opposite, postcompose_cba ) ) );
Assert( 0, IsCongruentForMorphisms( postcocompose_cba_op, Opposite( opposite, postcompose_abc ) ) );
fi;
if CanCompute( cat, "DualOnObjects" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'DualOnObjects' ..." );
fi;
a_dual := DualOnObjects( a );
b_dual := DualOnObjects( b );
a_codual_op := CoDualOnObjects( a_op );
b_codual_op := CoDualOnObjects( b_op );
Assert( 0, IsEqualForObjects( a_codual_op, Opposite( opposite, a_dual ) ) );
Assert( 0, IsEqualForObjects( b_codual_op, Opposite( opposite, b_dual ) ) );
fi;
if CanCompute( cat, "DualOnMorphisms" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'DualOnMorphisms' ..." );
fi;
dual_alpha := DualOnMorphisms( alpha );
dual_beta := DualOnMorphisms( beta );
codual_alpha_op := CoDualOnMorphisms( alpha_op );
codual_beta_op := CoDualOnMorphisms( beta_op );
Assert( 0, IsCongruentForMorphisms( codual_alpha_op, Opposite( opposite, dual_alpha ) ) );
Assert( 0, IsCongruentForMorphisms( codual_beta_op, Opposite( opposite, dual_beta ) ) );
fi;
if CanCompute( cat, "EvaluationForDual" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'EvaluationForDual' ..." );
fi;
ev_for_dual_a := EvaluationForDual( a );
ev_for_dual_b := EvaluationForDual( b );
cocl_ev_for_codual_a_op := CoclosedEvaluationForCoDual( a_op );
cocl_ev_for_codual_b_op := CoclosedEvaluationForCoDual( b_op );
Assert( 0, IsCongruentForMorphisms( cocl_ev_for_codual_a_op, Opposite( opposite, ev_for_dual_a ) ) );
Assert( 0, IsCongruentForMorphisms( cocl_ev_for_codual_b_op, Opposite( opposite, ev_for_dual_b ) ) );
fi;
if CanCompute( cat, "MorphismToBidual" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'MorphismToBidual' ..." );
fi;
morphism_to_bidual_a := MorphismToBidual( a );
morphism_to_bidual_b := MorphismToBidual( b );
morphism_from_cobidual_a_op := MorphismFromCoBidual( a_op );
morphism_from_cobidual_b_op := MorphismFromCoBidual( b_op );
Assert( 0, IsCongruentForMorphisms( morphism_from_cobidual_a_op, Opposite( opposite, morphism_to_bidual_a ) ) );
Assert( 0, IsCongruentForMorphisms( morphism_from_cobidual_b_op, Opposite( opposite, morphism_to_bidual_b ) ) );
fi;
if CanCompute( cat, "TensorProductInternalHomCompatibilityMorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'TensorProductInternalHomCompatibilityMorphism' ..." );
fi;
# Hom( a, b ) ⊗ Hom( c, d ) → Hom( a ⊗ c, b ⊗ d )
tensor_to_hom_compatibility_abcd := TensorProductInternalHomCompatibilityMorphism( [ a, b, c, d ] );
# Hom( c, a ) ⊗ Hom( d, b ) → Hom( c ⊗ d, a ⊗ b )
tensor_to_hom_compatibility_cadb := TensorProductInternalHomCompatibilityMorphism( [ c, a, d, b ] );
# Cohom( a ⊗ b, c ⊗ d ) → Cohom( a, c ) ⊗ Cohom( b, d )
cohom_to_tensor_compatibility_abcd_op := InternalCoHomTensorProductCompatibilityMorphism( [ a_op, b_op, c_op, d_op ] );
# Cohom( b ⊗ d, a ⊗ c ) → Cohom( b, a ) ⊗ Cohom( d, c )
cohom_to_tensor_compatibility_bdac_op := InternalCoHomTensorProductCompatibilityMorphism( [ b_op, d_op, a_op, c_op ] );
# coHom( a ⊗ b, c ⊗ d ) → coHom( a, c ) ⊗ coHom( b, d ) == op( Hom( c, a ) ⊗ Hom( d, b ) → Hom( c ⊗ d, a ⊗ b ) )
Assert( 0, IsCongruentForMorphisms( cohom_to_tensor_compatibility_abcd_op, Opposite( opposite, tensor_to_hom_compatibility_cadb ) ) );
# coHom( b ⊗ d, a ⊗ c ) → coHom( b, a ) ⊗ coHom( d, c ) == op( Hom( a, b ) ⊗ Hom( c, d ) → Hom( a ⊗ c, b ⊗ d ) )
Assert( 0, IsCongruentForMorphisms( cohom_to_tensor_compatibility_bdac_op, Opposite( opposite, tensor_to_hom_compatibility_abcd ) ) );
fi;
if CanCompute( cat, "TensorProductDualityCompatibilityMorphism" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'TensorProductDualityCompatibilityMorphism' ..." );
fi;
# a^v ⊗ b^v → (a ⊗ b)^v
tensor_product_duality_compatibility_ab := TensorProductDualityCompatibilityMorphism( a, b );
# b^v ⊗ a^v → (b ⊗ a)^v
tensor_product_duality_compatibility_ba := TensorProductDualityCompatibilityMorphism( b, a );
# (a ⊗ b)_v → a_v ⊗ b_v
coduality_tensor_product_compatibility_ab_op := CoDualityTensorProductCompatibilityMorphism( a_op, b_op );
# (b ⊗ a)_v → b_v ⊗ a_v
coduality_tensor_product_compatibility_ba_op := CoDualityTensorProductCompatibilityMorphism( b_op, a_op );
# (a ⊗ b)_v → a_v ⊗ b_v == op( a^v ⊗ b^v → (a ⊗ b)^v )
Assert( 0, IsCongruentForMorphisms( coduality_tensor_product_compatibility_ab_op, Opposite( opposite, tensor_product_duality_compatibility_ab ) ) );
# (b ⊗ a)_v → b_v ⊗ a_v == op( b^v ⊗ a^v → (b ⊗ a)^v )
Assert( 0, IsCongruentForMorphisms( coduality_tensor_product_compatibility_ba_op, Opposite( opposite, tensor_product_duality_compatibility_ba ) ) );
fi;
if CanCompute( cat, "MorphismFromTensorProductToInternalHom" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'MorphismFromTensorProductToInternalHom' ..." );
fi;
morphism_from_tensor_product_to_hom_ab := MorphismFromTensorProductToInternalHom( a, b );
morphism_from_tensor_product_to_hom_ba := MorphismFromTensorProductToInternalHom( b, a );
morphism_from_cohom_to_tensor_product_ab_op := MorphismFromInternalCoHomToTensorProduct( a_op, b_op );
morphism_from_cohom_to_tensor_product_ba_op := MorphismFromInternalCoHomToTensorProduct( b_op, a_op );
Assert( 0, IsCongruentForMorphisms( morphism_from_cohom_to_tensor_product_ab_op, Opposite( opposite, morphism_from_tensor_product_to_hom_ba ) ) );
Assert( 0, IsCongruentForMorphisms( morphism_from_cohom_to_tensor_product_ba_op, Opposite( opposite, morphism_from_tensor_product_to_hom_ab ) ) );
fi;
if CanCompute( cat, "IsomorphismFromDualObjectToInternalHomIntoTensorUnit" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'IsomorphismFromDualObjectToInternalHomIntoTensorUnit' ..." );
fi;
isomorphism_from_dual_to_hom_a := IsomorphismFromDualObjectToInternalHomIntoTensorUnit( a );
isomorphism_from_dual_to_hom_b := IsomorphismFromDualObjectToInternalHomIntoTensorUnit( b );
isomorphism_from_cohom_to_codual_a_op := IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( a_op );
isomorphism_from_cohom_to_codual_b_op := IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( b_op );
Assert( 0, IsCongruentForMorphisms( isomorphism_from_cohom_to_codual_a_op, Opposite( opposite, isomorphism_from_dual_to_hom_a ) ) );
Assert( 0, IsCongruentForMorphisms( isomorphism_from_cohom_to_codual_b_op, Opposite( opposite, isomorphism_from_dual_to_hom_b ) ) );
fi;
if CanCompute( cat, "IsomorphismFromInternalHomIntoTensorUnitToDualObject" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'IsomorphismFromInternalHomIntoTensorUnitToDualObject' ..." );
fi;
isomorphism_from_hom_to_dual_a := IsomorphismFromInternalHomIntoTensorUnitToDualObject( a );
isomorphism_from_hom_to_dual_b := IsomorphismFromInternalHomIntoTensorUnitToDualObject( b );
isomorphism_from_codual_to_cohom_a_op := IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit( a_op );
isomorphism_from_codual_to_cohom_b_op := IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit( b_op );
Assert( 0, IsCongruentForMorphisms( isomorphism_from_codual_to_cohom_a_op, Opposite( opposite, isomorphism_from_hom_to_dual_a ) ) );
Assert( 0, IsCongruentForMorphisms( isomorphism_from_codual_to_cohom_b_op, Opposite( opposite, isomorphism_from_hom_to_dual_b ) ) );
fi;
if CanCompute( cat, "UniversalPropertyOfDual" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'UniversalPropertyOfDual' ..." );
fi;
gamma_op := Opposite( opposite, gamma );
delta_op := Opposite( opposite, delta );
universal_property_of_dual_gamma := UniversalPropertyOfDual( a, b, gamma );
universal_property_of_dual_delta := UniversalPropertyOfDual( c, d, delta );
universal_property_of_codual_gamma_op := UniversalPropertyOfCoDual( a_op, b_op, gamma_op );
universal_property_of_codual_delta_op := UniversalPropertyOfCoDual( c_op, d_op, delta_op );
Assert( 0, IsCongruentForMorphisms( universal_property_of_codual_gamma_op, Opposite( opposite, universal_property_of_dual_gamma ) ) );
Assert( 0, IsCongruentForMorphisms( universal_property_of_codual_delta_op, Opposite( opposite, universal_property_of_dual_delta ) ) );
fi;
if CanCompute( cat, "LambdaIntroduction" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'LambdaIntroduction' ..." );
fi;
lambda_intro_alpha := LambdaIntroduction( alpha );
lambda_intro_beta := LambdaIntroduction( beta );
colambda_intro_alpha_op := CoLambdaIntroduction( alpha_op );
colambda_intro_beta_op := CoLambdaIntroduction( beta_op );
Assert( 0, IsCongruentForMorphisms( colambda_intro_alpha_op, Opposite( opposite, lambda_intro_alpha ) ) );
Assert( 0, IsCongruentForMorphisms( colambda_intro_beta_op, Opposite( opposite, lambda_intro_beta ) ) );
fi;
if CanCompute( cat, "LambdaElimination" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'LambdaElimination' ..." );
fi;
epsilon_op := Opposite( opposite, epsilon );
zeta_op := Opposite( opposite, zeta );
lambda_elim_epsilon := LambdaElimination( a, b, epsilon );
lambda_elim_zeta := LambdaElimination( c, d, zeta );
colambda_elim_epsilon_op := CoLambdaElimination( b_op, a_op, epsilon_op );
colambda_elim_zeta_op := CoLambdaElimination( d_op, c_op, zeta_op );
Assert( 0, IsCongruentForMorphisms( colambda_elim_epsilon_op, Opposite( opposite, lambda_elim_epsilon ) ) );
Assert( 0, IsCongruentForMorphisms( colambda_elim_zeta_op, Opposite( opposite, lambda_elim_zeta ) ) );
fi;
if CanCompute( cat, "IsomorphismFromObjectToInternalHom" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'IsomorphismFromObjectToInternalHom' ..." );
fi;
isomorphism_from_a_to_hom := IsomorphismFromObjectToInternalHom( a );
isomorphism_from_b_to_hom := IsomorphismFromObjectToInternalHom( b );
isomorphism_from_cohom_to_a_op := IsomorphismFromInternalCoHomToObject( a_op );
isomorphism_from_cohom_to_b_op := IsomorphismFromInternalCoHomToObject( b_op );
Assert( 0, IsCongruentForMorphisms( isomorphism_from_cohom_to_a_op, Opposite( opposite, isomorphism_from_a_to_hom ) ) );
Assert( 0, IsCongruentForMorphisms( isomorphism_from_cohom_to_b_op, Opposite( opposite, isomorphism_from_b_to_hom ) ) );
fi;
if CanCompute( cat, "IsomorphismFromInternalHomToObject" ) then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Testing 'IsomorphismFromInternalHomToObject' ..." );
fi;
isomorphism_from_hom_to_a := IsomorphismFromInternalHomToObject( a );
isomorphism_from_hom_to_b := IsomorphismFromInternalHomToObject( b );
isomorphism_from_a_to_cohom_op := IsomorphismFromObjectToInternalCoHom( a_op );
isomorphism_from_b_to_cohom_op := IsomorphismFromObjectToInternalCoHom( b_op );
Assert( 0, IsCongruentForMorphisms( isomorphism_from_a_to_cohom_op, Opposite( opposite, isomorphism_from_hom_to_a ) ) );
Assert( 0, IsCongruentForMorphisms( isomorphism_from_b_to_cohom_op, Opposite( opposite, isomorphism_from_hom_to_b ) ) );
fi;
if CanCompute( cat, "InternalHomOnObjects" ) and
CanCompute( cat, "ClosedMonoidalLeftEvaluationMorphism" ) and
CanCompute( cat, "InternalHomToTensorProductLeftAdjunctMorphism" )
then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Consistency between 'EvalutionMorphism' and 'AdjunctMorphism' ..." );
fi;
ev_ab := ClosedMonoidalLeftEvaluationMorphism( a, b );
ev_ba := ClosedMonoidalLeftEvaluationMorphism( b, a );
id_hom_ab := IdentityMorphism( InternalHomOnObjects( a, b ) );
id_hom_ba := IdentityMorphism( InternalHomOnObjects( b, a ) );
# Adjoint( Hom( a, b ) → Hom( a, b ) ) == Hom( a, b ) ⊗ a → b
hom_to_tensor_adjunction_on_id_hom_ab := InternalHomToTensorProductLeftAdjunctMorphism( a, b, id_hom_ab );
# Adjoint( Hom( b, a ) → Hom( b, a ) ) == Hom( b, a ) ⊗ b → a
hom_to_tensor_adjunction_on_id_hom_ba := InternalHomToTensorProductLeftAdjunctMorphism( b, a, id_hom_ba );
Assert( 0, IsCongruentForMorphisms( ev_ab, hom_to_tensor_adjunction_on_id_hom_ab ) );
Assert( 0, IsCongruentForMorphisms( ev_ba, hom_to_tensor_adjunction_on_id_hom_ba ) );
fi;
if CanCompute( cat, "TensorProductOnObjects" ) and
CanCompute( cat, "ClosedMonoidalLeftCoevaluationMorphism" ) and
CanCompute( cat, "TensorProductToInternalHomLeftAdjunctMorphism" )
then
if verbose then
# COVERAGE_IGNORE_NEXT_LINE
Display( "Consistency between 'CoevalutionMorphism' and 'AdjunctMorphism' ..." );
fi;
coev_ab := ClosedMonoidalLeftCoevaluationMorphism( a, b );
coev_ba := ClosedMonoidalLeftCoevaluationMorphism( b, a );
id_a_tensor_b := IdentityMorphism( TensorProductOnObjects( cat, a, b ) );
id_b_tensor_a := IdentityMorphism( TensorProductOnObjects( cat, b, a ) );
# Adjoint( a ⊗ b → a ⊗ b ) == a → Hom( b, a ⊗ b )
tensor_to_hom_adjunction_on_id_a_tensor_b := TensorProductToInternalHomLeftAdjunctMorphism( a, b, id_a_tensor_b );
# Adjoint( b ⊗ a → b ⊗ a ) == b → Hom( a, b ⊗ a )
tensor_to_hom_adjunction_on_id_b_tensor_a := TensorProductToInternalHomLeftAdjunctMorphism( b, a, id_b_tensor_a );
Assert( 0, IsCongruentForMorphisms( coev_ba, tensor_to_hom_adjunction_on_id_a_tensor_b ) );
Assert( 0, IsCongruentForMorphisms( coev_ab, tensor_to_hom_adjunction_on_id_b_tensor_a ) );
fi;
end );
[ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
]
|
