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 actionunital_shelf
is a shelf with a left and right unitrack
is a shelf whose action for each element is invertiblequandle
is a rack whose action for an element fixes that elementquandle.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 toquandle.conj
(to_envel_group.map
). The universality statements areto_envel_group.univ
andto_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
isshelf.act x y
x ◃⁻¹ y
israck.inv_act x y
S →◃ S'
isshelf_hom S S'
Use open_locale quandles
to use these.
Todo #
- If
g
is the Lie algebra of a Lie groupG
, 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 onX
, forming a quandle. - Alexander quandle with
a ◃ b = t * b + (1 - t) * b
, witha
andb
elements of a module overZ[t,t⁻¹]
. - If
G
is a group,H
a subgroup, andz
inH
, then there is a quandle(G/H;z)
defined byyH ◃ xH = yzy⁻¹xH
. Every homogeneous quandle (i.e., a quandleQ
whose automorphism group acts transitively onQ
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
- act : α → α → α
- self_distrib : ∀ {x y z : α}, shelf.act x (shelf.act y z) = shelf.act (shelf.act x y) (shelf.act x z)
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.
Instances of this typeclass
Instances of other typeclasses for shelf
- shelf.has_sizeof_inst
- to_shelf : shelf α
- to_has_one : has_one α
- one_act : ∀ (a : α), shelf.act 1 a = a
- act_one : ∀ (a : α), shelf.act a 1 = a
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
.
Instances for unital_shelf
- unital_shelf.has_sizeof_inst
- to_fun : S₁ → S₂
- map_act' : ∀ {x y : S₁}, self.to_fun (shelf.act x y) = shelf.act (self.to_fun x) (self.to_fun y)
The type of homomorphisms between shelves. This is also the notion of rack and quandle homomorphisms.
Instances for shelf_hom
- shelf_hom.has_sizeof_inst
- shelf_hom.has_coe_to_fun
- shelf_hom.inhabited
- quandle.shelf_hom.has_lift
- to_shelf : shelf α
- inv_act : α → α → α
- left_inv : ∀ (x : α), function.left_inverse (rack.inv_act x) (shelf.act x)
- right_inv : ∀ (x : α), function.right_inverse (rack.inv_act x) (shelf.act x)
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.
Instances of this typeclass
Instances of other typeclasses for rack
- rack.has_sizeof_inst
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 to_conj
from R
to
conj (R ≃ R)
defined by op'
.
The opposite rack, swapping the roles of ◃
and ◃⁻¹
.
Equations
- rack.opposite_rack = {to_shelf := {act := λ (x y : Rᵐᵒᵖ), mul_opposite.op (rack.inv_act (mul_opposite.unop x) (mul_opposite.unop y)), self_distrib := _}, inv_act := λ (x y : Rᵐᵒᵖ), mul_opposite.op (shelf.act (mul_opposite.unop x) (mul_opposite.unop y)), left_inv := _, right_inv := _}
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.self_apply_equiv R = {to_fun := λ (x : R), shelf.act x x, inv_fun := λ (x : R), rack.inv_act x x, left_inv := _, right_inv := _}
An involutory rack is one for which rack.op R x
is an involution for every x.
Equations
- rack.is_involutory R = ∀ (x : R), function.involutive (shelf.act x)
Equations
- shelf_hom.has_coe_to_fun = {coe := shelf_hom.to_fun _inst_2}
Equations
- shelf_hom.inhabited S = {default := shelf_hom.id S _inst_4}
A quandle is a rack such that each automorphism fixes its corresponding element.
Instances of this typeclass
Instances of other typeclasses for quandle
- quandle.has_sizeof_inst
Equations
The conjugation quandle of a group. Each element of the group acts by the corresponding inner automorphism.
Equations
- quandle.conj G = G
Instances for quandle.conj
Equations
- quandle.conj.quandle G = {to_rack := {to_shelf := {act := λ (x : quandle.conj G), ⇑(⇑mul_aut.conj x), self_distrib := _}, inv_act := λ (x : quandle.conj G), ⇑(mul_equiv.symm (⇑mul_aut.conj x)), left_inv := _, right_inv := _}, fix := _}
conj
is functorial
Equations
- quandle.shelf_hom.has_lift = {lift := quandle.conj.map _inst_3}
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 quandle.dihedral
Equations
- quandle.dihedral.quandle n = {to_rack := {to_shelf := {act := quandle.dihedral_act n, self_distrib := _}, inv_act := quandle.dihedral_act n, left_inv := _, right_inv := _}, fix := _}
This is the natural rack homomorphism to the conjugation quandle of the group R ≃ R
that acts on the rack.
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.
- unit : Π {R : Type u}, rack.pre_envel_group R
- incl : Π {R : Type u}, R → rack.pre_envel_group R
- mul : Π {R : Type u}, rack.pre_envel_group R → rack.pre_envel_group R → rack.pre_envel_group R
- inv : Π {R : Type u}, rack.pre_envel_group R → rack.pre_envel_group R
Free generators of the enveloping group.
Instances for rack.pre_envel_group
- rack.pre_envel_group.has_sizeof_inst
- rack.pre_envel_group.inhabited
- rack.pre_envel_group.setoid
Equations
- refl : Π {R : Type u} [_inst_1 : rack R] {a : rack.pre_envel_group R}, rack.pre_envel_group_rel' R a a
- symm : Π {R : Type u} [_inst_1 : rack R] {a b : rack.pre_envel_group R}, rack.pre_envel_group_rel' R a b → rack.pre_envel_group_rel' R b a
- trans : Π {R : Type u} [_inst_1 : rack R] {a b c : rack.pre_envel_group R}, rack.pre_envel_group_rel' R a b → rack.pre_envel_group_rel' R b c → rack.pre_envel_group_rel' R a c
- congr_mul : Π {R : Type u} [_inst_1 : rack R] {a b a' b' : rack.pre_envel_group R}, rack.pre_envel_group_rel' R a a' → rack.pre_envel_group_rel' R b b' → rack.pre_envel_group_rel' R (a.mul b) (a'.mul b')
- congr_inv : Π {R : Type u} [_inst_1 : rack R] {a a' : rack.pre_envel_group R}, rack.pre_envel_group_rel' R a a' → rack.pre_envel_group_rel' R a.inv a'.inv
- assoc : Π {R : Type u} [_inst_1 : rack R] (a b c : rack.pre_envel_group R), rack.pre_envel_group_rel' R ((a.mul b).mul c) (a.mul (b.mul c))
- one_mul : Π {R : Type u} [_inst_1 : rack R] (a : rack.pre_envel_group R), rack.pre_envel_group_rel' R (rack.pre_envel_group.unit.mul a) a
- mul_one : Π {R : Type u} [_inst_1 : rack R] (a : rack.pre_envel_group R), rack.pre_envel_group_rel' R (a.mul rack.pre_envel_group.unit) a
- mul_left_inv : Π {R : Type u} [_inst_1 : rack R] (a : rack.pre_envel_group R), rack.pre_envel_group_rel' R (a.inv.mul a) rack.pre_envel_group.unit
- act_incl : Π {R : Type u} [_inst_1 : rack R] (x y : R), rack.pre_envel_group_rel' R (((rack.pre_envel_group.incl x).mul (rack.pre_envel_group.incl y)).mul (rack.pre_envel_group.incl x).inv) (rack.pre_envel_group.incl (shelf.act x y))
Relations for the enveloping group. This is a type-valued relation because
to_envel_group.map_aux.well_def
inducts on it to show to_envel_group.map
is well-defined. The relation pre_envel_group_rel
is the Prop
-valued version,
which is used to define envel_group
itself.
Instances for rack.pre_envel_group_rel'
- rack.pre_envel_group_rel'.has_sizeof_inst
- rack.pre_envel_group_rel'.inhabited
- rel : ∀ {R : Type u} [_inst_1 : rack R] {a b : rack.pre_envel_group R}, rack.pre_envel_group_rel' R a b → rack.pre_envel_group_rel R a b
The pre_envel_group_rel
relation as a Prop
. Used as the relation for pre_envel_group.setoid
.
A quick way to convert a pre_envel_group_rel'
to a pre_envel_group_rel
.
Equations
- rack.pre_envel_group.setoid R = {r := rack.pre_envel_group_rel R _inst_1, iseqv := _}
The universal enveloping group for the rack R.
Equations
Instances for rack.envel_group
Equations
- rack.envel_group.div_inv_monoid R = {mul := λ (a b : rack.envel_group R), quotient.lift_on₂ a b (λ (a b : rack.pre_envel_group R), ⟦a.mul b⟧) _, mul_assoc := _, one := ⟦rack.pre_envel_group.unit⟧, one_mul := _, mul_one := _, npow := monoid.npow._default ⟦rack.pre_envel_group.unit⟧ (λ (a b : rack.envel_group R), quotient.lift_on₂ a b (λ (a b : rack.pre_envel_group R), ⟦a.mul b⟧) _) _ _, npow_zero' := _, npow_succ' := _, inv := λ (a : rack.envel_group R), quotient.lift_on a (λ (a : rack.pre_envel_group R), ⟦a.inv⟧) _, div := λ (a b : rack.envel_group R), quotient.lift_on₂ a (quotient.lift_on b (λ (a : rack.pre_envel_group R), ⟦a.inv⟧) _) (λ (a b : rack.pre_envel_group R), ⟦a.mul b⟧) _, div_eq_mul_inv := _, zpow := zpow_rec {inv := λ (a : rack.envel_group R), quotient.lift_on a (λ (a : rack.pre_envel_group R), ⟦a.inv⟧) _}, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _}
Equations
- rack.envel_group.group R = {mul := div_inv_monoid.mul (rack.envel_group.div_inv_monoid R), mul_assoc := _, one := div_inv_monoid.one (rack.envel_group.div_inv_monoid R), one_mul := _, mul_one := _, npow := div_inv_monoid.npow (rack.envel_group.div_inv_monoid R), npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv (rack.envel_group.div_inv_monoid R), div := div_inv_monoid.div (rack.envel_group.div_inv_monoid R), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow (rack.envel_group.div_inv_monoid R), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
Equations
- rack.envel_group.inhabited R = {default := 1}
The canonical homomorphism from a rack to its enveloping group.
Satisfies universal properties given by to_envel_group.map
and to_envel_group.univ
.
Equations
- rack.to_envel_group R = {to_fun := λ (x : R), ⟦rack.pre_envel_group.incl x⟧, map_act' := _}
The preliminary definition of the induced map from the enveloping group.
See to_envel_group.map
.
Equations
- rack.to_envel_group.map_aux f a.inv = (rack.to_envel_group.map_aux f a)⁻¹
- rack.to_envel_group.map_aux f (a.mul b) = rack.to_envel_group.map_aux f a * rack.to_envel_group.map_aux f b
- rack.to_envel_group.map_aux f (rack.pre_envel_group.incl x) = ⇑f x
- rack.to_envel_group.map_aux f rack.pre_envel_group.unit = 1
Show that to_envel_group.map_aux
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 envel_group
functor is left adjoint to quandle.conj
.
Equations
- rack.to_envel_group.map = {to_fun := λ (f : shelf_hom R (quandle.conj G)), {to_fun := λ (x : rack.envel_group R), quotient.lift_on x (rack.to_envel_group.map_aux f) _, map_one' := _, map_mul' := _}, inv_fun := λ (F : rack.envel_group R →* G), (quandle.conj.map F).comp (rack.to_envel_group R), left_inv := _, right_inv := _}
Given a homomorphism from a rack to a group, it factors through the enveloping group.
The homomorphism to_envel_group.map f
is the unique map that fits into the commutative
triangle in to_envel_group.univ
.
The induced group homomorphism from the enveloping group into bijections of the rack,
using rack.to_conj
. Satisfies the property envel_action_prop
.
This gives the rack R
the structure of an augmented rack over envel_group R
.