# Racks and Quandles #

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`UnitalShelf`

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.`ShelfHom`

is homomorphisms of shelves, racks, and quandles.`Rack.EnvelGroup`

gives the universal group the rack maps to as a conjugation quandle.`Rack.oppositeRack`

gives the rack with the action replaced by its inverse.

## Main statements #

`Rack.EnvelGroup`

is left adjoint to`Quandle.Conj`

(`toEnvelGroup.map`

). The universality statements are`toEnvelGroup.univ`

and`toEnvelGroup.univ_uniq`

.

## Implementation notes #

"Unital racks" are uninteresting (see `Rack.assoc_iff_id`

, `UnitalShelf.assoc`

), so we do not
define them.

## Notation #

The following notation is localized in `quandles`

:

Use `open 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

A *Shelf* is a structure with a self-distributive binary operation.
The binary operation is regarded as a left action of the type on itself.

- act : α → α → α
The action of the

`Shelf`

over`α`

- self_distrib : ∀ {x y z : α}, Shelf.act x (Shelf.act y z) = Shelf.act (Shelf.act x y) (Shelf.act x z)
A verification that

`act`

is self-distributive

## Instances

A *unital shelf* is a shelf equipped with an element `1`

such that, for all elements `x`

,
we have both `x ◃ 1`

and `1 ◃ x`

equal `x`

.

- act : α → α → α
- one : α

## Instances

The type of homomorphisms between shelves. This is also the notion of rack and quandle homomorphisms.

- toFun : S₁ → S₂
The function under the Shelf Homomorphism

The homomorphism property of a Shelf Homomorphism

## Instances For

A *rack* is an automorphic set (a set with an action on itself by
bijections) that is self-distributive. It is a shelf such that each
element's action is invertible.

The notations `x ◃ y`

and `x ◃⁻¹ y`

denote the action and the
inverse action, respectively, and they are right associative.

- act : α → α → α
- invAct : α → α → α
The inverse actions of the elements

- left_inv : ∀ (x : α), Function.LeftInverse (Rack.invAct x) (Shelf.act x)
Proof of left inverse

- right_inv : ∀ (x : α), Function.RightInverse (Rack.invAct x) (Shelf.act x)
Proof of right inverse

## Instances

Proof of left inverse

Proof of right inverse

Action of a Shelf

## Equations

- Quandles.«term_◃_» = Lean.ParserDescr.trailingNode `Quandles.«term_◃_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃ ") (Lean.ParserDescr.cat `term 65))

## Instances For

Inverse Action of a Rack

## Equations

- Quandles.«term_◃⁻¹_» = Lean.ParserDescr.trailingNode `Quandles.«term_◃⁻¹_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃⁻¹ ") (Lean.ParserDescr.cat `term 65))

## Instances For

Shelf Homomorphism

## Equations

- Quandles.«term_→◃_» = Lean.ParserDescr.trailingNode `Quandles.«term_→◃_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →◃ ") (Lean.ParserDescr.cat `term 25))

## Instances For

A monoid is *graphic* if, for all `x`

and `y`

, the *graphic identity*
`(x * y) * x = x * y`

holds. For a unital shelf, this graphic
identity holds.

The associativity of a unital shelf comes for free.

The *adjoint action* of a rack on itself is `op'`

, and the adjoint
action of `x ◃ y`

is the conjugate of the action of `y`

by the action
of `x`

. It is another way to understand the self-distributivity axiom.

This is used in the natural rack homomorphism `toConj`

from `R`

to
`Conj (R ≃ R)`

defined by `op'`

.

The opposite rack, swapping the roles of `◃`

and `◃⁻¹`

.

## Equations

- Rack.oppositeRack = Rack.mk (fun (x y : Rᵐᵒᵖ) => MulOpposite.op (Shelf.act (MulOpposite.unop x) (MulOpposite.unop y))) ⋯ ⋯

The map `x ↦ x ◃ x`

is a bijection. (This has applications for the
regular isotopy version of the Reidemeister I move for knot diagrams.)

## Equations

- Rack.selfApplyEquiv R = { toFun := fun (x : R) => Shelf.act x x, invFun := fun (x : R) => Rack.invAct x x, left_inv := ⋯, right_inv := ⋯ }

## Instances For

An involutory rack is one for which `Rack.oppositeRack R x`

is an involution for every x.

## Equations

- Rack.IsInvolutory R = ∀ (x : R), Function.Involutive (Shelf.act x)

## Instances For

The identity homomorphism

## Equations

