mathlib documentation

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.[FennRourke1992]

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
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 universal (to_envel_group.univ and to_envel_group.univ_uniq)

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)][Joyce1982].

Tags

rack, quandle

@[class]

structure shelf (α : Type u) :

Type u

act : α → α → α
self_distrib : ∀ {x y z : α}, x ◃ y ◃ z = (x ◃ y) ◃ 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

rack.to_shelf

theorem shelf_hom.ext {S₁ : Type u_1} {S₂ : Type u_2} {_inst_1 : shelf S₁} {_inst_2 : shelf S₂} (x y : S₁ →◃ S₂) (h : x.to_fun = y.to_fun) :

x = y

@[ext]

structure shelf_hom (S₁ : Type u_1) (S₂ : Type u_2) [shelf S₁] [shelf S₂] :

Type (max u_1 u_2)

to_fun : S₁ → S₂
map_act' : ∀ {x y : S₁}, c.to_fun (x ◃ y) = c.to_fun x ◃ c.to_fun y

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

theorem shelf_hom.ext_iff {S₁ : Type u_1} {S₂ : Type u_2} {_inst_1 : shelf S₁} {_inst_2 : shelf S₂} (x y : S₁ →◃ S₂) :

x = y ↔ x.to_fun = y.to_fun

@[class]

structure rack (α : Type u) :

Type u

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

theorem rack.self_distrib {R : Type u_1} [rack R] {x y z : R} :

x ◃ y ◃ z = (x ◃ y) ◃ x ◃ z

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

R ≃ R

A rack acts on itself by equivalences.

Equations

rack.act x = {to_fun := shelf.act x, inv_fun := rack.inv_act x, left_inv := _, right_inv := _}

@[simp]

theorem rack.act_apply {R : Type u_1} [rack R] (x y : R) :

⇑(rack.act x) y = x ◃ y

@[simp]

theorem rack.act_symm_apply {R : Type u_1} [rack R] (x y : R) :

⇑((rack.act x).symm) y = x ◃⁻¹ y

@[simp]

theorem rack.inv_act_apply {R : Type u_1} [rack R] (x y : R) :

⇑(rack.act x)⁻¹ y = x ◃⁻¹ y

@[simp]

theorem rack.inv_act_act_eq {R : Type u_1} [rack R] (x y : R) :

x ◃⁻¹ x ◃ y = y

@[simp]

theorem rack.act_inv_act_eq {R : Type u_1} [rack R] (x y : R) :

x ◃ x ◃⁻¹ y = y

