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 : α}, act x (act y z) = act (act x y) (act x z)) → Shelf α
Shelf
(
α: Type u
α
:
Type u: Type (u+1)
Type u
) where /-- The action of the `Shelf` over `α`-/
act: {α : Type u} → [self : Shelf α] → α → α → α
act
:
α: Type u
α
→
α: Type u
α
→
α: Type u
α
/--A verification that `act` is self-distributive-/
self_distrib: ∀ {α : Type u} [self : Shelf α] {x y z : α}, Shelf.act x (Shelf.act y z) = Shelf.act (Shelf.act x y) (Shelf.act x z)
self_distrib
: ∀ {
x: α
x
y: α
y
z: α
z
:
α: Type u
α
},
act: α → α → α
act
x: α
x
(
act: α → α → α
act
y: α
y
z: α
z
) =
act: α → α → α
act
(
act: α → α → α
act
x: α
x
y: α
y
) (
act: α → α → α
act
x: α
x
z: α
z
) #align shelf
Shelf: Type u → Type u
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
UnitalShelf: {α : Type u} → [toShelf : Shelf α] → [toOne : One α] → (∀ (a : α), Shelf.act 1 a = a) → (∀ (a : α), Shelf.act a 1 = a) → UnitalShelf α
UnitalShelf
(
α: Type u
α
:
Type u: Type (u+1)
Type u
) extends
Shelf: Type ?u.32 → Type ?u.32
Shelf
α: Type u
α
,
One: Type ?u.37 → Type ?u.37
One
α: Type u
α
:= (
one_act: ∀ {α : Type u} [self : UnitalShelf α] (a : α), Shelf.act 1 a = a
one_act
: ∀
a: α
a
:
α: Type u
α
,
act: α → α → α
act
1: ?m.46
1
a: α
a
=
a: α
a
) (
act_one: ∀ {α : Type u} [self : UnitalShelf α] (a : α), Shelf.act a 1 = a
act_one
: ∀
a: α
a
:
α: Type u
α
,
act: α → α → α
act
a: α
a
1: ?m.80
1
=
a: α
a
) #align unital_shelf
UnitalShelf: Type u → Type u
UnitalShelf
/-- The type of homomorphisms between shelves. This is also the notion of rack and quandle homomorphisms. -/ @[ext] structure
ShelfHom: (S₁ : Type u_1) → (S₂ : Type u_2) → [inst : Shelf S₁] → [inst : Shelf S₂] → Type (maxu_1u_2)
ShelfHom
(
S₁: Type ?u.110
S₁
:
Type _: Type (?u.110+1)
Type _
) (
S₂: Type ?u.113
S₂
:
Type _: Type (?u.113+1)
Type _
) [
Shelf: Type ?u.116 → Type ?u.116
Shelf
S₁: Type ?u.110
S₁
] [
Shelf: Type ?u.119 → Type ?u.119
Shelf
S₂: Type ?u.113
S₂
] where /-- The function under the Shelf Homomorphism -/
toFun: {S₁ : Type u_1} → {S₂ : Type u_2} → [inst : Shelf S₁] → [inst_1 : Shelf S₂] → ShelfHom S₁ S₂ → S₁ → S₂
toFun
:
S₁: Type ?u.110
S₁
→
S₂: Type ?u.113
S₂
/-- The homomorphism property of a Shelf Homomorphism-/
map_act': ∀ {S₁ : Type u_1} {S₂ : Type u_2} [inst : Shelf S₁] [inst_1 : Shelf S₂] (self : ShelfHom S₁ S₂) {x y : S₁}, ShelfHom.toFun self (Shelf.act x y) = Shelf.act (ShelfHom.toFun self x) (ShelfHom.toFun self y)
map_act'
: ∀ {
x: S₁
x
y: S₁
y
:
S₁: Type ?u.110
S₁
},
toFun: S₁ → S₂
toFun
(
Shelf.act: {α : Type ?u.134} → [self : Shelf α] → α → α → α
Shelf.act
x: S₁
x
y: S₁
y
) =
Shelf.act: {α : Type ?u.144} → [self : Shelf α] → α → α → α
Shelf.act
(
toFun: S₁ → S₂
toFun
x: S₁
x
) (
toFun: S₁ → S₂
toFun
y: S₁
y
) #align shelf_hom
ShelfHom: (S₁ : Type u_1) → (S₂ : Type u_2) → [inst : Shelf S₁] → [inst : Shelf S₂] → Type (maxu_1u_2)
ShelfHom
#align shelf_hom.ext_iff
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
ShelfHom.ext_iff
#align shelf_hom.ext
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.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
Rack: {α : Type u} → [toShelf : Shelf α] → (invAct : α → α → α) → (∀ (x : α), Function.LeftInverse (invAct x) (Shelf.act x)) → (∀ (x : α), Function.RightInverse (invAct x) (Shelf.act x)) → Rack α
Rack
(
α: Type u
α
:
Type u: Type (u+1)
Type u
) extends
Shelf: Type ?u.524 → Type ?u.524
Shelf
α: Type u
α
where /-- The inverse actions of the elements -/
invAct: {α : Type u} → [self : Rack α] → α → α → α
invAct
:
α: Type u
α
→
α: Type u
α
→
α: Type u
α
/-- Proof of left inverse -/
left_inv: ∀ {α : Type u} [self : Rack α] (x : α), Function.LeftInverse (Rack.invAct x) (Shelf.act x)
left_inv
: ∀
x: ?m.536
x
,
Function.LeftInverse: {α : Sort ?u.540} → {β : Sort ?u.539} → (β → α) → (α → β) → Prop
Function.LeftInverse
(
invAct: α → α → α
invAct
x: ?m.536
x
) (
act: α → α → α
act
x: ?m.536
x
) /-- Proof of right inverse -/
right_inv: ∀ {α : Type u} [self : Rack α] (x : α), Function.RightInverse (Rack.invAct x) (Shelf.act x)
right_inv
: ∀
x: ?m.557
x
,
Function.RightInverse: {α : Sort ?u.561} → {β : Sort ?u.560} → (β → α) → (α → β) → Prop
Function.RightInverse
(
invAct: α → α → α
invAct
x: ?m.557
x
) (
act: α → α → α
act
x: ?m.557
x
) #align rack
Rack: Type u → Type u
Rack
/-- Action of a Shelf-/ scoped[Quandles] infixr:65 " ◃ " =>
Shelf.act: {α : Type u} → [self : Shelf α] → α → α → α
Shelf.act
/-- Inverse Action of a Rack-/ scoped[Quandles] infixr:65 " ◃⁻¹ " =>
Rack.invAct: {α : Type u} → [self : Rack α] → α → α → α
Rack.invAct
/-- Shelf Homomorphism-/ scoped[Quandles] infixr:25 " →◃ " =>
ShelfHom: (S₁ : Type u_1) → (S₂ : Type u_2) → [inst : Shelf S₁] → [inst : Shelf S₂] → Type (maxu_1u_2)
ShelfHom
open Quandles namespace UnitalShelf open Shelf variable {
S: Type ?u.24347
S
:
Type _: Type (?u.24347+1)
Type _
} [
UnitalShelf: Type ?u.24350 → Type ?u.24350
UnitalShelf
S: Type ?u.24347
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
act_act_self_eq: ∀ (x y : S), (x ◃ y) ◃ x = x ◃ y
act_act_self_eq
(
x: S
x
y: S
y
:
S: Type ?u.24111
S
) : (
x: S
x
◃
y: S
y
) ◃
x: S
x
=
x: S
x
◃
y: S
y
:=

Goals accomplished! 🐙
S: Type u_1

inst✝: UnitalShelf S

x, y: S


(x ◃ y) ◃ x = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S


(x ◃ y) ◃ x = x ◃ y

Goals accomplished! 🐙
S: Type u_1

inst✝: UnitalShelf S

x, y: S


(x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
S: Type u_1

inst✝: UnitalShelf S

x, y: S


(x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1
S: Type u_1

inst✝: UnitalShelf S

x, y: S


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

Goals accomplished! 🐙
S: Type u_1

inst✝: UnitalShelf S

x, y: S


(x ◃ y) ◃ x = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1


(x ◃ y) ◃ x = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1


(x ◃ y) ◃ x ◃ 1 = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1


(x ◃ y) ◃ x = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1


x ◃ y ◃ 1 = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1


(x ◃ y) ◃ x = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: (x ◃ y) ◃ x = (x ◃ y) ◃ x ◃ 1


x ◃ y = x ◃ y

Goals accomplished! 🐙
#align unital_shelf.act_act_self_eq
UnitalShelf.act_act_self_eq: ∀ {S : Type u_1} [inst : UnitalShelf S] (x y : S), (x ◃ y) ◃ x = x ◃ y
UnitalShelf.act_act_self_eq
lemma
act_idem: ∀ {S : Type u_1} [inst : UnitalShelf S] (x : S), x ◃ x = x
act_idem
(
x: S
x
:
S: Type ?u.24347
S
) : (
x: S
x
◃
x: S
x
) =
x: S
x
:=

Goals accomplished! 🐙
S: Type u_1

inst✝: UnitalShelf S

x: S


x ◃ x = x
S: Type u_1

inst✝: UnitalShelf S

x: S


x ◃ x = x
S: Type u_1

inst✝: UnitalShelf S

x: S


(x ◃ 1) ◃ x ◃ 1 = x ◃ 1
S: Type u_1

inst✝: UnitalShelf S

x: S


x ◃ x = x
S: Type u_1

inst✝: UnitalShelf S

x: S


x ◃ 1 ◃ 1 = x ◃ 1
S: Type u_1

inst✝: UnitalShelf S

x: S


x ◃ x = x
S: Type u_1

inst✝: UnitalShelf S

x: S


x ◃ 1 = x ◃ 1
S: Type u_1

inst✝: UnitalShelf S

x: S


x ◃ x = x
S: Type u_1

inst✝: UnitalShelf S

x: S


x = x

Goals accomplished! 🐙
#align unital_shelf.act_idem
UnitalShelf.act_idem: ∀ {S : Type u_1} [inst : UnitalShelf S] (x : S), x ◃ x = x
UnitalShelf.act_idem
lemma
act_self_act_eq: ∀ {S : Type u_1} [inst : UnitalShelf S] (x y : S), x ◃ x ◃ y = x ◃ y
act_self_act_eq
(
x: S
x
y: S
y
:
S: Type ?u.24475
S
) :
x: S
x
◃ (
x: S
x
◃
y: S
y
) =
x: S
x
◃
y: S
y
:=

Goals accomplished! 🐙
S: Type u_1

inst✝: UnitalShelf S

x, y: S


x ◃ x ◃ y = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S


x ◃ x ◃ y = x ◃ y

Goals accomplished! 🐙
S: Type u_1

inst✝: UnitalShelf S

x, y: S


x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S


x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S



Goals accomplished! 🐙
S: Type u_1

inst✝: UnitalShelf S

x, y: S


x ◃ x ◃ y = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y


x ◃ x ◃ y = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y


(x ◃ 1) ◃ x ◃ y = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y


x ◃ x ◃ y = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y


x ◃ 1 ◃ y = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y


x ◃ x ◃ y = x ◃ y
S: Type u_1

inst✝: UnitalShelf S

x, y: S

h: x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y


x ◃ y = x ◃ y

Goals accomplished! 🐙
#align unital_shelf.act_self_act_eq
UnitalShelf.act_self_act_eq: ∀ {S : Type u_1} [inst : UnitalShelf S] (x y : S), x ◃ x ◃ y = x ◃ y
UnitalShelf.act_self_act_eq
/-- The associativity of a unital shelf comes for free. -/ lemma
assoc: ∀ (x y z : S), (x ◃ y) ◃ z = x ◃ y ◃ z
assoc
(
x: S
x
y: S
y
z: S
z
:
S: Type ?u.24709
S
) : (
x: S
x
◃
y: S
y
) ◃
z: S
z
=
x: S
x
◃
y: S
y
◃
z: S
z
:=

Goals accomplished! 🐙
S: Type u_1

inst✝: UnitalShelf S

x, y, z: S


(x ◃ y) ◃ z = x ◃ y ◃ z
S: Type u_1

inst✝: UnitalShelf S

x, y, z: S


(x ◃ y) ◃ z = x ◃ y ◃ z
S: Type u_1

inst✝: UnitalShelf S

x, y, z: S


(x ◃ y) ◃ z = (x ◃ y) ◃ x ◃ z
S: Type u_1

inst✝: UnitalShelf S

x, y, z: S


(x ◃ y) ◃ z = x ◃ y ◃ z
S: Type u_1

inst✝: UnitalShelf S

x, y, z: S


(x ◃ y) ◃ z = ((x ◃ y) ◃ x) ◃ (x ◃ y) ◃ z
S: Type u_1

inst✝: UnitalShelf S

x, y, z: S


(x ◃ y) ◃ z = x ◃ y ◃ z
S: Type u_1

inst✝: UnitalShelf S

x, y, z: S


(x ◃ y) ◃ z = (x ◃ y) ◃ (x ◃ y) ◃ z
S: Type u_1

inst✝: UnitalShelf S

x, y, z: S


(x ◃ y) ◃ z = x ◃ y ◃ z
S: Type u_1

inst✝: UnitalShelf S

x, y, z: S


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

Goals accomplished! 🐙
#align unital_shelf.assoc
UnitalShelf.assoc: ∀ {S : Type u_1} [inst : UnitalShelf S] (x y z : S), (x ◃ y) ◃ z = x ◃ y ◃ z
UnitalShelf.assoc
end UnitalShelf namespace Rack variable {
R: Type ?u.24951
R
:
Type _: Type (?u.29184+1)
Type _
} [
Rack: Type ?u.24954 → Type ?u.24954
Rack
R: Type ?u.24951
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
act': {R : Type u_1} → [inst : Rack R] → R → R ≃ R
act'
(
x: R
x
:
R: Type ?u.24957
R
) :
R: Type ?u.24957
R
≃
R: Type ?u.24957
R
where toFun :=
Shelf.act: {α : Type ?u.24975} → [self : Shelf α] → α → α → α
Shelf.act
x: R
x
invFun :=
invAct: {α : Type ?u.25000} → [self : Rack α] → α → α → α
invAct
x: R
x
left_inv :=
left_inv: ∀ {α : Type ?u.25011} [self : Rack α] (x : α), Function.LeftInverse (invAct x) (Shelf.act x)
left_inv
x: R
x
right_inv :=
right_inv: ∀ {α : Type ?u.25021} [self : Rack α] (x : α), Function.RightInverse (invAct x) (Shelf.act x)
right_inv
x: R
x
#align rack.act
Rack.act': {R : Type u_1} → [inst : Rack R] → R → R ≃ R
Rack.act'
@[simp] theorem
act'_apply: ∀ (x y : R), ↑(act' x) y = x ◃ y
act'_apply
(
x: R
x
y: R
y
:
R: Type ?u.25088
R
) :
act': {R : Type ?u.25099} → [inst : Rack R] → R → R ≃ R
act'
x: R
x
y: R
y
=
x: R
x
◃
y: R
y
:=
rfl: ∀ {α : Sort ?u.25211} {a : α}, a = a
rfl
#align rack.act_apply
Rack.act'_apply: ∀ {R : Type u_1} [inst : Rack R] (x y : R), ↑(act' x) y = x ◃ y
Rack.act'_apply
@[simp] theorem
act'_symm_apply: ∀ {R : Type u_1} [inst : Rack R] (x y : R), ↑(act' x).symm y = x ◃⁻¹ y
act'_symm_apply
(
x: R
x
y: R
y
:
R: Type ?u.25246
R
) : (
act': {R : Type ?u.25257} → [inst : Rack R] → R → R ≃ R
act'
x: R
x
).
symm: {α : Sort ?u.25264} → {β : Sort ?u.25263} → α ≃ β → β ≃ α
symm
y: R
y
=
x: R
x
◃⁻¹
y: R
y
:=
rfl: ∀ {α : Sort ?u.25368} {a : α}, a = a
rfl
#align rack.act_symm_apply
Rack.act'_symm_apply: ∀ {R : Type u_1} [inst : Rack R] (x y : R), ↑(act' x).symm y = x ◃⁻¹ y
Rack.act'_symm_apply
@[simp] theorem
invAct_apply: ∀ {R : Type u_1} [inst : Rack R] (x y : R), ↑(act' x)⁻¹ y = x ◃⁻¹ y
invAct_apply
(
x: R
x
y: R
y
:
R: Type ?u.25406
R
) : (
act': {R : Type ?u.25420} → [inst : Rack R] → R → R ≃ R
act'
x: R
x
)⁻¹
y: R
y
=
x: R
x
◃⁻¹
y: R
y
:=
rfl: ∀ {α : Sort ?u.25653} {a : α}, a = a
rfl
#align rack.inv_act_apply
Rack.invAct_apply: ∀ {R : Type u_1} [inst : Rack R] (x y : R), ↑(act' x)⁻¹ y = x ◃⁻¹ y
Rack.invAct_apply
@[simp] theorem
invAct_act_eq: ∀ {R : Type u_1} [inst : Rack R] (x y : R), x ◃⁻¹ x ◃ y = y
invAct_act_eq
(
x: R
x
y: R
y
:
R: Type ?u.25691
R
) :
x: R
x
◃⁻¹
x: R
x
◃
y: R
y
=
y: R
y
:=
left_inv: ∀ {α : Type ?u.25730} [self : Rack α] (x : α), Function.LeftInverse (invAct x) (Shelf.act x)
left_inv
x: R
x
y: R
y
#align rack.inv_act_act_eq
Rack.invAct_act_eq: ∀ {R : Type u_1} [inst : Rack R] (x y : R), x ◃⁻¹ x ◃ y = y
Rack.invAct_act_eq
@[simp] theorem
act_invAct_eq: ∀ {R : Type u_1} [inst : Rack R] (x y : R), x ◃ x ◃⁻¹ y = y
act_invAct_eq
(
x: R
x
y: R
y
:
R: Type ?u.25760
R
) :
x: R
x
◃
x: R
x
◃⁻¹
y: R
y
=
y: R
y
:=
right_inv: ∀ {α : Type ?u.25794} [self : Rack α] (x : α), Function.RightInverse (invAct x) (Shelf.act x)
right_inv
x: R
x
y: R
y
#align rack.act_inv_act_eq
Rack.act_invAct_eq: ∀ {R : Type u_1} [inst : Rack R] (x y : R), x ◃ x ◃⁻¹ y = y
Rack.act_invAct_eq
theorem
left_cancel: ∀ (x : R) {y y' : R}, x ◃ y = x ◃ y' ↔ y = y'
left_cancel
(
x: R
x
:
R: Type ?u.25824
R
) {
y: R
y
y': R
y'
:
R: Type ?u.25824
R
} :
x: R
x
◃
y: R
y
=
x: R
x
◃
y': R
y'
↔
y: R
y
=
y': R
y'
:=

Goals accomplished! 🐙
R: Type u_1

inst✝: Rack R

x, y, y': R


x ◃ y = x ◃ y' ↔ y = y'
R: Type u_1

inst✝: Rack R

x, y, y': R


mp
x ◃ y = x ◃ y' → y = y'
R: Type u_1

inst✝: Rack R

x, y, y': R


mpr
y = y' → x ◃ y = x ◃ y'
R: Type u_1

inst✝: Rack R

x, y, y': R


x ◃ y = x ◃ y' ↔ y = y'
R: Type u_1

inst✝: Rack R

x, y, y': R


mpr
y = y' → x ◃ y = x ◃ y'
R: Type u_1

inst✝: Rack R

x, y, y': R


x ◃ y = x ◃ y' ↔ y = y'
R: Type u_1

inst✝: Rack R

x, y: R


mpr
x ◃ y = x ◃ y
R: Type u_1

inst✝: Rack R

x, y, y': R


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

Goals accomplished! 🐙
#align rack.left_cancel
Rack.left_cancel: ∀ {R : Type u_1} [inst : Rack R] (x : R) {y y' : R}, x ◃ y = x ◃ y' ↔ y = y'
Rack.left_cancel
theorem
left_cancel_inv: ∀ (x : R) {y y' : R}, x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'
left_cancel_inv
(
x: R
x
:
R: Type ?u.25925
R
) {
y: R
y
y': R
y'
:
R: Type ?u.25925
R
} :
x: R
x
◃⁻¹
y: R
y
=
x: R
x
◃⁻¹
y': R
y'
↔
y: R
y
=
y': R
y'
:=

Goals accomplished! 🐙
R: Type u_1

inst✝: Rack R

x, y, y': R


R: Type u_1

inst✝: Rack R

x, y, y': R


mp
x ◃⁻¹ y = x ◃⁻¹ y' → y = y'
R: Type u_1

inst✝: Rack R

x, y, y': R


mpr
y = y' → x ◃⁻¹ y = x ◃⁻¹ y'
R: Type u_1

inst✝: Rack R

x, y, y': R


R: Type u_1

inst✝: Rack R

x, y, y': R


mpr
y = y' → x ◃⁻¹ y = x ◃⁻¹ y'
R: Type u_1

inst✝: Rack R

x, y, y': R


R: Type u_1

inst✝: Rack R

x, y: R


mpr
R: Type u_1

inst✝: Rack R

x, y, y': R



Goals accomplished! 🐙
#align rack.left_cancel_inv
Rack.left_cancel_inv: ∀ {R : Type u_1} [inst : Rack R] (x : R) {y y' : R}, x ◃⁻¹ y = x ◃⁻¹ y' ↔ y = y'
Rack.left_cancel_inv
theorem
self_distrib_inv: ∀ {x y z : R}, x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z
self_distrib_inv
{
x: R
x
y: R
y
z: R
z
:
R: Type ?u.26023
R
} :
x: R
x
◃⁻¹
y: R
y
◃⁻¹
z: R
z
= (
x: R
x
◃⁻¹
y: R
y
) ◃⁻¹
x: R
x
◃⁻¹
z: R
z
:=

Goals accomplished! 🐙
R: Type u_1

inst✝: Rack R

x, y, z: R


R: Type u_1

inst✝: Rack R

x, y, z: R


R: Type u_1

inst✝: Rack R

x, y, z: R


R: Type u_1

inst✝: Rack R

x, y, z: R


R: Type u_1

inst✝: Rack R

x, y, z: R


R: Type u_1

inst✝: Rack R

x, y, z: R


z = z

Goals accomplished! 🐙
#align rack.self_distrib_inv
Rack.self_distrib_inv: ∀ {R : Type u_1} [inst : Rack R] {x y z : R}, x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z
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
ad_conj: ∀ {R : Type u_1} [inst : Rack R] (x y : R), act' (x ◃ y) = act' x * act' y * (act' x)⁻¹
ad_conj
{
R: Type u_1
R
:
Type _: Type (?u.26289+1)
Type _
} [
Rack: Type ?u.26292 → Type ?u.26292
Rack
R: Type ?u.26289
R
] (
x: R
x
y: R
y
:
R: Type ?u.26289
R
) :
act': {R : Type ?u.26300} → [inst : Rack R] → R → R ≃ R
act'
(
x: R
x
◃
y: R
y
) =
act': {R : Type ?u.26330} → [inst : Rack R] → R → R ≃ R
act'
x: R
x
*
act': {R : Type ?u.26333} → [inst : Rack R] → R → R ≃ R
act'
y: R
y
* (
act': {R : Type ?u.26339} → [inst : Rack R] → R → R ≃ R
act'
x: R
x
)⁻¹ :=

Goals accomplished! 🐙
R✝: Type ?u.26283

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y: R


R✝: Type ?u.26283

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y: R


R✝: Type ?u.26283

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y: R


act' (x ◃ y) * act' x = act' x * act' y
R✝: Type ?u.26283

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y: R


act' (x ◃ y) * act' x = act' x * act' y
R✝: Type ?u.26283

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y: R


act' (x ◃ y) * act' x = act' x * act' y
R✝: Type ?u.26283

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y: R


R✝: Type ?u.26283

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y, z: R


H
↑(act' (x ◃ y) * act' x) z = ↑(act' x * act' y) z
R✝: Type ?u.26283

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y: R



Goals accomplished! 🐙
#align rack.ad_conj
Rack.ad_conj: ∀ {R : Type u_1} [inst : Rack R] (x y : R), act' (x ◃ y) = act' x * act' y * (act' x)⁻¹
Rack.ad_conj
/-- The opposite rack, swapping the roles of `◃` and `◃⁻¹`. -/ instance
oppositeRack: Rack Rᵐᵒᵖ
oppositeRack
:
Rack: Type ?u.27758 → Type ?u.27758
Rack
R: Type ?u.27752
R
ᵐᵒᵖ where act
x: ?m.27768
x
y: ?m.27771
y
:=
op: {α : Type ?u.27773} → α → αᵐᵒᵖ
op
(
invAct: {α : Type ?u.27776} → [self : Rack α] → α → α → α
invAct
(
unop: {α : Type ?u.27781} → αᵐᵒᵖ → α
unop
x: ?m.27768
x
) (
unop: {α : Type ?u.27783} → αᵐᵒᵖ → α
unop
y: ?m.27771
y
)) self_distrib :=

Goals accomplished! 🐙
R: Type ?u.27752

inst✝: Rack R


∀ {x y z : Rᵐᵒᵖ}, (fun x y => op (unop x ◃⁻¹ unop y)) x ((fun x y => op (unop x ◃⁻¹ unop y)) y z) = (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) x y) ((fun x y => op (unop x ◃⁻¹ unop y)) x z)
R: Type ?u.27752

inst✝: Rack R

x, y, z: Rᵐᵒᵖ


(fun x y => op (unop x ◃⁻¹ unop y)) x ((fun x y => op (unop x ◃⁻¹ unop y)) y z) = (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) x y) ((fun x y => op (unop x ◃⁻¹ unop y)) x z)
R: Type ?u.27752

inst✝: Rack R


∀ {x y z : Rᵐᵒᵖ}, (fun x y => op (unop x ◃⁻¹ unop y)) x ((fun x y => op (unop x ◃⁻¹ unop y)) y z) = (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) x y) ((fun x y => op (unop x ◃⁻¹ unop y)) x z)
R: Type ?u.27752

inst✝: Rack R

y, z: Rᵐᵒᵖ

X✝: R


h
(fun x y => op (unop x ◃⁻¹ unop y)) (op X✝) ((fun x y => op (unop x ◃⁻¹ unop y)) y z) = (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝) y) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝) z)
R: Type ?u.27752

