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