Smith Normal Form #710
Smith Normal Form #710
Conversation
…into smithexistence
|
Can you merge master and change your invocation of |
Merge Master
|
@ice1000 Done！ |
Cubical/Algebra/Matrix.agda
Outdated
| @@ -36,6 +36,8 @@ private | |||
| ℓ ℓ' : Level | |||
| A : Type ℓ | |||
|
|
|||
| pattern one = suc zero | |||
There was a problem hiding this comment.
Wait, this should maybe not be here?
There was a problem hiding this comment.
Move it to Cubical.Data.FinData.
|
PS: a lot of things were developed for 2x2 matrices. It would be good to generalize in the future, but this would involve a lot of work. If you're planning to go in this direction I recommend you to look at the mathematical components library (https://math-comp.github.io/), they have an extremely well-designed linear algebra library |
|
I add a benchmark file My wish is to develop some theories about finitely presented abelian groups, maybe in near future. Design pattern is what I need admittedly. I felt difficult in just organizing these things well :) I'll see if I could learn from math-comp, thanks for that suggestion! |
| makeMat3×3 _ _ _ _ _ a12 _ _ _ one two = a12 | ||
| makeMat3×3 _ _ _ _ _ _ a20 _ _ two zero = a20 | ||
| makeMat3×3 _ _ _ _ _ _ _ a21 _ two one = a21 | ||
| makeMat3×3 _ _ _ _ _ _ _ _ a22 two two = a22 |
There was a problem hiding this comment.
There was a problem hiding this comment.
I tried before. The result performs a bit slower than this direct definition, so I decided to use this one. Though it seems somewhat silly...
There was a problem hiding this comment.
@ice1000 I'll comment it in future PR :P
|
Probably. One thing I've noticed is, if one only runs reduction step by step, the total time cost seems much less than running the whole function. (I've tried this months before, not contained in the benchmark file.) So I think if we can force Agda to fully normalize the result to numerals in each step, the function could be more efficient (I don't know whether Agda supports this or how to do that). Sadly I'm no expert of implementation details of Agda, so maybe it's just my non-sense. |
This PR contains the existence proof of Smith normal form for Integers, based on the divisibility result of #705. Hope this could pave the way towards a general theory for finitely presented abelian group, that used tons of times in algebraic topology. Maybe I would do some of them soon or later.