Equiv.Perm from a list of mappings

Stream: mathlib4

[James Gallicchio]

Hi all! I'm doing some proofs on combinatorial objects (specifically Keller graphs), and in a few places I need to define "a permutation of Fin n which maps 0 to x and 1 to y". Any such permutation suffices, so long as it is easy to prove application on 0/1 returns x/y respectively.

I have a working implementation, but is there a simpler way to do this in Mathlib?

My current approach was to define a way to insert mappings into Equiv, as here:

/-- Returns a function which maps `a ↦ b` and `f⁻¹ b ↦ f a`.
All other elements are mapped as they are in `f`.  -/
def Equiv.insert [DecidableEq α] [DecidableEq β] (a : α) (b : β) (f : α ≃ β) : α ≃ β := ...

which I could then generalize to a list of mappings, as

def extend [DecidableEq α] (L : List (α × α)) : α ≃ α :=
  match L with
  | [] => Equiv.refl _
  | (a,b) :: tail => (extend tail).insert a b

(the type can be generalized but I only needed permutations). This works fine, and I can prove that assuming domain points and codomain points are distinct lists, if (x,y) \in L then extend L x = y. which is all I need.

[Eric Wieser]

I have some vague memory of Equiv.insert already exists, but the closest I can find is docs#Equiv.removeNone

[Aaron Liu]

Eric Wieser said:

I have some vague memory of Equiv.insert already exists, but the closest I can find is docs#Equiv.removeNone

Are you thinking of docs#Equiv.setValue

[Eric Wieser]

Nice find, thanks!

[Kevin Buzzard]

It seems that there's no API other than a proof of setValue f a b a = b so it might be tricky to go from that to something which has two prescribed values.

[Kevin Buzzard]

It seems to be f composed with a transposition, so maybe one could just use this trick directly: if x isn't 1 then you compose swap 0 x with swap 1 y, and if it is but y isn't 0 then you compose them the other way around, and if x=1 and y=0 you just swap 0 and 1?

[James Gallicchio]

ah! I must not have had that file imported. well, I'll rename extend to setAll for consistency. Is there interest in a PR to add the list variant?

[Eric Wieser]

Is swap a typo above?

[James Gallicchio]

whoops, yes, just should be extend

[Kevin Buzzard]

import Mathlib

variable {α : Type*} [DecidableEq α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≠ a₂) (hb : b₁ ≠ b₂)

def Equiv.setValue₂ (_ha : a₁ ≠ a₂) (_hb : b₁ ≠ b₂) : α ≃ α :=
  if a₁ = b₂ then
    (if a₂ = b₁ then swap a₁ b₁ else swap a₂ b₂ * swap a₁ b₁)
  else (swap a₁ b₁) * (swap a₂ b₂)

example : Equiv.setValue₂ ha hb a₁ = b₁ := by
  unfold Equiv.setValue₂
  split_ifs with h1 h2
  · rw [Equiv.swap_apply_left]
  · rw [Equiv.Perm.coe_mul, Function.comp_apply, Equiv.swap_apply_left,
      Equiv.swap_apply_of_ne_of_ne (Ne.symm h2) hb]
  · rw [Equiv.Perm.coe_mul, Function.comp_apply, Equiv.swap_apply_of_ne_of_ne ha h1,
      Equiv.swap_apply_left]

example : Equiv.setValue₂ ha hb a₂ = b₂ := by
  unfold Equiv.setValue₂
  split_ifs with h1 h2
  · rw [h1, h2, Equiv.swap_apply_right]
  · rw [Equiv.Perm.coe_mul, Function.comp_apply, Equiv.swap_apply_of_ne_of_ne ha.symm h2,
      Equiv.swap_apply_left]
  · rw [Equiv.Perm.coe_mul, Function.comp_apply, Equiv.swap_apply_left,
      Equiv.swap_apply_of_ne_of_ne (Ne.symm h1) hb.symm]

[James Gallicchio]

