Building a type for "all permutations"

Stream: new members

[Philippe Duchon]

I am trying to formalize some enumerative combinatorics, and would like to have a type for "permutations of all sizes" (in a setting where a "permutation" is usually a permutation on $\{1,\dots, n\}$ for some $n$). It seems to me that a reasonable definition would use a Σ type: Σ n, Equiv.Perm (Fin n).

To recover the "size" of a permutation, I then define a size function which is just the first projection.

Then, I would like an explicit bijection between Equiv.Perm (Fin n) and the type of all permutations with size n; but when I try to build one, I run into a problem which seems to be that tactic mode is too clever.

import Mathlib

def allPerms := Σ n, Equiv.Perm (Fin n)

def size : allPerms → ℕ :=
  fun ⟨ n, _ ⟩ ↦ n

def bijection (n:ℕ) : Equiv.Perm (Fin n) ≃ size ⁻¹' {n} where
  toFun := fun p ↦ ⟨ ⟨ n, p⟩, by rfl⟩

  invFun := fun ⟨ ⟨ m,p⟩, h⟩ ↦ by
    simp [size] at h
    rw [← h]
    -- would use "exact p" but rw closes the goal

  left_inv := by
    intro p
    simp
    -- the inverse function uses Equiv.refl, i.e. the identity map?
    sorry

  right_inv := sorry

def inverse (n:ℕ): size ⁻¹' {n} → Equiv.Perm (Fin n) :=
  fun ⟨ ⟨ m, p⟩ , h⟩ ↦ by
    simp [size] at h
    rw [← h]

#print inverse

Quite likely, I am doing this wrong - building a function in tactic mode means I don't have the same control as if building it in term mode; but I don't know how to do it in term mode.

Also, it's quite possible that my initial definition of permutations is not a good idea. I would like to set up a "combinatorial class" class, consisting of a type with a "size" mapping to the naturals with the condition that the set of terms with a given size is always finite, so this definition for permutations seemed like the right one (even though the "permutations" with size $n$ are not directly Equiv.Perm (Fin n), they should be close enough).

[Daniel Weber]

You can use docs#finCongr and docs#Equiv.permCongr:

def bijection (n:ℕ) : Equiv.Perm (Fin n) ≃ size ⁻¹' {n} where
  toFun p := ⟨⟨n, p⟩, rfl⟩

  invFun v := (finCongr v.2).permCongr v.1.2

  left_inv _ := rfl

  right_inv := by
    rintro ⟨_, rfl⟩
    rfl

[Daniel Weber]

For inverse you can use (bijection n).symm

[Daniel Weber]

You can also fix the tactic definition by using rewrite instead of rw - rw tries to close the goal by rfl, which works here but with the wrong permutation, while rewrite doesn't

[Eric Wieser]

I think FIn and Perm are distractions here, this holds more generally as

def Equiv.sigmaFstPreimage {α : ι → Type*} : α i ≃ Sigma.fst (β := α) ⁻¹' {i} where
  toFun x := ⟨⟨_, x⟩, rfl⟩
  invFun x := cast (congr_arg α x.prop) x.val.2
  left_inv x := rfl
  right_inv := by
    rintro ⟨⟨i, a⟩, rfl⟩
    rfl

[Philippe Duchon]

Thanks! I knew I was doing something not quite right. I also tried the generalized version but again, I was doing something (else?) wrong.