Documentation

TauCeti.Combinatorics.Brauer.Relations

The Brauer relations between two cap-cup diagrams #

TauCeti/Combinatorics/Brauer/Generator.lean proves the Brauer relations that involve a single cap-cup diagram e and the permutation diagrams: e * e = δ • e, s * e = e * s = e, the far commutation of e with a permutation diagram that renames its pair to itself, and the mixed relation e * (s * e) = e. This file proves the relations that involve two different cap-cup diagrams, which are the remaining defining relations of the Brauer algebra B_k(δ):

Two cap-cup diagrams sharing exactly one point stack to a relabelled cap-cup diagram. TauCeti.composeDiagram_capCup_capCup_eq_relabel_left says that stacking e_{b,c} above e_{a,b} renames the top boundary of e_{a,b} by the three-cycle Equiv.swap a b * Equiv.swap b c carrying a ↦ b ↦ c ↦ a, and TauCeti.composeDiagram_capCup_capCup_eq_relabel_right says that stacking them the other way round renames the bottom boundary by the same three-cycle. Equivalently, by TauCeti.composeDiagram_permToBrauer_left, stacking e_{b,c} above e_{a,b} has the same effect as stacking the diagram of that three-cycle above e_{a,b}: the horizontal arcs of the upper copy are absorbed by those of the lower one. They are the sharpest statement about a stack of two overlapping pairs: the three relations on overlapping pairs below are the consequences of them that the presentation of B_k(δ) names, and a consumer needing such a stack in some other combination should reach for them rather than for those relations. The values of the three-cycle are TauCeti.swap_mul_swap_apply_left, TauCeti.swap_mul_swap_apply_middle and TauCeti.swap_mul_swap_apply_right in TauCeti/GroupTheory/Perm/Basic.lean.

The suffixes _left and _right name which factor of TauCeti.composeDiagram the overlapping pair e_{b,c} is, as in TauCeti.composeDiagram_permToBrauer_left and TauCeti.composeDiagram_permToBrauer_right: _left is the stack with e_{b,c} above e_{a,b} and _right the stack with e_{b,c} below it.

Disjoint pairs do not overlap at all, so their stack is not a relabelled cap-cup diagram but a genuinely new one, the diagram with two caps and two cups; TauCeti.composeDiagram_capCup_capCup_comm says that this diagram does not depend on the order the two copies are stacked in.

Each relation here has a mirror, the same stack turned upside down. Reflection in a horizontal line carries one to the other: it reverses the stacking (TauCeti.flip_composeDiagram), leaves the number of loops closing up in the middle alone (TauCeti.middleLoopCount_flip) and fixes a cap-cup diagram (TauCeti.BrauerDiagram.flip_capCup), so the _right statements below are the reflections of their _left companions.

Each relation comes with the middle-loop count of every stack it names, so that it is a relation for the loop-weighted multiplication D₁ * D₂ = δ ^ middleLoopCount D₁ D₂ • composeDiagram D₁ D₂ of the Brauer algebra on the diagram basis and not only for the underlying matchings. All of the counts here vanish, and the hypotheses that make them vanish are exactly the ones that make the pairs genuinely distinct: on a repeated pair the stack closes up a loop and TauCeti.middleLoopCount_capCup_capCup counts it.

Main results #

References #

Two cap-cup diagrams sharing one point #

source
theorem TauCeti.composeDiagram_capCup_capCup_eq_relabel_left {k : ℕ} {a b : Fin k} (hab : a ≠ b) (c : Fin k) :
composeDiagram (capCup b c) (capCup a b) = (capCup a b).relabel 1 (Equiv.swap a b * Equiv.swap b c)

Two cap-cup diagrams sharing a point stack to a relabelled cap-cup diagram. Stacking e_{b,c} as the left, upper factor, above e_{a,b}, renames the top boundary of e_{a,b} by the three-cycle a ↦ b ↦ c ↦ a: the cap of the upper copy joins the two middle points b and c, one of which the cup of the lower copy already uses, so the upper copy contributes no horizontal arc of its own and only permutes the ends of the lower one. By TauCeti.composeDiagram_permToBrauer_left the right-hand side is equally the stack of the diagram of that three-cycle above e_{a,b}.

The degenerate pairs are covered: for c = b the upper copy is the identity diagram and the three-cycle is the transposition of the pair, which fixes e_{a,b} (TauCeti.BrauerDiagram.relabel_one_swap_capCup); for c = a the two copies are equal, the three-cycle is the identity, and the statement is TauCeti.composeDiagram_capCup_capCup. Only a ≠ b is needed, and it is needed: for a = b the lower copy is the identity diagram, the left-hand side is the cap-cup diagram e_{a,c} and the right-hand side a permutation diagram.

