Zulip Chat Archive

Stream: maths

Topic: Card structure on `Group`


view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:03):

@Jason KY. , @Giulia Carfora and I have been wrestling all summer with Sylow's theorems, and this is something which came from this.

If GG is a finite group and gGg\in G, then the order of the element divides the order of the group. If we define "order of the element" to be the ideal of Z\mathbb{Z} corresponding to the kernel of ngnn\mapsto g^n then this works well even for elements of infinite order. In fact, because groups are pointed sets (they have a canonical identity element), if they are finite they can never have size 0, so one could define an interesting "cardinality" function on the category of groups, where the cardinality of a group is the ideal of Z\mathbb{Z} generated by its cardinality if it's finite, and the zero ideal otherwise. The cardinality of the product is the product of the cardinalities. Statements like "the order of gg divides the order of GG" now become o(G)o(g)o(G)\subseteq o(g), a statement which is also true for infinite groups. Note that ideals have a lattice structure so this is just an inequality. If HH is a subgroup of GG then there's a monic homomorphism from HH to GG, and there is an invariant [o(G):o(H)][o(G):o(H)] or [o(H):o(G)][o(H):o(G)] attached to the morphism, which is the index of HH in GG (I can't remember which way round the standard notation is). This invariant is well-defined for general morphisms, but suffers from nat subtraction issues if the maps aren't injective, so we can let it take values in the monoid of fractions of the ideals of Z\mathbb{Z} and then I bet function composition will again be multiplicative without any finiteness assumptions at all.

Theorems like [G:K]=[G:H][H:K][G:K]=[G:H][H:K] when KHGK\subseteq H\subseteq G and GG is "the ambient group" are a real problem in Lean right now because there are several ways to say it and it's a bumpy ride moving from one to the other. This re-interpretation in Group feels more natural to me. Or is it just a competing standard?

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:08):

The proofs of Sylow's theorems are all counting. I am not sure we ever add cardinalities. The fundamental structure is the target, a canonically ordered monoid with 0 called "naturals without addition", whose corresponding group-with-zero-of-fractions is the target of the "ratio of cardinalities" function from morphisms in Group. For Sylow we sometimes use that this monoid with 0 is the free monoid with 0 on the primes.

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:10):

Are Sylow's theorems true for infinite groups?

view this post on Zulip Johan Commelin (Aug 28 2020 at 13:11):

@Kevin Buzzard but why use ideals of int if you could use ordinary int as well? I think in the end that will be easier to use...

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:11):

You mean ordinary nat?

view this post on Zulip Johan Commelin (Aug 28 2020 at 13:12):

oh, either of the two

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:12):

Ideals of int are canonically isomorphic to ordinary nat, but the partial order is wrong

view this post on Zulip Johan Commelin (Aug 28 2020 at 13:12):

I would like newcard (zmod p) = p to be true

view this post on Zulip Johan Commelin (Aug 28 2020 at 13:12):

And we don't want to coerce the right hand side to an ideal

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:13):

For what I have in mind, which is a bunch of counting, and claiming divisibility, and never using addition, the structures on ideal int are better suited.

view this post on Zulip Johan Commelin (Aug 28 2020 at 13:13):

Kevin Buzzard said:

Ideals of int are canonically isomorphic to ordinary nat, but the partial order is wrong

So you want to use \| instead of < in your theorems about card

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:13):

right

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:14):

I'm sad

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:20):

What do I use for the monoid with 0 of fractions @Johan Commelin ? It's Q0\mathbb{Q}_{\geq0} which we have no API for AFAIK...

view this post on Zulip Johan Commelin (Aug 28 2020 at 13:21):

Can you just use rat + nonneg lemmas?

view this post on Zulip Johan Commelin (Aug 28 2020 at 13:22):

At some point we might get api for it... but that won't be tomorrow (-;

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:22):

Interesting idea!

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:22):

but it's a group with zero!

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 13:22):

they're your favourite things! I think that mathematicians missed a trick with this stuff.

view this post on Zulip Kyle Miller (Aug 28 2020 at 17:56):

With theorems like

[G:K]=[G:H][H:K][G:K]=[G:H][H:K] when KHGK\subseteq H\subseteq G

does it makes sense to use the kind of approach in https://hal.inria.fr/hal-00825074v1/document, where KK, HH, and GG are all subgroups of some ambient group? You can always set GG to to get the one where GG is the ambient group.

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 17:57):

Right -- in the odd order work they made all groups into terms of type subgroup G. I'm wondering whether it's better to make all groups into terms of type Group.

view this post on Zulip Reid Barton (Aug 28 2020 at 17:58):

Johan Commelin said:

Kevin Buzzard said:

Ideals of int are canonically isomorphic to ordinary nat, but the partial order is wrong

So you want to use \| instead of < in your theorems about card

As everyone knows, Lagrange's theorem says the order of a subgroup of G is at most the order of G.

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 17:59):

The disjoint union of two groups is not a useful concept, and hence we don't need addition of orders.

view this post on Zulip Kyle Miller (Aug 28 2020 at 18:00):

Does it make sense talking about different Groups as being subgroups of one another?

view this post on Zulip Kyle Miller (Aug 28 2020 at 18:01):

(I'm just not too familiar with Group. Just that it is a type along with a group instance.)

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 18:15):

No, you instead have monic morphisms.

view this post on Zulip Reid Barton (Aug 28 2020 at 18:21):

Don't you need some class equation thing where you argue that there has to be a conjugacy class of size not divisible by p? Or is that another thing?

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 18:25):

For Sylow 1 you need that if a p-group acts on a finite set then the cardinality of the set is congruent to the cardinality of the fixed points mod p (proof: every divisor of p^n which isn't 1 is a multiple of p) and then you need that if the index of a p-group H in G is a multiple of p then so is the index of the p-group in its normaliser, which comes from letting H act on the cosets of H and observing that a coset is fixed iff it's in the normaliser.

view this post on Zulip Reid Barton (Aug 28 2020 at 18:26):

Kevin Buzzard said:

the cardinality of the set is congruent to the cardinality of the fixed points mod p (proof: every divisor of p^n which isn't 1 is a multiple of p)

Isn't there a step in here where you write the cardinality of a set as a sum of quantities derived from the orders of subgroups?

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 18:27):

the set is the disjoint union of the orbits, yes.

view this post on Zulip Kevin Buzzard (Aug 28 2020 at 18:27):

But that's the cardinality of a set


Last updated: May 14 2021 at 19:21 UTC