I unfortunately need up to 4 elements I think :joy: which is why I just went with a list. This might be too specific for mathlib at the moment.

[Kevin Buzzard]

Can you get away with the 4 source elements being disjoint from the 4 target elements?

[Kevin Buzzard]

If so then you can just do products of transpositions naively. All the if then else stuff is dealing with edge cases.

[Eric Wieser]

Or maybe docs#List.formPerm helps with what you want?

[Kevin Buzzard]

One thing which would be nice would be: given f : A equiv A and i : A -> B an injection, you get g : B equiv B such that the obvious square commutes (both vertical maps are i). This would be a practical general tool for you I should think.

[Kevin Buzzard]

Something even more general would be: given f : A equiv A' and i: A -> B and j: A' -> B' injections and a bijection between B - A and B' - A' , you get out a bijection B -> B making the diagram commute

[James Gallicchio]

Eric Wieser said:

Or maybe docs#List.formPerm helps with what you want?

Unfortunately no :( in this application I only know that the source points are distinct and the target points are distinct. They might form a single big cycle, they might be 4 unrelated transpositions that commute

[Aaron Liu]

Kevin Buzzard said:

One thing which would be nice would be: given f : A equiv A and i : A -> B an injection, you get g : B equiv B such that the obvious square commutes (both vertical maps are i). This would be a practical general tool for you I should think.

For you :)

import Mathlib.Data.Set.Operations
import Mathlib.Logic.Embedding.Basic

open Classical in
noncomputable
def Equiv.push {X Y : Type*} (f : X ↪ Y) (e : X ≃ X) : Y ≃ Y where
  toFun y := if h : y ∈ Set.range f then f (e h.choose) else y
  invFun y := if h : y ∈ Set.range f then f (e.symm h.choose) else y
  left_inv b := by
    dsimp
    split
    · obtain ⟨y, rfl⟩ := ‹b ∈ Set.range f›
      simp
    · rfl
  right_inv a := by
    dsimp
    split
    · obtain ⟨y, rfl⟩ := ‹a ∈ Set.range f›
      simp
    · rfl

theorem Equiv.push_apply_apply {X Y : Type*} {f : X ↪ Y} {e : X ≃ X} {x : X} :
    e.push f (f x) = f (e x) := by
  simp_rw [push, ← Equiv.toFun_as_coe]
  simp

theorem Equiv.push_symm_apply_apply {X Y : Type*} {f : X ↪ Y} {e : X ≃ X} {x : X} :
    (e.push f).symm (f x) = f (e.symm x) := by
  simp_rw [push, ← Equiv.invFun_as_coe]
  simp

theorem Equiv.push_apply_of_not_mem_range {X Y : Type*} {f : X ↪ Y} {e : X ≃ X} {y : Y}
    (hy : y ∉ Set.range f) : e.push f y = y := by
  simp_rw [push, ← Equiv.toFun_as_coe]
  simp [hy]

theorem Equiv.push_symm_apply_of_not_mem_range {X Y : Type*} {f : X ↪ Y} {e : X ≃ X} {y : Y}
    (hy : y ∉ Set.range f) : (e.push f).symm y = y := by
  simp_rw [push, ← Equiv.invFun_as_coe]
  simp [hy]

Should this be added to mathlib? If so, how do I add this to mathlib?

[James Gallicchio]

noncomputable in the Equiv namespace is causing alarm bells in my head! (I might be wrong here...)

[Aaron Liu]

There's not really any other way to do it...

[Eric Wieser]

You could provide a left inverse of f?

[Eric Wieser]

Then the test becomes f (g y) = y and the choice (g y)

[James Gallicchio]

Kevin Buzzard said:

One thing which would be nice would be: given f : A equiv A and i : A -> B an injection, you get g : B equiv B such that the obvious square commutes (both vertical maps are i). This would be a practical general tool for you I should think.

I'm not sure I see how this would work for my application. Could you elaborate? :/

