Coq-Combi - Algebraic combinatorics in Coq
Date of the last release: 26 October 2015
Person in charge :
HIVERT Florent
- the Littlewood-Richardson rule using Schützeberger approach, it includes
the Robinson-Schensted correspondance
the construction of the plactic monoïd
the Littlewood-Richardson and Pieri rules using the combinatorial (tableau definition of Schur polynomials).
- basic theory of symmetric functions including
Schur function and Kostka numbers and the equivalence of the combinatorial and algebraic (Jacobi) definition of Schur functions
the classical bases, Newton formulas and various basis changes
the scalar product and the Cauchy formula.
- the character theory of the symmetric Groups. We do not use representations but rather goes as fast as possible to Frobenius isomorphism and then uses computations with symmetric polynomials. it includes
cycle types for permutations (together with Thibaut Benjamin)
The tower structure and the restriction and induction formulas for class indicator (together with Thibaut Benjamin)
structure of the centralizer of a permutation
Young character and Young Rule
the theory of Frobenius characteristic and Frobenius character formula
the Littlewood-Richardson rule for irreducible character
- the Hook-Length Formula for standard Young tableaux (together with Christine Paulin and Olivier Stietel)
- the Erdös Szekeres theorem about increassing and decreassing subsequences
- various Combinatorial objects including
totally and partially ordered types,
integer partitions and compositions,
tableaux, standard tableaux, skew tableaux,
subsequences, integer vectors,
standard words and permutations,
Yamanouchi words
- the Coxeter presentation of the symmetric group.
- the factorization of the Vandermonde determinant as the product of differences.
More information: https://github.com/hivert/Coq-Combi
Software
Research activities
Members
HIVERT Florent
Group
