permutations preserving a function

Stream: Is there code for X?

[Yury G. Kudryashov]

Do we have this subgroup? If no, then how should I call it?

def  name_me {X Y} (f : X -> Y) : subgroup (equiv.perm X) :=
{ carrier := {e | \forall x, f (e x) = f x}
 .. }

[Kyle Miller]

Should it be f : X -> X? Otherwise I'm not sure how to make sense of e (f x) = e x

[Yury G. Kudryashov]

Fixed: should be f (e x) = f x

[Kyle Miller]

Do we have a way to specify the equiv.perm X and equiv.perm Y actions on X -> Y? Then name_me would be the docs#mul_action.stabilizer of the action of equiv.perm X on X -> Y. (There should be an op in there for this action.)

[Damiano Testa]

You could also abstract this by having a group acting on both X and Y and looking at equivariants for the action. The case that Yury mentions is the one where the action on Y is trivial (and the group is equiv.perm X).
EDIT: I think that I confused the quantification over X and over f! :face_palm:
Sorry for the noise.

[Kyle Miller]

Category theory has docs#category_theory.End.mul_action_left for nearly the relevant action (but it's the action of X -> X rather than equiv.perm X).

docs#pi.mul_action gives the action of equiv.perm Y on X -> Y, but I haven't been able to find the action of equiv.perm X on X -> Y.

[Yaël Dillies]

Looks like the f locus of the stabilizer of the action of perm X on X to me.

[Eric Wieser]

We don't have any such right actions by functions

[Eric Wieser]

What would the action of f : (perm A)ᵐᵒᵖ on g : A → (perm A)ᵐᵒᵖ be?

• The left action via docs#pi.mul_action gives
  λ x, op (λ y, (g x).unoo (f.unop y))

• The right action that you want above would gives
  λ x, op (λ y, (g (f.unop x)).unop y)

