Rem_3: Binary Vector Notation

Statement

Throughout this work, we abuse notation by identifying a subset of vertices, edges, or cycles with its characteristic binary vector over $\mathbb{Z}_2 = \mathbb{F}_2$. For a set $S$ of vertices/edges/cycles, the corresponding binary vector has a 1 in position $i$ if and only if element $i$ belongs to $S$. Addition of binary vectors corresponds to symmetric difference of sets. This identification allows us to use linear algebra over $\mathbb{Z}_2$ to reason about graph-theoretic properties.

Main Definitions

• BinaryVector : The type of binary vectors over a finite index set, i.e., functions α → ZMod 2
• characteristicVector : Maps a subset S to its characteristic binary vector
• fromBinaryVector : Maps a binary vector back to the corresponding subset

Key Properties

• characteristicVector_mem_iff : Position i is 1 iff element i belongs to S
• characteristicVector_add : Addition corresponds to symmetric difference
• characteristicVector_injective : The identification is injective (subsets uniquely determine vectors)
• characteristicVector_bijective : The identification is a bijection

Corollaries

• This identification makes Finset α into a ZMod 2-vector space
• Linear algebra over ZMod 2 can be applied to reason about set operations

Binary Vectors over ZMod 2

@[reducible, inline]

abbrev BinaryVector (α : Type u_1) : Type u_1

A binary vector over an index set α is a function to ZMod 2. This is the type of characteristic vectors.

Equations

• BinaryVector α = (α → ZMod 2)

def BinaryVector.zero {α : Type u_1} : BinaryVector α

The zero vector (all zeros)

Equations

• BinaryVector.zero x✝ = 0

def BinaryVector.ones {α : Type u_1} : BinaryVector α

The all-ones vector

Equations

• BinaryVector.ones x✝ = 1

def BinaryVector.add {α : Type u_1} (v w : BinaryVector α) : BinaryVector α

Addition of binary vectors (componentwise in ZMod 2)

Equations

• v.add w i = v i + w i

instance BinaryVector.instZero {α : Type u_1} : Zero (BinaryVector α)

Equations

• BinaryVector.instZero = { zero := BinaryVector.zero }

instance BinaryVector.instAdd {α : Type u_1} : Add (BinaryVector α)

Equations

• BinaryVector.instAdd = { add := BinaryVector.add }

@[simp]

theorem BinaryVector.zero_apply {α : Type u_1} (i : α) : 0 i = 0

@[simp]

theorem BinaryVector.add_apply {α : Type u_1} (v w : BinaryVector α) (i : α) : (v + w) i = v i + w i

instance BinaryVector.instAddCommGroup {α : Type u_1} : AddCommGroup (BinaryVector α)

Binary vectors form an additive group (every element is its own inverse in ZMod 2)

Equations

• BinaryVector.instAddCommGroup = Pi.addCommGroup

instance BinaryVector.instModuleZModOfNatNat {α : Type u_1} : Module (ZMod 2) (BinaryVector α)

Binary vectors form a ZMod 2 module (i.e., a vector space over F_2)

Equations

• BinaryVector.instModuleZModOfNatNat = Pi.module α (fun (x : α) => ZMod 2) (ZMod 2)

Characteristic Vector of a Set

def characteristicVector {α : Type u_1} [DecidableEq α] (S : Finset α) : BinaryVector α

The characteristic vector of a finset S: position i has value 1 iff i ∈ S.

Equations

• characteristicVector S i = if i ∈ S then 1 else 0

noncomputable def characteristicVector' {α : Type u_1} (S : Finset α) : BinaryVector α

Alternative definition using Set.indicator

Equations

• characteristicVector' S = (↑S).indicator fun (x : α) => 1

@[simp]

theorem characteristicVector_apply_mem {α : Type u_1} [DecidableEq α] (S : Finset α) (i : α) (h : i ∈ S) : characteristicVector S i = 1

@[simp]

theorem characteristicVector_apply_not_mem {α : Type u_1} [DecidableEq α] (S : Finset α) (i : α) (h : i ∉ S) : characteristicVector S i = 0

theorem characteristicVector_mem_iff {α : Type u_1} [DecidableEq α] (S : Finset α) (i : α) : characteristicVector S i = 1 ↔ i ∈ S

Key characterization: position i is 1 iff element i belongs to S