inst✝: Rack R


∀ {x y z : Rᵐᵒᵖ}, (fun x y => op (unop x ◃⁻¹ unop y)) x ((fun x y => op (unop x ◃⁻¹ unop y)) y z) = (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) x y) ((fun x y => op (unop x ◃⁻¹ unop y)) x z)
R: Type ?u.27752

inst✝: Rack R

z: Rᵐᵒᵖ

X✝¹, X✝: R


h.h
(fun x y => op (unop x ◃⁻¹ unop y)) (op X✝¹) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝) z) = (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝¹) (op X✝)) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝¹) z)
R: Type ?u.27752

inst✝: Rack R


∀ {x y z : Rᵐᵒᵖ}, (fun x y => op (unop x ◃⁻¹ unop y)) x ((fun x y => op (unop x ◃⁻¹ unop y)) y z) = (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) x y) ((fun x y => op (unop x ◃⁻¹ unop y)) x z)
R: Type ?u.27752

inst✝: Rack R

X✝², X✝¹, X✝: R


h.h.h
(fun x y => op (unop x ◃⁻¹ unop y)) (op X✝²) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝¹) (op X✝)) = (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝²) (op X✝¹)) ((fun x y => op (unop x ◃⁻¹ unop y)) (op X✝²) (op X✝))
R: Type ?u.27752

