1 (edited by qed 2020-05-02 12:25:35)

Topic: Categories and Bounties

Here are four qed documents about categories that resolved some conjectures that had bounties on them.

CategoryF:

http://s000.tinyupload.com/index.php?fi … 9363794828

https://dalilcoin.com/proofexplorer/que … 26cd024801

CategoryG:

http://s000.tinyupload.com/index.php?fi … 4291239926

https://dalilcoin.com/proofexplorer/que … 67277770c8

CategoryH:

http://s000.tinyupload.com/index.php?fi … 2436065439

https://dalilcoin.com/proofexplorer/que … 27b73aa895

CategoryI:

http://s000.tinyupload.com/index.php?fi … 8127912084

https://dalilcoin.com/proofexplorer/que … 32ee2d5b36

To get an idea of what is proven in the documents, taken together they the categories Set and SmallSet are topoi.

To even formulate these theorems I had to spend time translating (by hand) information from the documents published with the Dalilcoin source code into a more readable qed syntax. Specifically much of the content from here:

https://github.com/dalcoder/dalilcoin/b … nctordefs1
https://github.com/dalcoder/dalilcoin/b … goryconjs1
https://github.com/dalcoder/dalilcoin/b … goryconjs2
https://github.com/dalcoder/dalilcoin/b … goryconjs3

During this process it became clear that some of the definitions of the categories in question (Grp, AbGrp, Rng, etc.) are wrong. In the case of Grp, the objects of the category are not actually groups. The condition that the carrier set must be closed under the inverse operation is missing. The same is true for the other categories I mentioned (AbGrp, Rng, etc), and there are other missing properties for rings. It looks like "rings" aren't even required to have the multiplication of two elements in the ring to be an element in the ring. As a consequence, it's unclear if the conjectures with bounties about these "categories" are true or false. For example, mathematically it's clear that the actual category of groups has products, but it's not clear if the category as defined in categoryconjs2 (if it even is a category) has products. The questions also don't appear to be mathematically interesting, but I wanted to point out that it's likely people could claim some bounties by debugging these definitions enough to determine if the conjectures or their negations are provable. It's likely to be "low hanging fruit" for someone willing to go into the tedious details.

To prevent someone else from needing to redo the translation, here is an unfinished qed document that has much of the infrastructure for stating the conjectures in a qed file:

http://s000.tinyupload.com/index.php?fi … 2943755359

There are some comments in the file about what's "wrong" with the definitions of the last 6 categories. I stopped formulating the conjectures after realizing they were buggy and uninteresting, but the conjectures formulated earlier in the file can be used as a guide for formulating the missing ones.