Definition 28: Iota and Pi Maps #
Let X be a finite graph with a free right H = ℤ_ℓ-action (Def_24), L a local code
with H-invariant labeling (Def_25), and C(X,L) ⊗_{ℤ_ℓ} C(C_ℓ) the balanced product
Tanner cycle code (Def_26).
We define 𝔽₂-linear maps between the homology of the quotient Tanner code C(X/H, L)
and the horizontal homology H₁ʰ = H₁(C(X,L)) ⊗_H H₀(C_ℓ) (Def_27):
ι : H₁(C(X/H, L)) → H₁ʰ— lifts a cycle on the quotient graph to the balanced product by summing over orbit representatives:ι[∑ a_𝓔 𝓔] = [(∑ a_𝓔 ∑_{e ∈ 𝓔} e ⊗ y₀, 0)]π : H₁ʰ → H₁(C(X/H, L))— projects from the horizontal homology back to the quotient by collapsing orbits:π[(∑ aₑ e ⊗ y₀, 0)] = [∑ aₑ eH]
Both maps are well-defined: ι maps cycles to cycles by the orbit structure of the
balanced product differential, and π is well-defined because horizontal homology classes
have coefficients constant on orbits.
Main Definitions #
quotientTannerComplex— the Tanner code complex on the quotient graphX/HquotientTannerHomology—H₁(C(X/H, L))iotaMap—ι : H₁(C(X/H, L)) → H₁ʰpiMap—π : H₁ʰ → H₁(C(X/H, L))
Main Results #
piMap_comp_iotaMap—π ∘ ι = ℓ · id(over𝔽₂, this equalsidwhenℓis odd)iotaMap_comp_piMap—ι ∘ π = id
Quotient Tanner Code Complex #
The quotient graph X/H has its own Tanner code complex C(X/H, L), built from
the quotient cell complex (Def_24) with the descended labeling (Def_25).
The chain spaces are C₁(X/H) = (X₁/H → 𝔽₂) and C₀(X/H) = (X₀/H → Fin s → 𝔽₂).
The chain space of 1-chains on the quotient graph: C₁(X/H) = (X₁/H → 𝔽₂).
Equations
- IotaPiMaps.quotientC1 X = (X.quotientEdges → 𝔽₂)
Instances For
The chain space of 0-chains on the quotient graph: C₀(X/H) = (X₀/H → Fin s → 𝔽₂).
Equations
- IotaPiMaps.quotientC0 X = (X.quotientVertices → Fin s → 𝔽₂)
Instances For
The quotient local view: for a vertex orbit [v] and a 1-chain c on X/H,
the local view reads off the coefficients of incident edge orbits via the quotient labeling.
Equations
- IotaPiMaps.quotientLocalView X Λ hΛ V = { toFun := fun (c : X.quotientEdges → 𝔽₂) (i : Fin s) => c ↑((GraphWithGroupAction.quotientLabeling Λ hΛ V).symm i), map_add' := ⋯, map_smul' := ⋯ }
Instances For
The Tanner differential on the quotient graph: ∂ : C₁(X/H) → C₀(X/H).
Sends c to v ↦ localView_v(c).
Equations
- IotaPiMaps.quotientTannerDifferential X Λ hΛ = { toFun := fun (c : X.quotientEdges → 𝔽₂) (V : X.quotientVertices) => (IotaPiMaps.quotientLocalView X Λ hΛ V) c, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The quotient Tanner code complex C(X/H, L) as a chain complex over 𝔽₂.
C₁ = (X₁/H → 𝔽₂) in degree 1, C₀ = (X₀/H → Fin s → 𝔽₂) in degree 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The homology H₁(C(X/H, L)) of the quotient Tanner code complex.
Equations
- IotaPiMaps.quotientTannerHomology X Λ hΛ = (IotaPiMaps.quotientTannerComplex X Λ hΛ).homology' 1
Instances For
Abbreviations from Def_27 #
The Iota Map #
The map ι : H₁(C(X/H, L)) → H₁ʰ lifts a cycle on the quotient graph to the
balanced product by summing over orbit representatives.
For an edge orbit 𝓔 = eH, define the orbit indicator 1_𝓔 ∈ C₁(X) as the
function with 1_𝓔(e') = 1 iff e' ∈ 𝓔. Then:
ι[∑_𝓔 a_𝓔 𝓔] = [(∑_𝓔 a_𝓔 [1_𝓔 ⊗ δ_{y₀}], 0)]
The map is well-defined:
- The orbit indicator
1_𝓔isH-invariant, so[1_𝓔 ⊗ g] = [1_𝓔 ⊗ g']for anyg, g'in the same orbit ofC₀(C_ℓ). - ι maps cycles to cycles because the balanced product differential respects the orbit structure.
- ι maps boundaries to boundaries (well-defined on homology classes).
The construction requires:
- Building the orbit indicator function for each edge orbit
- Tensoring with a fixed 0-cell
y₀ofC_ℓin the balanced product - Embedding into the total complex degree-1 chain space
- Showing the resulting element is a cycle when the input is a cycle
- Showing independence of the homology class representative
The ι map: H₁(C(X/H, L)) → H₁ʰ(C(X,L) ⊗_H C(C_ℓ)).
Maps a homology class [∑_𝓔 a_𝓔 𝓔] in the quotient Tanner code to
[(∑_𝓔 a_𝓔 ∑_{e ∈ 𝓔} e ⊗ y₀, 0)] in the horizontal homology of the
balanced product. Here y₀ is a fixed 0-cell of the cycle graph C_ℓ.
Well-definedness: The orbit indicator ∑_{e ∈ 𝓔} δ_e is H-invariant in
C₁(X,L), so tensoring with δ_{y₀} ∈ C₀(C_ℓ) gives a well-defined element
of C₁(X,L) ⊗_H C₀(C_ℓ). The map sends cycles to cycles (the quotient
differential is compatible with the balanced product differential) and
boundaries to boundaries (well-defined on homology).
The Pi Map #
The map π : H₁ʰ → H₁(C(X/H, L)) projects from horizontal homology to the
quotient Tanner code homology by collapsing orbits.
By the Künneth decomposition (Def_27), elements of H₁ʰ = H₁(C(X,L)) ⊗_H H₀(C_ℓ)
are represented by cycles of the form (∑_e a_e e ⊗ y₀, 0) with coefficients
a_e constant on H-orbits. The map sends this to [∑_e a_e eH] in H₁(C(X/H, L)).
Well-definedness: The coefficients a_e are constant on orbits (from the balanced
product structure), so the sum ∑_e a_e eH is well-defined (each orbit contributes
a_𝓔 · 𝓔). The map sends cycles to cycles because the quotient differential is
compatible with the balanced product differential (Def_24).
Key Properties #
π ∘ ι = ℓ · id. Over 𝔽₂ with ℓ odd, ℓ · id = id, so π ∘ ι = id.
Each orbit 𝓔 = eH has |H| = ℓ elements. Applying ι to [𝓔] gives
[∑_{e ∈ 𝓔} e ⊗ y₀], and then π maps each e ⊗ y₀ back to 𝓔,
giving ℓ · [𝓔]. Since ℓ is odd, ℓ ≡ 1 (mod 2), so ℓ · [𝓔] = [𝓔] in 𝔽₂.
ι ∘ π = id.
For a horizontal class [(∑_e a_e e ⊗ y₀, 0)] with a_e constant on orbits,
π sends it to [∑_e a_e eH], and ι lifts back to [(∑_e a_e ∑_{e' ∈ eH} e' ⊗ y₀, 0)].
Since each orbit of size ℓ contributes ℓ copies, and ℓ ≡ 1 (mod 2), this equals
the original class.
Satisfiability Witnesses #
We construct a trivial example: H = Unit acting on a graph with cells n = Unit for all n,
empty boundary maps, s = 0, and ℓ = 3. This gives non-empty vertex and edge sets while
satisfying all required properties vacuously.
Trivial graph with one vertex and one edge, with trivial Unit action.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Trivial labeling with s = 0 (no edges are incident to any vertex).
Equations
- IotaPiMaps.witnessLabeling x✝ = { toFun := fun (e : ↥(IotaPiMaps.witnessGraph.cellIncidentEdges x✝)) => absurd ⋯ ⋯, invFun := fun (i : Fin 0) => i.elim0, left_inv := ⋯, right_inv := ⋯ }
Instances For
The trivial labeling is vacuously invariant (no incident edges).
Trivial MulAction of Unit on Fin 3.
Equations
- IotaPiMaps.witnessUnitMulAction = { smul := fun (x : Unit) (i : Fin 3) => i, mul_smul := IotaPiMaps.witnessUnitMulAction._proof_1, one_smul := IotaPiMaps.witnessUnitMulAction._proof_2 }
Instances For
The trivial action is cycle-compatible.
Witness: iotaMap premises are satisfiable with a non-trivial graph.
We use H = Unit acting on a graph with one vertex and one edge.
Witness: piMap_comp_iotaMap premises are satisfiable (includes oddness).
Witness: iotaMap_comp_piMap premises are satisfiable (includes oddness).
Corollaries #
The ι map is injective (since π ∘ ι = id).
The π map is surjective (since π ∘ ι = id).
The π map is injective (since ι ∘ π = id).
The ι map is surjective (since ι ∘ π = id).
The ι map is a linear isomorphism (since π ∘ ι = id and ι ∘ π = id).
Equations
- IotaPiMaps.iotaEquiv X Λ ℓ hΛ hcompat hℓ_odd hodd = LinearEquiv.ofBijective (IotaPiMaps.iotaMap X Λ ℓ hΛ hcompat) ⋯
Instances For
The π map is a linear isomorphism.
Equations
- IotaPiMaps.piEquiv X Λ ℓ hΛ hcompat hℓ_odd hodd = LinearEquiv.ofBijective (IotaPiMaps.piMap X Λ ℓ hΛ hcompat) ⋯
Instances For
Witness: the quotient Tanner homology is nonempty (contains 0).
Witness: the iota equivalence is nonempty.