Stream: Beginner Questions

Topic: group theory


view this post on Zulip Anthony Bordg (Dec 01 2020 at 11:50):

Given a (abelian) group GG and a family {gi}\lbrace g_i \rbrace of elements of GG indexed by a set II, is there a notation for the elements iIgi\sum_{i \in I} g_i in one of the many formalizations of group theory in the main library or in the AFP?

view this post on Zulip Manuel Eberl (Dec 01 2020 at 12:23):

The ‘canonical’ formalisation of group theory is HOL-Algebra. Groups are written multiplicatively in HOL-Algebra, and the concept you are looking for is called finprod in HOL-Algebra.Finite_Product: ⨂⇘G⇙ i∈I. g i

This is defined for any commutative monoid.

view this post on Zulip Anthony Bordg (Dec 01 2020 at 16:16):

I tried to parse their code but I don't immediately see why they require the index set (named A there) to be finite. What does prevent A from being infinite?

view this post on Zulip Manuel Eberl (Dec 01 2020 at 16:17):

If it's infinite, it might not even be well-defined.

view this post on Zulip Manuel Eberl (Dec 01 2020 at 16:17):

You would need a topological group for that to even make sense

view this post on Zulip Manuel Eberl (Dec 01 2020 at 16:17):

I don't think we have topological groups in HOL-Algebra

view this post on Zulip Manuel Eberl (Dec 01 2020 at 16:18):

If you're not interested in abstract algebra but your groups are very "concrete", it might make more sense to define a type for them and just use the "normal" operations for indexed sums and products.

view this post on Zulip Manuel Eberl (Dec 01 2020 at 16:19):

For infinite sums, it depends a bit on what kind of summation you want. If the summation order is fixed, there's suminf. Otherwise I don't think we have terribly much, unfortunately.

view this post on Zulip Manuel Eberl (Dec 01 2020 at 16:19):

But let's not get ahead of ourselves, what kind of objects are you trying to sum?

view this post on Zulip Anthony Bordg (Dec 01 2020 at 18:30):

I realized tonight that I could express what I wanted without introducing these arbitrary sums of elements of an abelian group. So, my problem is solved, at least for now. Thanks for your help.


Last updated: Aug 13 2022 at 05:18 UTC