Rack.self_act_act_eq
theorem Rack.self_act_act_eq :
∀ {R : Type u_1} [inst : Rack R] {x y : R}, Shelf.act (Shelf.act x x) y = Shelf.act x y
This theorem states that for any type `R` that forms a `Rack`, given any elements `x` and `y` of `R`, the result of the operation `Shelf.act` twice on `x` and then on `y` (i.e., `Shelf.act (Shelf.act x x) y`) is the same as the result of the operation `Shelf.act` on `x` and `y` (i.e., `Shelf.act x y`). This can be interpreted as a kind of idempotence property of the `Shelf.act` operation when applied twice to the same element in the context of a `Rack`.
More concisely: For any `Rack` type `R` and elements `x` and `y` in `R`, `Shelf.act (Shelf.act x x) y` equals `Shelf.act x y`.
|
Rack.ad_conj
theorem Rack.ad_conj :
∀ {R : Type u_2} [inst : Rack R] (x y : R),
Rack.act' (Shelf.act x y) = Rack.act' x * Rack.act' y * (Rack.act' x)⁻¹
The theorem `Rack.ad_conj` states that for any given rack `R` and any two elements `x` and `y` from `R`, the adjoint action of `R` on itself, represented as `Rack.act' (Shelf.act x y)`, is equivalent to the conjugation of the action of `y` by the action of `x`, represented as `Rack.act' x * Rack.act' y * (Rack.act' x)⁻¹`. This underlies the self-distributivity axiom and is used in the natural rack homomorphism `toConj` from `R` to `Conj (R ≃ R)` defined by `op'`. In other words, acting on `y` with `x` and then acting on the result with `x` inverted is the same as first acting on `x`, then acting on `y`, and finally acting on the result with `x` inverted.
More concisely: For any rack `R` and elements `x, y` in `R`, the adjoint action of `x` on `y` is equivalent to the conjugation of the action of `y` by `x`.
|
Rack.right_inv
theorem Rack.right_inv : ∀ {α : Type u} [self : Rack α] (x : α), Function.RightInverse (Rack.invAct x) (Shelf.act x)
This theorem, `Rack.right_inv`, states that for any type `α` that has a `Rack` structure, and for any element `x` of this type `α`, the function `Rack.invAct x` is a right inverse to the function `Shelf.act x`. In other words, if you first apply `Shelf.act x` and then `Rack.invAct x`, you will get back the original element. This is expressed in functional terms as `Shelf.act x ∘ Rack.invAct x = id`, where `id` is the identity function.
More concisely: For any type equipped with a `Rack` structure and any of its elements `x`, the functions `Shelf.act x` and `Rack.invAct x` are right inverse to each other, that is, `Shelf.act x ∘ Rack.invAct x = id`.
|
ShelfHom.map_act'
theorem ShelfHom.map_act' :
∀ {S₁ : Type u_1} {S₂ : Type u_2} [inst : Shelf S₁] [inst_1 : Shelf S₂] (self : ShelfHom S₁ S₂) {x y : S₁},
self.toFun (Shelf.act x y) = Shelf.act (self.toFun x) (self.toFun y)
The theorem `ShelfHom.map_act'` states that for all types `S₁` and `S₂` that have a `Shelf` structure, and for all shelf homomorphisms `self` from `S₁` to `S₂`, and for all elements `x` and `y` of `S₁`, the homomorphism property holds. In other words, applying the `Shelf` action to `x` and `y` in `S₁` and then mapping the result to `S₂` using `self`, is the same as first mapping `x` and `y` to `S₂` and then applying the `Shelf` action in `S₂`. In mathematical terms, this is stating that for a shelf homomorphism `f: S₁ → S₂`, the equation `f(s∘t) = f(s)∘f(t)` holds for all `s,t ∈ S₁`, where `∘` denotes the `Shelf` action.
More concisely: For any shelf homomorphisms `f: S₁ → S₂` between shelves `S₁` and `S₂`, the composition of the `Shelf` actions `f(s∘t) = f(s)∘f(t)` holds for all `s,t ∈ S₁`.
|
Rack.act_invAct_eq
theorem Rack.act_invAct_eq : ∀ {R : Type u_1} [inst : Rack R] (x y : R), Shelf.act x (Rack.invAct x y) = y
This theorem states that for all types `R` that have a structure of a `Rack`, and for all elements `x` and `y` of `R`, the `Shelf` action of `x` on the inverse action of `x` on `y` equals `y`. Intuitively, this says that the `Rack` inverse action behaves like a "reverse operation" for the `Shelf` action.
More concisely: For all types `R` with a `Rack` structure and all elements `x` in `R`, the `Shelf` action of `x` on the inverse action of `x` on `y` equals `y`. In mathematical notation, `x * (x ^-1 * y) = y`.
|
Rack.PreEnvelGroupRel'.rel
theorem Rack.PreEnvelGroupRel'.rel :
∀ {R : Type u} [inst : Rack R] {a b : Rack.PreEnvelGroup R},
Rack.PreEnvelGroupRel' R a b → Rack.PreEnvelGroupRel R a b
This theorem provides a fast method to convert a `PreEnvelGroupRel'` into a `PreEnvelGroupRel` for any given rack `R`. For all elements `a` and `b` of the pre-envelope group of `R`, if there exists a `PreEnvelGroupRel'` relation between `a` and `b`, then there also exists a `PreEnvelGroupRel` relation between `a` and `b`. The proof of this theorem is not shown here.
More concisely: For any rack R, if two elements of its pre-envelope group are related by a `PreEnvelGroupRel'`, then they are also related by a `PreEnvelGroupRel`.
|
Rack.toEnvelGroup.mapAux.well_def
theorem Rack.toEnvelGroup.mapAux.well_def :
∀ {R : Type u_1} [inst : Rack R] {G : Type u_2} [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G))
{a b : Rack.PreEnvelGroup R},
Rack.PreEnvelGroupRel' R a b → Rack.toEnvelGroup.mapAux f a = Rack.toEnvelGroup.mapAux f b
The theorem `Rack.toEnvelGroup.mapAux.well_def` demonstrates that the function `toEnvelGroup.mapAux` behaves well under equivalence. More specifically, it says that for any rack `R`, group `G`, and shelf homomorphism `f` from `R` to the conjugation quandle of `G`, if two pre-envelope group elements `a` and `b` of `R` are equivalent under the `Rack.PreEnvelGroupRel'` relation, then applying the `toEnvelGroup.mapAux` function to `a` and `b` will yield the same result. This shows that the `toEnvelGroup.mapAux` function respects the equivalence relation `Rack.PreEnvelGroupRel'`.
More concisely: Given a rack `R`, group `G`, shelf homomorphism `f` from `R` to the conjugation quandle of `G`, and equivalent pre-envelope group elements `a` and `b` of `R` under the `Rack.PreEnvelGroupRel'` relation, `toEnvelGroup.mapAux f a` is equal to `toEnvelGroup.mapAux f b`.
|
Shelf.self_distrib
theorem Shelf.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)
This theorem states that the action operation, `act`, on a structure `Shelf` with elements of type `α` is self-distributive. Specifically, for any elements `x`, `y`, and `z` of type `α`, the action of `x` on the result of the action of `y` on `z` is the same as the action of the result of the action of `x` on `y` on the result of the action of `x` on `z`. In mathematical terms, this can be written as `x ∗ (y ∗ z) = (x ∗ y) ∗ (x ∗ z)`, where `∗` represents the `act` operation.
More concisely: For all elements `x`, `y`, and `z` of type `α` in a structure `Shelf`, the action of `x` on the product of the actions of `y` and `z` is equal to the product of the actions of `x` with `y` and `x` with `z`. In symbols: `x ∗ (y ∗ z) = (x ∗ y) ∗ (x ∗ z)`.
|
Quandle.fix
theorem Quandle.fix : ∀ {α : Type u_1} [self : Quandle α] {x : α}, Shelf.act x x = x
The theorem `Quandle.fix` states that for any type `α` that forms a Quandle, for every element `x` of `α`, the Shelf action of `x` on itself results in `x`. This theorem expresses the fixing property of a Quandle, which in essence states that, when an operation is performed on an element with itself in a Quandle, the result is the element itself.
More concisely: For any Quandle `α`, the Shelf operation `shelf x x` equals `x` for all `x` in `α`.
|
Rack.toEnvelGroup.univ_uniq
theorem Rack.toEnvelGroup.univ_uniq :
∀ (R : Type u_1) [inst : Rack R] (G : Type u_2) [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G))
(g : Rack.EnvelGroup R →* G), f = (Quandle.Conj.map g).comp (Rack.toEnvelGroup R) → g = Rack.toEnvelGroup.map f
The theorem `Rack.toEnvelGroup.univ_uniq` states that for any type `R` with a `Rack` structure, any type `G` with a `Group` structure, a shelf homomorphism `f` from `R` to the conjugation quandle of `G`, and a group homomorphism `g` from the enveloping group of `R` to `G`, if `f` is equal to the composition of the map `Quandle.Conj.map g` and `Rack.toEnvelGroup R`, then `g` is equal to the map `Rack.toEnvelGroup.map f`. In other words, the homomorphism `Rack.toEnvelGroup.map f` is the unique map that completes the respective commutative diagram. This theorem ensures the universality of the canonical homomorphism from a rack to its enveloping group.
More concisely: Given a rack `R` with a group `G` and homomorphisms `f: R -> Quandle.Conj G` and `g: EnvelopingGroup R -> G`, if `f = Quandle.Conj.map g ∘ Rack.toEnvelGroup R`, then `g = Rack.toEnvelGroup.map f`.
|
UnitalShelf.act_act_self_eq
theorem UnitalShelf.act_act_self_eq :
∀ {S : Type u_1} [inst : UnitalShelf S] (x y : S), Shelf.act (Shelf.act x y) x = Shelf.act x y
The theorem `UnitalShelf.act_act_self_eq` states that for any unital shelf, specified by the type `S`, and any elements `x` and `y` of this type, the following property called the *graphic identity* is satisfied: applying the shelf action to `x` and `y`, and then applying the shelf action to the result and `x` again, yields the same result as just applying the shelf action to `x` and `y`. In other words, for all `x` and `y` in the unital shelf, `(x * y) * x` equals `x * y`. This property is one of the defining characteristics of a *graphic monoid*.
More concisely: For any unital shelf type `S`, and all `x` and `y` in `S`, the graphic identity holds: `(x * y) * x = x * y`.
|
Rack.assoc_iff_id
theorem Rack.assoc_iff_id :
∀ {R : Type u_2} [inst : Rack R] {x y z : R},
Shelf.act x (Shelf.act y z) = Shelf.act (Shelf.act x y) z ↔ Shelf.act x z = z
This theorem states that for any type `R` with a `Rack` structure, and for any three elements `x`, `y`, and `z` of type `R`, the `Shelf` action of `x` on the result of the `Shelf` action of `y` on `z` is equal to the `Shelf` action of the result of the `Shelf` action of `x` on `y` on `z` if and only if the `Shelf` action of `x` on `z` equals `z`. In more mathematical terms, it is stating that the `Shelf` action is associative if and only if the `Shelf` action of any element on any other element is the second element itself.
More concisely: For any type `R` with a `Rack` structure, the `Shelf` action is associative if and only if for all `x, y, z` in `R`, `x * (y * z) = (x * y) * z <=> x * z = z`.
|
Rack.toEnvelGroup.univ
theorem Rack.toEnvelGroup.univ :
∀ (R : Type u_1) [inst : Rack R] (G : Type u_2) [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G)),
(Quandle.Conj.map (Rack.toEnvelGroup.map f)).comp (Rack.toEnvelGroup R) = f
The theorem `Rack.toEnvelGroup.univ` asserts that given a homomorphism from a rack (a mathematical structure) to a group, this homomorphism can be factored through the enveloping group of the rack. In more detail, for any rack `R`, group `G`, and homomorphism `f` from `R` to the conjugation quandle of `G`, the composition of the map induced by `f` on the enveloping group of `R` and the canonical homomorphism from `R` to its enveloping group equals `f`. This theorem essentially states the universal property of the enveloping group of a rack.
More concisely: Given a rack homomorphism to a group's conjugation quandle, this homomorphism factors through the enveloping group of the rack, preserving the group structure.
|
Rack.left_cancel
theorem Rack.left_cancel :
∀ {R : Type u_1} [inst : Rack R] (x : R) {y y' : R}, Shelf.act x y = Shelf.act x y' ↔ y = y'
This theorem, `Rack.left_cancel`, states that for any type `R` with a `Rack` structure, and for any elements `x`, `y`, and `y'` of `R`, the action of `x` on `y` being equal to the action of `x` on `y'` is equivalent to `y` being equal to `y'`. In other words, it asserts the left-cancellative property of the operation `Shelf.act` in a rack: if `x * y = x * y'`, then `y = y'`.
More concisely: For any rack `R` and elements `x`, `y`, `y'` in `R`, `x * y = x * y'` implies `y = y'`.
|
Rack.left_inv
theorem Rack.left_inv : ∀ {α : Type u} [self : Rack α] (x : α), Function.LeftInverse (Rack.invAct x) (Shelf.act x) := by
sorry
This theorem states that for all elements 'x' of some type 'α' in a Rack structure, the `invAct` function (representing the inverse actions of the elements) is a left inverse to the `Shelf.act` function (representing the action of the `Shelf` over `α`). In other words, for every element 'x', if you first apply the `Shelf.act` function to 'x' and then apply the `Rack.invAct` function to the result, you get 'x' back. This could be interpreted in terms of the mathematical concept of a Rack, where the operations `Shelf.act` and `Rack.invAct` are related by this left inverse property.
More concisely: For every element x in a Rack, the inverse action `Rack.invAct x (Shelf.act x)` equals x.
|
UnitalShelf.assoc
theorem UnitalShelf.assoc :
∀ {S : Type u_1} [inst : UnitalShelf S] (x y z : S), Shelf.act (Shelf.act x y) z = Shelf.act x (Shelf.act y z) := by
sorry
This theorem states the associativity property for a unital shelf. Specifically, for any type `S` that has a `UnitalShelf` structure, and for any three elements `x`, `y`, and `z` of type `S`, the action of the `Shelf` on the pair `(Shelf.act x y, z)` is equal to the action of the `Shelf` on the pair `(x, Shelf.act y z)`. This is analogous to the associativity property in algebra, where for all `x`, `y`, `z` in a group, the equation `(x * y) * z = x * (y * z)` holds.
More concisely: For any unital shelf type `S` and elements `x, y, z` of `S`, `Shelf.act (Shelf.act x y) z = Shelf.act x (Shelf.act y z)`.
|