inst✝: Rack R


∀ {x y z : Rᵐᵒᵖ}, (fun x y => op (unop x ◃⁻¹ unop y)) x ((fun x y => op (unop x ◃⁻¹ unop y)) y z) = (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) x y) ((fun x y => op (unop x ◃⁻¹ unop y)) x z)
R: Type ?u.27752

inst✝: Rack R

X✝², X✝¹, X✝: R


h.h.h
X✝² ◃⁻¹ X✝¹ ◃⁻¹ X✝ = (X✝² ◃⁻¹ X✝¹) ◃⁻¹ X✝² ◃⁻¹ X✝
R: Type ?u.27752

inst✝: Rack R


∀ {x y z : Rᵐᵒᵖ}, (fun x y => op (unop x ◃⁻¹ unop y)) x ((fun x y => op (unop x ◃⁻¹ unop y)) y z) = (fun x y => op (unop x ◃⁻¹ unop y)) ((fun x y => op (unop x ◃⁻¹ unop y)) x y) ((fun x y => op (unop x ◃⁻¹ unop y)) x z)
R: Type ?u.27752

inst✝: Rack R

X✝², X✝¹, X✝: R


h.h.h
X✝² ◃⁻¹ X✝¹ ◃⁻¹ X✝ = (X✝² ◃⁻¹ X✝¹) ◃⁻¹ X✝² ◃⁻¹ X✝
R: Type ?u.27752

