Add the walking splitting

[ScriptRaccoon]

This PR implements #123 by adding the walking spliting, the category generated by two morphism $i : 0 \to 1$, $p : 1 \to 0$ satisfying $pi = \mathrm{id}_0$.

I find it quite amusing that this category is pointed and preadditive. It is a skeleton of the category of $\mathbb{F}_2$-vector spaces of dimension $\leq 1$.

All properties have been decided.

[ScriptRaccoon]

@ykawase5048 Do you know if this category has sifted colimits?

[ykawase5048]

@ykawase5048 Do you know if this category has sifted colimits?

It seems that this category does not have pullbacks, so it is hard to determine whether it has sifted colimits, though I expect that it does.
Probably, many aspects of sifted colimits are still not well understood, even among experts.

[ScriptRaccoon]

@ykawase5048 Yes pullbacks do not exist (we have a terminal object, but no binary products). Can we say if the subcategory $\mathbf{Vect}^{\leq 1} \hookrightarrow \mathbf{Vect}$ is closed under sifted colimits? (Which would be stronger.) Here the supscript means spaces of dimension $\leq 1$. I already checked (this is contained in this PR) that this inclusion preserves filtered colimits.

[ScriptRaccoon]

@ykawase5048 I have found a simple proof. Can you check it please?

I have merely used the following property of a sifted category: for finitely many objects $i_1,\dotsc,i_n$ there is an object $k$ with morphisms $i_1 \to k, \dotsc, i_n \to k$. This follows by induction, right? (I am asking because I am rather new to sifted categories and are never sure if I do something which only works for filtered categories.)

PS: it should then also follow that this category is a generalized variety.

[ykawase5048]

@ykawase5048 I have found a simple proof. Can you check it please?

The proof looks correct and elegant to me! I didn’t expect that such a linear-algebraic argument would work here.

I have merely used the following property of a sifted category: for finitely many objects i 1 , … , i n there is an object k with morphisms i 1 → k , … , i n → k . This follows by induction, right? (I am asking because I am rather new to sifted categories and are never sure if I do something which only works for filtered categories.)

Yes, it follows.

PS: it should then also follow that this category is a generalized variety.

We need an additional argument to show that every object in this category is atomic with respect to sifted colimits (strongly finitely presentable), but it seems easy to verify.