Add proof dependencies (WIP)

[ScriptRaccoon]

WIP

Why we need proof dependencies

Many proofs of properties depend on other properties. While the deduction system takes care of many proofs of this type, some proofs cannot be done automatically via implications. In these cases, this information was stored only in the proof text and was not validated at all.

For example, if a proof referred to the "fact" that Grp is abelian, no contradiction would be detected, even though the database of course contains the information that Grp is not abelian. It might also happen that a proof uses the fact that a certain category has a property, even though the database does not contain this information at all, i.e. the property has not been decided yet.

The mentioned issues can easily be prevented with a good review process. However, the worst case is that we discover that some proof is wrong and cannot be fixed. In that case, we remove the assignment (or even negate it!), but we cannot be sure whether any other proof depends on the removed assignment or how to locate these proofs. This is a non-trivial problem, since the proofs might depend on properties that were deduced from the deleted assignment. (This is actually a big problem in the mathematical literature, which cannot be fixed in that context.)

This PR fixes this by checking that all proof dependencies are valid. As a necessary step, all proof dependencies now need to be documented.

How

Concretely, for every property assignment that depends on another property assignment, this dependency must be added manually alongside the assignment. Here is a typical example from Alg(R).yaml:

  - property: cofiltered-limit-stable epimorphisms
    proof: We already know that <a href="/category/CAlg(R)">$\CAlg(R)$</a> does not have this property. Now apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> to the forgetful functor $\CAlg(R) \to \Alg(R)$. It preserves epimorphisms by <a href="https://math.stackexchange.com/questions/5133488" target="_blank">MSE/5133488</a>.
    dependencies:
      - id: CAlg(R)
        type: category
        property: cofiltered-limit-stable epimorphisms
        satisfied: false

The seed script writes these dependencies to a new table in the database called required_property_assignments. The checks cannot be performed at this point since some requirements refer to deduced properties. (For example, the proof that Cat is infinitary extensive depends on the fact that Set is infinitary extensive, and the latter is deduced from the fact that it is a Grothendieck topos.) Thus, we first let the deduction script run and only perform the checks in the test script (pnpm db:test). There, a new function test_proof_dependencies checks whether all claimed properties are actually valid.

References are dependencies

References to facts are treated as dependencies as well, since otherwise they do not make any sense. For example, here is a passage from CAlg(R) (with a proof excerpt):

  - property: regular quotient object classifier
    proof: 'The strategy is similar to the one for <a href="/category/CRing">$\CRing$</a>: Assume that [...]'
    dependencies:
      - id: CRing
        type: category
        property: regular quotient object classifier
        satisfied: false

Here is another example from CAlg(R):

  - property: Malcev
    proof: This follows in the same way as for <a href="/category/Grp">$\Grp$</a>, see also Example 2.2.5 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>.
    dependencies:
      - id: Grp
        type: category
        property: Malcev
        satisfied: true

Technical stuff

We need to add the type information (which is currently either category, functor, or morphism) to each dependency since a property is no longer uniquely determined by its name (cf. #263). One could derive the type from the id, which still identifies structures, but for now I have decided not to do that.

TODOs

• go through all categories (already started)
• go through all functors
• go through all morphisms

Next

Another issue is to prevent circularity. This can be checked in another PR.

This work can also be seen as a preparation for #22.