Definition 8: Cycle Graph

The cycle graph C_ℓ (for ℓ ≥ 3) is a cell complex (Def_7) with ℓ 1-cells (edges) σ_1, ..., σ_ℓ and ℓ 0-cells (vertices) τ_1, ..., τ_ℓ such that ∂σ_i = {τ_i, τ_{i+1}} where indices are taken modulo ℓ.

Its chain complex is C_1 →[∂_1] C_0 where C_1 ≅ 𝔽₂^ℓ and C_0 ≅ 𝔽₂^ℓ, and ∂_1 is the ℓ × ℓ circulant matrix with two 1-entries per column.

The kernel ker(∂_1) is the repetition code span{(1,...,1)} of dimension 1. The homology satisfies dim H_1(C_ℓ) = 1 and dim H_0(C_ℓ) = 1.

Main Definitions

• CycleGraph.cycleGraph — the cycle graph cell complex C_ℓ (as a CellComplex, Def_7)
• CycleGraph.differential — the algebraic differential ∂_1 : 𝔽₂^ℓ → 𝔽₂^ℓ
• CycleGraph.differentialMap_eq_differential — cell complex differential agrees with ∂_1
• CycleGraph.ker_differential_eq_span — ker(∂_1) = span{(1,...,1)}
• CycleGraph.finrank_ker_differential — dim ker(∂_1) = 1
• CycleGraph.finrank_range_differential — dim im(∂_1) = ℓ - 1
• CycleGraph.dim_H1_cycleGraph — dim H_1(C_ℓ) = 1
• CycleGraph.dim_H0_cycleGraph — dim H_0(C_ℓ) = 1
• CycleGraph.repetitionCode — the repetition code as a ClassicalCode (Def_3)

The cycle graph differential as a linear map on Fin ℓ → 𝔽₂

noncomputable def CycleGraph.differential (ℓ : ℕ) [NeZero ℓ] : (Fin ℓ → 𝔽₂) →ₗ[𝔽₂] Fin ℓ → 𝔽₂

The differential ∂_1 : 𝔽₂^ℓ → 𝔽₂^ℓ of the cycle graph, defined by (∂_1 f)(i) = f(i) + f((i + ℓ - 1) % ℓ). On basis vectors e_j, ∂_1(e_j) = e_j + e_{(j+1) % ℓ}, so column j of the matrix has 1-entries in rows j and (j+1) % ℓ (the boundary relation ∂σ_j = {τ_j, τ_{j+1}}). The i-th entry of ∂_1(f) counts how many edges incident to vertex i have nonzero coefficient in f, modulo 2.

Equations

