# Zulip Chat Archive

## Stream: maths

### Topic: Card structure on `Group`

#### 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 $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 (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.

#### Kevin Buzzard (Aug 28 2020 at 13:10):

Are Sylow's theorems true for infinite groups?

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

#### Kevin Buzzard (Aug 28 2020 at 13:11):

You mean ordinary nat?

#### Johan Commelin (Aug 28 2020 at 13:12):

oh, either of the two

#### Kevin Buzzard (Aug 28 2020 at 13:12):

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

#### Johan Commelin (Aug 28 2020 at 13:12):

I would like `newcard (zmod p) = p`

to be true

#### Johan Commelin (Aug 28 2020 at 13:12):

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

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

#### 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

#### Kevin Buzzard (Aug 28 2020 at 13:13):

right

#### Kevin Buzzard (Aug 28 2020 at 13:14):

I'm sad

#### Kevin Buzzard (Aug 28 2020 at 13:20):

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 (Aug 28 2020 at 13:21):

Can you just use `rat`

+ `nonneg`

lemmas?

#### Johan Commelin (Aug 28 2020 at 13:22):

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

#### Kevin Buzzard (Aug 28 2020 at 13:22):

Interesting idea!

#### Kevin Buzzard (Aug 28 2020 at 13:22):

but it's a group with zero!

#### Kevin Buzzard (Aug 28 2020 at 13:22):

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

#### Kyle Miller (Aug 28 2020 at 17:56):

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 (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`

.

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

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

#### Kyle Miller (Aug 28 2020 at 18:00):

Does it make sense talking about different `Group`

s as being subgroups of one another?

#### 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.)

#### Kevin Buzzard (Aug 28 2020 at 18:15):

No, you instead have monic morphisms.

#### 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?

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

#### 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?

#### Kevin Buzzard (Aug 28 2020 at 18:27):

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

#### 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