Infinite index definition

Stream: maths

[Chris Birkbeck]

This is likely a stupid question but, using our current definition of subgroup index, where an index of zero means it has infinite index, how does one formalise the proof of transitivity of commensurability here : https://planetmath.org/commensurablesubgroups

Since with the current definitions, one wants to prove some index is not zero, but that isn't ruled out by the proof given.

Doesn't having zero represent the infinite index break proofs where one tries to bound the index? (or at least make it so we need alternative proofs?). I expect I'm just being silly, and this is a non-issue.

[Eric Wieser]

(docs#subgroup.index for reference)

[Eric Wieser]

If you want to talk about infinite indices, you can use # (quotient_group.quotient H)

[Eric Wieser]

index is just that, converted to a nat.

[Alex J. Best]

You could do the contrapositive quite neatly if $[S_1 : S_1 \cap S_3] = 0$ then $[S_1 : S_1 \cap S_2 \cap S_3] = 0$ (this should be a general lean lemma) so $[S_1 : S_1 \cap S_2][S_1\cap S_2 : S_1\cap S_2 \cap S_3] = 0$ (rewriting), but $[S_1 : S_1 \cap S_2] \ne 0$ so $[S_1\cap S_2 : S_1\cap S_2 \cap S_3] = 0$ aaand now I'm confused does this imply $[ S_1 : \cap S_1 \cap S_3] =0$

[Chris Birkbeck]

aha, sure, I think I was just being silly then. Both these things would work. I still wonder why not just have index map into enat? is it that much better to have it into nat?

[Johan Commelin]

I've never enjoyed working with enat.

[Johan Commelin]

I don't know exactly what is wrong about it's API, but I never really look forward to using it

[Yaël Dillies]

Isn't it still the problem that it's not with_top ℕ?

[Alex J. Best]

One issue is that enat doesn't have a multiplication defined it seems

[Alex J. Best]

So for this sort of thing (subgroup indices) you've fallen at the first hurdle

[Yaël Dillies]

Uh what

[Chris Birkbeck]

Alex J. Best said:

One issue is that enat doesn't have a multiplication defined it seems

Ahh ok then I take it back, I dont want enat then.

[Alex J. Best]

Well maybe we should define mul on it, I think the issue is that having both zero and infinity means its impossible to make it a linear_ordered_comm_monoid so all the lemmas you'd have to prove by hand excluding the edge cases anyway. What you really want for values of an index is the non-existing epnat of positive naturals including infinity, but at that point maybe its just easiest to use nat

[Alex J. Best]

There is a mul on with_top nat though

[Yakov Pechersky]

epnat is just (with_top pnat), no?

[Alex J. Best]

Yes but I'm not sure that definition will have enough api on its own without some more work going into it?

[Yakov Pechersky]

Right, building that api is separate from having the right api for subgroup.index

[Kevin Buzzard]

I think that subgroup index being 0 when it's infinite is a good idea -- stuff like "order of element divides order of group" works great with this convention. In a parallel universe we wouldn't say "infinite order" for elements of a group, we'd say "order 0" because "g has order n" then means that the ideal of integers $t$ such that $g^t=1$ is generated by $n$ in all cases. There is no math-nice multiplication on enat because what do we do with $0\times\infty$? However "infinite index is 0" turns out to be math-nice I think, and well-behaved under multiplication (for example the tower law is true with this convention).

[Eric Wieser]

Is there a reason not to work with the underlying cardinals directly here?

[Eric Wieser]

Or are they worse than enat?

[Johan Commelin]

Yes, I think the order of a group is tightly related to the order of elements. And as Kevin points out, ℕ works very well there.

[Kevin Buzzard]

The point is an index of two groups, like the order of a group, cannot actually be 0, so 0 is a great place put the infinite index stuff. Yes we could use cardinals but this would make things more complex and it's not clear whether the payoff is any better because in reality mathematicians do not use cardinals. Cardinals are used for a fine-grained study of the infinite, but most mathematics away from set theory does not need such a fine-grained measure of the infinite, something is either finite or countable or uncountable, and this will do in 99.9% of mathematics (100% of mathematics?) away from foundational questions which are not our main object of concern.

[Kevin Buzzard]

For example the fact that CH is undecidable is actually very good evidence that it's the wrong question in terms of mainstream mathematics

[Chris Birkbeck]

Kevin Buzzard said:

I think that subgroup index being 0 when it's infinite is a good idea -- stuff like "order of element divides order of group" works great with this convention. In a parallel universe we wouldn't say "infinite order" for elements of a group, we'd say "order 0" because "g has order n" then means that the ideal of integers $t$ such that $g^t=1$ is generated by $n$ in all cases. There is no math-nice multiplication on enat because what do we do with $0\times\infty$? However "infinite index is 0" turns out to be math-nice I think, and well-behaved under multiplication (for example the tower law is true with this convention).

Yeah I think I see why this is a good idea now and I'd rather make miniscule changes to the proofs instead of making some epnat api.

[David Wärn]

I agree that with_top pnat would be a natural domain for the index of a subgroup. But this monoid is isomorphic to nat (by identifying $\infty$ with 0), so you may as well work with nat.

One way of understanding this isomorphism is that it maps n : nat to the cardinality of zmod n i.e. the index of $n\mathbb Z$ in $\mathbb Z$. When you define the order of a group, it's natural to work directly with ideals in $\mathbb Z$, and so "order 0" makes a lot of sense. But I don't think it makes any immediate sense to say that the index of a subgroup is 0 (the index is a cardinality, not an ideal) -- it's really only justified by the isomorphism with_top pnat = nat.

[Alex J. Best]

It's not isomorphic to nat as an ordered monoid though, which is why the proof gets a little more annoying than the one Chris posted

[Johan Commelin]

Isn't the relevant ordering the divisibility relation?

[Alex J. Best]

I've been struggling to understand whether this is another case where we should treat junk values as 0 (like defining 1/x to be 0 for x = 0) or whether it would be good to use with_top pnat if the API was more developed, this case feels somehow different to the usual junk value story but i can't put my finger on why...

[Yakov Pechersky]

It's different because you're never using the addition of indices or orders.

[Yakov Pechersky]

Closely related to the divisibility ordering