burnside!

Stream: maths

[Kenny Lau]

theorem burnside : nonempty ((Σ g, fixed G X g) ≃ (orbits G X × G)) :=
⟨calc  (Σ g, fixed G X g)
    ≃ (Σ x, stab G X x) :
  ⟨λ z, ⟨z.2.1, z.1, z.2.2⟩, λ z, ⟨z.2.1, z.1, z.2.2⟩, λ ⟨g, x, h⟩, rfl, λ ⟨x, g, h⟩, rfl⟩
... ≃ (Σ A : orbits G X, Σ x : { x | ⟦x⟧ = A }, stab G X x) :
  ⟨λ z, ⟨⟦z.1⟧, ⟨_, rfl⟩, z.2⟩, λ z, ⟨z.2.1.1, z.2.2⟩, λ ⟨x, z⟩, rfl, λ ⟨A, ⟨x, (hx : ⟦x⟧ = A)⟩, z⟩, sigma.eq hx $ by subst hx⟩
... ≃ (Σ A : orbits G X, Σ x : { x | ⟦x⟧ = A }, stab G X (quotient.out A)) :
  equiv.sigma_congr_right (λ A, equiv.sigma_congr_right (λ ⟨x, (hx : ⟦x⟧ = A)⟩,
    stab_equiv G X _ _ _ (classical.some_spec (quotient.exact (hx.trans (quotient.out_eq A).symm)))))
... ≃ (Σ A : orbits G X, { x | ⟦x⟧ = A } × stab G X (quotient.out A)) :
  equiv.sigma_congr_right (λ A, equiv.sigma_equiv_prod _ _)
... ≃ (Σ A : orbits G X, orbit G X (quotient.out A) × stab G X (quotient.out A)) :
  equiv.sigma_congr_right (λ A, by rw orbit_out_eq_fibre)
... ≃ (Σ A : orbits G X, G) :
  equiv.sigma_congr_right (λ A, classical.choice $ orbit_stab G X _)
... ≃ (orbits G X × G) :
  equiv.sigma_equiv_prod _ _⟩

[Kenny Lau]

@Kevin Buzzard

[Kevin Buzzard]

Now you could do Sylow's theorems :-) but they might not be to your taste. I wonder if there's anything to learn from the Coq presentation of all this. I would imagine they use this sort of stuff everywhere in the odd order theorem.

[Kenny Lau]

@Kevin Buzzard sylow uses burnside?

[Kevin Buzzard]

One proof I've seen does. I'm sure there are others :-) but it wouldn't surprise me if all of them used "counting" in some way.

[Johannes Hölzl]

There is also Sylow's first theorem in Lean2 https://github.com/leanprover/lean2/tree/master/library/theories/finite_group_theory/pgroup.lean
We never did the effort to port this development to Lean 3, and a lot of stuff changed since them. But I think it would be worthwhile to take a look.

[Kenny Lau]

I say, the theory of (finite) cardinality in Lean is not well-developed

[Johannes Hölzl]

Come on, you know that mathlib is a open source project. It's only as developed, as people put an effort into developing it.
This includes by the way answering comments on pull requests ;-)

[Kenny Lau]

well

[Kenny Lau]

fixing those things created more error for me, so I need time to de-frustrate myself and to fix those errors

[Kevin Buzzard]

...and revise for mechanics. I might soon need some other localization facts which aren't there yet, but I still didn't finish wrestling with compactness. Is Johannes talking about localization or something else?

[Kenny Lau]

free group

[Kenny Lau]

https://github.com/leanprover/mathlib/pull/89#discussion_r179398893