Built with doc-gen4, running Lean4.
Bubbles () indicate interactive fragments: hover for details, tap to reveal contents.
Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus.
On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2020 Kyle Miller. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kyle Miller
! This file was ported from Lean 3 source module algebra.quandle
! leanprover-community/mathlib commit 28aa996fc6fb4317f0083c4e6daf79878d81be33
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.Equiv.Basic
import Mathlib.Algebra.Hom.Aut
import Mathlib.Data.ZMod.Defs
import Mathlib.Tactic.Ring
/-!
# 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
* `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`:
* `x ◃ y` is `Shelf.act x y`
* `x ◃⁻¹ y` is `Rack.inv_act x y`
* `S →◃ S'` is `ShelfHom S S'`
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)][Joyce1982].
## Tags
rack, quandle
-/
open MulOpposite
universe u v
/-- 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.
-/
class
Shelf: {α : Type u} → (act : α → α → α) → (∀ {x y z : α}, actx (actyz)=act (actxy) (actxz)) → Shelfα
Shelf
/--
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`.
-/
class
ShelfHom: (S₁ : Type u_1) → (S₂ : Type u_2) → [inst : ShelfS₁] → [inst : ShelfS₂] → Type (maxu_1u_2)
ShelfHom#align shelf_hom.ext_iff
ShelfHom.ext_iff: ∀ {S₁ : Type u_1} {S₂ : Type u_2} {inst : ShelfS₁} {inst_1 : ShelfS₂} (x y : ShelfHomS₁S₂),
x=y↔x.toFun=y.toFun
ShelfHom.ext_iff#align shelf_hom.ext
ShelfHom.ext: ∀ {S₁ : Type u_1} {S₂ : Type u_2} {inst : ShelfS₁} {inst_1 : ShelfS₂} (x y : ShelfHomS₁S₂),
x.toFun=y.toFun → x=y
ShelfHom.ext
/-- 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.
-/
class
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.
-/
lemma
R]
--porting note: No longer a need for `Rack.self_distrib`
export Shelf (self_distrib)
-- porting note, changed name to `act'` to not conflict with `Shelf.act`
/-- A rack acts on itself by equivalences.
-/
def
Rack.self_distrib_inv
/-- 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'`.
-/
theorem
Rack.self_invAct_eq_iff_eq: ∀ {R : Type u_1} [inst : RackR] {x y : R}, x◃⁻¹x=y◃⁻¹y↔x=y
Rack.self_invAct_eq_iff_eq
/-- The map `x ↦ x ◃ x` is a bijection. (This has applications for the
regular isotopy version of the Reidemeister I move for knot diagrams.)
-/
def
Quandle.oppositeQuandle
/-- The conjugation quandle of a group. Each element of the group acts by
the corresponding inner automorphism.
-/
--porting note: no need for `nolint` and added `reducible`
@[reducible]
def
∀ {x y z : ConjG},
(fun x => ↑(↑MulAut.conjx)) x ((fun x => ↑(↑MulAut.conjx)) yz)=(fun x => ↑(↑MulAut.conjx)) ((fun x => ↑(↑MulAut.conjx)) xy) ((fun x => ↑(↑MulAut.conjx)) xz)
(fun x => ↑(↑MulAut.conjx)) x ((fun x => ↑(↑MulAut.conjx)) yz)=(fun x => ↑(↑MulAut.conjx)) ((fun x => ↑(↑MulAut.conjx)) xy) ((fun x => ↑(↑MulAut.conjx)) xz)
∀ {x y z : ConjG},
(fun x => ↑(↑MulAut.conjx)) x ((fun x => ↑(↑MulAut.conjx)) yz)=(fun x => ↑(↑MulAut.conjx)) ((fun x => ↑(↑MulAut.conjx)) xy) ((fun x => ↑(↑MulAut.conjx)) xz)
∀ {x y z : ConjG},
(fun x => ↑(↑MulAut.conjx)) x ((fun x => ↑(↑MulAut.conjx)) yz)=(fun x => ↑(↑MulAut.conjx)) ((fun x => ↑(↑MulAut.conjx)) xy) ((fun x => ↑(↑MulAut.conjx)) xz)
Quandle.Conj.map
-- porting note: I don't think HasLift exists
-- instance {G : Type _} {H : Type _} [Group G] [Group H] : HasLift (G →* H) (Conj G →◃ Conj H)
-- where lift := Conj.map
/-- The dihedral quandle. This is the conjugation quandle of the dihedral group restrict to flips.
Used for Fox n-colorings of knots.
-/
-- porting note: Removed nolint
def
Quandle.Dihedral
/-- The operation for the dihedral quandle. It does not need to be an equivalence
because it is an involution (see `dihedralAct.inv`).
-/
def