Not a simp lemma: simp rewrites the right-hand side further, through TauCeti.BrauerDiagram.relabel_val_inr, so it is not a simp-normal form of the left-hand side.

source
theorem TauCeti.composeDiagram_capCup_capCup_eq_relabel_right {k : ℕ} {a b : Fin k} (hab : a ≠ b) (c : Fin k) :
composeDiagram (capCup a b) (capCup b c) = (capCup a b).relabel (Equiv.swap a b * Equiv.swap b c) 1

Two cap-cup diagrams sharing a point stack to a relabelled cap-cup diagram, the other way round: with e_{b,c} as the right, lower factor, so that e_{a,b} is stacked above e_{b,c}, it is the bottom boundary of e_{a,b} that is renamed, by the same three-cycle a ↦ b ↦ c ↦ a that TauCeti.composeDiagram_capCup_capCup_eq_relabel_left renames the top boundary by.

Not a simp lemma, for the reason given for TauCeti.composeDiagram_capCup_capCup_eq_relabel_left.

The relations of two overlapping pairs #

source
theorem TauCeti.composeDiagram_capCup_capCup_capCup {k : ℕ} {a b : Fin k} (hab : a ≠ b) (c : Fin k) :
composeDiagram (capCup a b) (composeDiagram (capCup b c) (capCup a b)) = capCup a b

