Remark 2: Notation Conventions

We establish the following notation conventions used throughout this formalization:

• ∂ (boundary/differential): In Mathlib, this is HomologicalComplex.d i j for a homological complex. For chain complexes (ComplexShape.down ℤ), d i j maps from degree i to degree j = i - 1.

• δ (coboundary/transpose of ∂): For cochain complexes (ComplexShape.up ℤ), the differential d i j maps from degree i to degree j = i + 1. The transpose of a linear map is Module.Dual.transpose.

• im (image of a linear map): LinearMap.range f in Mathlib.

• id (identity map): LinearMap.id in Mathlib.

• Tot (total complex functor): HomologicalComplex.total in Mathlib.

• Z_i(C) (cycles) = ker ∂_i: In Mathlib, HomologicalComplex.cycles C i.

• B_i(C) (boundaries) = im ∂_{i+1}: In Mathlib, HomologicalComplex.opcycles C i captures the cokernel side; boundaries are the image of the incoming differential.

• H_i(C) (homology) = Z_i(C)/B_i(C): In Mathlib, HomologicalComplex.homology C i.

• Similarly for cochains: Z^i, B^i, H^i use the same Mathlib API applied to cochain complexes (CochainComplex).

Main Definitions

• ChainComplex𝔽₂: chain complexes of 𝔽₂-modules indexed by ℤ
• CochainComplex𝔽₂: cochain complexes of 𝔽₂-modules indexed by ℤ

Key Mathlib Correspondences

• HomologicalComplex.d — differential (∂ or δ depending on chain/cochain)
• HomologicalComplex.cycles — cycles (Z_i or Z^i)
• HomologicalComplex.homology — homology (H_i or H^i)
• LinearMap.range — image of a linear map (im)
• Module.Dual.transpose — transpose/coboundary construction (δ = ∂ᵀ)
• LinearMap.id — identity map (id)

Chain and cochain complexes over 𝔽₂

@[reducible, inline]

abbrev ChainComplex𝔽₂ : Type (u_1 + 1)

A chain complex of 𝔽₂-vector spaces indexed by ℤ. The differential d i j maps from degree i to degree j where j + 1 = i (i.e., j = i - 1). This corresponds to the paper's (C_•, ∂).

Equations

• ChainComplex𝔽₂ = ChainComplex (ModuleCat 𝔽₂) ℤ

@[reducible, inline]

abbrev CochainComplex𝔽₂ : Type (u_1 + 1)

A cochain complex of 𝔽₂-vector spaces indexed by ℤ. The differential d i j maps from degree i to degree j where i + 1 = j. In the paper, the coboundary δ^i : C^i → C^{i+1} is the transpose of ∂_{i+1}.

Equations

• CochainComplex𝔽₂ = CochainComplex (ModuleCat 𝔽₂) ℤ

Notation dictionary

The following section documents the precise correspondence between paper notation and Mathlib definitions. We provide abbreviations for frequently used constructions.

@[reducible, inline]

abbrev NotationConventions.boundary (C : ChainComplex𝔽₂) (i j : ℤ) : C.X i ⟶ C.X j

The boundary/differential map ∂_i : C_i → C_{i-1} in a chain complex is C.d i j in Mathlib where (ComplexShape.down ℤ).Rel i j.

Equations

• NotationConventions.boundary C i j = C.d i j

@[reducible, inline]

abbrev NotationConventions.coboundary (C : CochainComplex𝔽₂) (i j : ℤ) : C.X i ⟶ C.X j

The coboundary map δ^i : C^i → C^{i+1} in a cochain complex is C.d i j in Mathlib where (ComplexShape.up ℤ).Rel i j.

Equations

• NotationConventions.coboundary C i j = C.d i j

@[reducible, inline]

abbrev NotationConventions.im {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddCommMonoid N] [Module 𝔽₂ M] [Module 𝔽₂ N] (f : M →ₗ[𝔽₂] N) : Submodule 𝔽₂ N

The image of a linear map f, denoted im f in the paper, corresponds to LinearMap.range f in Mathlib.

Equations

• NotationConventions.im f = f.range

@[reducible, inline]

abbrev NotationConventions.idMap (M : Type u_1) [AddCommMonoid M] [Module 𝔽₂ M] : M →ₗ[𝔽₂] M

The identity linear map, denoted id in the paper, corresponds to LinearMap.id in Mathlib.

Equations

• NotationConventions.idMap M = LinearMap.id

@[reducible, inline]

abbrev NotationConventions.transpose {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddCommMonoid N] [Module 𝔽₂ M] [Module 𝔽₂ N] (f : M →ₗ[𝔽₂] N) : Module.Dual 𝔽₂ N →ₗ[𝔽₂] Module.Dual 𝔽₂ M

The transpose (dual) of a linear map f : M → N is Module.Dual.transpose f : N* → M*. In the paper, δ = ∂ᵀ.

Equations

• NotationConventions.transpose f = Module.Dual.transpose f

Basic properties connecting paper notation to Mathlib

theorem NotationConventions.boundary_comp_boundary (C : ChainComplex𝔽₂) (i j k : ℤ) : CategoryTheory.CategoryStruct.comp (C.d i j) (C.d j k) = 0

The differential in a chain complex satisfies ∂² = 0, i.e., d ≫ d = 0.

theorem NotationConventions.coboundary_comp_coboundary (C : CochainComplex𝔽₂) (i j k : ℤ) : CategoryTheory.CategoryStruct.comp (C.d i j) (C.d j k) = 0

The differential in a cochain complex satisfies δ² = 0, i.e., d ≫ d = 0.

theorem NotationConventions.im_eq_range {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddCommMonoid N] [Module 𝔽₂ M] [Module 𝔽₂ N] (f : M →ₗ[𝔽₂] N) : im f = f.range

The image of a linear map equals its range: im f = LinearMap.range f.

theorem NotationConventions.idMap_eq_id (M : Type u_1) [AddCommMonoid M] [Module 𝔽₂ M] : idMap M = LinearMap.id

The identity map is LinearMap.id.