This is a diamond :(

[Yury G. Kudryashov]

Anyway, this would define a subgroup in the opposite group. While I can use docs#subgroup.opposite to bring it back to the group of permutations, this is a rather long line and gives poor definitional equalities.

[Yury G. Kudryashov]

So, I would prefer to add my definition under some name to the library. How would you call it?

[Junyan Xu]

docs#subgroup.opposite is definitionally the identity as far as carrier is concerned, and I don't think your definition will be non-defeq to it...

[Eric Wieser]

It probably will be non-defeq because of the irreducible attribute on docs#mul_opposite. Personally I think we should remove that attribute, docs#add_opposite doesn't have the attribute.

[Junyan Xu]

#16760

[Antoine Chambert-Loir]

I am going back to this stuff, because I need to prove an isomorphism between the group of permutations f : Equiv.Perm X preserving p : X → Y (this is MulAction.Stabilizer (Equiv.Perm X) p), where the action is given by docs#arrowAction, and the product of the groups Equiv.Perm {x | p x = y}, for y: Y.
The arrow from MulAction.Stabilizer (Equiv.Perm X) p is easy to define, but the other one poses me some problems.
I could define it in the case that ultimately interests me, when X and Y are finite, but there is no reason for this restriction.

import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.GroupTheory.GroupAction.Basic

/-  Subgroup of `Equiv.Perm α` preserving a fibration `p : α → ι` -/

variable {α ι : Type*} {p : α → ι}

open Equiv MulAction

local instance  : MulAction (Equiv.Perm α) (α → ι) := arrowAction

lemma arrowAction.mem_stabilizer_iff {g : Perm α} :
    g ∈ stabilizer (Perm α) p ↔ p ∘ g = p := by
  rw [MulAction.mem_stabilizer_iff]
  change p ∘ (g⁻¹ : Perm α) = p ↔ _
  constructor
  all_goals {
    intro h
    conv_lhs => rw [← h]
    ext a
    simp only [Function.comp_apply, Equiv.Perm.inv_apply_self, Equiv.Perm.apply_inv_self] }

def Φ : stabilizer (Perm α) p ≃* ((i : ι) → Perm {a | p a = i}) := {
  toFun := fun g i ↦ by
    apply Perm.subtypePerm g
    intro a
    simp only [Set.mem_setOf_eq]
    rw [← Function.comp_apply (f := p), arrowAction.mem_stabilizer_iff.mp g.prop]
  invFun := sorry
  left_inv := sorry
  right_inv := sorry
  map_mul' := fun g h ↦ by
    ext i
    dsimp }

Now, if I wish to fill the sorry and define the inverse function, I can start nicely with

def φ_invFun : ((i : ι) → Perm {a | p a = i}) → α → α :=
  fun g a ↦ g (p a) (⟨a, by simp only [Set.mem_setOf_eq]⟩ : {x | p x = p a})


lemma comp_φ_invFun (g : (i : ι) → Perm {a | p a = i}) (a) : p (φ_invFun g a) = p a := by
  unfold φ_invFun
  simp only [Set.mem_setOf_eq, Set.coe_setOf]
  exact (g (p a) (⟨a, by simp only [Set.mem_setOf_eq]⟩ : {x | p x = p  a})).prop

but I am then rapidly stuck because I can't rewrite the natural equalities given by comp_φ_invFun. (Motive is not type-correct…)

[Antoine Chambert-Loir]

(As for naming this subgroup, @Yury G. Kudryashov , if it doesn't have a name yet, it could be called something like Equiv.FibrewisePerm p…)

[Kevin Buzzard]

I don't yet understand where you get stuck. Don't you want something like this:

def φ_invFun_equiv (f : (i : ι) → Perm {a | p a = i}) : Perm α where
  toFun := φ_invFun f
  invFun := φ_invFun (fun i ↦ (f i).symm)
  left_inv := sorry
  right_inv := sorry

def Φ : stabilizer (Perm α) p ≃* ((i : ι) → Perm {a | p a = i}) := {
  toFun := fun g i ↦ by
    apply Perm.subtypePerm g
    intro a
    simp only [Set.mem_setOf_eq]
    rw [← Function.comp_apply (f := p), arrowAction.mem_stabilizer_iff.mp g.prop]
  invFun := fun i ↦ ⟨φ_invFun_equiv i, sorry⟩
...

or are you stuck somewhere else?

[Kevin Buzzard]

Having tried to fill in the sorries I now understand your question...

[Junyan Xu]

Adding a lemma

lemma φ_invFun_eq (g : ∀ i, Perm {a | p a = i}) {a : α} {i : ι} (h : p a = i) :
    φ_invFun g a = g i ⟨a, h⟩ := by subst h; rfl

allows you to rewrite, and this works:

import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.GroupTheory.GroupAction.Basic

/-  Subgroup of `Equiv.Perm α` preserving a fibration `p : α → ι` -/

variable {α ι : Type*} {p : α → ι}

open Equiv MulAction

local instance  : MulAction (Equiv.Perm α) (α → ι) := arrowAction

lemma arrowAction.mem_stabilizer_iff {g : Perm α} :
    g ∈ stabilizer (Perm α) p ↔ p ∘ g = p := by rw [eq_comm, ← g.comp_symm_eq]; rfl

def φ_invFun (g : ∀ i, Perm {a | p a = i}) (a : α) : α := g (p a) ⟨a, rfl⟩

lemma φ_invFun_eq (g : ∀ i, Perm {a | p a = i}) {a : α} {i : ι} (h : p a = i) :
    φ_invFun g a = g i ⟨a, h⟩ := by subst h; rfl

lemma comp_φ_invFun (g : ∀ i, Perm {a | p a = i}) (a : α) : p (φ_invFun g a) = p a :=
  (g (p a) ⟨a, rfl⟩).prop

def φ_invFun_equiv (g : ∀ i, Perm {a | p a = i}) : Perm α where
  toFun := φ_invFun g
  invFun := φ_invFun (fun i ↦ (g i).symm)
  left_inv a := by
    rw [φ_invFun_eq _ (comp_φ_invFun g a)]
    exact congr_arg Subtype.val ((g <| p a).left_inv _)
  right_inv a := by
    rw [φ_invFun_eq _ (comp_φ_invFun _ a)]
    exact congr_arg Subtype.val ((g <| p a).right_inv _)

def Φ : stabilizer (Perm α) p ≃* (∀ i, Perm {a | p a = i}) where
  toFun g i := Perm.subtypePerm g fun a ↦ by
    simp only [Set.mem_setOf_eq]
    rw [← Function.comp_apply (f := p), arrowAction.mem_stabilizer_iff.mp g.prop]
  invFun g := ⟨φ_invFun_equiv g, by
    ext a; exact comp_φ_invFun (fun i ↦ (g i).symm) a⟩
  left_inv g := rfl
  right_inv g := by ext i a; apply φ_invFun_eq
  map_mul' g h := rfl

[Junyan Xu]

(deleted)