Documentation

TauCeti.Algebra.BrauerAlgebra.Basic

The Brauer algebra #

The Brauer algebra B_k(δ) on k strands with loop value δ, over a commutative semiring R, is the free R-module on the Brauer diagrams on k strands (TauCeti.BrauerDiagram k), multiplied by stacking: for diagrams D₁ and D₂,

D₁ * D₂ = δ ^ c • (D₁ ∘ D₂),

where D₁ ∘ D₂ = TauCeti.composeDiagram D₁ D₂ is the diagram read off by placing D₁ above D₂ and c = TauCeti.middleLoopCount D₁ D₂ is the number of closed loops left in the middle. It is a unital associative R-algebra with the identity diagram as unit and the diagrams as a basis, so it has rank (2 * k - 1)‼. Brauer introduced it because, for V = ℂⁿ with its standard symmetric form, B_k(n) acts on the tensor power V^{⊗k} with image the commutant of the orthogonal group, and with δ = -2l the same holds for the symplectic group on ℂ^{2l}. This file builds the algebra itself; its action on tensor powers is not constructed here.

All of the combinatorics is already available: stacking is associative (TauCeti.composeDiagram_assoc), the loop counts of the two bracketings of a triple stack agree (TauCeti.middleLoopCount_add_middleLoopCount_composeDiagram), and the identity diagram is a two-sided unit for stacking that closes no loop. Those are exactly the associativity and unit laws of the multiplication on the diagram basis, and bilinear extension does the rest.

The symmetric group sits inside: a permutation diagram closes no loop against anything, and stacking permutation diagrams multiplies the permutations (TauCeti.composeDiagram_permToBrauer), so σ ↦ permToBrauer σ extends to an injective algebra map from the group algebra of Sₖ (TauCeti.BrauerAlgebra.ofPerm). The cap-cup generators satisfy Brauer's relations e * e = δ • e, s * e = e = e * s and σ e_{a,b} σ⁻¹ = e_{σ a, σ b}.

Main definitions #

Main results #

Implementation notes #

TauCeti.BrauerAlgebra R δ k is a one-field structure around the coefficient function BrauerDiagram k →₀ R, as Mathlib's MonoidAlgebra is, rather than a type synonym: the loop value δ enters only the multiplication, and a structure keeps the loop-weighted product from being confused with the pointwise product that Finsupp already carries. The additive and module structures are transported from the coefficients along TauCeti.BrauerAlgebra.coeffEquiv.

The twisted monoid algebra TauCeti.twistedMonoidAlgebra does not apply: it twists a monoid by a factor set with values in the units of the base ring, whereas the weight δ ^ c of the loop rule is not a unit in general (it vanishes at δ = 0).

References #

source
structure TauCeti.BrauerAlgebra (R : Type u_1) [CommSemiring R] (δ : R) (k : ℕ) :
Type u_1

The Brauer algebra B_k(δ) on k strands with loop value δ over R: the free R-module on the Brauer diagrams on k strands, with the multiplication that stacks two diagrams and weights the result by δ to the number of closed loops left in the middle (TauCeti.BrauerAlgebra.of_mul_of). An element is given by its coefficients in the diagram basis.

  • ofCoeff :: (
    • coeff : BrauerDiagram k →₀ R

      The coefficients of an element of the Brauer algebra in the diagram basis.

  • )
