Documentation

TauCeti.RepresentationTheory.ClassicalGroups.BrauerGenerators.Orthogonal.TensorPower

The Brauer generators on a tensor power, and the relations they satisfy #

A Brauer diagram on d strands acts on the d-th tensor power of V = kⁿ by permuting the slots along its through strands, contracting each pair of bottom points against the coordinate dot product, and expanding each pair of top points through the dual 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 on the d-th tensor power, TauCeti.orthogonalCupCapAt, and proves the relations it satisfies, which is what an algebra homomorphism out of the Brauer algebra has to check.

The two-strand case is TauCeti.orthogonalCupCap of TauCeti/RepresentationTheory/ClassicalGroups/BrauerGenerators/Orthogonal/Basic.lean, which this file reproduces at d = 2 (TauCeti.orthogonalCupCapAt_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 c-th basis vector through the two chosen strands and the identity through all the others, and summing over a and c: the sum over a is the cap, which contracts the two slots coordinatewise, and the sum over c is the cup, which re-expands them diagonally.

The relations #

Writing e i j for the generator and s σ for the permutation action TauCeti.permTensorAction of the symmetric group on the tensor factors, the relations proved here are

Together with s being a monoid homomorphism — which already gives s σ * s τ = s (σ * τ), hence s² = 1 for a transposition and the braid relations — these are the defining relations of the Brauer algebra B_d(n), and the renaming relation specializes to the mixed relation s σ * e i j = e i j * s σ whenever σ fixes both i and j (TauCeti.commute_permTensorAction_orthogonalCupCapAt). They are the tensor-power mirror of the diagram-level relations of TauCeti/Combinatorics/Brauer/Generator.lean and TauCeti/Combinatorics/Brauer/Relations.lean, which prove the same identities for the stacking of Brauer diagrams and its middle-loop count.

The generator and all five relations need no subtraction and no inverses, so they are stated over a commutative semiring; only the orthogonal group itself, and hence the closing commutation theorem, needs a commutative ring. Everything here is the symmetric (orthogonal) form: the arc is an unordered pair of strands (TauCeti.orthogonalCupCapAt_comm), which is exactly what fails for an alternating form, so the symplectic mirror is not a relabelling of this file but needs a chosen ordering of each arc.

Implementation notes #

Every proof here reduces to the same piece of plumbing: the tuple obtained from v by setting the two slots i and j to the c-th standard basis vector of kⁿ, spelled as a pair of nested Function.updates. The four update_pair_* lemmas read its three kinds of entry and compose two such plugs; they are private because they are steps of this file's argument, specific to the shape the cup produces, and say nothing about tensor powers. The one genuinely linear-algebraic step is the expansion of those two slots in the standard basis, which the invariance of the cup runs on; it is general infrastructure and lives in TauCeti/LinearAlgebra/PiTensorProduct/BasisExpansion.lean as TauCeti.tprod_update_pair_expand.

Each summand of the generator is a PiTensorProduct.map, so the relations that do not read the arc through the dot product are strandwise statements about the family TauCeti.cupCapStrand: PiTensorProduct.map_comp turns a product of two summands into the summand of the pointwise composite, and the commutation of two arcs on disjoint pairs of strands is then the observation that at every strand one of the two factors is the identity.

Main definitions #

Main results #

References #

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

The Brauer generator e on the strands i and j of the d-th tensor power of kⁿ: a cap contracting the slots i and j against the coordinate dot product, closed off by a cup re-expanding those two slots as ∑_c e_c ⊗ e_c.

At i = j the two strands coincide, so the cap and the cup land on the same slot and the result is not an arc of a Brauer diagram: it is not a contraction of the slot i against itself, which would be quadratic rather than linear, but the rank-one map replacing that slot by the sum of its coordinates times the all-ones vector (TauCeti.orthogonalCupCapAt_self_tprod). The relations that read the arc through the dot product therefore carry the hypothesis i ≠ j; the ones that are strandwise statements — TauCeti.permTensorAction_mul_orthogonalCupCapAt, the two absorptions of the crossing, and the commutation of two generators on disjoint pairs of strands TauCeti.commute_orthogonalCupCapAt_of_disjoint — hold for coincident strands too.

Equations
Instances For

    The value on a pure tensor #

    source
    @[simp]
    theorem TauCeti.orthogonalCupCapAt_tprod {k : Type u} {n d : ℕ} [CommSemiring k] {i j : Fin d} (hij : i ≠ j) (v : Fin d → Fin n → k) :
    (orthogonalCupCapAt k n d i j) ((PiTensorProduct.tprod k) v) = (v i ⬝ᵥ v j) • ∑ c : Fin n, (PiTensorProduct.tprod k) (Function.update (Function.update v i (Pi.single c 1)) j (Pi.single c 1))

    The generator on a pure tensor: the two chosen factors are contracted against one another by the dot product, and both slots are replaced by the c-th standard basis vector, summed over c. Every relation below but the renaming one is proved from this formula; renaming is bookkeeping on the index set and is read off the definition.

    source
    @[simp]
    theorem TauCeti.orthogonalCupCapAt_self_tprod {k : Type u} {n d : ℕ} [CommSemiring k] (i : Fin d) (v : Fin d → Fin n → k) :
    (orthogonalCupCapAt k n d i i) ((PiTensorProduct.tprod k) v) = (∑ a : Fin n, v i a) • ∑ c : Fin n, (PiTensorProduct.tprod k) (Function.update v i (Pi.single c 1))

    The degenerate value at coincident strands: at i = j the cap and the cup land on the same slot, and TauCeti.orthogonalCupCapAt k n d i i is not the contraction of that slot against itself — which would be quadratic in v i, not linear — but the rank-one map replacing it by (∑ a, v i a) • 1. This is why the relations that read the arc through the dot product assume i ≠ j.

    source
    theorem TauCeti.orthogonalCupCapAt_comm {k : Type u} {n d : ℕ} [CommSemiring k] (i j : Fin d) :
    orthogonalCupCapAt k n d i j = orthogonalCupCapAt k n d j i

    The generator depends only on the unordered pair of strands: the arc joining i to j is the arc joining j to i.

    The loop rule #

    source
    @[simp]
    theorem TauCeti.orthogonalCupCapAt_mul_self {k : Type u} {n d : ℕ} [CommSemiring k] {i j : Fin d} (hij : i ≠ j) :
    orthogonalCupCapAt k n d i j * orthogonalCupCapAt k n d i j = ↑n • orthogonalCupCapAt k n d i j

    The loop rule e² = δ e at the loop value δ = n = dim V: stacking the arc on itself closes a loop in the middle, and a closed loop evaluates to the trace n of the dot product.

    The crossing on the arc, and the renaming of the arc #

    source
    theorem TauCeti.permTensorAction_swap_mul_orthogonalCupCapAt {k : Type u} {n d : ℕ} [CommSemiring k] (i j : Fin d) :
    (permTensorAction k n d) (Equiv.swap i j) * orthogonalCupCapAt k n d i j = orthogonalCupCapAt k n d i j

    The relation s e = e: the crossing of the two strands of the arc is absorbed by the cup on top of the generator.

    source
    theorem TauCeti.orthogonalCupCapAt_mul_permTensorAction_swap {k : Type u} {n d : ℕ} [CommSemiring k] (i j : Fin d) :
    orthogonalCupCapAt k n d i j * (permTensorAction k n d) (Equiv.swap i j) = orthogonalCupCapAt k n d i j

    The relation e s = e: the crossing of the two strands of the arc is absorbed by the cap at the bottom of the generator, the dot product being symmetric.

    source
    theorem TauCeti.permTensorAction_mul_orthogonalCupCapAt {k : Type u} {n d : ℕ} [CommSemiring k] (σ : Equiv.Perm (Fin d)) (i j : Fin d) :
    (permTensorAction k n d) σ * orthogonalCupCapAt k n d i j = orthogonalCupCapAt k n d (σ i) (σ j) * (permTensorAction k n d) σ

    The renaming relation: permuting the strands renames the arc. Every mixed relation between a crossing and a generator is an instance of this one. Renaming is bookkeeping on the index set and does not read the arc through the dot product, so it needs no hypothesis on i and j: at coincident strands it renames the rank-one operator of TauCeti.orthogonalCupCapAt_self_tprod instead.

    source
    theorem TauCeti.commute_permTensorAction_orthogonalCupCapAt {k : Type u} {n d : ℕ} [CommSemiring k] {σ : Equiv.Perm (Fin d)} {i j : Fin d} (hi : σ i = i) (hj : σ j = j) :
    Commute ((permTensorAction k n d) σ) (orthogonalCupCapAt k n d i j)

    A permutation fixing both strands of the arc commutes with the generator: the mixed relation between a distant crossing and a generator.

    Two arcs #

    source
    theorem TauCeti.commute_orthogonalCupCapAt_of_disjoint {k : Type u} {n d : ℕ} [CommSemiring k] {i j a b : Fin d} (hia : i ≠ a) (hib : i ≠ b) (hja : j ≠ a) (hjb : j ≠ b) :
    Commute (orthogonalCupCapAt k n d i j) (orthogonalCupCapAt k n d a b)

    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 dot product: it only needs each strand to be touched by at most one of the two generators.

    source
    theorem TauCeti.orthogonalCupCapAt_mul_mul_self {k : Type u} {n d : ℕ} [CommSemiring k] {i j l : Fin d} (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) :
    orthogonalCupCapAt k n d i j * orthogonalCupCapAt k n d j l * orthogonalCupCapAt k n d i j = orthogonalCupCapAt k n d i j

    Two arcs sharing one strand: e i j * e j l * e i j = e i j, the relation that makes two generators on overlapping pairs absorb one another.

    The arc as an intertwiner #

    source
    theorem TauCeti.commute_orthogonalCupCapAt_piTensorProductMap {k : Type u} {n d : ℕ} [CommSemiring k] {A : Matrix (Fin n) (Fin n) k} (hA : A.transpose * A = 1) (hA' : A * A.transpose = 1) {i j : Fin d} (hij : i ≠ j) :
    Commute (orthogonalCupCapAt k n d i j) (PiTensorProduct.map fun (x : Fin d) => A.mulVecLin)

    The generator commutes with the diagonal action of a two-sidedly orthogonal matrix: the cap consumes Aᵀ * A = 1, which is exactly preservation of the coordinate dot product, and the cup consumes A * Aᵀ = 1, the orthonormality of the rows. Over a commutative semiring there is nothing deriving the second identity from the first, so both are hypotheses; a matrix in Matrix.orthogonalGroup satisfies both (Matrix.mem_orthogonalGroup_iff and Matrix.mem_orthogonalGroup_iff'), which is how TauCeti.commute_orthogonalCupCapAt_tensorPower discharges them.

    source
    theorem TauCeti.orthogonalCupCapAt_zero_one {k : Type u} {n : ℕ} [CommSemiring k] :
    orthogonalCupCapAt k n 2 0 1 = orthogonalCupCap k n

    On two strands the generator is TauCeti.orthogonalCupCap, the composite cup ∘ₗ cap through the tensor square.

    source
    theorem TauCeti.commute_orthogonalCupCapAt_tensorPower (k : Type u) (n d : ℕ) [CommRing k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) {i j : Fin d} (hij : i ≠ j) :
    Commute (orthogonalCupCapAt k n d i j) (((stdOrthogonalRep k n).tensorPower d) g)

    Every single-arc Brauer diagram acts by an intertwiner: the generator commutes with the diagonal action of the orthogonal group on the d-th tensor power, membership in the group supplying both orthogonality identities that TauCeti.commute_orthogonalCupCapAt_piTensorProductMap asks for. The two-strand case is TauCeti.commute_orthogonalCupCap_tensorPower.