inst✝: Rack R

X✝², X✝¹, X✝: R


h.h.h
(X✝² ◃⁻¹ X✝¹) ◃⁻¹ X✝² ◃⁻¹ X✝ = (X✝² ◃⁻¹ X✝¹) ◃⁻¹ X✝² ◃⁻¹ X✝

Goals accomplished! 🐙
invAct
x: ?m.27793
x
y: ?m.27796
y
:=
op: {α : Type ?u.27798} → α → αᵐᵒᵖ
op
(
Shelf.act: {α : Type ?u.27800} → [self : Shelf α] → α → α → α
Shelf.act
(
unop: {α : Type ?u.27810} → αᵐᵒᵖ → α
unop
x: ?m.27793
x
) (
unop: {α : Type ?u.27812} → αᵐᵒᵖ → α
unop
y: ?m.27796
y
)) left_inv :=
MulOpposite.rec': ∀ {α : Type ?u.27825} {F : αᵐᵒᵖ → Sort ?u.27826}, (∀ (X : α), F (op X)) → ∀ (X : αᵐᵒᵖ), F X
MulOpposite.rec'
fun
x: ?m.27888
x
=>
MulOpposite.rec': ∀ {α : Type ?u.27890} {F : αᵐᵒᵖ → Sort ?u.27891}, (∀ (X : α), F (op X)) → ∀ (X : αᵐᵒᵖ), F X
MulOpposite.rec'
fun
y: ?m.27952
y
=>

Goals accomplished! 🐙
R: Type ?u.27752

inst✝: Rack R

x, y: R


(fun x y => op (unop x ◃ unop y)) (op x) (op x ◃ op y) = op y

Goals accomplished! 🐙
right_inv :=
MulOpposite.rec': ∀ {α : Type ?u.27856} {F : αᵐᵒᵖ → Sort ?u.27857}, (∀ (X : α), F (op X)) → ∀ (X : αᵐᵒᵖ), F X
MulOpposite.rec'
fun
x: ?m.27920
x
=>
MulOpposite.rec': ∀ {α : Type ?u.27922} {F : αᵐᵒᵖ → Sort ?u.27923}, (∀ (X : α), F (op X)) → ∀ (X : αᵐᵒᵖ), F X
MulOpposite.rec'
fun
y: ?m.27958
y
=>

Goals accomplished! 🐙
R: Type ?u.27752

inst✝: Rack R

x, y: R


op x ◃ (fun x y => op (unop x ◃ unop y)) (op x) (op y) = op y

Goals accomplished! 🐙
#align rack.opposite_rack
Rack.oppositeRack: {R : Type u_1} → [inst : Rack R] → Rack Rᵐᵒᵖ
Rack.oppositeRack
@[simp] theorem
op_act_op_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, op x ◃ op y = op (x ◃⁻¹ y)
op_act_op_eq
{
x: R
x
y: R
y
:
R: Type ?u.28629
R
} :
op: {α : Type ?u.28643} → α → αᵐᵒᵖ
op
x: R
x
◃
op: {α : Type ?u.28646} → α → αᵐᵒᵖ
op
y: R
y
=
op: {α : Type ?u.28662} → α → αᵐᵒᵖ
op
(
x: R
x
◃⁻¹
y: R
y
) :=
rfl: ∀ {α : Sort ?u.28675} {a : α}, a = a
rfl
#align rack.op_act_op_eq
Rack.op_act_op_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, op x ◃ op y = op (x ◃⁻¹ y)
Rack.op_act_op_eq
@[simp] theorem
op_invAct_op_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, op x ◃⁻¹ op y = op (x ◃ y)
op_invAct_op_eq
{
x: R
x
y: R
y
:
R: Type ?u.28705
R
} :
op: {α : Type ?u.28719} → α → αᵐᵒᵖ
op
x: R
x
◃⁻¹
op: {α : Type ?u.28722} → α → αᵐᵒᵖ
op
y: R
y
=
op: {α : Type ?u.28732} → α → αᵐᵒᵖ
op
(
x: R
x
◃
y: R
y
) :=
rfl: ∀ {α : Sort ?u.28756} {a : α}, a = a
rfl
#align rack.op_inv_act_op_eq
Rack.op_invAct_op_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, op x ◃⁻¹ op y = op (x ◃ y)
Rack.op_invAct_op_eq
@[simp] theorem
self_act_act_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, (x ◃ x) ◃ y = x ◃ y
self_act_act_eq
{
x: R
x
y: R
y
:
R: Type ?u.28786
R
} : (
x: R
x
◃
x: R
x
) ◃
y: R
y
=
x: R
x
◃
y: R
y
:=

Goals accomplished! 🐙
R: Type u_1

inst✝: Rack R

x, y: R


(x ◃ x) ◃ y = x ◃ y
R: Type u_1

inst✝: Rack R

x, y: R


(x ◃ x) ◃ y = x ◃ y
R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


(x ◃ x) ◃ y = x ◃ y
R: Type u_1

inst✝: Rack R

x, y: R



Goals accomplished! 🐙
#align rack.self_act_act_eq
Rack.self_act_act_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, (x ◃ x) ◃ y = x ◃ y
Rack.self_act_act_eq
@[simp] theorem
self_invAct_invAct_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y
self_invAct_invAct_eq
{
x: R
x
y: R
y
:
R: Type ?u.28896
R
} : (
x: R
x
◃⁻¹
x: R
x
) ◃⁻¹
y: R
y
=
x: R
x
◃⁻¹
y: R
y
:=

Goals accomplished! 🐙
R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R

h: (op x ◃ op x) ◃ op y = op x ◃ op y


R: Type u_1

inst✝: Rack R

x, y: R



Goals accomplished! 🐙
#align rack.self_inv_act_inv_act_eq
Rack.self_invAct_invAct_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y
Rack.self_invAct_invAct_eq
@[simp] theorem
self_act_invAct_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, (x ◃ x) ◃⁻¹ y = x ◃⁻¹ y
self_act_invAct_eq
{
x: R
x
y: R
y
:
R: Type ?u.29184
R
} : (
x: R
x
◃
x: R
x
) ◃⁻¹
y: R
y
=
x: R
x
◃⁻¹
y: R
y
:=

Goals accomplished! 🐙
R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R


y = y

