Restricting permutations

Stream: Is there code for X?

[Anne Baanen]

I have a permutation σ : equiv.perm ℕ, and I know that σ doesn't send anything < k to anything ≥ k. Is there a nice way to write σ as the composition of some σ' : equiv.perm (fin k) and τ : equiv.perm ℕ?

[Mario Carneiro]

Take σ' = 1?

[Mario Carneiro]

I guess you mean some kind of horizontal composition

[Mario Carneiro]

Is there a function that takes the disjoint sum of permutations? That would at least let you write the theorem statement

[Anne Baanen]

The statement is something like σ = σ'.extend_domain (equiv.of_left_inverse coe _ _) * τ ∧ ∀ n, τ n ≠ n → n ≥ k

[Mario Carneiro]

Oh, I was thinking of something more like \exists σ' τ, σ = e.perm_congr (perm.sum σ' τ) where e : ℕ ⊕ fin k ≃ ℕ

[Mario Carneiro]

the definitions of equiv.perm_congr : A ~= B -> perm A ~= perm B and perm.sum : perm A -> perm B -> perm (A ⊕ B) should be obvious

[Anne Baanen]

Ah, I see. That would be a lot nicer than what I have now :P

[Anne Baanen]

Those are docs#equiv.perm_congr and docs#equiv.sum_congr respectively

[Mario Carneiro]

I just love it when I can wish theorems into existence like that :grinning_face_with_smiling_eyes:

[Mario Carneiro]

actually the second one is docs#equiv.perm.sum_congr, although I think that's defeq to an instantiation of docs#equiv.sum_congr

[Yaël Dillies]

This lemma doesn't seem to exist.

protected def perm.compl_equiv {α : Type*} [decidable_eq α] (s : set α) [decidable_pred (∈ s)] :
  perm (sᶜ : set α) ≃ {f : perm α | ∀ a ∈ s, f a = a} :=
(equiv.set.compl (equiv.refl _)).symm.trans (subtype_equiv_right $ by simp)

But I'm wondering whether it's written the correct way. Should I replace s by a prop and perm (sᶜ : set α) by perm {a // ¬p a}?

[Eric Wieser]

Is the right-hand side {f : perm α // f.support = s}? (docs#equiv.perm.support)

[Eric Wieser]

Oh, that's only for fintypes

[Yakov Pechersky]

I've thought about generalizing perm.support to arbitrary types, but it gets difficult to work with cardinality of supports then.

[Yakov Pechersky]

The equiv you're looking for can be made using the equiv that splits a type along a prop into a sum of compl subtypes, then refl for the left one. I worked and added the one recently, don't remember it's name.

[Yaël Dillies]

I ended up making it by hand using equiv.perm.subtype_perm and equiv.perm.of_subtype. See #8691