## Stream: maths

### Topic: burnside!

#### Kenny Lau (Apr 16 2018 at 05:03):

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 _ _⟩


@Kevin Buzzard

#### Kevin Buzzard (Apr 16 2018 at 06:37):

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 (Apr 16 2018 at 06:39):

@Kevin Buzzard sylow uses burnside?

#### Kevin Buzzard (Apr 16 2018 at 06:49):

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 (Apr 16 2018 at 07:11):

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 (Apr 16 2018 at 07:11):

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

#### Johannes Hölzl (Apr 16 2018 at 07:20):

Come on, you know that mathlib is a open source project. It's only as developed, as people put an effort into developing it.

well

#### Kenny Lau (Apr 16 2018 at 07:23):

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

#### Kevin Buzzard (Apr 16 2018 at 07:25):

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

free group

#### Kenny Lau (Apr 16 2018 at 07:25):

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

Last updated: May 14 2021 at 19:21 UTC