I wrote:
>
> Martin Baker wrote:
> >
> > My initial thoughts about group domains related to homotopy in FriCAS is
> > that there is a need for at least 4 group domains shown at each corner
> > of this square:
> >
> > PermutationGroup <-----equivalent-----> GroupPresentation
> > | if finite |
> > | |
> > contains set of contains set of
> > | |
> > V V
> > Permutation <-------------------------------> Word
> >
> > The domains at the bottom of the diagram are implementations of Group
> > category. So in these cases % will contain something representing a
> > single element of the group such as a single permutation or a single
> > word. Functions will be from Group such as '*'.
> >
> > The domains at the top of the diagram have % which holds information
> > about the whole group so it identifies it as say 'cyclic group 5' or
> > 'dihedral group 3'. The functions will be functions on the whole group
> > such as: sum, product, quotient, subgroup, order, orbit, etc.
> >
> > (I don't think Bill likes this way of describing it? I think the
> > distinction is valid but can you think of a more mathematical way to
> > describe the distinction? Perhaps in terms of initial and terminal
> > algebras?)
> >
> > So how does FinitelyPresentedGroup fit in this? It seems to me that
> > FinitelyPresentedGroup is of type: Type whereas GroupPresentation is of
> > a specific type:
> >
> > (1) -> F:=FPG([x,y,z],[])
> >
> > (1) FinitelyPresentedGroup([x,y,z],[])
> > Type: Type
> >
> > (2) -> F2 := groupPresentation([1,2,3],[])
> >
> > (2) <a b c | >
> > Type: GroupPresentation
> >
> > Given this, is it possible to construct functions like sum, product,
> > quotient, subgroup, order, orbit, etc. on something of type: Type?
> >
> > If it is possible to do this, why is PermutationGroup not constructed
> > this way?
>
> Hmm, there are several ways to look at group. First you can
> look at groups as objects (that frequently happens in homological
> algebra). Within such point of view you may consider various
> notion of equivalence/equality. Plain equality is of limited
> use, as we may get entirely trivial differences.
> Isomorphism is important, but sometimes we need more coarse
> equivalence relation, sometimes we need more than isomorphism.
> Quite a lot of things done at this level in not computable:
> there are various results but very little algorithms.
>
> Treating groups as objects is frequently bundled with categorical
> approach: there are various categories and people build
> functors from those cateries to groups (or diagrams of groups).
>
> Another point of view is that groups are sets with specific
> operations: in FriCAS this is expressed by Group. There
> is some intermediate levels: one can look at say subgroups
> of given group or group representations.
>
> Now, for finite groups subgroup is the same as fintely
> generated subgroup, so one can represent subgroups
> via (finite) sets of generators. In this sense
> PermutationGroup implements subgroup of permutation group
> (for given parameter we get single subgroup, while
> varying parameters we get all of the subgroups).
> In similar spirit we could have MatrixGroup for
> subgroup(s) of matrices. We could also look at
> subgroups of free group, but that is less interesting
> because subgroup of free group is again a free group.
>
> In principle for finite groups we could easily represent
> quotients, but here is a little catch: if we represent
> subgroup via generators, then testing elements of
> a group for membership in a subgroup may be tricky
> (for infinite groups membership in a subgroup is
> undecidable). In other words, we can only do
> things which are efficiently computable. This
> largely explains why PermutationGroup has its
> current form: there is efficient algorithms which
> uses specific _representation_ of permutations.
> This algorithm is efficient _only_ for permutation
> groups, trying to treat other groups as permutation
> groups would lead to quite inefficient method.
> Nowadays there are algorithms which obtain similar
> results for matrix groups, but they use specific
> properties of matrices.
>
> I have to finish now, I will later write more about
> your proposal.
About your proposal: note that notion of permutation
group is closely related to notion of subgroup (and
at categorical level with final object of a category).
Finitely presented groups are related to quotients
(and first object of a category). As a little remark
note that in both cases we natuarally get semigroup
first, in case of permutations semigroup of all mappings
from a set to itself, in case of free group we get
free semigroup. Then we "correct" deficiency, in
case of permutations taking subsemigroup of
invertible maps, in case of free group taking
quotient (declaring some generators of free semigroup
as inverses of group generators).
Now, one natural thing would be a way to produce group
given group presentation. There is very strong
obstacle to this due to unsolvability of word problem.
IMO the right way to go forward it to look at cases
when word problem is solvable. This happens if
we know something special about groups, for example
for abelian groups word problem is solvable. This
happens if presentation has special form, like
for result of Knuth-Bendix completition. We could
try postpone solving hard problems and require that
to create finitely presented group the user has
to provide solver for word problem
Concerning structure on Type: currently this is done by
declaring specific categories/domains. Union represets
/implements sum. There is Product domain. There is
Subdomian. Each are very special I do not see how
to "generalize" them at computational level. In principle
we could try to add "quotient" constructor. Namely,
to get quotient we need equvalence relation and we could
have something like:
Quitient(S : Type, = : (S, S) -> Boolean) : ....
but that would be of limited use, because for products
there are important features which are preserved, while
for quotients everything depends on equivalence relation.
Existing algebra cheats in some cases, uncoditionaly
declaring features which are valid only if special
conditions are satisfied. For quotient I do not
think cheats are appropriate -- we can not even claim
that features are preserved "in most interesting cases".
And I would like to get rid of cheating.
Orbits need extra structure for example semigroup structure.
Orbits of group actions have specific properties, so
they probably should be studied separately from more
general notions of orbits. And efficient computations
with orbits are possible only in some specific situations.
So no, I think that currently it is not possible to put
more _useful_ general structure on Type.
--
Waldek Hebisch
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
