add 'LinearCombinationOfMorphisms' to the method record #1408
Conversation
Codecov ReportPatch coverage:
Additional details and impacted files@@ Coverage Diff @@
## master #1408 +/- ##
=======================================
Coverage 80.63% 80.63%
=======================================
Files 492 492
Lines 62516 62562 +46
=======================================
+ Hits 50407 50446 +39
- Misses 12109 12116 +7
Flags with carried forward coverage won't be shown. Click here to find out more.
☔ View full report in Codecov by Sentry. |
|
@mohamed-barakat Fabian and I think |
Yes, good idea. |
kamalsaleh
changed the title
kamalsaleh
force-pushed
the
lincomb
branch
3 times, most recently
from
98dcb0b
to
2b58213
Compare
|
I have some thoughts which I would like to discuss in the context of this PR (although this does not necessarily block the PR): Currently, LinearCombinationOfMorphisms is derived from SumOfMorphisms and MultiplyWithElementOfCommutativeRing, but not the other way round. This makes LinearCombinationOfMorphisms look like a convenience operation. This situation also occurs at other places: For example, MorphismBetweenDirectSums and ComponentOfMorphismInto/FromDirectSum are derived from other operations for direct sums but not the other way round. From an implementation standpoint this makes sense: Implementing SumOfMorphisms (or even only AdditionForMorphisms) and MultiplyWithElementOfCommutativeRing is easier and much less error prone than implementing LinearCombinationOfMorphisms directly. However, from a mathematical standpoint and in the context of ur-algorithms, I think we usually want to use the operation with more semantics, that is, LinearCombinationOfMorphisms, whose semantics is being the inverse operation for BasisOfExternalHom and CoefficientsOfMorphisms. So I think theoretically it would be nice to derive SumOfMorphisms and Multiply... from LinearCombinationOfMorphisms. But then again I would never recommend implementing LinearCombinationOfMorphisms directly. Hence, I'm not sure what the best way forward is. Background information: The context in which I first came across this question is showing that AdditiveClosure is indeed additive using CompilerForCAP. Using "higher-level" operations like MorphismBetweenDirectSums make the proof shorter, but usually no one would implement MorphismBetweenDirectSums directly. |
|
Please fix the commit-message of the first commit. |
'list_of_elements_of_commutative_ring_of_linear_structure' while adding methods to the opposite category
and bump CAP to V2023.08-07 and LinearAlgebraForCAP to V2023.08-02
…hisms' operation) and bump FreydCategoriesForCAP to V2023.08-02
|
As just discussed:
|
|
Was about to write please do not merge yet :) |
Sorry, I thought you wanted to address all effects of the CAP changes in CategoricalTowers at once. |
No problem, now I will :) |
@mohamed-barakat @zickgraf
An implementation of what we discussed yesterday.