permutations : of_subtype vs extend_domain

Stream: maths

[Antoine Chambert-Loir]

I noticed that there are two ways to extend a permutation from a subtype to the ambient type, either via .of_subtype, or via .extend_domain.
For both of them, there are some lemmas that compare properties of the subpermutation with those of the larger one, but not all. Also, the two different definitions are not compared.

I needed this lemma :

lemma equiv.perm.of_subtype_eq_extend_domain {α : Type*} [decidable_eq α] [fintype α]
  {p : α → Prop} [decidable_pred p]
  {g : equiv.perm (subtype p)} : g.of_subtype = g.extend_domain (equiv.refl (subtype p)) :=
begin
  ext x,
  cases dec_em (p x),
    { rw equiv.perm.extend_domain_apply_subtype g (equiv.refl (subtype p)) h,
      rw equiv.perm.of_subtype_apply_of_mem g h,
      refl, },
    { rw equiv.perm.extend_domain_apply_not_subtype g (equiv.refl (subtype p)) h,
      rw equiv.perm.of_subtype_apply_of_not_mem g h, },
end

In particular, because I needed that one :

lemma equiv.perm.of_subtype.cycle_type {α : Type*} [decidable_eq α] [fintype α]
  {p : α → Prop} [decidable_pred p]
  {g : equiv.perm (subtype p)} :  (g.of_subtype).cycle_type = g.cycle_type :=
begin
  rw equiv.perm.of_subtype_eq_extend_domain,
  rw equiv.perm.cycle_type_extend_domain,
end

Did I miss something ?

[Johan Commelin]

Probably the best thing to do would be to redefine of_subtype in terms of extend_domain?

[Eric Wieser]

(for reference: docs#equiv.perm.of_subtype, docs#equiv.perm.extend_domain)

[Antoine Chambert-Loir]

Ok! I'll do that…

[Antoine Chambert-Loir]

This is PR #16484