The way I am thinking about this is that I have a partial map with a finite number of pairs, and I want to extend it to a full equivalence, thus the name I gave it originally.

[James Gallicchio]

I guess I am defining an embedding from {a : A | a \in [a1,a2,a3]} to B. I should be able to prove that I can extend such an embedding to an equivalence over the full types, given an arbitrary equivalence between the full types

[James Gallicchio]

hm. and then I can have a function like embeddingFromList which turns a list of pairs into an embedding of the appropriate subtypes, given that domain and codomain are pairwise distinct

[James Gallicchio]

I'm unsure if this is cleaner in practice, but it is more general!

[Aaron Liu]

Eric Wieser said:

Then the test becomes f (g y) = y and the choice (g y)

import Mathlib.Data.Set.Operations
import Mathlib.Logic.Equiv.Defs

def Equiv.push {X Y : Type*} [DecidableEq Y] {f : X → Y} {g : Y → X}
    (hfg : g.LeftInverse f) (e : X ≃ X) : Y ≃ Y where
  toFun y := if f (g y) = y then f (e (g y)) else y
  invFun y := if f (g y) = y then f (e.symm (g y)) else y
  left_inv b := by
    dsimp
    by_cases h : b ∈ Set.range f
    · obtain ⟨a, rfl⟩ := h
      simp [show ∀ (x : X), g (f x) = x from hfg]
    · have hne : f (g b) ≠ b := fun hb ↦ h (hb ▸ Set.mem_range_self (g b))
      simp [hne]
  right_inv a := by
    dsimp
    by_cases h : a ∈ Set.range f
    · obtain ⟨b, rfl⟩ := h
      simp [show ∀ (x : X), g (f x) = x from hfg]
    · have hne : f (g a) ≠ a := fun hb ↦ h (hb ▸ Set.mem_range_self (g a))
      simp [hne]

theorem Equiv.push_apply_apply {X Y : Type*} [DecidableEq Y] {f : X → Y} {g : Y → X}
    {hfg : g.LeftInverse f} {e : X ≃ X} {x : X} :
    e.push hfg (f x) = f (e x) := by
  simp_rw [push, ← Equiv.toFun_as_coe]
  simp [show ∀ (x : X), g (f x) = x from hfg]

theorem Equiv.push_symm_apply_apply {X Y : Type*} [DecidableEq Y] {f : X → Y} {g : Y → X}
    {hfg : g.LeftInverse f} {e : X ≃ X} {x : X} :
    (e.push hfg).symm (f x) = f (e.symm x) := by
  simp_rw [push, ← Equiv.invFun_as_coe]
  simp [show ∀ (x : X), g (f x) = x from hfg]

theorem Equiv.push_apply_of_not_mem_range {X Y : Type*} [DecidableEq Y] {f : X → Y} {g : Y → X}
    {hfg : g.LeftInverse f} {e : X ≃ X} {y : Y}
    (hy : y ∉ Set.range f) : e.push hfg y = y := by
  simp_rw [push, ← Equiv.toFun_as_coe]
  have hne : f (g y) ≠ y := fun heq ↦ hy (heq ▸ Set.mem_range_self (g y))
  simp [hne]

theorem Equiv.push_symm_apply_of_not_mem_range {X Y : Type*} [DecidableEq Y] {f : X → Y} {g : Y → X}
    {hfg : g.LeftInverse f} {e : X ≃ X} {y : Y}
    (hy : y ∉ Set.range f) : (e.push hfg).symm y = y := by
  simp_rw [push, ← Equiv.invFun_as_coe]
  have hne : f (g y) ≠ y := fun heq ↦ hy (heq ▸ Set.mem_range_self (g y))
  simp [hne]

[Mitchell Lee]

Here is a related question (actually, maybe even the same question) from a few weeks ago: #Is there code for X? > nodup_eq_len_imp_eqv

[James Gallicchio]

Ooo! Thank you for finding, let me read through the thread.