Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Permanent polynomials and symmetric projections

Lax461425.Permanent · concepts/Lax461425/Permanent.lean · lax-461425

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The permanent polynomial, affine linear polynomials, and symmetric affine projections of permanents. The order of the projected permanent is unrestricted.

    Concept map
    4 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax461425.SymmetricFamilies
    2import Mathlib.LinearAlgebra.Matrix.Permanent
    3import Mathlib.Algebra.MvPolynomial.Rename
    4import Lax461425.MatrixSymmetry
    5
    6/-!
    7---
    8title: Permanent polynomials and symmetric projections
    9type: definition
    10---
    11The permanent polynomial, affine linear polynomials, and symmetric affine projections of
    12permanents. The order of the projected permanent is unrestricted.
    13-/
    14
    15open Lax461425.SymmetricFamilies (MatrixPolynomial)
    16
    17namespace Lax461425.Permanent
    18
    19open MatrixSymmetry
    20
    21/-- The permanent polynomial on an `n × n` variable matrix. -/
    22noncomputable def permanent (K : Type*) [CommSemiring K] (n : ℕ) :
    23 MatrixPolynomial n K :=
    24 Matrix.permanent (fun i j => MvPolynomial.X (i, j))
    25
    26/-- An affine linear polynomial, given by a constant and finitely many variable coefficients. -/
    27def IsAffine {V K : Type*} [CommSemiring K] (p : MvPolynomial V K) : Prop :=
    28 ∃ (c : K) (s : Finset V) (a : V → K),
    29 p = MvPolynomial.C c + ∑ v ∈ s, MvPolynomial.C (a v) * MvPolynomial.X v
    30
    31/-- A symmetric affine projection of a permanent, with no restriction on the source order.
    32The finite index type is nonempty, corresponding to source order at least one. -/
    33def IsSymmetricProjection {V G K : Type*} [Group G] [CommSemiring K]
    34 (ρ : G →* Equiv.Perm V) (p : MvPolynomial V K) : Prop :=
    35 ∃ (A : Type) (_ : Fintype A) (_ : DecidableEq A) (_ : Nonempty A)
    36 (M : Matrix A A (MvPolynomial V K)),
    37 p = Matrix.permanent M ∧ (∀ i j, IsAffine (M i j)) ∧
    38 ∀ γ, ∃ α β : Equiv.Perm A,
    39 ∀ i j, M (α i) (β j) = MvPolynomial.rename (ρ γ) (M i j)
    40
    41end Lax461425.Permanent
    42
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…