Support lemmas

[ScriptRaccoon]

Why we need lemmas

The implications in the database have a quite strict format:

if a category C has properties P, Q, ..., then it has property X.

Even though this covers many results of category theory, some results are slightly different: either because property X is not interesting in its own right, so that it does not "deserve" to be added as a property to the database, or because the conclusion is actually a disjunction like "X or Y".

However, the deduction system currently does not support disjunctions (this would blow it up and could also yield non-constructive proofs, which I would like to avoid).

Lemmas try to solve this issue by allowing results in arbitrary formats. Lemmas also support many categorical structures at once. For instance, they can make some conclusions about a category based on the existence of functors with some properties.

What are lemmas in CatDat?

Here is a typical example of a lemma:

if a category is finitary algebraic and thin, then it is trivial or equivalent to {0 < 1}.

We do not want to add the property "is equivalent to {0 < 1}" to the database, since it is not interesting in its own right (and probably has no name either).

Here is another example, "Hilbert's Hotel":

In a category with countable powers, for every object $X$ there is an object $P$ such that $P \cong X \times P$ and which has a morphism $X \to P$.

Here is a third example:

Let $C,D$ be two categories. Assume that $D$ is inhabited. If $C \times D$ has limits of a given shape, then $C$ also has limits of this shape.

Lemmas have no strict relationships with other data in the database, i.e., the lemmas table has no foreign keys. Hence, the deduction system cannot use them, and the data integrity is not tested automatically when lemmas are being used. For this reason, lemmas should be used only in rare cases when implications are not sufficient. In the future, they might be replaced with entities that do have proper relationships (cf. #22).

Nevertheless, lemmas can be used in property assignments to avoid repeating arguments. For example, the result about thin finitary algebraic categories above can be used to show that the three categories N_oo, walking_commutative_square, and walking_composable_pair are not finitary algebraic. And Hilbert's Hotel can be used to show that various categories such as FinAb do not have countable powers.

Details

Lemmas are defined in a new table:

CREATE TABLE lemmas (
    id TEXT PRIMARY KEY,
    title TEXT NOT NULL UNIQUE,
    claim TEXT NOT NULL,
    proof TEXT NOT NULL
);

Individual lemmas are recorded in the file database/data/010_lemmas/000_lemmas.sql. Here is an example:

(
    'hilberts_hotel',
    'Hilbert''s Hotel',
    'Let $\mathcal{C}$ be a category with countable powers. Then for every object
    $X \in \mathcal{C}$ there is an object $P \in \mathcal{C}$ with $P \cong X \times P$
    and which has a morphism $X \to P$.',
    'Take $P := X^{\mathbb{N}}$. Since $\mathbb{N} \cong 1 + \mathbb{N}$ as sets,
    we have $P \cong X \times P$. The diagonal provides a morphism $X \to P$.'
);

Each lemma has a separate page src/routes/lemma/[id]/+page.svelte where its title, statement and proof are displayed.

To refer to this lemma in a proof (manual property assignment), just create a link to it. For example, this is a proof that the categoryFinAb has not all countable powers – located in its file database/data/004_property-assignments/FinAb.sql.

(
	'FinAb',
	'countable powers',
	FALSE,
	'If countable powers exist, then by <a href="/lemma/hilberts_hotel">Hilbert''s Hotel</a>
	there is some object $P$ with $P \cong \mathbb{Z}/2 \times P$. If $P$ has $n$ elements,
	this means $n = 2n$, i.e. $n = 0$, a contradiction.'
),

There is no page which lists all lemmas in CatDat (since, as mentioned, they should only play a secondary role).