Instances For
    source
    theorem TauCeti.BrauerAlgebra.ext {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} {x y : BrauerAlgebra R δ k} (h : x.coeff = y.coeff) :
    x = y

    Two elements of the Brauer algebra are equal when their coefficients are.

    source
    theorem TauCeti.BrauerAlgebra.ext_iff {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} {x y : BrauerAlgebra R δ k} :
    x = y ↔ x.coeff = y.coeff
    source
    @[simp]
    theorem TauCeti.BrauerAlgebra.coeff_ofCoeff {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (f : BrauerDiagram k →₀ R) :
    { coeff := f }.coeff = f
    source
    @[simp]
    theorem TauCeti.BrauerAlgebra.ofCoeff_coeff {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (x : BrauerAlgebra R δ k) :
    { coeff := x.coeff } = x
    source
    def TauCeti.BrauerAlgebra.coeffEquiv (R : Type u_1) [CommSemiring R] (δ : R) (k : ℕ) :
    BrauerAlgebra R δ k ≃ (BrauerDiagram k →₀ R)

    The coefficients in the diagram basis, as an equivalence.

    Instances For
      source
      @[instance_reducible]
      noncomputable instance TauCeti.BrauerAlgebra.instAddCommMonoid {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
      AddCommMonoid (BrauerAlgebra R δ k)
      source
      @[simp]
      theorem TauCeti.BrauerAlgebra.coeff_zero {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
      coeff 0 = 0
      source
      @[simp]
      theorem TauCeti.BrauerAlgebra.coeff_add {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (x y : BrauerAlgebra R δ k) :
      (x + y).coeff = x.coeff + y.coeff
      source
      noncomputable def TauCeti.BrauerAlgebra.coeffAddEquiv (R : Type u_1) [CommSemiring R] (δ : R) (k : ℕ) :
      BrauerAlgebra R δ k ≃+ (BrauerDiagram k →₀ R)

      The coefficients in the diagram basis, as an additive equivalence.

      Instances For
        source
        @[instance_reducible]
        noncomputable instance TauCeti.BrauerAlgebra.instModule {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
        Module R (BrauerAlgebra R δ k)
        source
        @[simp]
        theorem TauCeti.BrauerAlgebra.coeff_smul {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (r : R) (x : BrauerAlgebra R δ k) :
        (r • x).coeff = r • x.coeff
        source
        noncomputable def TauCeti.BrauerAlgebra.coeffLinearEquiv (R : Type u_1) [CommSemiring R] (δ : R) (k : ℕ) :
        BrauerAlgebra R δ k ≃ₗ[R] BrauerDiagram k →₀ R

        The coefficients in the diagram basis, as a linear equivalence.

        Instances For
          source
          @[simp]
          theorem TauCeti.BrauerAlgebra.coeffLinearEquiv_apply {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (x : BrauerAlgebra R δ k) :
          (coeffLinearEquiv R δ k) x = x.coeff
          source
          @[simp]
          theorem TauCeti.BrauerAlgebra.coeffLinearEquiv_symm_apply {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (f : BrauerDiagram k →₀ R) :
          (coeffLinearEquiv R δ k).symm f = { coeff := f }

          The multiplication #

          source
          noncomputable def TauCeti.BrauerAlgebra.mulCoeff {R : Type u_1} [CommSemiring R] (δ : R) {k : ℕ} :
          (BrauerDiagram k →₀ R) →ₗ[R] (BrauerDiagram k →₀ R) →ₗ[R] BrauerDiagram k →₀ R

          The loop-weighted stacking on coefficients, as a bilinear map: on basis vectors it sends (D₁, D₂) to δ ^ middleLoopCount D₁ D₂ times the basis vector of composeDiagram D₁ D₂.

          Instances For
            source
            theorem TauCeti.BrauerAlgebra.mulCoeff_single_single {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (D₁ D₂ : BrauerDiagram k) (a b : R) :
            ((mulCoeff δ) (Finsupp.single D₁ a)) (Finsupp.single D₂ b) = Finsupp.single (composeDiagram D₁ D₂) (δ ^ middleLoopCount D₁ D₂ * (a * b))

            The loop-weighted stacking of two basis vectors of coefficients.

            source
            theorem TauCeti.BrauerAlgebra.mulCoeff_assoc {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (f g h : BrauerDiagram k →₀ R) :
            ((mulCoeff δ) (((mulCoeff δ) f) g)) h = ((mulCoeff δ) f) (((mulCoeff δ) g) h)

            The loop-weighted stacking is associative: this is where the associativity of stacking (TauCeti.composeDiagram_assoc) and the agreement of the loop counts of the two bracketings (TauCeti.middleLoopCount_add_middleLoopCount_composeDiagram) enter.

            source
            theorem TauCeti.BrauerAlgebra.mulCoeff_one_left {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (f : BrauerDiagram k →₀ R) :
            ((mulCoeff δ) (Finsupp.single (permToBrauer 1) 1)) f = f

            The identity diagram is a left unit for the loop-weighted stacking.

            source
            theorem TauCeti.BrauerAlgebra.mulCoeff_one_right {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (f : BrauerDiagram k →₀ R) :
            ((mulCoeff δ) f) (Finsupp.single (permToBrauer 1) 1) = f

            The identity diagram is a right unit for the loop-weighted stacking.

            source
            @[instance_reducible]
            noncomputable instance TauCeti.BrauerAlgebra.instMul {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
            Mul (BrauerAlgebra R δ k)
            source
            theorem TauCeti.BrauerAlgebra.coeff_mul {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (x y : BrauerAlgebra R δ k) :
            (x * y).coeff = ((mulCoeff δ) x.coeff) y.coeff

            The coefficients of a product are the loop-weighted stacking of the coefficients.

            source
            @[instance_reducible]
            noncomputable instance TauCeti.BrauerAlgebra.instOne {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
            One (BrauerAlgebra R δ k)
            source
            theorem TauCeti.BrauerAlgebra.coeff_one {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
            coeff 1 = Finsupp.single (permToBrauer 1) 1

            The coefficients of the unit: the identity diagram, with coefficient 1.

            source
            @[instance_reducible]
            noncomputable instance TauCeti.BrauerAlgebra.instSemiring {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
            Semiring (BrauerAlgebra R δ k)
            source
            @[instance_reducible]
            noncomputable instance TauCeti.BrauerAlgebra.instAlgebra {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
            Algebra R (BrauerAlgebra R δ k)

            The ring structure over a commutative ring #

            source
            @[instance_reducible]
            noncomputable instance TauCeti.BrauerAlgebra.instAddCommGroup {R : Type u_2} [CommRing R] {δ : R} {k : ℕ} :
            AddCommGroup (BrauerAlgebra R δ k)
            source
            @[simp]
            theorem TauCeti.BrauerAlgebra.coeff_neg {R : Type u_2} [CommRing R] {δ : R} {k : ℕ} (x : BrauerAlgebra R δ k) :
            (-x).coeff = -x.coeff
            source
            @[simp]
            theorem TauCeti.BrauerAlgebra.coeff_sub {R : Type u_2} [CommRing R] {δ : R} {k : ℕ} (x y : BrauerAlgebra R δ k) :
            (x - y).coeff = x.coeff - y.coeff
            source
            @[instance_reducible]
            noncomputable instance TauCeti.BrauerAlgebra.instRing {R : Type u_2} [CommRing R] {δ : R} {k : ℕ} :
            Ring (BrauerAlgebra R δ k)

            The diagram basis #

            source
            noncomputable def TauCeti.BrauerAlgebra.of {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (D : BrauerDiagram k) :
            BrauerAlgebra R δ k

            The basis element of the Brauer algebra at the Brauer diagram D.

            Instances For
              source
              @[simp]
              theorem TauCeti.BrauerAlgebra.coeff_of {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (D : BrauerDiagram k) :
              (of D).coeff = Finsupp.single D 1
              source
              @[simp]
              theorem TauCeti.BrauerAlgebra.ofCoeff_single {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (D : BrauerDiagram k) (r : R) :
              { coeff := Finsupp.single D r } = r • of D

              An element with a single nonzero coefficient is a multiple of a basis element.

              source
              @[simp]
              theorem TauCeti.BrauerAlgebra.of_mul_of {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (D₁ D₂ : BrauerDiagram k) :
              of D₁ * of D₂ = δ ^ middleLoopCount D₁ D₂ • of (composeDiagram D₁ D₂)

              The loop rule. The product of two diagrams is their stack, weighted by δ to the number of closed loops left in the middle.

              source
              theorem TauCeti.BrauerAlgebra.of_mul_of_of_middleLoopCount_eq_zero {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} {D₁ D₂ : BrauerDiagram k} (h : middleLoopCount D₁ D₂ = 0) :
              of D₁ * of D₂ = of (composeDiagram D₁ D₂)

              A loop-free stack is a product: when stacking D₁ above D₂ closes up no loop, the product of the two diagrams is their composite, with no power of δ.

              source
              theorem TauCeti.BrauerAlgebra.one_def {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
              1 = of (permToBrauer 1)

              The unit of the Brauer algebra is the identity diagram.

              source
              noncomputable def TauCeti.BrauerAlgebra.basis (R : Type u_1) [CommSemiring R] (δ : R) (k : ℕ) :
              Module.Basis (BrauerDiagram k) R (BrauerAlgebra R δ k)

              The diagram basis of the Brauer algebra.

              Instances For
                source
                @[simp]
                theorem TauCeti.BrauerAlgebra.basis_apply {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (D : BrauerDiagram k) :
                (basis R δ k) D = of D
                source
                @[simp]
                theorem TauCeti.BrauerAlgebra.basis_repr {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (x : BrauerAlgebra R δ k) :
                (basis R δ k).repr x = x.coeff
                source
                instance TauCeti.BrauerAlgebra.instFree {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
                Module.Free R (BrauerAlgebra R δ k)
                source
                instance TauCeti.BrauerAlgebra.instFinite {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
                Module.Finite R (BrauerAlgebra R δ k)
                source
                theorem TauCeti.BrauerAlgebra.finrank_eq_doubleFactorial (R : Type u_1) [CommSemiring R] (δ : R) (k : ℕ) [StrongRankCondition R] :
                Module.finrank R (BrauerAlgebra R δ k) = (2 * k - 1).doubleFactorial

                The rank of the Brauer algebra: it is free on the (2 * k - 1)‼ Brauer diagrams on k strands.

                source
                theorem TauCeti.BrauerAlgebra.algHom_ext {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} {A : Type u_2} [Semiring A] [Algebra R A] {f g : BrauerAlgebra R δ k →ₐ[R] A} (h : ∀ (D : BrauerDiagram k), f (of D) = g (of D)) :
                f = g

                An algebra map out of the Brauer algebra is determined by its values on the diagrams.

                source
                theorem TauCeti.BrauerAlgebra.algHom_ext_iff {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} {A : Type u_2} [Semiring A] [Algebra R A] {f g : BrauerAlgebra R δ k →ₐ[R] A} :
                f = g ↔ ∀ (D : BrauerDiagram k), f (of D) = g (of D)
                source
                noncomputable def TauCeti.BrauerAlgebra.lift {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} {A : Type u_2} [Semiring A] [Algebra R A] (F : BrauerDiagram k → A) (h_one : F (permToBrauer 1) = 1) (h_mul : ∀ (D₁ D₂ : BrauerDiagram k), F D₁ * F D₂ = δ ^ middleLoopCount D₁ D₂ • F (composeDiagram D₁ D₂)) :
                BrauerAlgebra R δ k →ₐ[R] A

                Maps out of the Brauer algebra. An assignment of elements of an R-algebra to the diagrams that sends the identity diagram to 1 and obeys the loop rule extends to an algebra map.

                Instances For
                  source
                  @[simp]
                  theorem TauCeti.BrauerAlgebra.lift_of {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} {A : Type u_2} [Semiring A] [Algebra R A] (F : BrauerDiagram k → A) (h_one : F (permToBrauer 1) = 1) (h_mul : ∀ (D₁ D₂ : BrauerDiagram k), F D₁ * F D₂ = δ ^ middleLoopCount D₁ D₂ • F (composeDiagram D₁ D₂)) (D : BrauerDiagram k) :
                  (lift F h_one h_mul) (of D) = F D
                  source
                  theorem TauCeti.BrauerAlgebra.eq_lift {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} {A : Type u_2} [Semiring A] [Algebra R A] (F : BrauerDiagram k → A) (h_one : F (permToBrauer 1) = 1) (h_mul : ∀ (D₁ D₂ : BrauerDiagram k), F D₁ * F D₂ = δ ^ middleLoopCount D₁ D₂ • F (composeDiagram D₁ D₂)) {f : BrauerAlgebra R δ k →ₐ[R] A} (h : ∀ (D : BrauerDiagram k), f (of D) = F D) :
                  f = lift F h_one h_mul

                  An algebra map out of the Brauer algebra is the lift of its values on the diagrams.

                  The symmetric group inside the Brauer algebra #

                  source
                  theorem TauCeti.BrauerAlgebra.of_permToBrauer_mul_of_permToBrauer {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (σ τ : Equiv.Perm (Fin k)) :
                  of (permToBrauer σ) * of (permToBrauer τ) = of (permToBrauer (σ * τ))

                  A permutation diagram closes no loop, so the permutation diagrams multiply as the permutations do.

                  source
                  noncomputable def TauCeti.BrauerAlgebra.ofPerm (R : Type u_1) [CommSemiring R] (δ : R) (k : ℕ) :
                  MonoidAlgebra R (Equiv.Perm (Fin k)) →ₐ[R] BrauerAlgebra R δ k

                  The group algebra of Sₖ inside the Brauer algebra: the algebra map sending a permutation to its diagram.

                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.BrauerAlgebra.ofPerm_single {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (σ : Equiv.Perm (Fin k)) (r : R) :
                    (ofPerm R δ k) (MonoidAlgebra.single σ r) = r • of (permToBrauer σ)
                    source
                    theorem TauCeti.BrauerAlgebra.coeff_ofPerm {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (x : MonoidAlgebra R (Equiv.Perm (Fin k))) :
                    ((ofPerm R δ k) x).coeff = Finsupp.mapDomain permToBrauer x.coeff

                    The coefficients of the image of an element of the group algebra are its coefficients moved along permToBrauer.

                    source
                    theorem TauCeti.BrauerAlgebra.ofPerm_injective {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} :
                    Function.Injective ⇑(ofPerm R δ k)

                    The group algebra of Sₖ embeds in the Brauer algebra, because distinct permutations have distinct diagrams.

                    Brauer's relations for the cap-cup generators #

                    source
                    theorem TauCeti.BrauerAlgebra.of_capCup_mul_of_capCup {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} {a b : Fin k} (hab : a ≠ b) :
                    of (capCup a b) * of (capCup a b) = δ • of (capCup a b)

                    e * e = δ • e: stacking a cap-cup diagram on itself closes exactly one loop.

                    source
                    theorem TauCeti.BrauerAlgebra.of_permToBrauer_swap_mul_of_capCup {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (a b : Fin k) :
                    of (permToBrauer (Equiv.swap a b)) * of (capCup a b) = of (capCup a b)

                    s * e = e: the transposition of the pair of a cap-cup diagram, stacked above it, is absorbed.

                    source
                    theorem TauCeti.BrauerAlgebra.of_capCup_mul_of_permToBrauer_swap {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (a b : Fin k) :
                    of (capCup a b) * of (permToBrauer (Equiv.swap a b)) = of (capCup a b)

                    e * s = e: the transposition of the pair of a cap-cup diagram, stacked below it, is absorbed.

                    source
                    theorem TauCeti.BrauerAlgebra.of_permToBrauer_mul_of_capCup_mul_of_permToBrauer_inv {R : Type u_1} [CommSemiring R] {δ : R} {k : ℕ} (a b : Fin k) (σ : Equiv.Perm (Fin k)) :
                    of (permToBrauer σ) * of (capCup a b) * of (permToBrauer σ⁻¹) = of (capCup (σ a) (σ b))

                    The mixed permutation/generator relation σ e_{a,b} σ⁻¹ = e_{σ a, σ b}: conjugating a cap-cup diagram by a permutation diagram renames its pair.