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 MIPRE.LCS.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_reducible]

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

Equations

• MIPRE.LCS.instDecidableEqSolutionGen = MIPRE.LCS.instDecidableEqSolutionGen.decEq

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

Equations

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

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 MIPRE.LCS.genVar {S : LinearSystem} (j : Fin S.layout.s) : FreeGroup (SolutionGen S)

The free-group generator attached to variable j.

Equations

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

def MIPRE.LCS.genJ {S : LinearSystem} : FreeGroup (SolutionGen S)

The distinguished central free-group generator.

Equations

• MIPRE.LCS.genJ = FreeGroup.of MIPRE.LCS.SolutionGen.J

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

The relator forcing x to be an involution.

Equations

• MIPRE.LCS.involutionRel x = x ^ 2

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

The commutator relator forcing x and y to commute.

Equations

• MIPRE.LCS.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 MIPRE.LCS.eqSupport (S : LinearSystem) (i : Fin S.layout.r) : Finset (Fin S.layout.s)

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

Equations

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

def MIPRE.LCS.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

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

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

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

Equations

• MIPRE.LCS.equationRelator S i = MIPRE.LCS.equationWord S i * (MIPRE.LCS.genJ ^ (S.b i).val)⁻¹

def MIPRE.LCS.SameEquation (S : LinearSystem) (j k : Fin S.layout.s) : Prop

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

Equations

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

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

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

Equations

• MIPRE.LCS.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 MIPRE.LCS.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 MIPRE.LCS.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 MIPRE.LCS.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 MIPRE.LCS.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 MIPRE.LCS.SolutionGroup (S : LinearSystem) : Type

The solution group of a binary linear system: the group presented by the defining relators of solutionRelators.

Equations

• MIPRE.LCS.SolutionGroup S = PresentedGroup (MIPRE.LCS.solutionRelators S)

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

The distinguished quotient element attached to variable j.

Equations

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

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

The distinguished quotient element J.

Equations

• MIPRE.LCS.SolutionGroup.J = PresentedGroup.of MIPRE.LCS.SolutionGen.J

@[simp]

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

@[simp]

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

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

theorem MIPRE.LCS.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 MIPRE.LCS.SolutionGroup.equation_holds {S : LinearSystem} (i : Fin S.layout.r) : (PresentedGroup.mk (solutionRelators S)) (equationWord S i) = J ^ (S.b i).val