• CycleGraph.differential ℓ = { toFun := fun (f : Fin ℓ → 𝔽₂) (i : Fin ℓ) => f i + f ⟨(↑i + ℓ - 1) % ℓ, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

def CycleGraph.onesVec (ℓ : ℕ) : Fin ℓ → 𝔽₂

The all-ones vector (1, 1, ..., 1) ∈ 𝔽₂^ℓ.

Equations

• CycleGraph.onesVec ℓ x✝ = 1

theorem CycleGraph.differential_onesVec (ℓ : ℕ) [NeZero ℓ] : (differential ℓ) (onesVec ℓ) = 0

The differential maps the all-ones vector to zero.

@[simp]

theorem CycleGraph.differential_apply (ℓ : ℕ) [NeZero ℓ] (f : Fin ℓ → 𝔽₂) (i : Fin ℓ) : (differential ℓ) f i = f i + f ⟨(↑i + ℓ - 1) % ℓ, ⋯⟩

Apply formula for the differential.

Kernel of the differential equals span of the all-ones vector

theorem CycleGraph.ker_differential_succ (ℓ : ℕ) [NeZero ℓ] (f : Fin ℓ → 𝔽₂) (hf : (differential ℓ) f = 0) (i : ℕ) (hi : i + 1 < ℓ) : f ⟨i + 1, hi⟩ = f ⟨i, ⋯⟩

Helper: from the kernel condition, f(i+1) = f(i) for i+1 < ℓ.

theorem CycleGraph.ker_differential_const (ℓ : ℕ) [NeZero ℓ] (f : Fin ℓ → 𝔽₂) (hf : (differential ℓ) f = 0) (i : Fin ℓ) : f i = f ⟨0, ⋯⟩

If f is in the kernel of the differential, then f i = f 0 for all i.

theorem CycleGraph.ker_differential_eq_span (ℓ : ℕ) [NeZero ℓ] : (differential ℓ).ker = 𝔽₂ ∙ onesVec ℓ

The kernel of the differential is exactly span{onesVec}.

theorem CycleGraph.onesVec_ne_zero (ℓ : ℕ) (hℓ1 : ℓ ≥ 1) : onesVec ℓ ≠ 0

The all-ones vector is nonzero when ℓ ≥ 1.

theorem CycleGraph.finrank_ker_differential (ℓ : ℕ) [NeZero ℓ] (hℓ1 : ℓ ≥ 1) : Module.finrank 𝔽₂ ↥(differential ℓ).ker = 1

The kernel of the differential has dimension 1 (assuming ℓ ≥ 1).

The cycle graph as a cell complex (Def_7)

def CycleGraph.cellType (ℓ : ℕ) : ℤ → Type

The type of n-cells for the cycle graph: Fin ℓ in dimensions 0 and 1, PEmpty elsewhere. Uses match on the integer dimension.

Equations

• CycleGraph.cellType ℓ 0 = Fin ℓ
• CycleGraph.cellType ℓ 1 = Fin ℓ
• CycleGraph.cellType ℓ x✝ = PEmpty.{1}

noncomputable instance CycleGraph.cellType_fintype (ℓ : ℕ) (n : ℤ) : Fintype (cellType ℓ n)

Equations

• CycleGraph.cellType_fintype ℓ 0 = Fin.fintype ℓ
• CycleGraph.cellType_fintype ℓ 1 = Fin.fintype ℓ
• CycleGraph.cellType_fintype ℓ (Int.ofNat n.succ.succ) = inferInstanceAs (Fintype PEmpty.{1})
• CycleGraph.cellType_fintype ℓ (Int.negSucc a) = inferInstanceAs (Fintype PEmpty.{1})

instance CycleGraph.cellType_deceq (ℓ : ℕ) (n : ℤ) : DecidableEq (cellType ℓ n)

Equations

• CycleGraph.cellType_deceq ℓ 0 = inferInstanceAs (DecidableEq (Fin ℓ))
• CycleGraph.cellType_deceq ℓ 1 = inferInstanceAs (DecidableEq (Fin ℓ))
• CycleGraph.cellType_deceq ℓ (Int.ofNat n.succ.succ) = inferInstanceAs (DecidableEq PEmpty.{1})
• CycleGraph.cellType_deceq ℓ (Int.negSucc a) = inferInstanceAs (DecidableEq PEmpty.{1})

def CycleGraph.cellBdry (ℓ : ℕ) [NeZero ℓ] {n : ℤ} : cellType ℓ n → Finset (cellType ℓ (n - 1))

The boundary map for the cycle graph. For a 1-cell σ_i, ∂σ_i = {τ_i, τ_{(i+1) % ℓ}}. For all other cells, the boundary is empty.

Equations

• CycleGraph.cellBdry ℓ i = {i, ⟨(↑i + 1) % ℓ, ⋯⟩}
• CycleGraph.cellBdry ℓ x_2 = ∅
• CycleGraph.cellBdry ℓ σ = σ.elim
• CycleGraph.cellBdry ℓ σ = σ.elim

theorem CycleGraph.cellBdry_bdry (ℓ : ℕ) [NeZero ℓ] (n : ℤ) (σ : cellType ℓ n) (ρ : cellType ℓ (n - 1 - 1)) : Even {τ ∈ cellBdry ℓ σ | ρ ∈ cellBdry ℓ τ}.card

The chain complex condition for the cycle graph is vacuously true since for the only nontrivial boundary (n=1), the target cells(n-1-1) = cells(-1) = PEmpty makes the condition vacuous.

noncomputable def CycleGraph.cycleGraph (ℓ : ℕ) [NeZero ℓ] : CellComplex

The cycle graph C_ℓ as a cell complex (Def_7). The 1-cells and 0-cells are both indexed by Fin ℓ, with boundary ∂σ_i = {τ_i, τ_{(i+1) % ℓ}}. All other cell sets are empty. The chain complex condition is vacuously true.

Equations

• One or more equations did not get rendered due to their size.

Cells of the cycle graph are Fin ℓ

theorem CycleGraph.cycleGraph_cells_one (ℓ : ℕ) [NeZero ℓ] : (cycleGraph ℓ).cells 1 = Fin ℓ

The 1-cells of the cycle graph are Fin ℓ (definitionally).

theorem CycleGraph.cycleGraph_cells_zero (ℓ : ℕ) [NeZero ℓ] : (cycleGraph ℓ).cells 0 = Fin ℓ

The 0-cells of the cycle graph are Fin ℓ (definitionally).

theorem CycleGraph.pred_mod_succ (ℓ : ℕ) (hℓ : ℓ ≥ 1) (i : Fin ℓ) : ((↑i + ℓ - 1) % ℓ + 1) % ℓ = ↑i

Helper: ((i+ℓ-1)%ℓ + 1)%ℓ = i for i : Fin ℓ.

theorem CycleGraph.fin_ne_succ_mod (ℓ : ℕ) (hℓ : ℓ ≥ 2) (x : Fin ℓ) : x ≠ ⟨(↑x + 1) % ℓ, ⋯⟩

For ℓ ≥ 2, an element x : Fin ℓ is never equal to (x+1) % ℓ.

theorem CycleGraph.fin_ne_pred_mod (ℓ : ℕ) (hℓ : ℓ ≥ 2) (i : Fin ℓ) : i ≠ ⟨(↑i + ℓ - 1) % ℓ, ⋯⟩

For ℓ ≥ 2, i ≠ pred(i) mod ℓ.

theorem CycleGraph.differentialMap_filter_eq (ℓ : ℕ) [NeZero ℓ] (hℓ : ℓ ≥ 2) (i : Fin ℓ) : have j := ⟨(↑i + ℓ - 1) % ℓ, ⋯⟩; {σ : (cycleGraph ℓ).cells 1 | i ∈ (cycleGraph ℓ).bdry σ} = {i, j}

Helper: the filter set {σ | i ∈ bdry σ} for the cycle graph equals {i, pred(i)}.

theorem CycleGraph.differentialMap_eq_differential (ℓ : ℕ) [NeZero ℓ] (hℓ : ℓ ≥ 2) : (cycleGraph ℓ).differentialMap 1 = differential ℓ

The cell complex differential ∂_1 from degree 1 to degree 0 agrees with CycleGraph.differential: both map f ↦ (i ↦ f(i) + f((i + ℓ - 1) % ℓ)). Requires ℓ ≥ 2 so that each edge has two distinct boundary vertices.

Rank of the image and homology dimensions

theorem CycleGraph.finrank_F2_fin (ℓ : ℕ) : Module.finrank 𝔽₂ (Fin ℓ → 𝔽₂) = ℓ

The dimension of 𝔽₂^ℓ is ℓ.

theorem CycleGraph.finrank_range_differential (ℓ : ℕ) [NeZero ℓ] (hℓ1 : ℓ ≥ 1) : Module.finrank 𝔽₂ ↥(differential ℓ).range = ℓ - 1

The rank of the image of ∂_1 is ℓ - 1, by rank-nullity.

Homology dimensions

theorem CycleGraph.dim_H1_cycleGraph (ℓ : ℕ) [NeZero ℓ] (hℓ1 : ℓ ≥ 1) : Module.finrank 𝔽₂ ↥(differential ℓ).ker = 1

dim H_1(C_ℓ) = 1: Since there are no 2-cells, im(∂_2) = 0 and H_1 = ker(∂_1) / 0 ≅ ker(∂_1), which has dimension 1. Here we express this purely in terms of the differential, since the cycle graph has only degrees 0 and 1.

theorem CycleGraph.dim_H0_cycleGraph (ℓ : ℕ) [NeZero ℓ] (hℓ1 : ℓ ≥ 1) : Module.finrank 𝔽₂ ((Fin ℓ → 𝔽₂) ⧸ (differential ℓ).range) = 1

dim H_0(C_ℓ) = 1: We have ker(∂_0) = C_0 = 𝔽₂^ℓ (since ∂_0 = 0) and im(∂_1) has dimension ℓ - 1, so H_0 = C_0 / im(∂_1) has dimension ℓ - (ℓ - 1) = 1. We express H_0 as the quotient (Fin ℓ → 𝔽₂) ⧸ im(∂_1).

Classical code interpretation

noncomputable def CycleGraph.repetitionCode (ℓ : ℕ) [NeZero ℓ] : ClassicalCode ℓ

The repetition code of length ℓ: the classical code with codeword space ker(∂_1) = span{(1,...,1)} ⊆ 𝔽₂^ℓ.

Equations

• CycleGraph.repetitionCode ℓ = ClassicalCode.ofParityCheck (CycleGraph.differential ℓ)

theorem CycleGraph.repetitionCode_eq_ker (ℓ : ℕ) [NeZero ℓ] : (repetitionCode ℓ).code = (differential ℓ).ker

The repetition code equals ker(∂_1).

theorem CycleGraph.repetitionCode_dimension (ℓ : ℕ) [NeZero ℓ] (hℓ1 : ℓ ≥ 1) : (repetitionCode ℓ).dimension = 1

The repetition code has dimension 1.