Goals accomplished! 🐙
#align rack.self_act_inv_act_eq
Rack.self_act_invAct_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, (x ◃ x) ◃⁻¹ y = x ◃⁻¹ y
Rack.self_act_invAct_eq
@[simp] theorem
self_invAct_act_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, (x ◃⁻¹ x) ◃ y = x ◃ y
self_invAct_act_eq
{
x: R
x
y: R
y
:
R: Type ?u.29389
R
} : (
x: R
x
◃⁻¹
x: R
x
) ◃
y: R
y
=
x: R
x
◃
y: R
y
:=

Goals accomplished! 🐙
R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R

h: (op x ◃ op x) ◃⁻¹ op y = op x ◃⁻¹ op y


R: Type u_1

inst✝: Rack R

x, y: R



Goals accomplished! 🐙
#align rack.self_inv_act_act_eq
Rack.self_invAct_act_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, (x ◃⁻¹ x) ◃ y = x ◃ y
Rack.self_invAct_act_eq
theorem
self_act_eq_iff_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, x ◃ x = y ◃ y ↔ x = y
self_act_eq_iff_eq
{
x: R
x
y: R
y
:
R: Type ?u.29687
R
} :
x: R
x
◃
x: R
x
=
y: R
y
◃
y: R
y
↔
x: R
x
=
y: R
y
:=

Goals accomplished! 🐙
R: Type u_1

inst✝: Rack R

x, y: R


x ◃ x = y ◃ y ↔ x = y
R: Type u_1

inst✝: Rack R

x, y: R


mp
x ◃ x = y ◃ y → x = y
R: Type u_1

inst✝: Rack R

x, y: R


mpr
x = y → x ◃ x = y ◃ y
R: Type u_1

inst✝: Rack R

x, y: R


mp
x ◃ x = y ◃ y → x = y
R: Type u_1

inst✝: Rack R

x, y: R


mpr
x = y → x ◃ x = y ◃ y
R: Type u_1

inst✝: Rack R

x, y: R


x ◃ x = y ◃ y ↔ x = y
R: Type u_1

inst✝: Rack R

x, y: R


mpr
x = y → x ◃ x = y ◃ y
R: Type u_1

inst✝: Rack R

x, y: R


mp
x ◃ x = y ◃ y → x = y
R: Type u_1

inst✝: Rack R

x, y: R


mpr
x = y → x ◃ x = y ◃ y
R: Type u_1

inst✝: Rack R

x, y: R


mp
x ◃ x = y ◃ y → x = y
R: Type u_1

inst✝: Rack R

x, y: R


x ◃ x = y ◃ y ↔ x = y
R: Type u_1

inst✝: Rack R

x: R


mpr
x ◃ x = x ◃ x
R: Type u_1

inst✝: Rack R

x, y: R


mp
x ◃ x = y ◃ y → x = y
R: Type u_1

inst✝: Rack R

x: R


mpr
x ◃ x = x ◃ x
R: Type u_1

inst✝: Rack R

x, y: R


mp
x ◃ x = y ◃ y → x = y
R: Type u_1

inst✝: Rack R

x, y: R


x ◃ x = y ◃ y ↔ x = y
R: Type u_1

inst✝: Rack R

x, y: R


mp
x ◃ x = y ◃ y → x = y
R: Type u_1

inst✝: Rack R

x, y: R


x ◃ x = y ◃ y ↔ x = y
R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


mp
x = y
R: Type u_1

inst✝: Rack R

x, y: R


x ◃ x = y ◃ y ↔ x = y
R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R


x ◃ x = y ◃ y ↔ x = y
R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


(x ◃ x) ◃ x = x ◃ x
R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


x ◃ x = x ◃ x
R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R


x ◃ x = y ◃ y ↔ x = y
R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


y ◃ y = (y ◃ y) ◃ y
R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


R: Type u_1

inst✝: Rack R

x, y: R

h: x ◃ x = y ◃ y


y ◃ y = y ◃ y

Goals accomplished! 🐙
#align rack.self_act_eq_iff_eq
Rack.self_act_eq_iff_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, x ◃ x = y ◃ y ↔ x = y
Rack.self_act_eq_iff_eq
theorem
self_invAct_eq_iff_eq: ∀ {R : Type u_1} [inst : Rack R] {x y : R}, x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y
self_invAct_eq_iff_eq
{
x: R
x
y: R
y
:
R: Type ?u.30017
R
} :
x: R
x
◃⁻¹
x: R
x
=
y: R
y
◃⁻¹
y: R
y
↔
x: R
x
=
y: R
y
:=

Goals accomplished! 🐙
R: Type u_1

inst✝: Rack R

x, y: R


R: Type u_1

inst✝: Rack R

x, y: R

h: op x ◃ op x = op y ◃ op y ↔ op x = op y


R: Type u_1

inst✝: Rack R

x, y: R



