OKlibrary  0.2.1.6
UniquelySolvableElements.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 8.7.2008 (Swansea) */
00002 /* Copyright 2008, 2009 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 /*
00023   In a general (possibly infinite) groupoid V we have the following
00024   notions for an element x:
00025   - x is left- resp. right-solvable if the left- resp. right-translation
00026     by x is surjective.
00027   - x is left- resp. right-cancellable if the left- resp. right-translation
00028     by x is injective.
00029   - Let's denote "left-solvable and left-cancellable", i.e., left-translation
00030     is a bijection, by "left-uniquely-solvable", "right-solvable and 
00031     right-cancellable" by "right-uniquely-solvable", and 
00032     "solvable and cancellable" by "uniquely-solvable".
00033 
00034   Now for a finite groupoid both conditions are equivalent, and are
00035   equivalent to the condition that left resp. right-translations
00036   are permutations.
00037 */
00038 
00039 /* Check whether x induces a permutation for groupoid V: */
00040 leftpermutation_el_grd(V,x) := is(length(map(lambda([y],V[2](x,y)),V[1])) = length(V[1]))$
00041 rightpermutation_el_grd(V,x) := is(length(map(lambda([y],V[2](y,x)),V[1])) = length(V[1]))$
00042 permutation_el_grd(V,x) := leftpermutation_el_grd(V,x) and rightpermutation_el_grd(V,x)$
00043 
00044 /* Whether a groupoid is uniquely solvable:
00045 */
00046 uniquelysolvable_bydef_grd(V) := every_s(lambda([x],permutation_el_grd(V,x)),V[1])$
00047 /* The condition "qgrp_p" for a groupoid additionally just checks whether
00048    we have a groupoid at all.
00049 */
00050 
00051