feat(algebra/quandle): Unital shelves (#17839)

Extend shelves to include the unital case, as well as a few basic results about unital shelves from https://arxiv.org/pdf/1603.08590.pdf 

This culminates in providing a monoid instance for a unital shelf.



Co-authored-by: Jim Fowler <fowler@math.osu.edu>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

docs/references.bib

@@ -600,6 +600,24 @@ @Book{            coxlittleoshea1997
   isbn          = {978-0-387-94680-1}
 }
 
+@Article{         crans2017,
+  author        = {Crans, Alissa S. and Mukherjee, Sujoy and Przytycki,
+                  J\'{o}zef H.},
+  title         = {On homology of associative shelves},
+  journal       = {J. Homotopy Relat. Struct.},
+  fjournal      = {Journal of Homotopy and Related Structures},
+  volume        = {12},
+  year          = {2017},
+  number        = {3},
+  pages         = {741--763},
+  issn          = {2193-8407},
+  mrclass       = {18G60 (20M32 20N02 57M25)},
+  mrnumber      = {3691304},
+  mrreviewer    = {Mahender Singh},
+  doi           = {10.1007/s40062-016-0164-9},
+  url           = {https://doi.org/10.1007/s40062-016-0164-9}
+}
+
 @Book{            davey_priestley,
   author        = {Davey, B. A. and Priestley, H. A.},
   title         = {Introduction to lattices and order},

src/algebra/quandle.lean

@@ -34,7 +34,7 @@ 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]
+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
@@ -43,6 +43,7 @@ group.
 ## Main definitions
 
 * `shelf` is a type with a self-distributive action
+* `unital_shelf` 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.
@@ -54,6 +55,11 @@ group.
 * `rack.envel_group` is left adjoint to `quandle.conj` (`to_envel_group.map`).
   The universality statements are `to_envel_group.univ` and `to_envel_group.univ_uniq`.
 
+## Implementation notes
+
+"Unital racks" are uninteresting (see `rack.assoc_iff_id`, `unital_shelf.assoc`), so we do not
+define them.
+
 ## Notation
 
 The following notation is localized in `quandles`:
@@ -92,6 +98,14 @@ class shelf (α : Type u) :=
 (act : α → α → α)
 (self_distrib : ∀ {x y z : α}, act x (act y z) = act (act x y) (act x z))
 
+/--
+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 unital_shelf (α : Type u) extends shelf α, has_one α :=
+(one_act : ∀ a : α, act 1 a = a)
+(act_one : ∀ a : α, act a 1 = a)
+
 /--
 The type of homomorphisms between shelves.
 This is also the notion of rack and quandle homomorphisms.
@@ -120,6 +134,38 @@ localized "infixr (name := shelf_hom) ` →◃ `:25 := shelf_hom" in quandles
 
 open_locale quandles
 
+namespace unital_shelf
+open shelf
+
+variables {S : Type*} [unital_shelf 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 :=
+begin
+  have h : (x ◃ y) ◃ x = (x ◃ y) ◃ (x ◃ 1) := by rw act_one,
+  rw [h, ←shelf.self_distrib, act_one],
+end
+
+lemma act_idem (x : S) : (x ◃ x) = x := by rw [←act_one x, ←shelf.self_distrib, act_one, act_one]
+
+lemma act_self_act_eq (x y : S) : x ◃ (x ◃ y) = x ◃ y :=
+begin
+  have h : x ◃ (x ◃ y) = (x ◃ 1) ◃ (x ◃ y) := by rw act_one,
+  rw [h, ←shelf.self_distrib, one_act],
+end
+
+/--
+The associativity of a unital shelf comes for free.
+-/
+lemma assoc (x y z : S) : (x ◃ y) ◃ z = x ◃ y ◃ z :=
+by rw [self_distrib, self_distrib, act_act_self_eq, act_self_act_eq]
+
+end unital_shelf
+
 namespace rack
 variables {R : Type*} [rack R]