e * (e' * e) = e on the diagram basis: a cap-cup diagram absorbs a cap-cup diagram on an overlapping pair stacked between two copies of it. For consecutive pairs this is Brauer's relation eᵢ eᵢ₊₁ eᵢ = eᵢ.

Together with TauCeti.middleLoopCount_capCup_capCup_left_of_ne and TauCeti.middleLoopCount_capCup_composeDiagram_capCup_capCup, which say that no loop closes up in either middle once the three points are distinct, this is the relation e * (e' * e) = e for the loop-weighted multiplication; TauCeti.middleLoopCount_composeDiagram_capCup_capCup_capCup does the same for the other bracketing, which TauCeti.composeDiagram_assoc identifies with this one.

Not a simp lemma: simp reduces the left-hand side, through TauCeti.composeDiagram_capCup_capCup_eq_relabel_left and the relabelling lemmas, so it is not in simp-normal form.

source
theorem TauCeti.composeDiagram_permToBrauer_swap_capCup_capCup {k : ℕ} {a b : Fin k} (hab : a ≠ b) (c : Fin k) :
composeDiagram (permToBrauer (Equiv.swap a b)) (composeDiagram (capCup b c) (capCup a b)) = composeDiagram (permToBrauer (Equiv.swap b c)) (capCup a b)

The mixed relation s * (e' * e) = s' * e: stacking the diagram of the transposition of a pair above the stack of a cap-cup diagram on an overlapping pair and that pair replaces it by the transposition of the other pair. For consecutive pairs this is Brauer's relation sᵢ eᵢ₊₁ eᵢ = sᵢ₊₁ eᵢ. Once the two pairs are genuinely different, that is once a ≠ c, no loop closes up in any of the three middles, by TauCeti.middleLoopCount_capCup_capCup_left_of_ne and TauCeti.middleLoopCount_permToBrauer_left, so this is that relation for the loop-weighted multiplication. On c = a the inner stack repeats the pair {a, b} and does close up one loop (TauCeti.middleLoopCount_capCup_capCup); the identity of diagrams stated here needs only a ≠ b.

Not a simp lemma, for the reason given for TauCeti.composeDiagram_capCup_capCup_capCup.

source
theorem TauCeti.composeDiagram_capCup_capCup_permToBrauer_swap {k : ℕ} {a b : Fin k} (hab : a ≠ b) (c : Fin k) :
composeDiagram (composeDiagram (capCup a b) (capCup b c)) (permToBrauer (Equiv.swap a b)) = composeDiagram (capCup a b) (permToBrauer (Equiv.swap b c))

The mixed relation (e * e') * s = e * s', the mirror of TauCeti.composeDiagram_permToBrauer_swap_capCup_capCup: stacking the diagram of the transposition of a pair below the stack of a cap-cup diagram on that pair and one on an overlapping pair replaces it by the transposition of the other pair. For consecutive pairs this is Brauer's relation eᵢ eᵢ₊₁ sᵢ = eᵢ sᵢ₊₁. Once the two pairs are genuinely different, that is once a ≠ c, no loop closes up in any of the three middles, by TauCeti.middleLoopCount_capCup_capCup_right_of_ne and TauCeti.middleLoopCount_permToBrauer_right, so this is that relation for the loop-weighted multiplication. On c = a the inner stack repeats the pair {a, b} and does close up one loop (TauCeti.middleLoopCount_capCup_capCup); the identity of diagrams stated here needs only a ≠ b.

Not a simp lemma, for the reason given for TauCeti.composeDiagram_capCup_capCup_capCup.

The middle loops of two overlapping pairs #

source
@[simp]
theorem TauCeti.middleLoopCount_capCup_capCup_left_of_ne {k : ℕ} {a c : Fin k} (hac : a ≠ c) (b : Fin k) :
middleLoopCount (capCup b c) (capCup a b) = 0

Overlapping pairs close up no loop: stacking e_{b,c} as the left, upper factor, above e_{a,b}, closes up no loop in the middle. The only middle point keeping both of its arcs in the middle is the shared point b, whose cap in the upper copy runs to c, where the arc of the lower copy leaves for the boundary.

The hypothesis is needed and is exactly the one that makes the two pairs different as unordered pairs: on a = c the two copies are equal and TauCeti.middleLoopCount_capCup_capCup counts one loop.

source
@[simp]
theorem TauCeti.middleLoopCount_capCup_capCup_right_of_ne {k : ℕ} {a c : Fin k} (hac : a ≠ c) (b : Fin k) :
middleLoopCount (capCup a b) (capCup b c) = 0

Overlapping pairs close up no loop, the other way round: with e_{b,c} as the right, lower factor, so that e_{a,b} is stacked above e_{b,c}, no loop closes up in the middle either. The only middle point keeping both of its arcs in the middle is the shared point b, whose cup in the lower copy runs to c, where the arc of the upper copy leaves for the boundary.

The hypothesis is again exactly the one that makes the two pairs different as unordered pairs: on a = c the two copies are equal and TauCeti.middleLoopCount_capCup_capCup counts one loop.

source
@[simp]
theorem TauCeti.middleLoopCount_capCup_composeDiagram_capCup_capCup {k : ℕ} {a b c : Fin k} (hcb : c ≠ b) (hca : c ≠ a) :
middleLoopCount (capCup a b) (composeDiagram (capCup b c) (capCup a b)) = 0

The outer middle of e * (e' * e) closes up no loop. By TauCeti.composeDiagram_capCup_capCup_eq_relabel_left the lower factor is e_{a,b} with its top boundary renamed by the three-cycle a ↦ b ↦ c ↦ a, so it cups the pair {b, c}; the only middle point that the upper copy also caps is the shared point b, and the cup there runs to c, which the upper copy sends through to the boundary. On the degenerate pair a = b there is no cap at all: the upper copy is the identity diagram (TauCeti.capCup_self), which closes up no loop either, so no hypothesis on the pair {a, b} is needed.

source
@[simp]
theorem TauCeti.middleLoopCount_composeDiagram_capCup_capCup_capCup {k : ℕ} {a b c : Fin k} (hcb : c ≠ b) (hca : c ≠ a) :
middleLoopCount (composeDiagram (capCup a b) (capCup b c)) (capCup a b) = 0

The outer middle of (e * e') * e closes up no loop, the statement TauCeti.middleLoopCount_capCup_composeDiagram_capCup_capCup makes about the other bracketing. By TauCeti.composeDiagram_capCup_capCup_eq_relabel_right the upper factor is e_{a,b} with its bottom boundary renamed by the three-cycle a ↦ b ↦ c ↦ a, so it caps the pair {b, c}; the only middle point that the lower copy also cups is the shared point b, and the cap there runs to c, which the lower copy sends through to the boundary. On the degenerate pair a = b there is no cup at all: the lower copy is the identity diagram (TauCeti.capCup_self), which closes up no loop either, so no hypothesis on the pair {a, b} is needed.

The relation of two disjoint pairs #

source
theorem TauCeti.composeDiagram_capCup_capCup_comm {k : ℕ} {a b c d : Fin k} (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) :
composeDiagram (capCup a b) (capCup c d) = composeDiagram (capCup c d) (capCup a b)

Cap-cup diagrams on disjoint pairs commute. Neither copy uses a point of the other's pair, so each contributes its own cap and its own cup to the stack and the order in which they are stacked does not matter: in both orders the composite caps and cups both pairs and sends every other bottom point through to the top point with the same index. For consecutive pairs this is Brauer's relation eᵢ eⱼ = eⱼ eᵢ for |i - j| ≥ 2; together with TauCeti.middleLoopCount_capCup_capCup_of_disjoint, which says that no loop closes up in either middle, it is that relation for the loop-weighted multiplication.

source
@[simp]
theorem TauCeti.middleLoopCount_capCup_capCup_of_disjoint {k : ℕ} {a b c d : Fin k} (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) :
middleLoopCount (capCup a b) (capCup c d) = 0

Disjoint pairs close up no loop: stacking two cap-cup diagrams on disjoint pairs closes up no loop in the middle. A middle point keeping both of its arcs in the middle would have to be capped by the upper copy, hence lie in its pair, and cupped by the lower one, hence lie in the other pair.