The cap, the cup, and the Brauer relations on the tensor square

The orthogonal group acts on V = kⁿ preserving the coordinate dot product, and the dot product is a map V ⊗ V → k: read as a diagram it is a cap, an arc joining the two bottom points. The dual copairing k → V ⊗ V, the cup 1 ↦ ∑ⱼ eⱼ ⊗ eⱼ, is the same arc drawn at the top. It is the coordinate form read backwards rather than an inverse of the cap: the two have different sources and targets, and the composite cap ∘ cup is multiplication by n, not the identity. Composing a cap with a cup gives the diagram e on two strands, and permuting the two tensor factors gives the crossing s. Together with the identity these are the three Brauer diagrams on two strands, and this file proves the three relations they satisfy on V^{⊗2},

s * s = 1, e * e = δ • e, s * e = e * s = e, with the loop value δ = n = dim V,

together with the invariance of the cap and the cup under the orthogonal group, from which e commutes with the diagonal orthogonal action. The loop value is where the dimension enters: a closed loop, a cup stacked under a cap, evaluates to the trace n of the dot product.

The cap, the cup and the relations need no subtraction, so they are stated over a commutative semiring, as are the two invariance statements for a bare matrix; only the orthogonal group itself, and hence the last three results, needs a commutative ring.

The two invariance statements are recorded for a bare matrix rather than only for an element of Matrix.orthogonalGroup (Fin n) k, because they consume the defining identity from opposite sides: the cap is preserved by every A with Aᵀ * A = 1, and the cup by every A with A * Aᵀ = 1. The two conditions are equivalent, and Mathlib's orthogonal group records both, but which side a proof uses is the visible difference between contracting a pair of inputs and expanding a pair of outputs.

The crossing is not given a name of its own: it is the Layer 8 permutation action TauCeti.permTensorAction k n 2 (Equiv.swap 0 1) of the transposition, which is exactly the statement that the symmetric group sits inside the Brauer algebra as the diagrams with no arc.

Main definitions

• TauCeti.orthogonalCap: the cap V ⊗ V → k, the coordinate dot product.
• TauCeti.orthogonalCup: the cup k → V ⊗ V, 1 ↦ ∑ⱼ eⱼ ⊗ eⱼ.
• TauCeti.orthogonalCupCap: the Brauer generator e, the composite cup ∘ₗ cap of a cap on the two inputs with a cup on the two outputs.

Main results

• TauCeti.orthogonalCap_comp_orthogonalCup: the loop value, cap ∘ cup = n.
• TauCeti.orthogonalCupCap_mul_self: e * e = n • e.
• TauCeti.permTensorAction_swap_mul_orthogonalCupCap and TauCeti.orthogonalCupCap_mul_permTensorAction_swap: s * e = e and e * s = e.
• TauCeti.permTensorAction_swap_mul_self: s * s = 1.
• TauCeti.orthogonalCap_comp_piTensorProductMap and TauCeti.piTensorProductMap_comp_orthogonalCup: the cap and the cup are invariant.
• TauCeti.commute_orthogonalCupCap_tensorPower: the generator e commutes with the diagonal action of the orthogonal group. The corresponding statement for the crossing s is the restriction along TauCeti.orthogonalGroupToGL of the general-linear commute_permTensorAction_tensorPowerRep, in TauCeti.RepresentationTheory.ClassicalGroups.TensorPower.

References

• R. Brauer, On algebras which are connected with the semisimple continuous groups, Annals of Mathematics 38 (1937), 857-872.
• R. Goodman and N. R. Wallach, Symmetry, Representations, and Invariants, Springer GTM 255 (2009), Chapter 9.
• Schur--Weyl roadmap, Layer 9, "The invariant form and the action on V^{⊗k}", and the worked example "Brauer duality on (ℂ³)^{⊗2} for O(3)".

noncomputable def TauCeti.orthogonalCap (k : Type u) (n : ℕ) [CommSemiring k] : TensorPower k 2 (Fin n → k) →ₗ[k] k

