2 Rem 2: Notation Conventions
This chapter establishes the notation conventions used throughout the formalization, documenting the precise correspondence between paper notation and Mathlib definitions.
A chain complex of \(\mathbb {F}_2\)-vector spaces indexed by \(\mathbb {Z}\) is defined as
The differential \(\partial _i : C_i \to C_{i-1}\) is given by \(\mathtt{d}\, i\, j\) in Mathlib where the complex shape satisfies \(j + 1 = i\) (i.e. \(j = i - 1\)). This corresponds to the paper’s \((C_\bullet , \partial )\).
A cochain complex of \(\mathbb {F}_2\)-vector spaces indexed by \(\mathbb {Z}\) is defined as
The differential \(\delta ^i : C^i \to C^{i+1}\) is given by \(\mathtt{d}\, i\, j\) in Mathlib where \(i + 1 = j\). In the paper, the coboundary \(\delta ^i\) is the transpose of \(\partial _{i+1}\).
For a chain complex \(C \in \operatorname {ChainComplex}_{\mathbb {F}_2}\) and indices \(i, j \in \mathbb {Z}\), the boundary map \(\partial _i : C_i \to C_{i-1}\) is defined as
This is the paper’s differential \(\partial \) accessed via the Mathlib API HomologicalComplex.d.
For a cochain complex \(C \in \operatorname {CochainComplex}_{\mathbb {F}_2}\) and indices \(i, j \in \mathbb {Z}\), the coboundary map \(\delta ^i : C^i \to C^{i+1}\) is defined as
This corresponds to the paper’s coboundary \(\delta \), accessed via HomologicalComplex.d on cochain complexes.
For \(\mathbb {F}_2\)-modules \(M\) and \(N\) and a linear map \(f : M \to _{\mathbb {F}_2} N\), the image of \(f\), denoted \(\operatorname {im}(f)\) in the paper, is defined as
For an \(\mathbb {F}_2\)-module \(M\), the identity linear map, denoted \(\operatorname {id}\) in the paper, is defined as
For \(\mathbb {F}_2\)-modules \(M\) and \(N\) and a linear map \(f : M \to _{\mathbb {F}_2} N\), the transpose (dual) of \(f\) is defined as
In the paper, the coboundary satisfies \(\delta = \partial ^\top \).
For any chain complex \(C \in \operatorname {ChainComplex}_{\mathbb {F}_2}\) and indices \(i, j, k \in \mathbb {Z}\),
i.e. \(C.\mathtt{d}\, i\, j \, \gg \, C.\mathtt{d}\, j\, k = 0\).
This follows directly from the Mathlib lemma HomologicalComplex.d_comp_d, applied to \(C\) at indices \(i\), \(j\), \(k\). Specifically, we have \(C.\mathtt{d\_ comp\_ d}\, i\, j\, k = 0\) by the axioms of a homological complex, which states that consecutive differentials compose to zero.
For any cochain complex \(C \in \operatorname {CochainComplex}_{\mathbb {F}_2}\) and indices \(i, j, k \in \mathbb {Z}\),
i.e. \(C.\mathtt{d}\, i\, j \, \gg \, C.\mathtt{d}\, j\, k = 0\).
This follows directly from the Mathlib lemma HomologicalComplex.d_comp_d, applied to the cochain complex \(C\) at indices \(i\), \(j\), \(k\). Consecutive coboundary maps compose to zero by the axioms of a homological complex.
For \(\mathbb {F}_2\)-modules \(M\), \(N\) and a linear map \(f : M \to _{\mathbb {F}_2} N\),
This holds by reflexivity, since \(\operatorname {im}(f)\) is defined to be \(\operatorname {LinearMap.range}(f)\) by definition.
For any \(\mathbb {F}_2\)-module \(M\),
This holds by reflexivity, since \(\operatorname {idMap}(M)\) is defined to be \(\operatorname {LinearMap.id}_{\mathbb {F}_2,\, M}\) by definition.
[Mathlib Correspondence for Homological Algebra] The following Mathlib definitions correspond to the paper’s notation:
\(\partial \) or \(\delta \) (differential): HomologicalComplex.d i j
\(Z_i(C)\) (cycles \(= \ker \partial _i\)): HomologicalComplex.cycles C i
\(B_i(C)\) (boundaries \(= \operatorname {im}\, \partial _{i+1}\)): image of the incoming differential
\(H_i(C)\) (homology \(= Z_i(C)/B_i(C)\)): HomologicalComplex.homology C i
\(\operatorname {im}(f)\) (image): LinearMap.range f
\(\delta = \partial ^\top \) (coboundary as transpose): Module.Dual.transpose
\(\operatorname {id}\) (identity): LinearMap.id
\(\operatorname {Tot}\) (total complex functor): HomologicalComplex.total
The same Mathlib API applies to cochains (\(Z^i\), \(B^i\), \(H^i\)) via CochainComplex.