Definition 27: Horizontal/Vertical Homology Splitting

By the Künneth formula for balanced products (Lem_4), the degree-1 homology of the balanced product Tanner cycle code splits as $$H_1(C(X,L) \otimes_{\mathbb{Z}_\ell} C(C_\ell)) \cong H_1^h \oplus H_1^v$$ where:

• H₁ʰ = H₁(C(X,L)) ⊗_H H₀(C_ℓ) (horizontal part)
• H₁ᵛ = H₀(C(X,L)) ⊗_H H₁(C_ℓ) (vertical part)

We define the projection maps pʰ : H₁ → H₁ʰ and pᵛ : H₁ → H₁ᵛ as the compositions of the Künneth isomorphism with the canonical projections from the direct sum onto each summand. Similarly for cohomology.

Main Definitions

• H1h — horizontal homology H₁(C(X,L)) ⊗_H H₀(C_ℓ)
• H1v — vertical homology H₀(C(X,L)) ⊗_H H₁(C_ℓ)
• projH — projection H₁ → H₁ʰ
• projV — projection H₁ → H₁ᵛ
• coH1h — horizontal cohomology H¹(C(X,L)) ⊗_H H⁰(C_ℓ)
• coH1v — vertical cohomology H⁰(C(X,L)) ⊗_H H¹(C_ℓ)
• coprojH — cohomology projection H¹ → H¹_h
• coprojV — cohomology projection H¹ → H¹_v

@[reducible, inline]

abbrev HorizontalVerticalHomologySplitting.tannerHEq {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) : HEquivariantChainComplex H

The Tanner code H-equivariant chain complex.

Equations

• HorizontalVerticalHomologySplitting.tannerHEq X Λ hΛ = BalancedProductTannerCycleCode.tannerCodeHEquivariant X Λ hΛ

@[reducible, inline]

