Strong connectivity of the directed graph of a matrix

A square matrix A with entries in a partially ordered type determines a directed graph on its index set, with an edge from i to a distinct j when 0 < A i j. When the off-diagonal entries are nonnegative, strong connectivity of this directed graph is the same as the absence of a disconnecting cut: no nonempty proper set of indices has all of its outgoing entries zero.

For a symmetric A the directed graph is an ordinary graph and strong connectivity is ordinary connectedness; the cut condition is then the form in which Stacks, Tag 0C6Z states the connectedness condition on the intersection matrix of a numerical type.

Main results

• Matrix.forall_reflTransGen_ne_and_pos_iff: for a matrix with nonnegative off-diagonal entries, strong connectivity of its directed graph is the absence of a disconnecting cut.
• Matrix.eq_smul_of_mulVec_eq_zero: if a matrix over a linear ordered field has nonnegative off-diagonal entries and strongly connected positive-entry graph, then every vector in its kernel is proportional to any strictly positive vector in its kernel.

theorem Matrix.forall_reflTransGen_ne_and_pos_iff {C : Type u_1} {R : Type u_2} [PartialOrder R] [Zero R] (A : Matrix C C R) (hA : ∀ (i j : C), i ≠ j → 0 ≤ A i j) : (∀ (i j : C), Relation.ReflTransGen (fun (i j : C) => i ≠ j ∧ 0 < A i j) i j) ↔ ∀ (s : Set C), s.Nonempty → s ≠ Set.univ → ¬∀ i ∈ s, ∀ j ∉ s, A i j = 0

For a matrix A whose off-diagonal entries are nonnegative, strong connectivity of the directed graph with an edge from i to a distinct j when 0 < A i j is equivalent to the absence of a disconnecting cut: no nonempty proper set of indices s has all of its outgoing entries A i j, for i ∈ s and j ∉ s, zero. No symmetry of A is assumed, so the left-hand side is connectedness of an ordinary graph only when A is symmetric, as the intersection matrix of a numerical type is. The right-hand side is then the form in which Stacks, Tag 0C6Z states the connectedness condition on a numerical type, so this is what supplies the connected field of TauCeti.NumericalType when one is constructed.

The nonnegativity hypothesis is what turns a nonzero cross-entry into a positive one, and so cannot be dropped.

theorem Matrix.eq_smul_of_mulVec_eq_zero {C : Type u_1} {K : Type u_2} [Fintype C] [Field K] [LinearOrder K] [IsStrictOrderedRing K] (A : Matrix C C K) (hnonneg : ∀ (i j : C), i ≠ j → 0 ≤ A i j) (hconnected : ∀ (i j : C), Relation.ReflTransGen (fun (i j : C) => i ≠ j ∧ 0 < A i j) i j) (m x : C → K) (hm : ∀ (i : C), 0 < m i) (hAm : A.mulVec m = 0) (hAx : A.mulVec x = 0) : ∃ (c : K), x = c • m

The weighted maximum principle for a matrix over a linear ordered field: if its off-diagonal entries are nonnegative, its positive-entry graph is strongly connected, and its kernel contains a strictly positive vector m, then every kernel vector is a scalar multiple of m. This is useful for proving that kernels of connected intersection matrices have rank one.