The cap: the coordinate dot product, read as a linear map on the tensor square. It is the invariant symmetric form of the orthogonal group, drawn as an arc joining the two bottom points of a Brauer diagram.

Equations

• TauCeti.orthogonalCap k n = PiTensorProduct.lift (TauCeti.orthogonalCapMultilinear✝ k n)

@[simp]

theorem TauCeti.orthogonalCap_tprod (k : Type u) (n : ℕ) [CommSemiring k] (v : Fin 2 → Fin n → k) : (orthogonalCap k n) ((PiTensorProduct.tprod k) v) = v 0 ⬝ᵥ v 1

noncomputable def TauCeti.orthogonalCup (k : Type u) (n : ℕ) [CommSemiring k] : k →ₗ[k] TensorPower k 2 (Fin n → k)

The cup: the copairing 1 ↦ ∑ⱼ eⱼ ⊗ eⱼ dual to the cap, drawn as an arc joining the two top points of a Brauer diagram. It is not an inverse of the cap — the two have different sources and targets, and TauCeti.orthogonalCap_comp_orthogonalCup computes their composite to be multiplication by n.

Equations

• TauCeti.orthogonalCup k n = LinearMap.toSpanSingleton k (TensorPower k 2 (Fin n → k)) (∑ j : Fin n, (PiTensorProduct.tprod k) fun (x : Fin 2) => Pi.single j 1)

@[simp]

theorem TauCeti.orthogonalCup_apply (k : Type u) (n : ℕ) [CommSemiring k] (c : k) : (orthogonalCup k n) c = c • ∑ j : Fin n, (PiTensorProduct.tprod k) fun (x : Fin 2) => Pi.single j 1

theorem TauCeti.orthogonalCup_apply_one (k : Type u) (n : ℕ) [CommSemiring k] : (orthogonalCup k n) 1 = ∑ j : Fin n, (PiTensorProduct.tprod k) fun (x : Fin 2) => Pi.single j 1

theorem TauCeti.orthogonalCap_comp_orthogonalCup_apply (k : Type u) (n : ℕ) [CommSemiring k] (c : k) : (orthogonalCap k n) ((orthogonalCup k n) c) = ↑n * c

The loop value. A cup stacked under a cap closes into a loop, and the loop evaluates to the trace n of the coordinate dot product.

theorem TauCeti.orthogonalCap_comp_orthogonalCup (k : Type u) (n : ℕ) [CommSemiring k] : orthogonalCap k n ∘ₗ orthogonalCup k n = ↑n • LinearMap.id

The loop value, as an identity of linear maps: cap ∘ cup is multiplication by n.

noncomputable def TauCeti.orthogonalCupCap (k : Type u) (n : ℕ) [CommSemiring k] : Module.End k (TensorPower k 2 (Fin n → k))

The Brauer generator e on two strands: a cap on the two inputs followed by a cup on the two outputs. The name follows the written order of the composite cup ∘ₗ cap, as in TauCeti.orthogonalCap_comp_orthogonalCup for the loop.

Equations

• TauCeti.orthogonalCupCap k n = TauCeti.orthogonalCup k n ∘ₗ TauCeti.orthogonalCap k n

@[simp]

theorem TauCeti.orthogonalCupCap_apply (k : Type u) (n : ℕ) [CommSemiring k] (x : TensorPower k 2 (Fin n → k)) : (orthogonalCupCap k n) x = (orthogonalCup k n) ((orthogonalCap k n) x)

@[simp]

theorem TauCeti.orthogonalCupCap_mul_self (k : Type u) (n : ℕ) [CommSemiring k] : orthogonalCupCap k n * orthogonalCupCap k n = ↑n • orthogonalCupCap k n

The relation e² = δ e at the loop value δ = n: the middle of e * e is a closed loop.