abbrev HorizontalVerticalHomologySplitting.cycleHEq {H : Type} [Group H] [Fintype H] [DecidableEq H] (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : HEquivariantChainComplex H

The cycle graph H-equivariant chain complex.

Equations

• HorizontalVerticalHomologySplitting.cycleHEq ℓ hcompat = BalancedProductTannerCycleCode.cycleGraphHEquivariant ℓ hcompat

@[reducible, inline]

abbrev HorizontalVerticalHomologySplitting.bpComplex {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : ChainComplex𝔽₂

The balanced product complex C(X,L) ⊗_H C(C_ℓ).

Equations

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

@[reducible, inline]

abbrev HorizontalVerticalHomologySplitting.H1 {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : Type

The degree-1 homology of the balanced product complex.

Equations

• HorizontalVerticalHomologySplitting.H1 X Λ ℓ hΛ hcompat = (HorizontalVerticalHomologySplitting.bpComplex X Λ ℓ hΛ hcompat).homology' 1

Horizontal and vertical homology parts

@[reducible, inline]

abbrev HorizontalVerticalHomologySplitting.H1h {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : Type

The horizontal homology: H₁ʰ = H₁(C(X,L)) ⊗_H H₀(C_ℓ). This is the balanced Künneth summand at p = 1, q = 1 - 1 = 0.

Equations

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

@[reducible, inline]

abbrev HorizontalVerticalHomologySplitting.H1v {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : Type

The vertical homology: H₁ᵛ = H₀(C(X,L)) ⊗_H H₁(C_ℓ). This is the balanced Künneth summand at p = 0, q = 1 - 0 = 1.

Equations

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

def HorizontalVerticalHomologySplitting.kunnethIso {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : H1 X Λ ℓ hΛ hcompat ≃ₗ[𝔽₂] (tannerHEq X Λ hΛ).balancedKunnethSum (cycleHEq ℓ hcompat) 1

The Künneth isomorphism at degree 1: H₁(C(X,L) ⊗_H C(C_ℓ)) ≃ ⊕_p H_p(C(X,L)) ⊗_H H_{1-p}(C_ℓ).

Equations

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

def HorizontalVerticalHomologySplitting.directSumProj {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (p : ℤ) : (tannerHEq X Λ hΛ).balancedKunnethSum (cycleHEq ℓ hcompat) 1 →ₗ[𝔽₂] (tannerHEq X Λ hΛ).balancedKunnethSummand (cycleHEq ℓ hcompat) 1 p

The projection from the Künneth direct sum onto the p-th summand.

Equations

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

def HorizontalVerticalHomologySplitting.directSumInc {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (p : ℤ) : (tannerHEq X Λ hΛ).balancedKunnethSummand (cycleHEq ℓ hcompat) 1 p →ₗ[𝔽₂] (tannerHEq X Λ hΛ).balancedKunnethSum (cycleHEq ℓ hcompat) 1

The inclusion from the p-th summand into the Künneth direct sum.

Equations

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

Projection maps

def HorizontalVerticalHomologySplitting.projH {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : H1 X Λ ℓ hΛ hcompat →ₗ[𝔽₂] H1h X Λ ℓ hΛ hcompat

The horizontal projection pʰ : H₁ → H₁ʰ, defined as the composition of the Künneth isomorphism with the canonical projection onto the p = 1 summand.

Equations

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

def HorizontalVerticalHomologySplitting.projV {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : H1 X Λ ℓ hΛ hcompat →ₗ[𝔽₂] H1v X Λ ℓ hΛ hcompat

The vertical projection pᵛ : H₁ → H₁ᵛ, defined as the composition of the Künneth isomorphism with the canonical projection onto the p = 0 summand.

Equations

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

def HorizontalVerticalHomologySplitting.IsHorizontal {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) (x : H1 X Λ ℓ hΛ hcompat) : Prop

A homology class is horizontal if its image under the Künneth isomorphism lies in H₁ʰ ⊕ {0}, i.e., its vertical projection is zero.

Equations

• HorizontalVerticalHomologySplitting.IsHorizontal X Λ ℓ hΛ hcompat hodd x = ((HorizontalVerticalHomologySplitting.projV X Λ ℓ hΛ hcompat hodd) x = 0)

def HorizontalVerticalHomologySplitting.IsVertical {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) (x : H1 X Λ ℓ hΛ hcompat) : Prop

A homology class is vertical if its image under the Künneth isomorphism lies in {0} ⊕ H₁ᵛ, i.e., its horizontal projection is zero.

Equations

• HorizontalVerticalHomologySplitting.IsVertical X Λ ℓ hΛ hcompat hodd x = ((HorizontalVerticalHomologySplitting.projH X Λ ℓ hΛ hcompat hodd) x = 0)

Cohomology splitting

@[reducible, inline]

abbrev HorizontalVerticalHomologySplitting.coH1h {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : Type

The horizontal cohomology: H¹_h = H¹(C(X,L)) ⊗_H H⁰(C_ℓ). By the Künneth formula applied to cohomology (which equals homology in dimension over 𝔽₂ by Def_2), this is isomorphic to the p = 1 balanced Künneth summand. We use the homology-cohomology equivalence to define this.

Equations

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

@[reducible, inline]

abbrev HorizontalVerticalHomologySplitting.coH1v {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : Type

The vertical cohomology: H¹_v = H⁰(C(X,L)) ⊗_H H¹(C_ℓ).

Equations

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

def HorizontalVerticalHomologySplitting.coprojH {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : H1 X Λ ℓ hΛ hcompat →ₗ[𝔽₂] coH1h X Λ ℓ hΛ hcompat

The cohomology horizontal projection p_h : H¹ → H¹_h, defined analogously to projH using the Künneth isomorphism on cohomology. Since over 𝔽₂, homology and cohomology are isomorphic (Def_2), we use the same balanced Künneth summands.

Equations

• HorizontalVerticalHomologySplitting.coprojH X Λ ℓ hΛ hcompat hodd = HorizontalVerticalHomologySplitting.projH X Λ ℓ hΛ hcompat hodd

def HorizontalVerticalHomologySplitting.coprojV {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) : H1 X Λ ℓ hΛ hcompat →ₗ[𝔽₂] coH1v X Λ ℓ hΛ hcompat

The cohomology vertical projection p_v : H¹ → H¹_v.

Equations

• HorizontalVerticalHomologySplitting.coprojV X Λ ℓ hΛ hcompat hodd = HorizontalVerticalHomologySplitting.projV X Λ ℓ hΛ hcompat hodd

Key properties

theorem HorizontalVerticalHomologySplitting.projH_projV_jointly_surjective {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hodd : Odd (Fintype.card H)) (y_h : H1h X Λ ℓ hΛ hcompat) (y_v : H1v X Λ ℓ hΛ hcompat) : ∃ (x : H1 X Λ ℓ hΛ hcompat), (projH X Λ ℓ hΛ hcompat hodd) x = y_h ∧ (projV X Λ ℓ hΛ hcompat hodd) x = y_v

The horizontal and vertical projections jointly determine the Künneth decomposition: the map (pʰ, pᵛ) factors through the Künneth isomorphism, and the summands at p ∉ {0, 1} are zero (since both the Tanner and cycle complexes are 1-complexes).

Witness lemmas

theorem HorizontalVerticalHomologySplitting.H1h_nonempty {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : Nonempty (H1h X Λ ℓ hΛ hcompat)

Witness: H1h is nonempty (contains 0).

theorem HorizontalVerticalHomologySplitting.H1v_nonempty {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : Nonempty (H1v X Λ ℓ hΛ hcompat)

Witness: H1v is nonempty (contains 0).

theorem HorizontalVerticalHomologySplitting.H1_nonempty {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) : Nonempty (H1 X Λ ℓ hΛ hcompat)

Witness: H1 is nonempty (contains 0).