Set vs Subtype in Equiv.Perm

Stream: Is there code for X?

[Antoine Chambert-Loir]

Given a Type α, G : Subgroup (Equiv.Perm α) and s : Set α, I can construct an action of stabilizer G s either on s, or on Subtype s, but the former initially seemed easier to deal with, and has been sufficient up to now.

Here are the definitions, as I could give them… (The second one leads to universe issues in the Lean 4 playground)

import Mathlib.GroupTheory.GroupAction.Basic
import Mathlib.Data.Set.Pointwise.SMul


namespace MulAction

open scoped Pointwise

variable (G : Type*) (α : Type*) [Group G] [MulAction G α]

/-- The instance that makes the stabilizer of a set acting on that set -/
instance HasSmul.ofStabilizer (s : Set α) : SMul (stabilizer G s) s where
  smul g x := ⟨g • ↑x, by
    conv_rhs => rw [← mem_stabilizer_iff.mp g.prop]
    exact Set.smul_mem_smul_set x.prop⟩

@[simp]
theorem HasSmul.smul_stabilizer_def (s : Set α) (g : stabilizer G s) (x : s) :
    (g • x : α) = (g : G) • (x : α) := rfl

/-- The mul_action of stabilizer a set on that set -/
instance ofStabilizer_set (s : Set α) : MulAction (stabilizer G s) s  where
  one_smul x := by rw [← Subtype.coe_inj, HasSmul.smul_stabilizer_def,
    Subgroup.coe_one, one_smul]
  mul_smul g k x := by
    simp only [← Subtype.coe_inj, HasSmul.smul_stabilizer_def, Subgroup.coe_mul,
      MulAction.mul_smul]

/-- The mul_action of stabilizer a set on the associated subtype  -/
instance MulAction.ofStabilizer_subtype : MulAction (stabilizer G s) (Subtype s) where
  smul := fun g a ↦ by
    use g.val • a.val
    let this : g.val • a.val ∈ g.val • s := Set.smul_mem_smul_set a.prop
    simpa [mem_stabilizer_iff.mp g.prop] using this
  one_smul := fun ⟨a, ha⟩ ↦ by
    rw [Subtype.mk_eq_mk]
    apply one_smul
  mul_smul := fun ⟨g, hg⟩ ⟨h, hh⟩ ⟨a, ha⟩ ↦ by
    rw [Subtype.mk_eq_mk]
    apply mul_smul

The problem now appears when I want to make use ofEquiv.Perm.ofSubtype and Equiv.Perm.toSubtype because they seem to really make the difference between Equiv.Perm s and Equiv.Perm (Subtype s).
For example, if I am given g : Equiv.Perm s, then Equiv.Perm.ofSubtype g returns an error message.
What would you advice ? Have both definitions ?

[Eric Wieser]

That last one doesn't compile for me in the web editor

[Eric Wieser]

And with set_option autoImplicit false, it complains that you didn't specify s

[Eric Wieser]

Did you intend s to be a set or a α -> Prop?

[Antoine Chambert-Loir]

Neither does it compile for me there…
In my applications, s was a set, and I want to prove that φ : stabilizer G s → Equiv.Perm s := MulAction.toPerm is surjective.
After intro g, I am given g : Perm ↑s, and I have to prove ∃ a, φ a = g. However, use Equiv.Perm.ofSubtype g leads to an error.

[Eric Wieser]

If s is a set, then Subtype s is nonsense

[Eric Wieser]

If s is a α -> Prop, then stabilizer G s is nonsense

[Eric Wieser]

The non-nonsense version of that last declaration is

instance MulAction.ofStabilizer_subtype (p : α -> Prop) :
  MulAction (stabilizer G (setOf p)) (Subtype p) where

[Kyle Miller]

