modulo group action

Stream: maths

[Patrick Massot]

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]

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

[Chris Hughes]

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

[Patrick Massot]

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]

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

[Patrick Massot]

What is the status of this PR?

[Chris Hughes]

On hold because of the cardinals of finite sets issue.

[Patrick Massot]

Is this something someone is working on?

[Chris Hughes]

Not really.

[Chris Hughes]

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

[Chris Hughes]

But it could take a while

[Chris Hughes]

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]

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]

So I have my setoid

[Patrick Massot]

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

[Patrick Massot]

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

[Reid Barton]

fintype.of_surjective I guess

[Patrick Massot]

Thanks!