Zulip Chat Archive

Stream: maths

Topic: burnside!


view this post on Zulip 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 _ _⟩

view this post on Zulip Kenny Lau (Apr 16 2018 at 05:03):

@Kevin Buzzard

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 16 2018 at 06:39):

@Kevin Buzzard sylow uses burnside?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 16 2018 at 07:11):

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

view this post on Zulip 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.
This includes by the way answering comments on pull requests ;-)

view this post on Zulip Kenny Lau (Apr 16 2018 at 07:23):

well

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Apr 16 2018 at 07:25):

free group

view this post on Zulip 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