theorem characteristicVector_not_mem_iff {α : Type u_1} [DecidableEq α] (S : Finset α) (i : α) : characteristicVector S i = 0 ↔ i ∉ S

@[simp]

theorem characteristicVector_empty {α : Type u_1} [DecidableEq α] : characteristicVector ∅ = 0

The characteristic vector of the empty set is zero

@[simp]

theorem characteristicVector_bot {α : Type u_1} [DecidableEq α] : characteristicVector ⊥ = 0

The characteristic vector of the bottom element (used for symmDiff_self)

@[simp]

theorem characteristicVector_singleton {α : Type u_1} [DecidableEq α] (a : α) : characteristicVector {a} = fun (i : α) => if i = a then 1 else 0

The characteristic vector of a singleton

Symmetric Difference and Vector Addition

theorem characteristicVector_add {α : Type u_1} [DecidableEq α] (S T : Finset α) : characteristicVector S + characteristicVector T = characteristicVector (symmDiff S T)

Key theorem: Addition of characteristic vectors corresponds to symmetric difference. This is the fundamental property that allows linear algebra over Z_2 to encode set operations.

theorem characteristicVector_symmDiff {α : Type u_1} [DecidableEq α] (S T : Finset α) : characteristicVector (symmDiff S T) = characteristicVector S + characteristicVector T

Symmetric difference is encoded as addition

@[simp]

theorem characteristicVector_self_add {α : Type u_1} [DecidableEq α] (S : Finset α) : characteristicVector S + characteristicVector S = 0

Self-symmetric difference is empty (S Δ S = ∅)

theorem characteristicVector_neg_eq_self {α : Type u_1} [DecidableEq α] (S : Finset α) : -characteristicVector S = characteristicVector S

In ZMod 2, every element is its own additive inverse

Inverse Map: From Binary Vector to Finset

def fromBinaryVector {α : Type u_1} [Fintype α] (v : BinaryVector α) : Finset α

Convert a binary vector back to a finset (the support of the vector)

Equations

• fromBinaryVector v = {i : α | v i = 1}

@[simp]

theorem mem_fromBinaryVector {α : Type u_1} [DecidableEq α] [Fintype α] (v : BinaryVector α) (i : α) : i ∈ fromBinaryVector v ↔ v i = 1

@[simp]

theorem fromBinaryVector_characteristicVector {α : Type u_1} [DecidableEq α] [Fintype α] (S : Finset α) : fromBinaryVector (characteristicVector S) = S

Round-trip: characteristic vector then back to finset gives the original finset

@[simp]

theorem characteristicVector_fromBinaryVector {α : Type u_1} [DecidableEq α] [Fintype α] (v : BinaryVector α) : characteristicVector (fromBinaryVector v) = v

Round-trip: finset to vector then back gives the original vector (for vectors that only take values 0 and 1, which is automatic in ZMod 2)

theorem characteristicVector_injective {α : Type u_1} [DecidableEq α] [Fintype α] : Function.Injective characteristicVector

The characteristic vector map is injective

theorem characteristicVector_surjective {α : Type u_1} [DecidableEq α] [Fintype α] : Function.Surjective characteristicVector

The characteristic vector map is surjective

theorem characteristicVector_bijective {α : Type u_1} [DecidableEq α] [Fintype α] : Function.Bijective characteristicVector

The characteristic vector map is a bijection

def characteristicVectorEquiv {α : Type u_1} [DecidableEq α] [Fintype α] : Finset α ≃ BinaryVector α

The characteristic vector map as an equivalence

Equations

• characteristicVectorEquiv = { toFun := characteristicVector, invFun := fromBinaryVector, left_inv := ⋯, right_inv := ⋯ }

Algebraic Structure: Finsets as a Vector Space over ZMod 2

instance finsetAdd {α : Type u_1} [DecidableEq α] : Add (Finset α)

Addition on Finsets via symmetric difference

Equations

• finsetAdd = { add := fun (S T : Finset α) => symmDiff S T }

instance finsetZero {α : Type u_1} : Zero (Finset α)

Zero element is the empty set

Equations

• finsetZero = { zero := ∅ }

instance finsetNeg {α : Type u_1} : Neg (Finset α)

Negation is identity (every element is its own inverse)

Equations

• finsetNeg = { neg := id }

