Documentation

CslibFrontier.Foundations.LinearAlgebra.Matrix.EndpointIncidence

Incidence matrices with indexed endpoint pairs #

The two endpoints of each column contribute separately. In characteristic two a loop therefore gives a zero column, while different column indices retain parallel occurrences. No simple-graph edge-count convention is used.

Main definitions #

Main results #

source
def Matrix.endpointIncidence {V : Type u_1} {E : Type u_2} [DecidableEq V] (u v : E → V) :
Matrix V E (ZMod 2)

The characteristic-two incidence matrix of indexed endpoint pairs. Both ends contribute, so a loop contributes twice and cancels. Parallel occurrences retain their column indices.

Instances For
    source
    theorem Matrix.endpointIncidence_transpose_mulVec {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] (u v : E → V) (s : V → ZMod 2) (e : E) :
    (endpointIncidence u v).transpose.mulVec s e = s (u e) + s (v e)

    The transpose incidence map computes endpoint differences over the two-element field.

    source
    theorem Matrix.mem_ker_endpointIncidence_transpose {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] (u v : E → V) (s : V → ZMod 2) :
    s ∈ (endpointIncidence u v).transpose.mulVecLin.ker ↔ ∀ (e : E), s (u e) = s (v e)

    The kernel of the transpose incidence map consists exactly of endpoint-constant functions.

    source
    noncomputable def Matrix.endpointIncidenceKernelEquiv {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] (u v : E → V) (root : V) (hconn : ∀ (s : V → ZMod 2), (∀ (e : E), s (u e) = s (v e)) → ∀ (a b : V), s a = s b) :
    ZMod 2 ≃ₗ[ZMod 2] ↥(endpointIncidence u v).transpose.mulVecLin.ker

    In a connected endpoint system, constants give the whole transpose incidence kernel. The hypothesis states ordinary endpoint connectivity in its invariant-function form.

    Instances For
      source
      theorem Matrix.rank_endpointIncidence_add_one {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] (u v : E → V) (root : V) (hconn : ∀ (s : V → ZMod 2), (∀ (e : E), s (u e) = s (v e)) → ∀ (a b : V), s a = s b) :
      (endpointIncidence u v).rank + 1 = Fintype.card V

      A connected indexed incidence matrix has rank one less than its number of vertices. This counts endpoint names and indexed columns separately.

      source
      theorem Matrix.range_transpose_eq_ker_of_euler {V : Type u_1} {E : Type u_2} {F : Type u_3} [Fintype V] [Fintype E] [Fintype F] (B : Matrix V E (ZMod 2)) (D : Matrix F E (ZMod 2)) (hzero : D * B.transpose = 0) (hB : B.rank + 1 = Fintype.card V) (hD : D.rank + 1 = Fintype.card F) (hEuler : Fintype.card V + Fintype.card F = Fintype.card E + 2) :
      B.transpose.mulVecLin.range = D.mulVecLin.ker

      A zero matrix product and the connected Euler dimension equation force exactness. This finite-dimensional argument discharges the cycle/cut-space dimension step without a spanning-tree, cotree, or lifting certificate.