## 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: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?

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: May 11 2021 at 16:22 UTC