Documentation

Mathlib.Algebra.Quandle

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 [Joyce1982] 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 [FennRourke1992]. Unital shelves are discussed in [crans2017].

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 #

Main statements #

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 #

Tags #

rack, quandle

class Shelf (α : Type u) :

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
    theorem Shelf.self_distrib {α : Type u} [self : Shelf α] {x : α} {y : α} {z : α} :

    A verification that act is self-distributive

    class UnitalShelf (α : Type u) extends Shelf , One :

    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
      theorem UnitalShelf.one_act {α : Type u} [self : UnitalShelf α] (a : α) :
      Shelf.act 1 a = a
      theorem UnitalShelf.act_one {α : Type u} [self : UnitalShelf α] (a : α) :
      Shelf.act a 1 = a
      theorem ShelfHom.ext {S₁ : Type u_1} {S₂ : Type u_2} :
      ∀ {inst : Shelf S₁} {inst_1 : Shelf S₂} {x y : ShelfHom S₁ S₂}, x.toFun = y.toFunx = y
      theorem ShelfHom.ext_iff {S₁ : Type u_1} {S₂ : Type u_2} :
      ∀ {inst : Shelf S₁} {inst_1 : Shelf S₂} {x y : ShelfHom S₁ S₂}, x = y x.toFun = y.toFun
      structure ShelfHom (S₁ : Type u_1) (S₂ : Type u_2) [Shelf S₁] [Shelf S₂] :
      Type (max u_1 u_2)

      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

      • map_act' : ∀ {x y : S₁}, self.toFun (Shelf.act x y) = Shelf.act (self.toFun x) (self.toFun y)

        The homomorphism property of a Shelf Homomorphism

      Instances For
        theorem ShelfHom.map_act' {S₁ : Type u_1} {S₂ : Type u_2} [Shelf S₁] [Shelf S₂] (self : ShelfHom S₁ S₂) {x : S₁} {y : S₁} :
        self.toFun (Shelf.act x y) = Shelf.act (self.toFun x) (self.toFun y)

        The homomorphism property of a Shelf Homomorphism

        class Rack (α : Type u) extends Shelf :

        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
          theorem Rack.left_inv {α : Type u} [self : Rack α] (x : α) :

          Proof of left inverse

          theorem Rack.right_inv {α : Type u} [self : Rack α] (x : α) :

          Proof of right inverse

          Inverse Action of a Rack

          Equations
          Instances For
            theorem UnitalShelf.act_act_self_eq {S : Type u_1} [UnitalShelf S] (x : S) (y : S) :

            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.

            theorem UnitalShelf.act_idem {S : Type u_1} [UnitalShelf S] (x : S) :
            Shelf.act x x = x
            theorem UnitalShelf.act_self_act_eq {S : Type u_1} [UnitalShelf S] (x : S) (y : S) :
            theorem UnitalShelf.assoc {S : Type u_1} [UnitalShelf S] (x : S) (y : S) (z : S) :

            The associativity of a unital shelf comes for free.

            def Rack.act' {R : Type u_1} [Rack R] (x : R) :
            R R

            A rack acts on itself by equivalences.

            Equations
            Instances For
              @[simp]
              theorem Rack.act'_apply {R : Type u_1} [Rack R] (x : R) (y : R) :
              @[simp]
              theorem Rack.act'_symm_apply {R : Type u_1} [Rack R] (x : R) (y : R) :
              (Rack.act' x).symm y = Rack.invAct x y
              @[simp]
              theorem Rack.invAct_apply {R : Type u_1} [Rack R] (x : R) (y : R) :
              @[simp]
              theorem Rack.invAct_act_eq {R : Type u_1} [Rack R] (x : R) (y : R) :
              @[simp]
              theorem Rack.act_invAct_eq {R : Type u_1} [Rack R] (x : R) (y : R) :
              theorem Rack.left_cancel {R : Type u_1} [Rack R] (x : R) {y : R} {y' : R} :
              Shelf.act x y = Shelf.act x y' y = y'
              theorem Rack.left_cancel_inv {R : Type u_1} [Rack R] (x : R) {y : R} {y' : R} :
              Rack.invAct x y = Rack.invAct x y' y = y'
              theorem Rack.self_distrib_inv {R : Type u_1} [Rack R] {x : R} {y : R} {z : R} :
              theorem Rack.ad_conj {R : Type u_2} [Rack R] (x : R) (y : R) :

              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'.

              instance Rack.oppositeRack {R : Type u_1} [Rack R] :

              The opposite rack, swapping the roles of and ◃⁻¹.

              Equations
              @[simp]
              theorem Rack.op_act_op_eq {R : Type u_1} [Rack R] {x : R} {y : R} :
              @[simp]
              theorem Rack.op_invAct_op_eq {R : Type u_1} [Rack R] {x : R} {y : R} :
              @[simp]
              theorem Rack.self_act_act_eq {R : Type u_1} [Rack R] {x : R} {y : R} :
              @[simp]
              theorem Rack.self_invAct_invAct_eq {R : Type u_1} [Rack R] {x : R} {y : R} :
              @[simp]
              theorem Rack.self_act_invAct_eq {R : Type u_1} [Rack R] {x : R} {y : R} :
              @[simp]
              theorem Rack.self_invAct_act_eq {R : Type u_1} [Rack R] {x : R} {y : R} :
              theorem Rack.self_act_eq_iff_eq {R : Type u_1} [Rack R] {x : R} {y : R} :
              Shelf.act x x = Shelf.act y y x = y
              theorem Rack.self_invAct_eq_iff_eq {R : Type u_1} [Rack R] {x : R} {y : R} :
              def Rack.selfApplyEquiv (R : Type u_2) [Rack R] :
              R R

              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
              Instances For
                def Rack.IsInvolutory (R : Type u_2) [Rack R] :

                An involutory rack is one for which Rack.oppositeRack R x is an involution for every x.

                Equations
                Instances For
                  theorem Rack.involutory_invAct_eq_act {R : Type u_2} [Rack R] (h : Rack.IsInvolutory R) (x : R) (y : R) :
                  def Rack.IsAbelian (R : Type u_2) [Rack R] :

                  An abelian rack is one for which the mediality axiom holds.

                  Equations
                  Instances For
                    theorem Rack.assoc_iff_id {R : Type u_2} [Rack R] {x : R} {y : R} {z : R} :

                    Associative racks are uninteresting.

                    instance ShelfHom.instFunLike {S₁ : Type u_1} {S₂ : Type u_2} [Shelf S₁] [Shelf S₂] :
                    FunLike (ShelfHom S₁ S₂) S₁ S₂
                    Equations
                    • ShelfHom.instFunLike = { coe := ShelfHom.toFun, coe_injective' := }
                    @[simp]
                    theorem ShelfHom.toFun_eq_coe {S₁ : Type u_1} {S₂ : Type u_2} [Shelf S₁] [Shelf S₂] (f : ShelfHom S₁ S₂) :
                    f.toFun = f
                    @[simp]
                    theorem ShelfHom.map_act {S₁ : Type u_1} {S₂ : Type u_2} [Shelf S₁] [Shelf S₂] (f : ShelfHom S₁ S₂) {x : S₁} {y : S₁} :
                    f (Shelf.act x y) = Shelf.act (f x) (f y)
                    def ShelfHom.id (S : Type u_4) [Shelf S] :

                    The identity homomorphism

                    Equations
                    • ShelfHom.id S = { toFun := fun (x : S) => x, map_act' := }
                    Instances For
                      instance ShelfHom.inhabited (S : Type u_4) [Shelf S] :
                      Equations
                      def ShelfHom.comp {S₁ : Type u_1} {S₂ : Type u_2} {S₃ : Type u_3} [Shelf S₁] [Shelf S₂] [Shelf S₃] (g : ShelfHom S₂ S₃) (f : ShelfHom S₁ S₂) :
                      ShelfHom S₁ S₃

                      The composition of shelf homomorphisms

                      Equations
                      • g.comp f = { toFun := g.toFun f.toFun, map_act' := }
                      Instances For
                        @[simp]
                        theorem ShelfHom.comp_apply {S₁ : Type u_1} {S₂ : Type u_2} {S₃ : Type u_3} [Shelf S₁] [Shelf S₂] [Shelf S₃] (g : ShelfHom S₂ S₃) (f : ShelfHom S₁ S₂) (x : S₁) :
                        (g.comp f) x = g (f x)
                        class Quandle (α : Type u_1) extends Rack :
                        Type u_1

                        A quandle is a rack such that each automorphism fixes its corresponding element.

                        Instances
                          @[simp]
                          theorem Quandle.fix {α : Type u_1} [self : Quandle α] {x : α} :
                          Shelf.act x x = x

                          The fixing property of a Quandle

                          @[simp]
                          theorem Quandle.fix_inv {Q : Type u_1} [Quandle Q] {x : Q} :
                          Equations
                          @[reducible, inline]
                          abbrev Quandle.Conj (G : Type u_2) :
                          Type u_2

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

                          Equations
                          Instances For
                            @[simp]
                            theorem Quandle.conj_act_eq_conj {G : Type u_2} [Group G] (x : Quandle.Conj G) (y : Quandle.Conj G) :
                            Shelf.act x y = x * y * x⁻¹
                            theorem Quandle.conj_swap {G : Type u_2} [Group G] (x : Quandle.Conj G) (y : Quandle.Conj G) :
                            Shelf.act x y = y Shelf.act y x = x
                            def Quandle.Conj.map {G : Type u_2} {H : Type u_3} [Group G] [Group H] (f : G →* H) :

                            Conj is functorial

                            Equations
                            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
                              Instances For
                                def Quandle.dihedralAct (n : ) (a : ZMod n) :
                                ZMod nZMod n

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

                                Equations
                                Instances For
                                  def Rack.toConj (R : Type u_1) [Rack R] :

                                  This is the natural rack homomorphism to the conjugation quandle of the group R ≃ R that acts on the rack.

                                  Equations
                                  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.

                                    inductive Rack.PreEnvelGroup (R : Type u) :

                                    Free generators of the enveloping group.

                                    Instances For
                                      Equations

                                      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.

                                      Instances For
                                        instance Rack.PreEnvelGroupRel'.inhabited (R : Type u) [Rack R] :
                                        Inhabited (Rack.PreEnvelGroupRel' R Rack.PreEnvelGroup.unit Rack.PreEnvelGroup.unit)
                                        Equations

                                        The PreEnvelGroupRel relation as a Prop. Used as the relation for PreEnvelGroup.setoid.

                                        Instances For
                                          def Rack.EnvelGroup (R : Type u_1) [Rack R] :
                                          Type u_1

                                          The universal enveloping group for the rack R.

                                          Equations
                                          Instances For
                                            Equations

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

                                            Equations
                                            Instances For
                                              def Rack.toEnvelGroup.mapAux {R : Type u_1} [Rack R] {G : Type u_2} [Group G] (f : ShelfHom R (Quandle.Conj G)) :

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

                                              Equations
                                              Instances For

                                                Show that toEnvelGroup.mapAux sends equivalent expressions to equal terms.

                                                def Rack.toEnvelGroup.map {R : Type u_1} [Rack R] {G : Type u_2} [Group G] :

                                                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
                                                  theorem Rack.toEnvelGroup.univ (R : Type u_1) [Rack R] (G : Type u_2) [Group G] (f : ShelfHom R (Quandle.Conj G)) :
                                                  (Quandle.Conj.map (Rack.toEnvelGroup.map f)).comp (Rack.toEnvelGroup R) = f

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

                                                  theorem Rack.toEnvelGroup.univ_uniq (R : Type u_1) [Rack R] (G : Type u_2) [Group G] (f : ShelfHom R (Quandle.Conj G)) (g : Rack.EnvelGroup R →* G) (h : f = (Quandle.Conj.map g).comp (Rack.toEnvelGroup R)) :
                                                  g = Rack.toEnvelGroup.map f

                                                  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
                                                  Instances For
                                                    @[simp]
                                                    theorem Rack.envelAction_prop {R : Type u_1} [Rack R] (x : R) (y : R) :
                                                    (Rack.envelAction ((Rack.toEnvelGroup R) x)) y = Shelf.act x y