theorem rack.left_cancel {R : Type u_1} [rack R] (x : R) {y y' : R} :

x ◃ y = x ◃ y' ↔ y = y'

theorem rack.left_cancel_inv {R : Type u_1} [rack R] (x : R) {y y' : R} :

x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'

theorem rack.self_distrib_inv {R : Type u_1} [rack R] {x y z : R} :

x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z

theorem rack.ad_conj {R : Type u_1} [rack R] (x y : R) :

rack.act (x ◃ y) = ((rack.act x) * rack.act y) * (rack.act x)⁻¹

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

@[instance]

def rack.opposite_rack {R : Type u_1} [rack R] :

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

Equations

rack.opposite_rack = {to_shelf := {act := λ (x y : Rᵒᵖ), opposite.op (opposite.unop x ◃⁻¹ opposite.unop y), self_distrib := _}, inv_act := λ (x y : Rᵒᵖ), opposite.op (opposite.unop x ◃ opposite.unop y), left_inv := _, right_inv := _}

@[simp]

theorem rack.op_act_op_eq {R : Type u_1} [rack R] {x y : R} :

opposite.op x ◃ opposite.op y = opposite.op (x ◃⁻¹ y)

@[simp]

theorem rack.op_inv_act_op_eq {R : Type u_1} [rack R] {x y : R} :

opposite.op x ◃⁻¹ opposite.op y = opposite.op (x ◃ y)

@[simp]

theorem rack.self_act_act_eq {R : Type u_1} [rack R] {x y : R} :

(x ◃ x) ◃ y = x ◃ y

@[simp]

theorem rack.self_inv_act_inv_act_eq {R : Type u_1} [rack R] {x y : R} :

(x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y

@[simp]

theorem rack.self_act_inv_act_eq {R : Type u_1} [rack R] {x y : R} :

(x ◃ x) ◃⁻¹ y = x ◃⁻¹ y

@[simp]

theorem rack.self_inv_act_act_eq {R : Type u_1} [rack R] {x y : R} :

(x ◃⁻¹ x) ◃ y = x ◃ y

theorem rack.self_act_eq_iff_eq {R : Type u_1} [rack R] {x y : R} :

x ◃ x = y ◃ y ↔ x = y

theorem rack.self_inv_act_eq_iff_eq {R : Type u_1} [rack R] {x y : R} :

x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y

def rack.self_apply_equiv (R : Type u_1) [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

rack.self_apply_equiv R = {to_fun := λ (x : R), x ◃ x, inv_fun := λ (x : R), x ◃⁻¹ x, left_inv := _, right_inv := _}

def rack.is_involutory (R : Type u_1) [rack R] :

Prop

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)

theorem rack.involutory_inv_act_eq_act {R : Type u_1} [rack R] (h : rack.is_involutory R) (x y : R) :

x ◃⁻¹ y = x ◃ y

def rack.is_abelian (R : Type u_1) [rack R] :

Prop

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

Equations

rack.is_abelian R = ∀ (x y z w : R), (x ◃ y) ◃ z ◃ w = (x ◃ z) ◃ y ◃ w

theorem rack.assoc_iff_id {R : Type u_1} [rack R] {x y z : R} :

x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Associative racks are uninteresting.

@[instance]

def shelf_hom.has_coe_to_fun {S₁ : Type u_1} {S₂ : Type u_2} [shelf S₁] [shelf S₂] :

has_coe_to_fun (S₁ →◃ S₂)

Equations

shelf_hom.has_coe_to_fun = {F := λ (x : S₁ →◃ S₂), S₁ → S₂, coe := shelf_hom.to_fun _inst_2}

@[simp]

theorem shelf_hom.to_fun_eq_coe {S₁ : Type u_1} {S₂ : Type u_2} [shelf S₁] [shelf S₂] (f : S₁ →◃ S₂) :

f.to_fun = ⇑f

@[simp]

theorem shelf_hom.map_act {S₁ : Type u_1} {S₂ : Type u_2} [shelf S₁] [shelf S₂] (f : S₁ →◃ S₂) {x y : S₁} :

⇑f (x ◃ y) = ⇑f x ◃ ⇑f y

def shelf_hom.id (S : Type u_1) [shelf S] :

The identity homomorphism

Equations

shelf_hom.id S = {to_fun := id S, map_act' := _}

@[instance]

def shelf_hom.inhabited (S : Type u_1) [shelf S] :

inhabited (S →◃ S)

Equations

shelf_hom.inhabited S = {default := shelf_hom.id S _inst_4}

def shelf_hom.comp {S₁ : Type u_1} {S₂ : Type u_2} {S₃ : Type u_3} [shelf S₁] [shelf S₂] [shelf S₃] (g : S₂ →◃ S₃) (f : S₁ →◃ S₂) :

S₁ →◃ S₃

The composition of shelf homomorphisms

Equations

g.comp f = {to_fun := g.to_fun ∘ f.to_fun, map_act' := _}

@[simp]

theorem shelf_hom.comp_apply {S₁ : Type u_1} {S₂ : Type u_2} {S₃ : Type u_3} [shelf S₁] [shelf S₂] [shelf S₃] (g : S₂ →◃ S₃) (f : S₁ →◃ S₂) (x : S₁) :

⇑(g.comp f) x = ⇑g (⇑f x)

@[class]

structure quandle (α : Type u_1) :

Type u_1

to_rack : rack α
fix : ∀ {x : α}, x ◃ x = x

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

Instances

@[simp]

theorem quandle.fix_inv {Q : Type u_1} [quandle Q] {x : Q} :

x ◃⁻¹ x = x

@[instance]

def quandle.opposite_quandle {Q : Type u_1} [quandle Q] :

quandle Qᵒᵖ

Equations

quandle.opposite_quandle = {to_rack := rack.opposite_rack quandle.to_rack, fix := _}

@[nolint]

def quandle.conj (G : Type u_1) :

Type u_1

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

Equations

quandle.conj G = G

@[instance]

def quandle.conj.quandle (G : Type u_1) [group G] :

quandle (quandle.conj G)

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 := _}

@[simp]

theorem quandle.conj_act_eq_conj {G : Type u_1} [group G] (x y : quandle.conj G) :

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

theorem quandle.conj_swap {G : Type u_1} [group G] (x y : quandle.conj G) :

x ◃ y = y ↔ y ◃ x = x

def quandle.conj.map {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G →* H) :

quandle.conj G →◃ quandle.conj H

conj is functorial

Equations

quandle.conj.map f = {to_fun := ⇑f, map_act' := _}

@[instance]

def quandle.has_lift {G : Type u_1} {H : Type u_2} [group G] [group H] :

has_lift (G →* H) (quandle.conj G →◃ quandle.conj H)

Equations

quandle.has_lift = {lift := quandle.conj.map _inst_3}

@[nolint]

def quandle.dihedral (n : ℕ) :

Type

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

def quandle.dihedral_act (n : ℕ) (a a_1 : zmod n) :

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

Equations

quandle.dihedral_act n a = λ (b : zmod n), 2 * a - b

theorem quandle.dihedral_act.inv (n : ℕ) (a : zmod n) :

function.involutive (quandle.dihedral_act n a)

@[instance]

def quandle.quandle (n : ℕ) :

quandle (quandle.dihedral n)

Equations

quandle.quandle n = {to_rack := {to_shelf := {act := quandle.dihedral_act n, self_distrib := _}, inv_act := quandle.dihedral_act n, left_inv := _, right_inv := _}, fix := _}

def rack.to_conj (R : Type u_1) [rack R] :

R →◃ quandle.conj (R ≃ R)

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

Equations

rack.to_conj R = {to_fun := rack.act _inst_1, map_act' := _}

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.

inductive rack.pre_envel_group (R : Type u) :

Type u

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.

@[instance]

def rack.pre_envel_group.inhabited (R : Type u) :

inhabited (rack.pre_envel_group R)

Equations

rack.pre_envel_group.inhabited R = {default := rack.pre_envel_group.unit R}

inductive rack.pre_envel_group_rel' (R : Type u) [rack R] (a a_1 : rack.pre_envel_group R) :

Type u

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

@[instance]

def rack.pre_envel_group_rel'.inhabited (R : Type u) [rack R] :

inhabited (rack.pre_envel_group_rel' R rack.pre_envel_group.unit rack.pre_envel_group.unit)

Equations

rack.pre_envel_group_rel'.inhabited R = {default := rack.pre_envel_group_rel'.refl rack.pre_envel_group.unit}

inductive rack.pre_envel_group_rel (R : Type u) [rack R] (a a_1 : rack.pre_envel_group R) :

Prop

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.

theorem rack.pre_envel_group_rel'.rel {R : Type u} [rack R] {a b : rack.pre_envel_group R} (a_1 : rack.pre_envel_group_rel' R a b) :

rack.pre_envel_group_rel R a b

A quick way to convert a pre_envel_group_rel' to a pre_envel_group_rel.

theorem rack.pre_envel_group_rel.refl {R : Type u} [rack R] {a : rack.pre_envel_group R} :

rack.pre_envel_group_rel R a a

theorem rack.pre_envel_group_rel.symm {R : Type u} [rack R] {a b : rack.pre_envel_group R} (a_1 : rack.pre_envel_group_rel R a b) :

rack.pre_envel_group_rel R b a

theorem rack.pre_envel_group_rel.trans {R : Type u} [rack R] {a b c : rack.pre_envel_group R} (a_1 : rack.pre_envel_group_rel R a b) (a_2 : rack.pre_envel_group_rel R b c) :

rack.pre_envel_group_rel R a c

@[instance]

def rack.pre_envel_group.setoid (R : Type u_1) [rack R] :

setoid (rack.pre_envel_group R)

Equations

rack.pre_envel_group.setoid R = {r := rack.pre_envel_group_rel R _inst_1, iseqv := _}

def rack.envel_group (R : Type u_1) [rack R] :

Type u_1

The universal enveloping group for the rack R.

Equations

rack.envel_group R = quotient (rack.pre_envel_group.setoid R)

@[instance]

def rack.group (R : Type u_1) [rack R] :

group (rack.envel_group R)

Equations

rack.group 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 := _, inv := λ (a : rack.envel_group R), quotient.lift_on a (λ (a : rack.pre_envel_group R), ⟦a.inv ⟧) _, mul_left_inv := _}

@[instance]

def rack.envel_group.inhabited (R : Type u_1) [rack R] :

inhabited (rack.envel_group R)

Equations

rack.envel_group.inhabited R = {default := 1}

def rack.to_envel_group (R : Type u_1) [rack R] :

R →◃ quandle.conj (rack.envel_group R)

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' := _}

def rack.to_envel_group.map_aux {R : Type u_1} [rack R] {G : Type u_2} [group G] (f : R →◃ quandle.conj G) (a : rack.pre_envel_group R) :

G

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

theorem rack.to_envel_group.map_aux.well_def {R : Type u_1} [rack R] {G : Type u_2} [group G] (f : R →◃ quandle.conj G) {a b : rack.pre_envel_group R} (a_1 : rack.pre_envel_group_rel' R a b) :

rack.to_envel_group.map_aux f a = rack.to_envel_group.map_aux f b

Show that to_envel_group.map_aux sends equivalent expressions to equal terms.

def rack.to_envel_group.map {R : Type u_1} [rack R] {G : Type u_2} [group G] (f : R →◃ quandle.conj G) :

rack.envel_group R →* G

Given a map from a rack to a group, lift it to being a map from the enveloping group.

Equations

rack.to_envel_group.map f = {to_fun := λ (x : rack.envel_group R), quotient.lift_on x (rack.to_envel_group.map_aux f) _, map_one' := _, map_mul' := _}

theorem rack.to_envel_group.univ (R : Type u_1) [rack R] (G : Type u_2) [group G] (f : R →◃ quandle.conj G) :

(quandle.conj.map (rack.to_envel_group.map f)).comp (rack.to_envel_group R) = f

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

theorem rack.to_envel_group.univ_uniq (R : Type u_1) [rack R] (G : Type u_2) [group G] (f : R →◃ quandle.conj G) (g : rack.envel_group R →* G) (h : f = (quandle.conj.map g).comp (rack.to_envel_group R)) :

g = rack.to_envel_group.map f

The homomorphism to_envel_group.map f is the unique map that fits into the commutative triangle in to_envel_group.univ.

def rack.envel_action {R : Type u_1} [rack R] :

rack.envel_group R →* R ≃ R

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.

Equations

rack.envel_action = rack.to_envel_group.map (rack.to_conj R)

@[simp]

theorem rack.envel_action_prop {R : Type u_1} [rack R] (x y : R) :

⇑(⇑rack.envel_action (⇑(rack.to_envel_group R) x)) y = x ◃ y