A factored connection pairing has bounded rank

The edge-rank hypothesis asks for the rank of the connection map to be bounded. A pairing that factors through a finite index set — each row a combination of a fixed finite family of columns — has its whole range inside the span of that family, so the rank is at most the family's size.

This is the linear algebra behind writing a connection matrix as a Gram matrix: a Gram factorization exhibits each row as a combination of the columns indexed by the ambient space's coordinates.

theorem RS.rank_connectionMap_le_of_mem_span {f : ClosedFragment → ℂ} {t : ℕ} (s : Set (Fragment (Fin t) → ℂ)) (hmem : ∀ (F : Fragment (Fin t)), (fun (G : Fragment (Fin t)) => connectionPairing f t F G) ∈ Submodule.span ℂ s) : Module.rank ℂ ↥(connectionMap f t).range ≤ Cardinal.mk ↑s

A pairing whose rows lie in a span has rank at most that span's generating set.

theorem RS.rank_connectionMap_le_of_factor {f : ClosedFragment → ℂ} {t : ℕ} {χ : Type} [Fintype χ] (u : Fragment (Fin t) → χ → ℂ) (w : χ → Fragment (Fin t) → ℂ) (hfac : ∀ (F G : Fragment (Fin t)), connectionPairing f t F G = ∑ x : χ, u F x * w x G) : Module.rank ℂ ↥(connectionMap f t).range ≤ ↑(Fintype.card χ)

A pairing that factors through a finite index set has rank at most that set's size. The row at F is the combination of the columns w x with coefficients u F x.

theorem RS.edgeRankBounded_of_factor {f : ClosedFragment → ℂ} {R : ℕ} (χ : ℕ → Type) [(t : ℕ) → Fintype (χ t)] (hcard : ∀ (t : ℕ), Fintype.card (χ t) = R ^ t) (u : (t : ℕ) → Fragment (Fin t) → χ t → ℂ) (w : (t : ℕ) → χ t → Fragment (Fin t) → ℂ) (hfac : ∀ (t : ℕ) (F G : Fragment (Fin t)), connectionPairing f t F G = ∑ x : χ t, u t F x * w t x G) : EdgeRankBounded f R

A factored pairing at every arity gives the edge-rank bound.

theorem RS.edgeRankBounded_of_gram {f : ClosedFragment → ℂ} {R : ℕ} (χ : ℕ → Type) [(t : ℕ) → Fintype (χ t)] (hcard : ∀ (t : ℕ), Fintype.card (χ t) = R ^ t) (B : (t : ℕ) → χ t → χ t → ℂ) (T : (t : ℕ) → Fragment (Fin t) → χ t → ℂ) (hgram : ∀ (t : ℕ) (F G : Fragment (Fin t)), connectionPairing f t F G = ∑ x : χ t, ∑ y : χ t, B t x y * T t F x * T t G y) : EdgeRankBounded f R

A Gram factorization gives the edge-rank bound. If the connection pairing is the bilinear form B evaluated at vectors attached to the two fragments, its rank is bounded by the ambient space's dimension.