Stream: Beginner Questions

Topic: group theory

Anthony Bordg (Dec 01 2020 at 11:50):

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

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.

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?

Manuel Eberl (Dec 01 2020 at 16:17):

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

Manuel Eberl (Dec 01 2020 at 16:17):

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

Manuel Eberl (Dec 01 2020 at 16:17):

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

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.

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.

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?

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: Apr 19 2024 at 20:15 UTC