Zulip Chat Archive

Stream: maths

Topic: modulo group action


Patrick Massot (Sep 13 2018 at 19:23):

Do I understand correctly that we have a file defining group action and a file defining left and right cosets in a group, but no link between those? And we don't have G\X if G acts on X?

Kenny Lau (Sep 13 2018 at 19:32):

we do have orbit-stabalizer theorem, if that's what you mean

Chris Hughes (Sep 13 2018 at 19:33):

I'm not sure exactly what you mean, but it may well be part of my Sylow PR.

Patrick Massot (Sep 13 2018 at 19:43):

No, I don't mean orbit stabilizer. I mean: if G acts on X, quotient X by "x equivalent to y if there exists g such that y = g x"

Patrick Massot (Sep 13 2018 at 19:44):

This: https://github.com/leanprover/mathlib/pull/257/files#diff-a1c68f03014617e86345e35b6885b923R90

Patrick Massot (Sep 13 2018 at 19:45):

What is the status of this PR?

Chris Hughes (Sep 13 2018 at 19:46):

On hold because of the cardinals of finite sets issue.

Patrick Massot (Sep 13 2018 at 19:50):

Is this something someone is working on?

Chris Hughes (Sep 13 2018 at 19:50):

Not really.

Chris Hughes (Sep 13 2018 at 19:51):

I'm playing with tactics, and hope to be able to write a tactic to deal with it at some point.

Chris Hughes (Sep 13 2018 at 19:51):

But it could take a while

Chris Hughes (Sep 13 2018 at 19:53):

I could separate out the bits that aren't about finite sets, and PR them first if you're desperate for it. Do you want the fact that G acts on the cosets of a subgroup as well?

Patrick Massot (Sep 13 2018 at 19:54):

I'm not desperate, I wrote:

import group_theory.group_action

variables {X : Type*} {G : Type*} [group G] (ρ : G  X  X) [is_group_action ρ]

lemma is_group_action.inverse_left (g : G) : (ρ g⁻¹)  ρ g = id :=
begin
  ext x,
  change ρ g⁻¹ (ρ g x) =  x,
  rw  is_monoid_action.mul ρ g⁻¹ g x,
  simp [is_monoid_action.one ρ]
end

lemma is_group_action.inverse_right (g : G) : (ρ g)  ρ g⁻¹ = id :=
by simpa using is_group_action.inverse_left ρ g⁻¹

def action_rel : setoid X :=
⟨λ x y,  g, ρ g x = y, ⟨λ x, (1 : G),  is_monoid_action.one ρ x,
  begin
  { split,
    { rintros x y g, h,
      existsi g⁻¹,
      rw h,
      exact congr_fun (is_group_action.inverse_left ρ g) x },
    { rintros x y z g, h g', h',
      existsi g'*g,
      rw [is_monoid_action.mul ρ, h, h'] } }
  end⟩⟩

Patrick Massot (Sep 13 2018 at 19:54):

So I have my setoid

Patrick Massot (Sep 13 2018 at 19:55):

I don't think your PR contains much more in this direction

Patrick Massot (Sep 13 2018 at 20:16):

Does someone know where is the lemma saying that if a finite set surjects onto a type then this type is finite?

Reid Barton (Sep 13 2018 at 20:20):

fintype.of_surjective I guess

Patrick Massot (Sep 13 2018 at 20:27):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC