OKlibrary  0.2.1.6
InvertibleElements.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 8.7.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2012 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00023 
00024 
00025 /* **********
00026    * Basics *
00027    **********
00028 */
00029 
00030 /* Check whether x is left-invertible for unital groupoid V: */
00031 leftinvertible_el_ugrd(V,x) := some_s(lambda([y],is(V[2](y,x)=V[3])), V[1])$
00032 /* Check whether x is right-invertible for unital groupoid V: */
00033 rightinvertible_el_ugrd(V,x) := some_s(lambda([y],is(V[2](x,y)=V[3])), V[1])$
00034 /* Check whether x is invertible for unital groupoid V: */
00035 invertible_el_ugrd(V,x) := leftinvertible_el_ugrd(V,x) and rightinvertible_el_ugrd(V,x)$
00036 
00037 /* Checks whether f provides an inversion for a unital groupoid: */
00038 leftinversion_ugrd(V,f) := every_s(lambda([x],is(V[2](f(x),x)=V[3])),V[1])$
00039 rightinversion_ugrd(V,f) := every_s(lambda([x],is(V[2](x,f(x))=V[3])),V[1])$
00040 inversion_ugrd(V,f) := leftinversion_ugrd(V,f) and rightinversion_ugrd(V,f)$
00041 
00042 
00043 /* ***************
00044    * Involutions *
00045    ***************
00046 */
00047 
00048 /* Involutions are self-inverse elements. */
00049 
00050 /* The set of non-trivial involutions of a unital groupoid: */
00051 involutions_ugrd(V) :=
00052  subset(disjoin(V[3],V[1]), lambda([x], is(V[2](x,x) = V[3])))$
00053 /* Remark: The name of the function reflects that in the context of
00054    group-theory, involutions are non-trivial (not the neutral elemenet).
00055    However in the context of functions, the identity is considered to be
00056    an involution.
00057 */
00058