Symmetric ABP characterisation
Lax461425.SymmetricABPCharacterisation · concepts/Lax461425/SymmetricABPCharacterisation.lean · lax-461425
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Families computed by matrix-symmetric ABPs with polynomial vertex orbits and families computed by matrix-symmetric skew circuits with polynomial gate orbits coincide over a field of characteristic zero, that is, . The inclusion is the theorem on symmetric skew circuits from symmetric ABPs; the reverse inclusion follows from the characterisation of matrix-symmetric skew circuits by bounded-pathwidth patterns.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax461425.SymmetricABPs |
| 2 | import Lax461425.SkewFromABP |
| 3 | import Lax461425.ABPsForPatterns |
| 4 | import Lax461425.SkewCircuitCharacterisation |
| 5 | import Lax461425.HomomorphismSpanning |
| 6 | |
| 7 | /-! |
| 8 | --- |
| 9 | title: Symmetric ABP characterisation |
| 10 | type: theorem |
| 11 | --- |
| 12 | Families computed by matrix-symmetric ABPs with polynomial vertex orbits and families |
| 13 | computed by matrix-symmetric skew circuits with polynomial gate orbits coincide over a |
| 14 | field of characteristic zero, that is, `symVBP = symVS`. The inclusion `symVBP ⊆ symVS` |
| 15 | is the theorem on symmetric skew circuits from symmetric ABPs; the reverse inclusion follows |
| 16 | from the characterisation of matrix-symmetric skew circuits by bounded-pathwidth patterns. |
| 17 | -/ |
| 18 | |
| 19 | namespace Lax461425.SymmetricABPCharacterisation |
| 20 | |
| 21 | open SymmetricABPs SymmetricFamilies SymmetricClasses SymmetricVNP |
| 22 | |
| 23 | /-- Symmetric polynomial-orbit skew-circuit families have symmetric |
| 24 | polynomial-orbit ABPs. -/ |
| 25 | axiom inSymVBP_of_inSymVS {K : Type*} [Field K] [CharZero K] (f : MatrixFamily K) |
| 26 | (hf : InSymVS f) : InSymVBP f |
| 27 | |
| 28 | /-- Symmetric polynomial-orbit ABPs and skew circuits define the same class. -/ |
| 29 | axiom characterisation {K : Type*} [Field K] [CharZero K] (f : MatrixFamily K) : |
| 30 | InSymVBP f ↔ InSymVS f |
| 31 | |
| 32 | end Lax461425.SymmetricABPCharacterisation |
| 33 |
Builds on
Used by
none
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments