Card structure on `Group`

Stream: maths

[Kevin Buzzard]

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

If $G$ is a finite group and $g\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 $\mathbb{Z}$ corresponding to the kernel of $n\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 $\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 $g$ divides the order of $G$" now become $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 $H$ is a subgroup of $G$ then there's a monic homomorphism from $H$ to $G$, and there is an invariant $[o(G):o(H)]$ or $[o(H):o(G)]$ attached to the morphism, which is the index of $H$ in $G$ (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 $\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]$ when $K\subseteq H\subseteq G$ and $G$ 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?

[Kevin Buzzard]

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.

[Kevin Buzzard]

Are Sylow's theorems true for infinite groups?

[Johan Commelin]

@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...

[Kevin Buzzard]

You mean ordinary nat?

[Johan Commelin]

oh, either of the two

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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.

[Johan Commelin]

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

[Kevin Buzzard]

right

[Kevin Buzzard]

I'm sad

[Kevin Buzzard]

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

[Johan Commelin]

Can you just use rat + nonneg lemmas?

[Johan Commelin]

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

[Kevin Buzzard]

Interesting idea!

[Kevin Buzzard]

but it's a group with zero!

[Kevin Buzzard]

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

[Kyle Miller]

With theorems like

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

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

[Kevin Buzzard]

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.

[Reid Barton]

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.

[Kevin Buzzard]

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

[Kyle Miller]

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

[Kyle Miller]

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

[Kevin Buzzard]

No, you instead have monic morphisms.

[Reid Barton]

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?

[Kevin Buzzard]

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.

[Reid Barton]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

But that's the cardinality of a set