Goals accomplished! 🐙
#align rack.self_inv_act_eq_iff_eq
Rack.self_invAct_eq_iff_eq: ∀ {R : Type u_1} [inst : Rack R] {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
selfApplyEquiv: (R : Type u_1) → [inst : Rack R] → R ≃ R
selfApplyEquiv
(
R: Type ?u.30361
R
:
Type _: Type (?u.30361+1)
Type _
) [
Rack: Type ?u.30364 → Type ?u.30364
Rack
R: Type ?u.30361
R
] :
R: Type ?u.30361
R
≃
R: Type ?u.30361
R
where toFun
x: ?m.30379
x
:=
x: ?m.30379
x
◃
x: ?m.30379
x
invFun
x: ?m.30404
x
:=
x: ?m.30404
x
◃⁻¹
x: ?m.30404
x
left_inv
x: ?m.30416
x
:=

Goals accomplished! 🐙
R✝: Type ?u.30355

inst✝¹: Rack R✝

R: Type ?u.30361

inst✝: Rack R

x: R


(fun x => x ◃⁻¹ x) ((fun x => x ◃ x) x) = x

Goals accomplished! 🐙
right_inv
x: ?m.30422
x
:=

Goals accomplished! 🐙
R✝: Type ?u.30355

inst✝¹: Rack R✝

R: Type ?u.30361

inst✝: Rack R

x: R


(fun x => x ◃ x) ((fun x => x ◃⁻¹ x) x) = x

Goals accomplished! 🐙
#align rack.self_apply_equiv
Rack.selfApplyEquiv: (R : Type u_1) → [inst : Rack R] → R ≃ R
Rack.selfApplyEquiv
/-- An involutory rack is one for which `Rack.oppositeRack R x` is an involution for every x. -/ def
IsInvolutory: (R : Type ?u.30646) → [inst : Rack R] → Prop
IsInvolutory
(
R: Type ?u.30646
R
:
Type _: Type (?u.30646+1)
Type _
) [
Rack: Type ?u.30649 → Type ?u.30649
Rack
R: Type ?u.30646
R
] :
Prop: Type
Prop
:= ∀
x: R
x
:
R: Type ?u.30646
R
,
Function.Involutive: {α : Sort ?u.30658} → (α → α) → Prop
Function.Involutive
(
Shelf.act: {α : Type ?u.30660} → [self : Shelf α] → α → α → α
Shelf.act
x: R
x
) #align rack.is_involutory
Rack.IsInvolutory: (R : Type u_1) → [inst : Rack R] → Prop
Rack.IsInvolutory
theorem
involutory_invAct_eq_act: ∀ {R : Type u_1} [inst : Rack R], IsInvolutory R → ∀ (x y : R), x ◃⁻¹ y = x ◃ y
involutory_invAct_eq_act
{
R: Type ?u.30699
R
:
Type _: Type (?u.30699+1)
Type _
} [
Rack: Type ?u.30702 → Type ?u.30702
Rack
R: Type ?u.30699
R
] (h :
IsInvolutory: (R : Type ?u.30705) → [inst : Rack R] → Prop
IsInvolutory
R: Type ?u.30699
R
) (
x: R
x
y: R
y
:
R: Type ?u.30699
R
) :
x: R
x
◃⁻¹
y: R
y
=
x: R
x
◃
y: R
y
:=

Goals accomplished! 🐙
R✝: Type ?u.30693

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

h: IsInvolutory R

x, y: R


R✝: Type ?u.30693

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

h: IsInvolutory R

x, y: R


R✝: Type ?u.30693

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

h: IsInvolutory R

x, y: R


R✝: Type ?u.30693

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

h: IsInvolutory R

x, y: R


R✝: Type ?u.30693

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

h: IsInvolutory R

x, y: R


y = x ◃ x ◃ y
R✝: Type ?u.30693

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

h: IsInvolutory R

x, y: R


R✝: Type ?u.30693

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

h: IsInvolutory R

x, y: R


y = y

Goals accomplished! 🐙
#align rack.involutory_inv_act_eq_act
Rack.involutory_invAct_eq_act: ∀ {R : Type u_1} [inst : Rack R], IsInvolutory R → ∀ (x y : R), x ◃⁻¹ y = x ◃ y
Rack.involutory_invAct_eq_act
/-- An abelian rack is one for which the mediality axiom holds. -/ def
IsAbelian: (R : Type u_1) → [inst : Rack R] → Prop
IsAbelian
(
R: Type ?u.30806
R
:
Type _: Type (?u.30806+1)
Type _
) [
Rack: Type ?u.30809 → Type ?u.30809
Rack
R: Type ?u.30806
R
] :
Prop: Type
Prop
:= ∀
x: R
x
y: R
y
z: R
z
w: R
w
:
R: Type ?u.30806
R
, (
x: R
x
◃
y: R
y
) ◃
z: R
z
◃
w: R
w
= (
x: R
x
◃
z: R
z
) ◃
y: R
y
◃
w: R
w
#align rack.is_abelian
Rack.IsAbelian: (R : Type u_1) → [inst : Rack R] → Prop
Rack.IsAbelian
/-- Associative racks are uninteresting. -/ theorem
assoc_iff_id: ∀ {R : Type u_1} [inst : Rack R] {x y z : R}, x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
assoc_iff_id
{
R: Type ?u.30908
R
:
Type _: Type (?u.30908+1)
Type _
} [
Rack: Type ?u.30911 → Type ?u.30911
Rack
R: Type ?u.30908
R
] {
x: R
x
y: R
y
z: R
z
:
R: Type ?u.30908
R
} :
x: R
x
◃
y: R
y
◃
z: R
z
= (
x: R
x
◃
y: R
y
) ◃
z: R
z
↔
x: R
x
◃
z: R
z
=
z: R
z
:=

Goals accomplished! 🐙
R✝: Type ?u.30902

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y, z: R


x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
R✝: Type ?u.30902

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y, z: R


x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
R✝: Type ?u.30902

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y, z: R


(x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
R✝: Type ?u.30902

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y, z: R


(x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
R✝: Type ?u.30902

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y, z: R


x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
R✝: Type ?u.30902

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y, z: R


(x ◃ y) ◃ x ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
R✝: Type ?u.30902

inst✝¹: Rack R✝

R: Type u_1

inst✝: Rack R

x, y, z: R


x ◃ z = z ↔ x ◃ z = z

Goals accomplished! 🐙
#align rack.assoc_iff_id
Rack.assoc_iff_id: ∀ {R : Type u_1} [inst : Rack R] {x y z : R}, x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z
Rack.assoc_iff_id
end Rack namespace ShelfHom variable {
S₁: Type ?u.31476
S₁
:
Type _: Type (?u.31476+1)
Type _
} {
S₂: Type ?u.31056
S₂
:
Type _: Type (?u.31056+1)
Type _
} {
S₃: Type ?u.31482
S₃
:
Type _: Type (?u.31059+1)
Type _
} [
Shelf: Type ?u.31062 → Type ?u.31062
Shelf
S₁: Type ?u.31071
S₁
] [
Shelf: Type ?u.33230 → Type ?u.33230
Shelf
S₂: Type ?u.31074
S₂
] [
Shelf: Type ?u.31491 → Type ?u.31491
Shelf
S₃: Type ?u.31059
S₃
]
instance: {S₁ : Type u_1} → {S₂ : Type u_2} → [inst : Shelf S₁] → [inst_1 : Shelf S₂] → CoeFun (S₁ →◃ S₂) fun x => S₁ → S₂
instance
:
CoeFun: (α : Sort ?u.31090) → outParam (α → Sort ?u.31089) → Sort (max(max1?u.31090)?u.31089)
CoeFun
(
S₁: Type ?u.31071
S₁
→◃
S₂: Type ?u.31074
S₂
) fun
_: ?m.31106
_
=>
S₁: Type ?u.31071
S₁
→
S₂: Type ?u.31074
S₂
:= ⟨
ShelfHom.toFun: {S₁ : Type ?u.31137} → {S₂ : Type ?u.31136} → [inst : Shelf S₁] → [inst_1 : Shelf S₂] → (S₁ →◃ S₂) → S₁ → S₂
ShelfHom.toFun
⟩ -- Porting Note: Syntactically equal in Lean4 -- @[simp] -- theorem toFun_eq_coe (f : S₁ →◃ S₂) : f.toFun = f := -- rfl #noalign shelf_hom.to_fun_eq_coe @[simp] theorem
map_act: ∀ {S₁ : Type u_1} {S₂ : Type u_2} [inst : Shelf S₁] [inst_1 : Shelf S₂] (f : S₁ →◃ S₂) {x y : S₁}, toFun f (x ◃ y) = toFun f x ◃ toFun f y
map_act
(
f: S₁ →◃ S₂
f
:
S₁: Type ?u.31261
S₁
→◃
S₂: Type ?u.31264
S₂
) {
x: S₁
x
y: S₁
y
:
S₁: Type ?u.31261
S₁
} :
f: S₁ →◃ S₂
f
(
x: S₁
x
◃
y: S₁
y
) =
f: S₁ →◃ S₂
f
x: S₁
x
◃
f: S₁ →◃ S₂
f
y: S₁
y
:=
map_act': ∀ {S₁ : Type ?u.31411} {S₂ : Type ?u.31410} [inst : Shelf S₁] [inst_1 : Shelf S₂] (self : S₁ →◃ S₂) {x y : S₁}, toFun self (x ◃ y) = toFun self x ◃ toFun self y
map_act'
f: S₁ →◃ S₂
f
#align shelf_hom.map_act
ShelfHom.map_act: ∀ {S₁ : Type u_1} {S₂ : Type u_2} [inst : Shelf S₁] [inst_1 : Shelf S₂] (f : S₁ →◃ S₂) {x y : S₁}, toFun f (x ◃ y) = toFun f x ◃ toFun f y
ShelfHom.map_act
/-- The identity homomorphism -/ def
id: (S : Type ?u.31494) → [inst : Shelf S] → S →◃ S
id
(
S: Type ?u.31494
S
:
Type _: Type (?u.31494+1)
Type _
) [
Shelf: Type ?u.31497 → Type ?u.31497
Shelf
S: Type ?u.31494
S
] :
S: Type ?u.31494
S
→◃
S: Type ?u.31494
S
where toFun := fun
x: ?m.31526
x
=>
x: ?m.31526
x
map_act' :=

Goals accomplished! 🐙
S₁: Type ?u.31476

S₂: Type ?u.31479

S₃: Type ?u.31482

inst✝³: Shelf S₁

inst✝²: Shelf S₂

inst✝¹: Shelf S₃

S: Type ?u.31494

inst✝: Shelf S


∀ {x y : S}, (fun x => x) (x ◃ y) = (fun x => x) x ◃ (fun x => x) y

Goals accomplished! 🐙
#align shelf_hom.id
ShelfHom.id: (S : Type u_1) → [inst : Shelf S] → S →◃ S
ShelfHom.id
instance
inhabited: (S : Type u_1) → [inst : Shelf S] → Inhabited (S →◃ S)
inhabited
(
S: Type ?u.33236
S
:
Type _: Type (?u.33236+1)
Type _
) [
Shelf: Type ?u.33239 → Type ?u.33239
Shelf
S: Type ?u.33236
S
] :
Inhabited: Sort ?u.33242 → Sort (max1?u.33242)
Inhabited
(
S: Type ?u.33236
S
→◃
S: Type ?u.33236
S
) := ⟨
id: (S : Type ?u.33260) → [inst : Shelf S] → S →◃ S
id
S: Type ?u.33236
S
⟩ #align shelf_hom.inhabited
ShelfHom.inhabited: (S : Type u_1) → [inst : Shelf S] → Inhabited (S →◃ S)
ShelfHom.inhabited
/-- The composition of shelf homomorphisms -/ def
comp: (S₂ →◃ S₃) → (S₁ →◃ S₂) → S₁ →◃ S₃
comp
(
g: S₂ →◃ S₃
g
:
S₂: Type ?u.33307
S₂
→◃
S₃: Type ?u.33310
S₃
) (
f: S₁ →◃ S₂
f
:
S₁: Type ?u.33304
S₁
→◃
S₂: Type ?u.33307
S₂
) :
S₁: Type ?u.33304
S₁
→◃
S₃: Type ?u.33310
S₃
where toFun :=
g: S₂ →◃ S₃
g
.
toFun: {S₁ : Type ?u.33375} → {S₂ : Type ?u.33374} → [inst : Shelf S₁] → [inst_1 : Shelf S₂] → (S₁ →◃ S₂) → S₁ → S₂
toFun
∘
f: S₁ →◃ S₂
f
.
toFun: {S₁ : Type ?u.33388} → {S₂ : Type ?u.33387} → [inst : Shelf S₁] → [inst_1 : Shelf S₂] → (S₁ →◃ S₂) → S₁ → S₂
toFun
map_act' :=

Goals accomplished! 🐙
S₁: Type ?u.33304

S₂: Type ?u.33307

S₃: Type ?u.33310

inst✝²: Shelf S₁

inst✝¹: Shelf S₂

inst✝: Shelf S₃

g: S₂ →◃ S₃

f: S₁ →◃ S₂


∀ {x y : S₁}, (g.toFun ∘ f.toFun) (x ◃ y) = (g.toFun ∘ f.toFun) x ◃ (g.toFun ∘ f.toFun) y

Goals accomplished! 🐙
#align shelf_hom.comp
ShelfHom.comp: {S₁ : Type u_1} → {S₂ : Type u_2} → {S₃ : Type u_3} → [inst : Shelf S₁] → [inst_1 : Shelf S₂] → [inst_2 : Shelf S₃] → (S₂ →◃ S₃) → (S₁ →◃ S₂) → S₁ →◃ S₃
ShelfHom.comp
@[simp] theorem
comp_apply: ∀ (g : S₂ →◃ S₃) (f : S₁ →◃ S₂) (x : S₁), toFun (comp g f) x = toFun g (toFun f x)
comp_apply
(
g: S₂ →◃ S₃
g
:
S₂: Type ?u.35391
S₂
→◃
S₃: Type ?u.35394
S₃
) (
f: S₁ →◃ S₂
f
:
S₁: Type ?u.35388
S₁
→◃
S₂: Type ?u.35391
S₂
) (
x: S₁
x
:
S₁: Type ?u.35388
S₁
) : (
g: S₂ →◃ S₃
g
.
comp: {S₁ : Type ?u.35438} → {S₂ : Type ?u.35437} → {S₃ : Type ?u.35436} → [inst : Shelf S₁] → [inst_1 : Shelf S₂] → [inst_2 : Shelf S₃] → (S₂ →◃ S₃) → (S₁ →◃ S₂) → S₁ →◃ S₃
comp
f: S₁ →◃ S₂
f
)
x: S₁
x
=
g: S₂ →◃ S₃
g
(
f: S₁ →◃ S₂
f
x: S₁
x
) :=
rfl: ∀ {α : Sort ?u.35582} {a : α}, a = a
rfl
#align shelf_hom.comp_apply
ShelfHom.comp_apply: ∀ {S₁ : Type u_3} {S₂ : Type u_1} {S₃ : Type u_2} [inst : Shelf S₁] [inst_1 : Shelf S₂] [inst_2 : Shelf S₃] (g : S₂ →◃ S₃) (f : S₁ →◃ S₂) (x : S₁), toFun (comp g f) x = toFun g (toFun f x)
ShelfHom.comp_apply
end ShelfHom /-- A quandle is a rack such that each automorphism fixes its corresponding element. -/ class
Quandle: {α : Type u_1} → [toRack : Rack α] → (∀ {x : α}, x ◃ x = x) → Quandle α
Quandle
(
α: Type ?u.35625
α
:
Type _: Type (?u.35625+1)
Type _
) extends
Rack: Type ?u.35630 → Type ?u.35630
Rack
α: Type ?u.35625
α
where /-- The fixing property of a Quandle -/
fix: ∀ {α : Type u_1} [self : Quandle α] {x : α}, x ◃ x = x
fix
: ∀ {
x: α
x
:
α: Type ?u.35625
α
},
act: α → α → α
act
x: α
x
x: α
x
=
x: α
x
#align quandle
Quandle: Type u_1 → Type u_1
Quandle
namespace Quandle open Rack variable {
Q: Type ?u.35683
Q
:
Type _: Type (?u.63827+1)
Type _
} [
Quandle: Type ?u.77193 → Type ?u.77193
Quandle
Q: Type ?u.35667
Q
] attribute [simp]
fix: ∀ {α : Type u_1} [self : Quandle α] {x : α}, x ◃ x = x
fix
@[simp] theorem
fix_inv: ∀ {Q : Type u_1} [inst : Quandle Q] {x : Q}, x ◃⁻¹ x = x
fix_inv
{
x: Q
x
:
Q: Type ?u.35683
Q
} :
x: Q
x
◃⁻¹
x: Q
x
=
x: Q
x
:=

Goals accomplished! 🐙
Q: Type u_1

inst✝: Quandle Q

x: Q


Q: Type u_1

inst✝: Quandle Q

x: Q


Q: Type u_1

inst✝: Quandle Q

x: Q


Q: Type u_1

inst✝: Quandle Q

x: Q


Q: Type u_1

inst✝: Quandle Q

x: Q



Goals accomplished! 🐙
#align quandle.fix_inv
Quandle.fix_inv: ∀ {Q : Type u_1} [inst : Quandle Q] {x : Q}, x ◃⁻¹ x = x
Quandle.fix_inv
instance
oppositeQuandle: Quandle Qᵐᵒᵖ
oppositeQuandle
:
Quandle: Type ?u.35848 → Type ?u.35848
Quandle
Q: Type ?u.35842
Q
ᵐᵒᵖ where fix :=

Goals accomplished! 🐙
Q: Type ?u.35842

inst✝: Quandle Q


∀ {x : Qᵐᵒᵖ}, x ◃ x = x
Q: Type ?u.35842

inst✝: Quandle Q

x: Qᵐᵒᵖ


x ◃ x = x
Q: Type ?u.35842

inst✝: Quandle Q


∀ {x : Qᵐᵒᵖ}, x ◃ x = x
Q: Type ?u.35842

inst✝: Quandle Q

X✝: Q


h
op X✝ ◃ op X✝ = op X✝
Q: Type ?u.35842

inst✝: Quandle Q


∀ {x : Qᵐᵒᵖ}, x ◃ x = x

Goals accomplished! 🐙
#align quandle.opposite_quandle
Quandle.oppositeQuandle: {Q : Type u_1} → [inst : Quandle Q] → Quandle Qᵐᵒᵖ
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
Conj: Type u_1 → Type u_1
Conj
(
G: Type ?u.36048
G
:
Type _: Type (?u.36048+1)
Type _
) :=
G: Type ?u.36048
G
#align quandle.conj
Quandle.Conj: Type u_1 → Type u_1
Quandle.Conj
instance
Conj.quandle: (G : Type u_1) → [inst : Group G] → Quandle (Conj G)
Conj.quandle
(
G: Type ?u.36067
G
:
Type _: Type (?u.36067+1)
Type _
) [
Group: Type ?u.36070 → Type ?u.36070
Group
G: Type ?u.36067
G
] :
Quandle: Type ?u.36073 → Type ?u.36073
Quandle
(
Conj: Type ?u.36074 → Type ?u.36074
Conj
G: Type ?u.36067
G
) where act
x: ?m.36088
x
:= @
MulAut.conj: {G : Type ?u.36090} → [inst : Group G] → G →* MulAut G
MulAut.conj
G: Type ?u.36067
G
_
x: ?m.36088
x
self_distrib :=

Goals accomplished! 🐙
Q: Type ?u.36061

inst✝¹: Quandle Q

G: Type ?u.36067

inst✝: Group G


∀ {x y z : Conj G}, (fun x => ↑(↑MulAut.conj x)) x ((fun x => ↑(↑MulAut.conj x)) y z) = (fun x => ↑(↑MulAut.conj x)) ((fun x => ↑(↑MulAut.conj x)) x y) ((fun x => ↑(↑MulAut.conj x)) x z)
Q: Type ?u.36061

inst✝¹: Quandle Q

G: Type ?u.36067

inst✝: Group G

x, y, z: Conj G


(fun x => ↑(↑MulAut.conj x)) x ((fun x => ↑(↑MulAut.conj x)) y z) = (fun x => ↑(↑MulAut.conj x)) ((fun x => ↑(↑MulAut.conj x)) x y) ((fun x => ↑(↑MulAut.conj x)) x z)
Q: Type ?u.36061

inst✝¹: Quandle Q

G: Type ?u.36067

inst✝: Group G


∀ {x y z : Conj G}, (fun x => ↑(↑MulAut.conj x)) x ((fun x => ↑(↑MulAut.conj x)) y z) = (fun x => ↑(↑MulAut.conj x)) ((fun x => ↑(↑MulAut.conj x)) x y) ((fun x => ↑(↑MulAut.conj x)) x z)
Q: Type ?u.36061

inst✝¹: Quandle Q

G: Type ?u.36067

inst✝: Group G

x, y, z: Conj G


Q: Type ?u.36061

inst✝¹: Quandle Q

G: Type ?u.36067

inst✝: Group G


∀ {x y z : Conj G}, (fun x => ↑(↑MulAut.conj x)) x ((fun x => ↑(↑MulAut.conj x)) y z) = (fun x => ↑(↑MulAut.conj x)) ((fun x => ↑(↑MulAut.conj x)) x y) ((fun x => ↑(↑MulAut.conj x)) x z)

Goals accomplished! 🐙
invAct
x: ?m.43208
x
:= (@
MulAut.conj: {G : Type ?u.43210} → [inst : Group G] → G →* MulAut G
MulAut.conj
G: Type ?u.36067
G
_
x: ?m.43208
x
).
symm: {M : Type ?u.50264} → {N : Type ?u.50263} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N ≃* M
symm
left_inv
x: ?m.50721
x
y: ?m.50724
y
:=

Goals accomplished! 🐙
Q: Type ?u.36061

inst✝¹: Quandle Q

G: Type ?u.36067

inst✝: Group G

x, y: Conj G


(fun x => ↑(MulEquiv.symm (↑MulAut.conj x))) x (x ◃ y) = y

Goals accomplished! 🐙
right_inv
x: ?m.50732
x
y: ?m.50735
y
:=

Goals accomplished! 🐙
Q: Type ?u.36061

inst✝¹: Quandle Q

G: Type ?u.36067

inst✝: Group G

x, y: Conj G


x ◃ (fun x => ↑(MulEquiv.symm (↑MulAut.conj x))) x y = y

Goals accomplished! 🐙
fix :=

Goals accomplished! 🐙
Q: Type ?u.36061

inst✝¹: Quandle Q

G: Type ?u.36067

inst✝: Group G


∀ {x : Conj G}, x ◃ x = x

Goals accomplished! 🐙
#align quandle.conj.quandle
Quandle.Conj.quandle: (G : Type u_1) → [inst : Group G] → Quandle (Conj G)
Quandle.Conj.quandle
@[simp] theorem
conj_act_eq_conj: ∀ {G : Type u_1} [inst : Group G] (x y : Conj G), x ◃ y = x * y * x⁻¹
conj_act_eq_conj
{
G: Type u_1
G
:
Type _: Type (?u.62543+1)
Type _
} [
Group: Type ?u.62546 → Type ?u.62546
Group
G: Type ?u.62543
G
] (
x: Conj G
x
y: Conj G
y
:
Conj: Type ?u.62552 → Type ?u.62552
Conj
G: Type ?u.62543
G
) :
x: Conj G
x
◃
y: Conj G
y
= ((
x: Conj G
x
:
G: Type ?u.62543
G
) * (
y: Conj G
y
:
G: Type ?u.62543
G
) * (
x: Conj G
x
:
G: Type ?u.62543
G
)⁻¹ :
G: Type ?u.62543
G
) :=
rfl: ∀ {α : Sort ?u.63798} {a : α}, a = a
rfl
#align quandle.conj_act_eq_conj
Quandle.conj_act_eq_conj: ∀ {G : Type u_1} [inst : Group G] (x y : Conj G), x ◃ y = x * y * x⁻¹
Quandle.conj_act_eq_conj
theorem
conj_swap: ∀ {G : Type u_1} [inst : Group G] (x y : Conj G), x ◃ y = y ↔ y ◃ x = x
conj_swap
{
G: Type ?u.63833
G
:
Type _: Type (?u.63833+1)
Type _
} [
Group: Type ?u.63836 → Type ?u.63836
Group
G: Type ?u.63833
G
] (
x: Conj G
x
y: Conj G
y
:
Conj: Type ?u.63842 → Type ?u.63842
Conj
G: Type ?u.63833
G
) :
x: Conj G
x
◃
y: Conj G
y
=
y: Conj G
y
↔
y: Conj G
y
◃
x: Conj G
x
=
x: Conj G
x
:=

Goals accomplished! 🐙
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G


x ◃ y = y ↔ y ◃ x = x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G


x * y * x⁻¹ = y ↔ y * x * y⁻¹ = x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G


x * y * x⁻¹ = y ↔ y * x * y⁻¹ = x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G


x ◃ y = y ↔ y ◃ x = x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G


mp
x * y * x⁻¹ = y → y * x * y⁻¹ = x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G


mpr
y * x * y⁻¹ = x → x * y * x⁻¹ = y
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G


x ◃ y = y ↔ y ◃ x = x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G


mp
x * y * x⁻¹ = y → y * x * y⁻¹ = x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G


mpr
y * x * y⁻¹ = x → x * y * x⁻¹ = y
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G

h: x * y * x⁻¹ = y


mp
y * x * y⁻¹ = x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G

h: x * y * x⁻¹ = y


mp
y * x * y⁻¹ = x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G


mp
x * y * x⁻¹ = y → y * x * y⁻¹ = x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G

h: y * x * y⁻¹ = x


mpr
x * y * x⁻¹ = y
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G

h: x * y * x⁻¹ = y


x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G

h: y * x * y⁻¹ = x


Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G

h: x * y * x⁻¹ = y


Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G

h: x * y * x⁻¹ = y


Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G

h: x * y * x⁻¹ = y


x
Q: Type ?u.63827

inst✝¹: Quandle Q

G: Type u_1

inst✝: Group G

x, y: Conj G

h: y * x * y⁻¹ = x


#align quandle.conj_swap
Quandle.conj_swap: ∀ {G : Type u_1} [inst : Group G] (x y : Conj G), x ◃ y = y ↔ y ◃ x = x
Quandle.conj_swap
/-- `Conj` is functorial -/ def
Conj.map: {G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst_1 : Group H] → (G →* H) → Conj G →◃ Conj H
Conj.map
{
G: Type ?u.65083
G
:
Type _: Type (?u.65083+1)
Type _
} {
H: Type ?u.65086
H
:
Type _: Type (?u.65086+1)
Type _
} [
Group: Type ?u.65089 → Type ?u.65089
Group
G: Type ?u.65083
G
] [
Group: Type ?u.65092 → Type ?u.65092
Group
H: Type ?u.65086
H
] (
f: G →* H
f
:
G: Type ?u.65083
G
→*
H: Type ?u.65086
H
) :
Conj: Type ?u.65731 → Type ?u.65731
Conj
G: Type ?u.65083
G
→◃
Conj: Type ?u.65732 → Type ?u.65732
Conj
H: Type ?u.65086
H
where toFun :=
f: G →* H
f
map_act' :=

Goals accomplished! 🐙
Q: Type ?u.65077

inst✝²: Quandle Q

G: Type ?u.65083

H: Type ?u.65086

inst✝¹: Group G

inst✝: Group H

f: G →* H


∀ {x y : Conj G}, ↑f (x ◃ y) = ↑f x ◃ ↑f y

Goals accomplished! 🐙
#align quandle.conj.map
Quandle.Conj.map: {G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst_1 : Group H] → (G →* H) → Conj G →◃ Conj H
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
Dihedral: (n : ℕ) → ?m.77182 n
Dihedral
(n :
ℕ: Type
ℕ
) :=
ZMod: ℕ → Type
ZMod
n #align quandle.dihedral
Quandle.Dihedral: ℕ → Type
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
dihedralAct: (n : ℕ) → ZMod n → ZMod n → ZMod n
dihedralAct
(n :
ℕ: Type
ℕ
) (
a: ZMod n
a
:
ZMod: ℕ → Type
ZMod
n) :
ZMod: ℕ → Type
ZMod
n →
ZMod: ℕ → Type
ZMod
n := fun
b: ?m.77209
b
=>
2: ?m.77224
2
*
a: ZMod n
a
-
b: ?m.77209
b
#align quandle.dihedral_act
Quandle.dihedralAct: (n : ℕ) → ZMod n → ZMod n → ZMod n
Quandle.dihedralAct
theorem
dihedralAct.inv: ∀ (n : ℕ) (a : ZMod n), Function.Involutive (dihedralAct n a)
dihedralAct.inv
(n :
ℕ: Type
ℕ
) (
a: ZMod n
a
:
ZMod: ℕ → Type
ZMod
n) :
Function.Involutive: {α : Sort ?u.78961} → (α → α) → Prop
Function.Involutive
(
dihedralAct: (n : ℕ) → ZMod n → ZMod n → ZMod n
dihedralAct
n
a: ZMod n
a
) :=

Goals accomplished! 🐙
Q: Type ?u.78951

inst✝: Quandle Q

n: ℕ

a: ZMod n


Q: Type ?u.78951

inst✝: Quandle Q

n: ℕ

a, b: ZMod n


dihedralAct n a (dihedralAct n a b) = b
Q: Type ?u.78951

inst✝: Quandle Q

n: ℕ

a: ZMod n


Q: Type ?u.78951

inst✝: Quandle Q

n: ℕ

a, b: ZMod n


2 * a - (2 * a - b) = b
Q: Type ?u.78951

inst✝: Quandle Q

n: ℕ

a: ZMod n



Goals accomplished! 🐙
#align quandle.dihedral_act.inv
Quandle.dihedralAct.inv: ∀ (n : ℕ) (a : ZMod n), Function.Involutive (dihedralAct n a)
Quandle.dihedralAct.inv
instance: (n : ℕ) → Quandle (Dihedral n)
instance
(n :
ℕ: Type
ℕ
) :
Quandle: Type ?u.79297 → Type ?u.79297
Quandle
(
Dihedral: ℕ → Type
Dihedral
n) where act :=
dihedralAct: (n : ℕ) → ZMod n → ZMod n → ZMod n
dihedralAct
n self_distrib :=

Goals accomplished! 🐙
Q: Type ?u.79289

inst✝: Quandle Q

n: ℕ


∀ {x y z : Dihedral n}, dihedralAct n x (dihedralAct n y z) = dihedralAct n (dihedralAct n x y) (dihedralAct n x z)
Q: Type ?u.79289

inst✝: