Equiv.Perm.viaSetRange

Stream: mathlib4

[Wrenna Robson]

docs#Equiv.Perm.viaFintypeEmbedding

This refers to Equiv.Perm.viaSetRange. But I can't... find this. Did it get renamed? What is a good computational way nowadays to lift a permutation? Specifically, I would like to lift permutations from Fin n to Fin n to ones from Nat to Nat.

[Anne Baanen]

I can't find anything on https://mathlib-changelog.org about viaSetRange so apparently it never existed?

[Wrenna Robson]

Very strange.

[Yakov Pechersky]

Since I added that docstring, I need to help here!

[Yakov Pechersky]

Does docs#Equiv.Perm.extendDomain help you?

[Wrenna Robson]

I think so! I was just alarmed by the computational warning.

[Wrenna Robson]

I do note that the docstring of that describes f as a function

[Wrenna Robson]

But in fact it seems to be an equivalence...

[Wrenna Robson]

Indeed, because of that, "Set.range f" is in fact... the whole subtype. So there's also a problem with that docstring.

[Wrenna Robson]

extendDomain will have an obvious inverse (on the subtype of equivs which are fixed on the subtype)

[Wrenna Robson]

I think this is probably Equiv.Perm.subtypePerm, but it isn't described in the same terms.

[Wrenna Robson]

The formulation of extendDomain is most useful though - in particular it allows me to easily use Fin.equivSubtype

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib/pull/6959#discussion_r605014486

[Yakov Pechersky]

That's the origin of extendDomain, and what the docstring should refer to instead iiuc

[Wrenna Robson]

I agree, but extendDomain's docstring also needs fixing.

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib/pull/6959/commits/3647f4f1102b1f089f98bb75a7975f3460839b71 here is where I renamed it, forgetting to change the docstring references

[Kevin Buzzard]

Huh, I would expect the changelog to spot this but I can't make it do so.

[Yakov Pechersky]

docs#Equiv.ofLeftInverse'

[Yakov Pechersky]

So the extendDomain docstring needs help in changing the underscores to the right case

[Wrenna Robson]

Wrenna Robson said:

I think this is probably Equiv.Perm.subtypePerm, but it isn't described in the same terms.

Hmm, no, maybe this doesn't quite work.

[Wrenna Robson]

Right, I see. Here's an awfulhacky special case.

def equivNatEquivs : ((Fin n) ≃ (Fin n)) ≃
    {e : ℕ ≃ ℕ // (∀ i, (i < n ↔ e i < n) ∧ (n ≤ i → e i = i))} where
  toFun e := ⟨Equiv.Perm.extendDomain e (Fin.equivSubtype), fun i =>
    (Decidable.em (i < n)).by_cases (fun h => by simp [h, h.not_le,
      Equiv.Perm.extendDomain_apply_subtype, equivSubtype_symm_apply, equivSubtype_apply, is_lt])
      (fun h => by simp only [h, not_false_eq_true, Equiv.Perm.extendDomain_apply_not_subtype,
        gt_iff_lt, (le_of_not_lt), imp_self, and_self])⟩
  invFun e := (Fin.equivSubtype.symm).permCongr (Equiv.Perm.subtypePerm e.1 (fun i => (e.2 i).1))
  left_inv p := by
    simp [equivSubtype, Equiv.Perm.subtypePerm, Equiv.Perm.extendDomain,
      Equiv.Perm.subtypeCongr.left_apply_subtype, Equiv.permCongr_apply, Equiv.coe_fn_symm_mk,
      Equiv.coe_fn_mk, Equiv.ext_iff, Equiv.symm_symm, Fin.eta, implies_true, Equiv.permCongr,
      Equiv.equivCongr]
  right_inv p := by
    simp [Equiv.ext_iff, Subtype.ext_iff, equivSubtype, Equiv.Perm.subtypePerm,
    Equiv.Perm.extendDomain, Equiv.permCongr_symm_apply, Equiv.Perm.subtypeCongr, Equiv.permCongr,
    Equiv.equivCongr, Equiv.sumCompl]
    intro x
    by_cases h : x < n
    · simp only [h, ↓reduceDite, Sum.map_inl, Function.comp_apply, Sum.elim_inl]
    · simp [h, le_of_not_lt, (p.2 x).2]

[Wrenna Robson]

Ah, I think I want Equiv.Perm.subtypeEquivSubtypePerm

[Wrenna Robson]

It is quite odd that Equiv.Perm.extendDomain works differently - in that the user provides a (f : α' ≃ Subtype p) that mediates the equivalence.

[Wrenna Robson]

def equivNatEquivs : ((Fin n) ≃ (Fin n)) ≃ {e : ℕ ≃ ℕ // (∀ i, ¬ i < n → e i = i)} :=
(Equiv.permCongr Fin.equivSubtype).trans (Equiv.Perm.subtypeEquivSubtypePerm _)

[Yakov Pechersky]

Clarification, when you lift, do you want no permutation of things above n, or do you want to permute every kn+l?

[Wrenna Robson]

In fact I don't mind, but (Fin n) ≃ (Fin n) can only be equivalent to one of those, no?

[Wrenna Robson]

and I think it's the former.

[Yakov Pechersky]

Sure, your custom use of permCongr works to give the stronger equiv between Fin perms and perms of Nat fixing above n. extendDomain will give you the un-subtyped Nat perm, that by construction keeps things fixed

[Wrenna Robson]

I would rather work with the modulo, I think - I am actually dealing with functions that only manipulate below a certain bit, and so essentially I will have that the upper bits are unchanged.

[Wrenna Robson]

which feels like it ought to correspond to Fin (2^m) permutations.

[Wrenna Robson]

Is this also true?

[Wrenna Robson]

def equivNatEquivs' : ((Fin n) ≃ (Fin n)) ≃ {e : ℕ ≃ ℕ // (∀ i, e (i % n) = e i)} := sorry

[Wrenna Robson]

It feels like it ought to be - but I am not sure what the generalisation is, or how it can be constructed.

[Wrenna Robson]

Effectively this is constructed not from the injection from Fin n to N, but the surjection from N to Fin n.

[Yakov Pechersky]

I think from docs#Equiv.prodShear

[Yakov Pechersky]

Hmm maybe not

[Yakov Pechersky]

Nat \~- Nat x Fin, use that?

[Wrenna Robson]

Does that have a name?

[Yakov Pechersky]

I know how to construct your "periodic" perm explicitly, not sure how to do it by chaining existing equivs

[Yakov Pechersky]

No, I don't think so. There would be a separate one for each base, of course

[Wrenna Robson]

Ah, indeed.