instance finsetAddCommGroup {α : Type u_1} [DecidableEq α] [Fintype α] : AddCommGroup (Finset α)

Finsets form an additive commutative group with symmetric difference as addition

Equations

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

instance finsetSMul {α : Type u_1} : SMul (ZMod 2) (Finset α)

Scalar multiplication by ZMod 2: 0 * S = ∅, 1 * S = S

Equations

• finsetSMul = { smul := fun (c : ZMod 2) (S : Finset α) => if c = 0 then ∅ else S }

@[simp]

theorem zero_smul_finset {α : Type u_1} [DecidableEq α] [Fintype α] (S : Finset α) : 0 • S = ∅

@[simp]

theorem one_smul_finset {α : Type u_1} [DecidableEq α] [Fintype α] (S : Finset α) : 1 • S = S

instance finsetModule {α : Type u_1} [DecidableEq α] [Fintype α] : Module (ZMod 2) (Finset α)

Finsets form a module (vector space) over ZMod 2

Equations

• finsetModule = { toSMul := finsetSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

theorem characteristicVector_add_eq {α : Type u_1} [DecidableEq α] [Fintype α] (S T : Finset α) : characteristicVector (S + T) = characteristicVector S + characteristicVector T

The characteristic vector map is a linear map

theorem characteristicVector_smul {α : Type u_1} [DecidableEq α] [Fintype α] (c : ZMod 2) (S : Finset α) : characteristicVector (c • S) = c • characteristicVector S

The characteristic vector map preserves scalar multiplication

def characteristicVectorLinearEquiv {α : Type u_1} [DecidableEq α] [Fintype α] : Finset α ≃ₗ[ZMod 2] BinaryVector α

The characteristic vector map is a linear equivalence

Equations

• characteristicVectorLinearEquiv = { toFun := characteristicVector, map_add' := ⋯, map_smul' := ⋯, invFun := fromBinaryVector, left_inv := ⋯, right_inv := ⋯ }

Properties Useful for Graph Theory Applications

theorem characteristicVector_union_of_disjoint {α : Type u_1} [DecidableEq α] [Fintype α] (S T : Finset α) (h : Disjoint S T) : characteristicVector (S ∪ T) = characteristicVector S + characteristicVector T

The union of disjoint sets corresponds to addition (which is XOR/symmetric difference)

theorem characteristicVector_inter {α : Type u_1} [DecidableEq α] [Fintype α] (S T : Finset α) (i : α) : characteristicVector (S ∩ T) i = characteristicVector S i * characteristicVector T i

Intersection can be expressed in terms of the algebraic structure

theorem characteristicVector_compl {α : Type u_1} [DecidableEq α] [Fintype α] (S : Finset α) : characteristicVector Sᶜ = BinaryVector.ones + characteristicVector S

Complement relative to the universe

theorem card_eq_sum_characteristicVector {α : Type u_1} [DecidableEq α] [Fintype α] (S : Finset α) : S.card = ∑ i : α, (characteristicVector S i).val

The cardinality of a set can be recovered from its characteristic vector

theorem finset_eq_iff_characteristicVector_eq {α : Type u_1} [DecidableEq α] [Fintype α] (S T : Finset α) : S = T ↔ characteristicVector S = characteristicVector T

Two sets are equal iff their characteristic vectors are equal

theorem card_symmDiff_add_twice_inter {α : Type u_1} [DecidableEq α] [Fintype α] (S T : Finset α) : (symmDiff S T).card + 2 * (S ∩ T).card = S.card + T.card

The symmetric difference has cardinality related to the original sets

Summary

The binary vector notation convention establishes:

1. Identification: A finset S ⊆ α corresponds to its characteristic vector χ_S : α → ZMod 2 where χ_S(i) = 1 iff i ∈ S

2. Addition = Symmetric Difference: χ_{S Δ T} = χ_S + χ_T (componentwise in ZMod 2)

3. Bijectivity: This identification is a bijection, so sets and vectors can be used interchangeably

4. Linear Structure: Under this identification, Finset α becomes a ZMod 2-vector space where addition is symmetric difference

5. Application: This allows linear algebra techniques over F_2 to be applied to graph-theoretic problems involving sets of vertices, edges, or cycles.

The key insight is that XOR (symmetric difference) becomes ordinary addition in ZMod 2, making linear algebraic techniques available for reasoning about graph properties.