mul_actions

Stream: maths

[Antoine Chambert-Loir]

Given an action of a group G on a set X, one can define related actions such as the product X × X
and the complement of the diagonal { x : X × X | x.1 ≠ x.2 }.
It starts nicely, but then I can't manage to say that the obtained action has given properties.
It seems I have to define an instance, but I am told by Lean that sub_mul_action is not a class.

import group_theory.group_action.basic
import group_theory.group_action.prod
import group_theory.group_action.sub_mul_action

variables (G : Type*) [group G] (X : Type*) [mul_action G X]

open equiv.perm equiv

variables {G} {X}

def square_minus_diag (G : Type*) [group G] (X : Type*) [mul_action G X] :
 sub_mul_action G (X × X) :=
{ carrier := { x : X × X | x.1 ≠ x.2 },
  smul_mem' := λ g x hx,
  begin
    rw set.mem_set_of_eq at hx ⊢,
    simp only [hx, prod.smul_snd, prod.smul_fst, ne.def, smul_left_cancel_iff, not_false_iff],
  end, }

-- doesn't type
example [nontrivial X]: mul_action.is_pretransitive G (square_minus_diag.mul_action) :=
begin
  sorry,
end

[Adam Topaz]

Does deleting the last .mul_action fix it?

[Adam Topaz]

Maybe after adding additional variables G and X?

[Antoine Chambert-Loir]

No, I get zigouigouis (twiddles) under mul_action and under square_minus_diag.

[Adam Topaz]

Hmm... I'm on my phone so I can't be more helpful, but I try it out in a few mins on the computer

[Johan Commelin]

I would expect that you need to write

example [nontrivial X]: mul_action.is_pretransitive G (square_minus_diag G X) :=
begin
  sorry,
end

[Johan Commelin]

What is the exact error that you get?

[Antoine Chambert-Loir]

It was :

invalid field notation, type is not of the form (C ...) where C is a constant
  square_minus_diag
has type
  Π (G : Type ?) [_inst_3 : group G] (X : Type ?) [_inst_4 : mul_action G X], sub_mul_action G (X × X)

[Johan Commelin]

@Antoine Chambert-Loir Aha, but do I understand correctly that my suggestion works?

[Johan Commelin]

The error tells you that square_minus_diag expects explicit arguments G and X.

[Antoine Chambert-Loir]

I never understand those Type ? messages. I thought it meant Lean couldn't find the type, but apparently that's not exactly that.

[Kevin Buzzard]

The error means "you types square_minus_diag.mul_action , but the thing is, square_minus_diag is a function which wants to eat a group G and a G-module X, so in particular its type is a function type, so square_minus_diag.mul_action means something like function.mul_action square_minus_diag which makes no sense because function.mul_action doesn't exist"

[Kevin Buzzard]

PS I love the "pre-transitive" name! It's like pre-primes being 1 or prime.

[Antoine Chambert-Loir]

I am not responsible for pretransitive !
One comment in the #10253 is that primitive should be turned to preprimitive, removing the nonempty hypothesis.