- ShelfHom.id S = { toFun := fun (x : S) => x, map_act' := ⋯ }

## Instances For

## Equations

- ShelfHom.inhabited S = { default := ShelfHom.id S }

## Equations

- Quandle.oppositeQuandle = Quandle.mk ⋯

The conjugation quandle of a group. Each element of the group acts by the corresponding inner automorphism.

## Equations

- Quandle.Conj G = G

## Instances For

## Equations

`Conj`

is functorial

## Equations

- Quandle.Conj.map f = { toFun := ⇑f, map_act' := ⋯ }

## Instances For

The dihedral quandle. This is the conjugation quandle of the dihedral group restrict to flips.

Used for Fox n-colorings of knots.

## Equations

- Quandle.Dihedral n = ZMod n

## Instances For

The operation for the dihedral quandle. It does not need to be an equivalence
because it is an involution (see `dihedralAct.inv`

).

## Equations

- Quandle.dihedralAct n a b = 2 * a - b

## Instances For

## Equations

This is the natural rack homomorphism to the conjugation quandle of the group `R ≃ R`

that acts on the rack.

## Equations

- Rack.toConj R = { toFun := Rack.act', map_act' := ⋯ }

## Instances For

### Universal enveloping group of a rack #

The universal enveloping group `EnvelGroup R`

of a rack `R`

is the
universal group such that every rack homomorphism `R →◃ conj G`

is
induced by a unique group homomorphism `EnvelGroup R →* G`

.
For quandles, Joyce called this group `AdConj R`

.

The `EnvelGroup`

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 `EnvelGroup R →* G`

has a nice description.

Let's think of a group as being a one-object category. The first step
is to define `PreEnvelGroup`

, 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 `PreEnvelGroupRel'`

, 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 `PreEnvelGroupRel`

relation is a
`Prop`

-valued version of `PreEnvelGroupRel'`

, and making it
`Prop`

-valued essentially introduces enough 3-isomorphisms so that
every pair of compatible 2-morphisms is isomorphic. Now, while
composition in `PreEnvelGroup`

does not strictly satisfy the category
axioms, `PreEnvelGroup`

and `PreEnvelGroupRel'`

do form a weak
2-category.

Since we just want a 1-category, the last step is to quotient
`PreEnvelGroup`

by `PreEnvelGroupRel'`

, and the result is the
group `EnvelGroup`

.

For a homomorphism `f : R →◃ Conj G`

, how does
`EnvelGroup.map f : EnvelGroup 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 `PreEnvelGroup`

as expressions in `G`

(this is
`toEnvelGroup.mapAux`

), but we evaluate elements of
`PreEnvelGroup'`

as expressions of 2-morphisms of `G`

(this is
`toEnvelGroup.mapAux.well_def`

). That is to say,
`toEnvelGroup.mapAux.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
`EnvelGroup R →* G`

.

Note: `Type`

-valued relations are not common. The fact it is
`Type`

-valued is what makes `toEnvelGroup.mapAux.well_def`

have
well-founded recursion.

Free generators of the enveloping group.

- unit: {R : Type u} → Rack.PreEnvelGroup R
- incl: {R : Type u} → R → Rack.PreEnvelGroup R
- mul: {R : Type u} → Rack.PreEnvelGroup R → Rack.PreEnvelGroup R → Rack.PreEnvelGroup R
- inv: {R : Type u} → Rack.PreEnvelGroup R → Rack.PreEnvelGroup R

## Instances For

## Equations

- Rack.PreEnvelGroup.inhabited R = { default := Rack.PreEnvelGroup.unit }

Relations for the enveloping group. This is a type-valued relation because
`toEnvelGroup.mapAux.well_def`

inducts on it to show `toEnvelGroup.map`

is well-defined. The relation `PreEnvelGroupRel`

is the `Prop`

-valued version,
which is used to define `EnvelGroup`

itself.

- refl: {R : Type u} → [inst : Rack R] → {a : Rack.PreEnvelGroup R} → Rack.PreEnvelGroupRel' R a a
- symm: {R : Type u} → [inst : Rack R] → {a b : Rack.PreEnvelGroup R} → Rack.PreEnvelGroupRel' R a b → Rack.PreEnvelGroupRel' R b a
- trans: {R : Type u} → [inst : Rack R] → {a b c : Rack.PreEnvelGroup R} → Rack.PreEnvelGroupRel' R a b → Rack.PreEnvelGroupRel' R b c → Rack.PreEnvelGroupRel' R a c
- congr_mul: {R : Type u} → [inst : Rack R] → {a b a' b' : Rack.PreEnvelGroup R} → Rack.PreEnvelGroupRel' R a a' → Rack.PreEnvelGroupRel' R b b' → Rack.PreEnvelGroupRel' R (a.mul b) (a'.mul b')
- congr_inv: {R : Type u} → [inst : Rack R] → {a a' : Rack.PreEnvelGroup R} → Rack.PreEnvelGroupRel' R a a' → Rack.PreEnvelGroupRel' R a.inv a'.inv
- assoc: {R : Type u} → [inst : Rack R] → (a b c : Rack.PreEnvelGroup R) → Rack.PreEnvelGroupRel' R ((a.mul b).mul c) (a.mul (b.mul c))
- one_mul: {R : Type u} → [inst : Rack R] → (a : Rack.PreEnvelGroup R) → Rack.PreEnvelGroupRel' R (Rack.PreEnvelGroup.unit.mul a) a
- mul_one: {R : Type u} → [inst : Rack R] → (a : Rack.PreEnvelGroup R) → Rack.PreEnvelGroupRel' R (a.mul Rack.PreEnvelGroup.unit) a
- inv_mul_cancel: {R : Type u} → [inst : Rack R] → (a : Rack.PreEnvelGroup R) → Rack.PreEnvelGroupRel' R (a.inv.mul a) Rack.PreEnvelGroup.unit
- act_incl: {R : Type u} → [inst : Rack R] → (x y : R) → Rack.PreEnvelGroupRel' R (((Rack.PreEnvelGroup.incl x).mul (Rack.PreEnvelGroup.incl y)).mul (Rack.PreEnvelGroup.incl x).inv) (Rack.PreEnvelGroup.incl (Shelf.act x y))

## Instances For

## Equations

- Rack.PreEnvelGroupRel'.inhabited R = { default := Rack.PreEnvelGroupRel'.refl }

The `PreEnvelGroupRel`

relation as a `Prop`

. Used as the relation for `PreEnvelGroup.setoid`

.

- rel: ∀ {R : Type u} [inst : Rack R] {a b : Rack.PreEnvelGroup R}, Rack.PreEnvelGroupRel' R a b → Rack.PreEnvelGroupRel R a b

## Instances For

A quick way to convert a `PreEnvelGroupRel'`

to a `PreEnvelGroupRel`

.

## Equations

- Rack.PreEnvelGroup.setoid R = { r := Rack.PreEnvelGroupRel R, iseqv := ⋯ }

The universal enveloping group for the rack R.

## Equations

## Instances For

## Equations

- Rack.instDivInvMonoidEnvelGroup R = DivInvMonoid.mk ⋯ zpowRec ⋯ ⋯ ⋯

## Equations

## Equations

- Rack.EnvelGroup.inhabited R = { default := 1 }

The canonical homomorphism from a rack to its enveloping group.
Satisfies universal properties given by `toEnvelGroup.map`

and `toEnvelGroup.univ`

.

## Equations

- Rack.toEnvelGroup R = { toFun := fun (x : R) => ⟦Rack.PreEnvelGroup.incl x⟧, map_act' := ⋯ }

## Instances For

The preliminary definition of the induced map from the enveloping group.
See `toEnvelGroup.map`

.

## Equations

- Rack.toEnvelGroup.mapAux f Rack.PreEnvelGroup.unit = 1
- Rack.toEnvelGroup.mapAux f (Rack.PreEnvelGroup.incl x_1) = f x_1
- Rack.toEnvelGroup.mapAux f (a.mul b) = Rack.toEnvelGroup.mapAux f a * Rack.toEnvelGroup.mapAux f b
- Rack.toEnvelGroup.mapAux f a.inv = (Rack.toEnvelGroup.mapAux f a)⁻¹

## Instances For

Show that `toEnvelGroup.mapAux`

sends equivalent expressions to equal terms.

Given a map from a rack to a group, lift it to being a map from the enveloping group.
More precisely, the `EnvelGroup`

functor is left adjoint to `Quandle.Conj`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Given a homomorphism from a rack to a group, it factors through the enveloping group.

The homomorphism `toEnvelGroup.map f`

is the unique map that fits into the commutative
triangle in `toEnvelGroup.univ`

.

The induced group homomorphism from the enveloping group into bijections of the rack,
using `Rack.toConj`

. Satisfies the property `envelAction_prop`

.

This gives the rack `R`

the structure of an augmented rack over `EnvelGroup R`

.

## Equations

- Rack.envelAction = Rack.toEnvelGroup.map (Rack.toConj R)