Incidence algebras #1221
Incidence algebras #1221
Conversation
define type of inhabited intervals of 'P', then the 'R'-module of functions from inhabited intervals to 'R', then the convolution operation.
from inhabited intervals of 'P' to 'R'. further work stalled pending elementary development of module theory; could be done by hand, and I'll define the convolution before pushing upstream in fact
the commutative algebras library is needed. to-do...
There was a problem hiding this comment.
Nice pull request! Thanks so much for making a contribution to agda-unimath, and welcome!
One further thing to note about your pull request is that probably when people would be looking for inhabited intervals, they wouldn't think to do so in a file about incidence algebras. That is to say, inhabited intervals would be better placed in the file about intervals.
Our way of thinking is that all the prerequisites of a definition should probably go in other files, so that the file can be kept more focused on what is being defined.
Would you be willing to move the inhabited intervals to intervals?
types, moved code for inhabited intervals to intervals file
|
Worked your suggestions into the code. On to modules next, which I realized are in the ring-theory section instead of the commutative-algebra one; the unordered addition lemma pends, to my knowledge, and will be my next target. |
fixed typo - 'undderlying' to 'underlying' Co-authored-by: Egbert Rijke <[email protected]>
moved inhabited-interval definition to new module where (x,y) are not postulated Co-authored-by: Egbert Rijke <[email protected]>
|
Typechecker failed. Should the |
|
Thanks so much for the quick changes! If you run |
fixed typo - ```dule _``` to ```module _``` Co-authored-by: Egbert Rijke <[email protected]>
|
No worries! I needed to make minor changes after your module refactoring but it looks like everything will typecheck now. Running the pre-commit and will push soon. |
|
One more thing: Since you are a new contributor could add your contributor information to the file |
|
I believe I'm already in the contributors page - made another minor contribution back in March or so. Do I need to update the .toml again as it's been a while? |
Ah! Excellent, I was not aware of that. There's no need to edit it again. Then this pull request is done. Thanks so much! |
This reverts commit f5702e9.
|
Ay, I am sorry about the misattribution! Github automatically adds people who make Github Suggestions as coauthors, which we have to remove manually. I forgot to do that this time. My apologies! It is definitely not my intention to claim credit for your work! |
|
|
||
| ## Idea | ||
|
|
||
| For a [locally finite poset](order-theory.locally-finite-posets.md) 'P' and |
There was a problem hiding this comment.
Hey! I just wanted to point out that inline code needs to be escaped with backticks (`) and not apostrophes (').
Cf. how the current version is rendered on our website:
https://unimath.github.io/agda-unimath/order-theory.incidence-algebras.html
Much appreciated if you would fix this issue in your next contribution! :)
Very preliminary work on defining the incidence algebra of a locally finite poset, as towards defining more sophisticated objects such as Möbius inversion. Work stalled pending infrastructure in the commutative algebra library for "unordered" addition indexed by finite sets and for some module theory, but want to get this file with a thumbtack in the upstream before turning that way.