theorem TauCeti.permTensorAction_swap_mul_self (k : Type u) (n : ℕ) [CommSemiring k] : (permTensorAction k n 2) (Equiv.swap 0 1) * (permTensorAction k n 2) (Equiv.swap 0 1) = 1

The relation s² = 1: the crossing is an involution.

This and the two absorption relations below are deliberately not simp lemmas: the existing TauCeti.permTensorAction_apply rewrites permTensorAction k n 2 (Equiv.swap 0 1) to a PiTensorProduct.reindex, so their left-hand sides are not in simp-normal form.

theorem TauCeti.permTensorAction_swap_comp_orthogonalCup (k : Type u) (n : ℕ) [CommSemiring k] : (permTensorAction k n 2) (Equiv.swap 0 1) ∘ₗ orthogonalCup k n = orthogonalCup k n

The crossing fixes the cup: the cup joins the two top points, and swapping them is the same arc.

theorem TauCeti.orthogonalCap_comp_permTensorAction_swap (k : Type u) (n : ℕ) [CommSemiring k] : orthogonalCap k n ∘ₗ (permTensorAction k n 2) (Equiv.swap 0 1) = orthogonalCap k n

The crossing fixes the cap: the coordinate dot product is symmetric.

theorem TauCeti.permTensorAction_swap_mul_orthogonalCupCap (k : Type u) (n : ℕ) [CommSemiring k] : (permTensorAction k n 2) (Equiv.swap 0 1) * orthogonalCupCap k n = orthogonalCupCap k n

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

theorem TauCeti.orthogonalCupCap_mul_permTensorAction_swap (k : Type u) (n : ℕ) [CommSemiring k] : orthogonalCupCap k n * (permTensorAction k n 2) (Equiv.swap 0 1) = orthogonalCupCap k n

The relation e s = e: the crossing is absorbed by the cap at the bottom of e.

theorem TauCeti.orthogonalCap_comp_piTensorProductMap {k : Type u} {n : ℕ} [CommSemiring k] {A : Matrix (Fin n) (Fin n) k} (hA : A.transpose * A = 1) : (orthogonalCap k n ∘ₗ PiTensorProduct.map fun (x : Fin 2) => A.mulVecLin) = orthogonalCap k n

The cap is invariant under every matrix A with Aᵀ * A = 1: such a matrix preserves the coordinate dot product, which is what the cap contracts against.

TauCeti.stdOrthogonalRep_dotProduct_stdOrthogonalRep is the same computation for an element of the orthogonal group, but it is unavailable at this generality: the orthogonal group needs a commutative ring.

theorem TauCeti.piTensorProductMap_comp_orthogonalCup {k : Type u} {n : ℕ} [CommSemiring k] {A : Matrix (Fin n) (Fin n) k} (hA : A * A.transpose = 1) : (PiTensorProduct.map fun (x : Fin 2) => A.mulVecLin) ∘ₗ orthogonalCup k n = orthogonalCup k n

The cup is invariant under every matrix A with A * Aᵀ = 1. This is the other one-sided identity: the cap consumes Aᵀ * A = 1 and the cup consumes A * Aᵀ = 1.

theorem TauCeti.orthogonalCap_comp_tensorPower (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) : orthogonalCap k n ∘ₗ ((stdOrthogonalRep k n).tensorPower 2) g = orthogonalCap k n

The cap is invariant under the diagonal action of the orthogonal group.

theorem TauCeti.tensorPower_comp_orthogonalCup (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) : ((stdOrthogonalRep k n).tensorPower 2) g ∘ₗ orthogonalCup k n = orthogonalCup k n

The cup is invariant under the diagonal action of the orthogonal group.

theorem TauCeti.commute_orthogonalCupCap_tensorPower (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.orthogonalGroup (Fin n) k)) : Commute (orthogonalCupCap k n) (((stdOrthogonalRep k n).tensorPower 2) g)

The Brauer generator e commutes with the orthogonal group. This is the two-strand case of the statement that the diagram action and the orthogonal action centralize one another.