"nonsense" doesn't seem apt, since up to defeq Subtype s is "fine". But Subtype (· ∈ s) is how it's meant to be said (or {x // x ∈ s}) -- sets and predicates are the same by defeq but different syntactically.

[Antoine Chambert-Loir]

Here is a MWE of the problem with the first declaration (before I tried possibly non-sensical things)

import Mathlib.GroupTheory.GroupAction.Basic
import Mathlib.Data.Set.Pointwise.SMul


namespace MulAction

open scoped Pointwise

variable (G : Type*)  [Group G]
  (α : Type*) [DecidableEq α] [MulAction G α]
  (s : Set α) [DecidablePred fun x => x ∈ s]

/-- The instance that makes the stabilizer of a set acting on that set -/
instance HasSmul.ofStabilizer (s : Set α) : SMul (stabilizer G s) s where
  smul g x := ⟨g • ↑x, by
    conv_rhs => rw [← mem_stabilizer_iff.mp g.prop]
    exact Set.smul_mem_smul_set x.prop⟩

@[simp]
theorem HasSmul.smul_stabilizer_def (s : Set α) (g : stabilizer G s) (x : s) :
    (g • x : α) = (g : G) • (x : α) := rfl

/-- The mul_action of stabilizer a set on that set -/
instance ofStabilizer_set (s : Set α) : MulAction (stabilizer G s) s  where
  one_smul x := by rw [← Subtype.coe_inj, HasSmul.smul_stabilizer_def,
    Subgroup.coe_one, one_smul]
  mul_smul g k x := by
    simp only [← Subtype.coe_inj, HasSmul.smul_stabilizer_def, Subgroup.coe_mul,
      MulAction.mul_smul]

def φ : stabilizer G s → Equiv.Perm s := MulAction.toPerm

example : Function.Surjective (φ G α s) := by
  intro g
  -- gives an error
  use Equiv.Perm.ofSubtype g
  sorry

[Eric Wieser]

I don't understand what you're expecting the use to do there

[Eric Wieser]

You need a witness of type { x // x ∈ stabilizer G s }, you're giving a Perm α

[Antoine Chambert-Loir]

Two things that confuse me even more:

• Lean has another way to create a type from s : Set α, namely the type Elem s of elements of s.
• Some lemmas such as docs#Set.mem_def do not respect the syntactic distinction and simultaneously treat s as Set α and as α → Prop

[Eric Wieser]

x : s is notation for x : Elem s

[Antoine Chambert-Loir]

Eric Wieser said:

You need a witness of type { x // x ∈ stabilizer G s }, you're giving a Perm α

Oh, maybe I was just blocked by the different way Lean3 and Lean4 handle subtypes with use. Let me see!
(Lean3 asked me a proof of the subtype membership, and Lean4 just stops.)

[Eric Wieser]

Well in this case you need to provide a subtype of G not Perm α, so there isn't really a reasonable side-goal to emit

[Antoine Chambert-Loir]

Well, since the code compiled under Lean3, the problem is not only me writing pure nonsense stuff. But indeed, it seem that the problem is when Lean created 3 subgoals after use Equiv.Perm.ofSubtype g, Lean 4 whants me to type use <<Equiv.Perm.ofSubtype g, ?_>, ?_> for that.

[Antoine Chambert-Loir]

Thank you for your help and sorry for all the possible nonsense…

[Kyle Miller]

@Antoine Chambert-Loir I'm not sure if it helps, but there's now use!, which is like the Lean 3 use. If you're proving an existential whose domain is a subtype, use requires you give the whole element of that subtype, but use! is willing to let you give just the underlying value, leaving the membership as an extra goal.

[Eric Wieser]

Antoine Chambert-Loir said:

Lean 4 whants me to type use <<Equiv.Perm.ofSubtype g, ?_>, ?_> for that.

This doesn't work for me either in your example

[Antoine Chambert-Loir]

My MWE was sub-minimal and I had a bunch of other assumptions that allowed to fill the ?_.
(This belongs to the proof that MulAction.stabilizer (Equiv.Perm A) s is a maximal subgroup of Equiv.Perm A is a maximal subgroup of Equiv.Perm A when 2 * s.ncard < Fintype.card A.)

[Eric Wieser]

It's not that the ?_ contain things that are impossible to prove, but that Equiv.Perm.ofSubtype g still has the wrong type in your example

[Eric Wieser]

Either way, sounds like Kyle tracked down what your original issue was