1 Rem 1: Base Field
For the remainder of this manuscript we consider only vector spaces over the field \(\mathbb {F}_2\). All tensor products, linear maps, and homology computations are taken over \(\mathbb {F}_2\) unless stated otherwise.
The base field \(\mathbb {F}_2\) is the field with two elements, defined as \(\mathbb {F}_2 := \mathbb {Z}/2\mathbb {Z}\) (i.e., ZMod 2). All vector spaces, tensor products, linear maps, and homology computations in this paper are over \(\mathbb {F}_2\).
The cardinality of \(\mathbb {F}_2\) is \(2\), i.e., \(|\mathbb {F}_2| = 2\).
This follows directly from ZMod.card 2, which computes the cardinality of \(\mathbb {Z}/2\mathbb {Z}\) to be \(2\).
For every element \(a \in \mathbb {F}_2\), we have \(-a = a\).
Since \(\mathbb {F}_2\) has characteristic \(2\), the result follows from the general fact CharTwo.neg_eq, which states that in any ring of characteristic \(2\), negation is the identity map. Applying this to an arbitrary \(a \in \mathbb {F}_2\) gives \(-a = a\).
For every element \(a \in \mathbb {F}_2\), we have \(a + a = 0\).
Since \(\mathbb {F}_2\) has characteristic \(2\), this follows from CharTwo.add_self_eq_zero, which asserts that in any ring of characteristic \(2\), every element \(a\) satisfies \(a + a = 0\). Applying this to arbitrary \(a \in \mathbb {F}_2\) yields the result.
For all \(a, b \in \mathbb {F}_2\), we have \(a - b = a + b\).
Since \(\mathbb {F}_2\) has characteristic \(2\), we apply CharTwo.sub_eq_add, which states that in any ring of characteristic \(2\), subtraction coincides with addition (as \(-b = b\) for all \(b\)). Applying this to arbitrary \(a, b \in \mathbb {F}_2\) gives \(a - b = a + b\).