Solution Groups for Binary Linear Systems

This module defines the solution group attached to a binary linear system. For a system with variables g_j and distinguished generator J, the presentation is generated by the four standard families of relations:

• every g_j and J is an involution;
• each g_j commutes with J;
• variables that occur in a common equation commute;
• each equation imposes the product relation ∏_{j ∈ support(i)} g_j = J ^ b_i.

The main construction is SolutionGroup S, together with quotient elements SolutionGroup.var and SolutionGroup.J and lemmas showing that the four families of defining constraints hold in the presented group.

inductive SolutionGen (S : LinearSystem) : Type

Generators for the solution group of a binary linear system.

• var {S : LinearSystem} : Fin S.layout.s → SolutionGen S
• J {S : LinearSystem} : SolutionGen S

instance instDecidableEqSolutionGen {S✝ : LinearSystem} : DecidableEq (SolutionGen S✝)

Equations

• instDecidableEqSolutionGen = instDecidableEqSolutionGen.decEq

def instDecidableEqSolutionGen.decEq {S✝ : LinearSystem} (x✝ x✝¹ : SolutionGen S✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqSolutionGen.decEq (SolutionGen.var a) (SolutionGen.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqSolutionGen.decEq (SolutionGen.var a) SolutionGen.J = isFalse ⋯
• instDecidableEqSolutionGen.decEq SolutionGen.J (SolutionGen.var a) = isFalse ⋯
• instDecidableEqSolutionGen.decEq SolutionGen.J SolutionGen.J = isTrue ⋯

def instReprSolutionGen.repr {S✝ : LinearSystem} : SolutionGen S✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprSolutionGen.repr SolutionGen.J prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SolutionGen.J")).group prec✝

instance instReprSolutionGen {S✝ : LinearSystem} : Repr (SolutionGen S✝)

Equations

• instReprSolutionGen = { reprPrec := instReprSolutionGen.repr }

def formatRelator {S : LinearSystem} (word : FreeGroup (SolutionGen S)) : String

Pretty-print a free-group relator as a product of solution-group generators.

Equations

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

Defining Constraint Relators

The next definitions collect the free-group words used to impose the four families of constraints in the solution-group presentation.

def genVar {S : LinearSystem} (j : Fin S.layout.s) : FreeGroup (SolutionGen S)

The free-group generator attached to variable j.

Equations

• genVar j = FreeGroup.of (SolutionGen.var j)

def genJ {S : LinearSystem} : FreeGroup (SolutionGen S)

The distinguished central free-group generator.

Equations

• genJ = FreeGroup.of SolutionGen.J

def involutionRel {α : Type u_1} (x : FreeGroup α) : FreeGroup α

The relator forcing x to be an involution.

Equations

• involutionRel x = x ^ 2

def commuteRel {α : Type u_1} (x y : FreeGroup α) : FreeGroup α

The commutator relator forcing x and y to commute.

Equations

• commuteRel x y = x * y * x⁻¹ * y⁻¹

∏_{j ∈ support(i)} g_j = J ^ b_i

The next helper lemmas work towards the product for equation i equals J^(b_i)

def eqSupport (S : LinearSystem) (i : Fin S.layout.r) : Finset (Fin S.layout.s)

The support of equation i, extracted from the coefficient matrix.

Equations

• eqSupport S i = {j : Fin S.layout.s | S.A i j = 1}

def equationWord (S : LinearSystem) (i : Fin S.layout.r) : FreeGroup (SolutionGen S)

The left-hand-side word of equation i, ordered by the Finset order.

Equations

• equationWord S i = (List.map genVar ((eqSupport S i).sort fun (x1 x2 : Fin S.layout.s) => x1 ≤ x2)).prod

def equationRelator (S : LinearSystem) (i : Fin S.layout.r) : FreeGroup (SolutionGen S)

The relator encoding equation i as equationWord = J^(b i).

Equations

• equationRelator S i = equationWord S i * (genJ ^ ↑(S.b i))⁻¹

def sameEquation (S : LinearSystem) (j k : Fin S.layout.s) : Prop

Two variables are related when they appear together in some equation.

Equations

• sameEquation S j k = ∃ (i : Fin S.layout.r), S.A i j = 1 ∧ S.A i k = 1

def sameEquationBool (S : LinearSystem) (j k : Fin S.layout.s) : Bool

Computable test for sameEquation, used to build an inspectable relator list.

Equations

• sameEquationBool S j k = (List.finRange S.layout.r).any fun (i : Fin S.layout.r) => decide (S.A i j = 1 ∧ S.A i k = 1)

def solutionRelatorsList (S : LinearSystem) : List (FreeGroup (SolutionGen S))

List of the defining relators of the solution group of S.

Equations

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

Defining the relations as a set

def solutionRelators (S : LinearSystem) : Set (FreeGroup (SolutionGen S))

The defining relators of the solution group of S.

Equations

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

theorem sameEquationBool_iff (S : LinearSystem) (j k : Fin S.layout.s) : sameEquationBool S j k = true ↔ sameEquation S j k

The computable same-equation test agrees with the propositional predicate.

theorem mem_solutionRelatorsList_iff {S : LinearSystem} {w : FreeGroup (SolutionGen S)} : w ∈ solutionRelatorsList S ↔ w ∈ solutionRelators S

The list presentation has the same membership as the direct set presentation.

@[reducible, inline]

abbrev SolutionGroup (S : LinearSystem) : Type

!

The Presented Solution Group

The solution group of a linear system is the presented group with the relators defined above.

Equations

• SolutionGroup S = PresentedGroup (solutionRelators S)

def SolutionGroup.var {S : LinearSystem} (j : Fin S.layout.s) : SolutionGroup S

The distinguished quotient element attached to variable j.

Equations

• SolutionGroup.var j = PresentedGroup.of (SolutionGen.var j)

def SolutionGroup.J {S : LinearSystem} : SolutionGroup S

The distinguished quotient element J.

Equations

• SolutionGroup.J = PresentedGroup.of SolutionGen.J

@[simp]

theorem SolutionGroup.var_sq {S : LinearSystem} (j : Fin S.layout.s) : var j ^ 2 = 1

@[simp]

theorem SolutionGroup.J_sq {S : LinearSystem} : J ^ 2 = 1

theorem SolutionGroup.var_comm_J {S : LinearSystem} (j : Fin S.layout.s) : var j * J = J * var j

theorem SolutionGroup.var_comm_of_sameEquation {S : LinearSystem} {j k : Fin S.layout.s} (hjk : sameEquation S j k) : var j * var k = var k * var j

theorem SolutionGroup.equation_holds {S : LinearSystem} (i : Fin S.layout.r) : (PresentedGroup.mk (solutionRelators S)) (equationWord S i) = J ^ ↑(S.b i)