Cardinality of subgroup

Stream: Is there code for X?

[Johan Commelin]

What is the recommended way to talk about the card of a subgroup of a finite group?

[Mario Carneiro]

card S?

[Johan Commelin]

Which card is that?

[Mario Carneiro]

I guess fintype.card if you want a nat

[Johan Commelin]

Aah, with some coercions under the hood. Ok.

[Johan Commelin]

failed to synthesize type class instance for
α : Type u,
_inst_1 : group α,
_inst_3 : fintype α
fintype ↥(subgroup.center α)

[Johan Commelin]

Lean is not yet convinced :sad:

[Eric Wieser]

decidable_eq α?

[Johan Commelin]

Doesn't help

[Eric Wieser]

I think you need to add a decidable_pred (∈ center G) instance

[Eric Wieser]

Which probably falls out by just unfolding

[Eric Wieser]

Or as decidable.forall if that exists

[Eric Wieser]

We already have such an instance for range, docs#monoid_hom.decidable_mem_range

[Johan Commelin]

We really need fincard.

[Johan Commelin]

Because this issue is not just restricted to subgroup.center of course.

[Johan Commelin]

So we'll need > 57 of such instances, for all the variants.

[Eric Wieser]

Well, we already have to write mem_center by hand

[Eric Wieser]

So we just need a decidable_mem_center next to every one of those

[Eric Wieser]

Perhaps derive or simps could handle this type of thing

[Johan Commelin]

But we also need it for centralizer and for normalizer and for subfoo.whatever.

[Eric Wieser]

Yeah, but we need mem_ lemmas for all of those too

[Eric Wieser]

So it's only a constant factor more boilerplate than we're already obliged to write

[Eric Wieser]

In theory simps could generate those mem lemmas quite easily, but I'm pretty sure we haven't tried configuring it to.

[Kevin Buzzard]

Johan Commelin said:

We really need fincard.

We have it, right? Does docs#nat.card work?

[Johan Commelin]

Ooh! I didn't realize that we had it. Great!

[Eric Wieser]

#9825

[Johan Commelin]

Thanks!

[Johan Commelin]

variables (G) [group G] [fintype G] {M : Type*} [monoid M]

-- move this
lemma is_conj_comm (g h : M) : is_conj g h ↔ is_conj h g :=
⟨is_conj.symm, is_conj.symm⟩

-- move this
lemma mem_orbit_conj_act_iff {G : Type*} [group G] (g h : G) :
  g ∈ orbit (conj_act G) h ↔ is_conj g h :=
by { rw [is_conj_comm, is_conj_iff, mem_orbit_iff], exact iff.rfl }

-- move this
lemma orbit_rel_r (X : Type*) [mul_action G X] :
  (orbit_rel G X).r = λ x y, x ∈ orbit G y := rfl

-- move this
lemma orbit_rel_r_apply {X : Type*} [mul_action G X] (x y : X) :
  @setoid.r _ (orbit_rel G X) x y ↔ x ∈ orbit G y := iff.rfl

lemma class_equation' [decidable_rel (is_conj : G → G → Prop)] :
  ∑ (x : conj_classes G), x.fincarrier.card = fintype.card G :=
begin
  let e : quotient (orbit_rel (conj_act G) G) ≃ conj_classes G :=
  quotient.congr_right (λ g h, mem_orbit_conj_act_iff g h),
  letI : fintype (quotient (orbit_rel (conj_act G) G)) := by { classical, apply_instance },
  rw ← e.sum_comp,
  classical,
  rw card_eq_sum_card_group_div_card_stabilizer (conj_act G) G,
  refine finset.sum_congr rfl _,
  rintro ⟨g⟩ -,
  rw [← card_orbit_mul_card_stabilizer_eq_card_group (conj_act G) (quotient.out' (quot.mk _ g)),
    nat.mul_div_cancel, fintype.card_of_finset, conj_classes.fincarrier],
  swap, { rw fintype.card_pos_iff, apply_instance },
  intro h,
  simp only [true_and, finset.mem_univ, finset.mem_filter, mem_orbit_conj_act_iff,
    ← conj_classes.mk_eq_mk_iff_is_conj],
  refine eq_iff_eq_cancel_left.2 (conj_classes.mk_eq_mk_iff_is_conj.2 _),
  show is_conj g _,
  rw [← mem_orbit_conj_act_iff, ← orbit_rel_r_apply],
  apply quotient.exact',
  rw [quotient.out_eq'],
  refl
end

[Eric Wieser]

I wasn't aware of docs#conj_classes. What's fincarrier?

[Johan Commelin]

I just defined it. Sorry, I forgot to copy it.

[Eric Wieser]

I was wondering if it was similar to @Yaël Dillies's finpartition

[Yaël Dillies]

#9795 for reference

[Johan Commelin]

Oooh, I have no idea!

[Yaël Dillies]

finpartition is the finset bundled generalized version of setoid.partition.

[Eric Wieser]

docs#setoid.partition doesn't exist

[Eric Wieser]

I guess you meant docs#setoid.is_partition

[Johan Commelin]

I now have a sorry-free

lemma class_equation :
  nat.card (subgroup.center G) + ∑ᶠ x ∈ noncenter G, nat.card (carrier x) = nat.card G :=

(G is a group)

[Johan Commelin]

#9828