Characterisation of matrix-symmetric skew circuits
Lax461425.SkewCircuitCharacterisation · concepts/Lax461425/SkewCircuitCharacterisation.lean · lax-461425
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Over a field of characteristic zero, a reduced matrix-symmetric skew circuit on an matrix with support size at most , where and , computes a linear combination of homomorphism polynomials of patterns of pathwidth at most . Together with symmetric ABPs for patterns of bounded pathwidth, it follows that a family of polynomials is computed by matrix-symmetric skew circuits of polynomial orbit size if, and only if, there is a constant such that every is a linear combination of homomorphism polynomials of patterns of pathwidth at most .
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax461425.SymmetricFamilies |
| 2 | import Lax461425.SymmetricClasses |
| 3 | import Lax461425.SymmetricVNP |
| 4 | import Lax461425.SymmetricABPs |
| 5 | import Lax461425.SkewFromABP |
| 6 | import Lax461425.PatternWidths |
| 7 | import Lax461425.Supports |
| 8 | import Lax461425.SupportTheorem |
| 9 | import Lax461425.Rigidification |
| 10 | import Lax461425.ReducedRigid |
| 11 | import Mathlib.LinearAlgebra.Span.Defs |
| 12 | |
| 13 | /-! |
| 14 | --- |
| 15 | title: Characterisation of matrix-symmetric skew circuits |
| 16 | type: theorem |
| 17 | --- |
| 18 | Over a field of characteristic zero, a reduced matrix-symmetric skew circuit on an `n × n` |
| 19 | matrix with support size at most `k`, where `2 ≤ k` and `2k + 1 ≤ n`, computes a linear |
| 20 | combination of homomorphism polynomials of patterns of pathwidth at most `2k`. |
| 21 | Together with symmetric ABPs for patterns of bounded pathwidth, it follows that a family of |
| 22 | polynomials is computed by matrix-symmetric skew circuits of polynomial orbit size |
| 23 | if, and only if, there is a constant such that every is a |
| 24 | linear combination of homomorphism polynomials of patterns of pathwidth at |
| 25 | most . |
| 26 | -/ |
| 27 | namespace Lax461425.SkewCircuitCharacterisation |
| 28 | |
| 29 | open Circuits CircuitProperties MatrixSymmetry Supports |
| 30 | open SymmetricFamilies SymmetricClasses SymmetricVNP SymmetricABPs HomomorphismPolynomials |
| 31 | open PatternWidths |
| 32 | |
| 33 | /-- A bounded-support reduced skew circuit computes a combination of bounded-pathwidth |
| 34 | homomorphism polynomials. -/ |
| 35 | axiom mem_span_hom {K : Type*} [Field K] [CharZero K] {k n : ℕ} (hk : 2 ≤ k) |
| 36 | (hn : 2 * k + 1 ≤ n) (C : Circuit (Fin n × Fin n) K) |
| 37 | (hred : C.IsReduced) (hsym : IsMatrixSymmetric C) (hsize : supportSize C ≤ k) |
| 38 | (hskew : IsSkew C) {p : MatrixPolynomial n K} (hp : C.Computes p) : |
| 39 | p ∈ Submodule.span K {q | ∃ F : Pattern, PathwidthLE (2 * k) F ∧ hom K F n = q} |
| 40 | |
| 41 | /-- `symVS` consists of the families spanned by homomorphism polynomials of patterns of |
| 42 | bounded pathwidth. -/ |
| 43 | axiom characterisation {K : Type*} [Field K] [CharZero K] (f : MatrixFamily K) : |
| 44 | InSymVS f ↔ ∃ k : ℕ, ∀ n, |
| 45 | f n ∈ Submodule.span K {q | ∃ F : Pattern, PathwidthLE k F ∧ hom K F n = q} |
| 46 | |
| 47 | end Lax461425.SkewCircuitCharacterisation |
| 48 |
Builds on
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments