Documentation

TauCeti.RepresentationTheory.ClassicalGroups.BrauerGenerators.Symplectic.TensorPower

The symplectic Brauer arc on a tensor power #

A Brauer diagram on d strands acts on the d-th tensor power of V = k^{2n} by permuting the slots along its through strands, contracting each pair of bottom points against the invariant alternating form, and expanding each pair of top points through the inverse copairing. The horizontal arcs are therefore all built from the single-arc diagrams: a cap on the two bottom points i and j, closed off by a cup on the two top points i and j. This file builds that operator, TauCeti.symplecticCupCapAt, on the d-th tensor power of the symplectic standard module, and proves what an action of the Brauer algebra must respect of it among arcs alone: the loop rule, the commutation of arcs on disjoint pairs of strands, and the commutation with the diagonal action of the symplectic group.

The two-strand case is TauCeti.symplecticCupCap of TauCeti/RepresentationTheory/ClassicalGroups/BrauerGenerators/Symplectic/Basic.lean, which this file reproduces at d = 2 (TauCeti.symplecticCupCapAt_zero_one). There the generator is assembled as a composite cup ∘ₗ cap through the tensor square, a route unavailable for two strands sitting inside a larger tensor power, because splitting two of the d slots off a tensor power is not an equality of tensor powers. The operator here is instead built in one step, by pushing the a-th coordinate followed by the x-th basis vector through the strand i, the b-th coordinate followed by the y-th basis vector through the strand j, and the identity through all the others, weighted by J a b for the cap and -J x y for the cup and summed over all four indices.

The arc is an unordered pair of strands #

The cap and the cup are each antisymmetric: exchanging their two endpoints changes the sign, because the standard symplectic form is alternating (TauCeti.symplecticCap_comp_symplecticFlip and TauCeti.symplecticFlip_comp_symplecticCup). On a single arc the two sign changes cancel, so the generator e i j built here is unchanged by exchanging i and j (TauCeti.symplecticCupCapAt_comm), exactly as in the orthogonal case: an arc carries no orientation and is the unordered pair of the two strands it joins. What the antisymmetry does force instead is the sign on the crossing, which is minus the flip of the two slots (TauCeti.symplecticCrossing on two strands), and the negative loop value below.

The relations #

Writing e i j for the generator, the relations proved here are

The relations involving a crossing are not stated here: the Brauer crossing on two of d strands is the sign-twisted transposition of those two slots, and the sign-twisted action of the symmetric group on V^{⊗d} and its relations with the arcs are in TauCeti/RepresentationTheory/ClassicalGroups/BrauerGenerators/Symplectic/Crossing.lean. So is the absorption e i j * e j l * e i j = e i j of two arcs sharing a strand, which follows from them.

Implementation notes #

The cap and the cup are read through the entries of Matrix.J rather than through a partner involution of the index type Fin n ⊕ Fin n, matching TauCeti/RepresentationTheory/ClassicalGroups/BrauerGenerators/Symplectic/Basic.lean: the definition is then a fourfold sum, and the cap half of it is the double sum that Matrix.toBilin' already is.

At i = j the two strands coincide. The first branch of TauCeti.symplecticCupCapStrand then wins, the second plug of the definition is dead, and the operator is not an arc of a Brauer diagram but the rank-one map of TauCeti.symplecticCupCapAt_self_tprod: the slot i is paired with the all-ones vector and replaced by the row sums of J. Every statement that reads an arc through the form therefore carries the hypothesis i ≠ j; TauCeti.symplecticCupCapAt_comm and TauCeti.commute_symplecticCupCapAt_of_disjoint, which are strandwise statements, hold for coincident strands too.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.symplecticCupCapAt (k : Type u) (n d : ℕ) [CommRing k] (i j : Fin d) :
Module.End k (TensorPower k d (Fin n ⊕ Fin n → k))

The symplectic Brauer generator e on the strands i and j of the d-th tensor power of k^{2n}: a cap contracting the slots i and j against the standard alternating form, closed off by a cup re-expanding those two slots through the inverse copairing, the bivector of -J.

The cap contributes the weight J a b to the pair of coordinates it reads off the two slots, and the cup the weight -J x y to the pair of basis vectors it writes back into them. At i = j the two strands coincide and the result is not an arc of a Brauer diagram (TauCeti.symplecticCupCapAt_self_tprod); see the module docstring.

Instances For

    The value on a pure tensor #

    source
    @[simp]
    theorem TauCeti.symplecticCupCapAt_tprod {k : Type u} {n d : ℕ} [CommRing k] {i j : Fin d} (hij : i ≠ j) (v : Fin d → Fin n ⊕ Fin n → k) :
    (symplecticCupCapAt k n d i j) ((PiTensorProduct.tprod k) v) = ((stdSymplecticBilinForm k n) (v i)) (v j) • -∑ x : Fin n ⊕ Fin n, ∑ y : Fin n ⊕ Fin n, Matrix.J (Fin n) k x y • (PiTensorProduct.tprod k) (Function.update (Function.update v i (Pi.single x 1)) j (Pi.single y 1))

    The generator on a pure tensor: the two chosen factors are contracted against one another by the standard alternating form, and the two slots are re-expanded through the cup.

    source
    theorem TauCeti.symplecticCupCapAt_tprod_single {k : Type u} {n d : ℕ} [CommRing k] {i j : Fin d} (hij : i ≠ j) (f : Fin d → Fin n ⊕ Fin n) :
    (symplecticCupCapAt k n d i j) ((PiTensorProduct.tprod k) fun (t : Fin d) => Pi.single (f t) 1) = -(Matrix.J (Fin n) k (f i) (f j) • ∑ x : Fin n ⊕ Fin n, ∑ y : Fin n ⊕ Fin n, Matrix.J (Fin n) k x y • (PiTensorProduct.tprod k) fun (t : Fin d) => Pi.single (Function.update (Function.update f i x) j y t) 1)

    The generator on a monomial tensor of standard basis vectors, at distinct strands: the entry of J at the two labels, times the cup re-expanding the two slots as standard basis vectors.

    source
    @[simp]
    theorem TauCeti.symplecticCupCapAt_self_tprod {k : Type u} {n d : ℕ} [CommRing k] (i : Fin d) (v : Fin d → Fin n ⊕ Fin n → k) :
    (symplecticCupCapAt k n d i i) ((PiTensorProduct.tprod k) v) = ((stdSymplecticBilinForm k n) (v i)) 1 • -∑ x : Fin n ⊕ Fin n, ∑ y : Fin n ⊕ Fin n, Matrix.J (Fin n) k x y • (PiTensorProduct.tprod k) (Function.update v i (Pi.single x 1))

    The degenerate value at coincident strands: at i = j the cap and the cup land on the same slot, and the second plug of TauCeti.symplecticCupCapAt is dead. The operator is then not the contraction of that slot against itself -- which would be quadratic in v i, not linear -- but the rank-one map pairing the slot with the all-ones vector and refilling it with the row sums of J. This is why the relations that read the arc through the form assume i ≠ j.

    The matrix of an arc #

    source
    theorem TauCeti.piTensorProduct_repr_symplecticCupCapAt_piTensorProduct {k : Type u} {n d : ℕ} [CommRing k] {i j : Fin d} (hij : i ≠ j) (u w : Fin d → Fin n ⊕ Fin n) :
    ((Basis.piTensorProduct fun (x : Fin d) => Pi.basisFun k (Fin n ⊕ Fin n)).repr ((symplecticCupCapAt k n d i j) ((Basis.piTensorProduct fun (x : Fin d) => Pi.basisFun k (Fin n ⊕ Fin n)) u))) w = if ∀ (t : Fin d), t ≠ i → t ≠ j → w t = u t then -(Matrix.J (Fin n) k (u i) (u j) * Matrix.J (Fin n) k (w i) (w j)) else 0

    The matrix coefficients of an arc in the monomial basis: the coefficient of e_w in the image of e_u is -(J (u i) (u j) * J (w i) (w j)) when w agrees with u off the two strands, and 0 otherwise. The cap reads J off the two input labels and the cup writes -J at the two output labels.

    source
    theorem TauCeti.isHermitian_toMatrix_symplecticCupCapAt {k : Type u} {n d : ℕ} [CommRing k] [StarRing k] {i j : Fin d} (hij : i ≠ j) :
    ((LinearMap.toMatrix (Basis.piTensorProduct fun (x : Fin d) => Pi.basisFun k (Fin n ⊕ Fin n)) (Basis.piTensorProduct fun (x : Fin d) => Pi.basisFun k (Fin n ⊕ Fin n))) (symplecticCupCapAt k n d i j)).IsHermitian

    The matrix of an arc in the monomial basis is Hermitian, for every star structure on k: it is symmetric, by TauCeti.piTensorProduct_repr_symplecticCupCapAt_piTensorProduct, and its entries are integers, which star fixes. So an arc is self-adjoint for the Hermitian form in which the monomial basis is orthonormal.

    The orientation of the arc #

    source
    theorem TauCeti.symplecticCupCapAt_comm {k : Type u} {n d : ℕ} [CommRing k] (i j : Fin d) :
    symplecticCupCapAt k n d i j = symplecticCupCapAt k n d j i

    The generator depends only on the unordered pair of strands. Exchanging the two endpoints of the arc changes the sign of the cap and the sign of the cup, and the two changes cancel, so an arc of a diagram carries no orientation. The sign the alternating form does force is the one on the crossing, not one on an arc.

    Two strands #

    source
    theorem TauCeti.symplecticCupCapAt_zero_one {k : Type u} {n : ℕ} [CommRing k] :
    symplecticCupCapAt k n 2 0 1 = symplecticCupCap k n

    On two strands the generator is the two-strand one: the operator built here at d = 2 and the arc 0, 1 is the composite cup ∘ₗ cap of TauCeti/RepresentationTheory/ClassicalGroups/BrauerGenerators/Symplectic/Basic.lean.

    The loop rule #

    source
    @[simp]
    theorem TauCeti.symplecticCupCapAt_mul_self {k : Type u} {n d : ℕ} [CommRing k] {i j : Fin d} (hij : i ≠ j) :
    symplecticCupCapAt k n d i j * symplecticCupCapAt k n d i j = -(2 * ↑n) • symplecticCupCapAt k n d i j

    The loop rule e² = δ e at the symplectic loop value δ = -2n = -dim V: a cup stacked under a cap closes into a loop, which contracts the pairing J against the copairing -J.

    Two arcs #

    source
    theorem TauCeti.commute_symplecticCupCapAt_of_disjoint {k : Type u} {n d : ℕ} [CommRing k] {i j p q : Fin d} (hip : i ≠ p) (hiq : i ≠ q) (hjp : j ≠ p) (hjq : j ≠ q) :
    Commute (symplecticCupCapAt k n d i j) (symplecticCupCapAt k n d p q)

    Disjoint arcs commute: two generators whose pairs of strands are disjoint act in disjoint groups of slots. The two strands of either pair may coincide, since the proof never reads an arc through the form: it only needs each strand to be touched by at most one of the two generators.

    The arc as an intertwiner #

    source
    theorem TauCeti.commute_symplecticCupCapAt_piTensorProductMap {k : Type u} {n d : ℕ} [CommRing k] {A : Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) k} (hA : A.transpose * Matrix.J (Fin n) k * A = Matrix.J (Fin n) k) {i j : Fin d} (hij : i ≠ j) :
    Commute (symplecticCupCapAt k n d i j) (PiTensorProduct.map fun (x : Fin d) => A.mulVecLin)

    The generator commutes with the diagonal action of a symplectic matrix: the cap consumes Aᵀ * J * A = J, which is exactly preservation of the standard alternating form, and the cup the other one-sided identity A * J * Aᵀ = J, which SymplecticGroup.mem_iff derives from it.

    source
    theorem TauCeti.commute_symplecticCupCapAt_tensorPower {k : Type u} {n d : ℕ} [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) {i j : Fin d} (hij : i ≠ j) :
    Commute (symplecticCupCapAt k n d i j) (((stdSymplecticRep k n).tensorPower d) g)

    The symplectic Brauer arc commutes with the symplectic group. Membership in Matrix.symplecticGroup supplies preservation of the standard alternating form, so every single-arc diagram acts on the tensor power by an intertwiner of the diagonal symplectic action.