Racks and Quandles #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines racks and quandles, algebraic structures for sets that bijectively act on themselves with a self-distributivity property. If R is a rack and act : R → (R ≃ R) is the self-action, then the self-distributivity is, equivalently, that

act (act x y) = act x * act y * (act x)⁻¹

where multiplication is composition in R ≃ R as a group. Quandles are racks such that act x x = x for all x.

One example of a quandle (not yet in mathlib) is the action of a Lie algebra on itself, defined by act x y = Ad (exp x) y.

Quandles and racks were independently developed by multiple mathematicians. David Joyce introduced quandles in his thesis [Joy82] to define an algebraic invariant of knot and link complements that is analogous to the fundamental group of the exterior, and he showed that the quandle associated to an oriented knot is invariant up to orientation-reversed mirror image. Racks were used by Fenn and Rourke for framed codimension-2 knots and links in [FR92]. Unital shelves are discussed in [CMP17].

The name "rack" came from wordplay by Conway and Wraith for the "wrack and ruin" of forgetting everything but the conjugation operation for a group.

Main definitions #

• shelf is a type with a self-distributive action
• unital_shelf is a shelf with a left and right unit
• rack is a shelf whose action for each element is invertible
• quandle is a rack whose action for an element fixes that element
• quandle.conj defines a quandle of a group acting on itself by conjugation.
• shelf_hom is homomorphisms of shelves, racks, and quandles.
• rack.envel_group gives the universal group the rack maps to as a conjugation quandle.
• rack.opp gives the rack with the action replaced by its inverse.

Main statements #

• rack.envel_group is left adjoint to quandle.conj (to_envel_group.map). The universality statements are to_envel_group.univ and to_envel_group.univ_uniq.

Implementation notes #

"Unital racks" are uninteresting (see rack.assoc_iff_id, unital_shelf.assoc), so we do not define them.

Notation #

The following notation is localized in quandles:

• x ◃ y is shelf.act x y
• x ◃⁻¹ y is rack.inv_act x y
• S →◃ S' is shelf_hom S S'

Use open_locale quandles to use these.

Todo #

• If g is the Lie algebra of a Lie group G, then (x ◃ y) = Ad (exp x) x forms a quandle.
• If X is a symmetric space, then each point has a corresponding involution that acts on X, forming a quandle.
• Alexander quandle with a ◃ b = t * b + (1 - t) * b, with a and b elements of a module over Z[t,t⁻¹].
• If G is a group, H a subgroup, and z in H, then there is a quandle (G/H;z) defined by yH ◃ xH = yzy⁻¹xH. Every homogeneous quandle (i.e., a quandle Q whose automorphism group acts transitively on Q as a set) is isomorphic to such a quandle. There is a generalization to this arbitrary quandles in Joyce's paper (Theorem 7.2).

Tags #

rack, quandle

Universal enveloping group of a rack #

The universal enveloping group envel_group R of a rack R is the universal group such that every rack homomorphism R →◃ conj G is induced by a unique group homomorphism envel_group R →* G. For quandles, Joyce called this group AdConj R.

The envel_group functor is left adjoint to the conj forgetful functor, and the way we construct the enveloping group is via a technique that should work for left adjoints of forgetful functors in general. It involves thinking a little about 2-categories, but the payoff is that the map envel_group R →* G has a nice description.

Let's think of a group as being a one-object category. The first step is to define pre_envel_group, which gives formal expressions for all the 1-morphisms and includes the unit element, elements of R, multiplication, and inverses. To introduce relations, the second step is to define pre_envel_group_rel', which gives formal expressions for all 2-morphisms between the 1-morphisms. The 2-morphisms include associativity, multiplication by the unit, multiplication by inverses, compatibility with multiplication and inverses (congr_mul and congr_inv), the axioms for an equivalence relation, and, importantly, the relationship between conjugation and the rack action (see rack.ad_conj).

None of this forms a 2-category yet, for example due to lack of associativity of trans. The pre_envel_group_rel relation is a Prop-valued version of pre_envel_group_rel', and making it Prop-valued essentially introduces enough 3-isomorphisms so that every pair of compatible 2-morphisms is isomorphic. Now, while composition in pre_envel_group does not strictly satisfy the category axioms, pre_envel_group and pre_envel_group_rel' do form a weak 2-category.

Since we just want a 1-category, the last step is to quotient pre_envel_group by pre_envel_group_rel', and the result is the group envel_group.

For a homomorphism f : R →◃ conj G, how does envel_group.map f : envel_group R →* G work? Let's think of G as being a 2-category with one object, a 1-morphism per element of G, and a single 2-morphism called eq.refl for each 1-morphism. We define the map using a "higher quotient.lift" -- not only do we evaluate elements of pre_envel_group as expressions in G (this is to_envel_group.map_aux), but we evaluate elements of pre_envel_group' as expressions of 2-morphisms of G (this is to_envel_group.map_aux.well_def). That is to say, to_envel_group.map_aux.well_def recursively evaluates formal expressions of 2-morphisms as equality proofs in G. Now that all morphisms are accounted for, the map descends to a homomorphism envel_group R →* G.

Note: Type-valued relations are not common. The fact it is Type-valued is what makes to_envel_group.map_aux.well_def have well-founded recursion.