Nat.card version of card_orbit_mul_card_stabilizer_eq_card_g

Stream: Is there code for X?

[Xavier Roblot]

we have docs#MulAction.card_orbit_mul_card_stabilizer_eq_card_group which uses Fintype and thus can be difficult to use in some cases. The Nat.card version is very easy to prove (well, it's essentially the same proof) but seems to be lacking:

module

public import Mathlib.Data.Set.Card
public import Mathlib.GroupTheory.GroupAction.Quotient

open MulAction

@[to_additive]
theorem MulAction.card_orbit_mul_card_stabilizer_eq_card_group' (α : Type*) {β : Type*} [Group α]
    [MulAction α β] (b : β) :
    Nat.card (orbit α b) * Nat.card (stabilizer α b) = Nat.card α := by
  simpa using Nat.card_congr (MulAction.orbitProdStabilizerEquivGroup α b)

Does it exist somewhere in another form? Should it be added to Mathlib otherwise? Note that it cannot be in the same file as docs#MulAction.card_orbit_mul_card_stabilizer_eq_card_group since this file contains the line

assert_not_exists Cardinal

[Ruben Van de Velde]

I have a branch to redefine Nat.card without cardinals that I should have another look at

[Thomas Browning]

Xavier Roblot said:

Does it exist somewhere in another form?

Yes: docs#MulAction.index_stabilizer (but I agree that the cardinal dependence is annoying and should be removed).

[Violeta Hernández]

Why do we want Nat.card without cardinals? I think the real goal should be to minimize cardinal imports.

[Violeta Hernández]

Or split out the material that doesn't depend on choice or Schröder-Bernstein or all the actually technical stuff

[Ruben Van de Velde]

I don't know that "we" (as in the mathlib maintainer) want it, but cardinals seem somewhat heavy just to get the number of elements in a finite type, so I wanted to figure out how much work it would be not to use them

[Violeta Hernández]

Cardinals are nothing more than a Quotient of Type. We could probably define them in Init if we wanted to.