nodup_eq_len_imp_eqv

Stream: Is there code for X?

[Paige Thomas]

(deleted)

[Paige Thomas]

(deleted)

[Paige Thomas]

(deleted)

[Paige Thomas]

(deleted)

[Paige Thomas]

I'm wondering if it should be possible to prove

theorem nodup_eq_len_imp_eqv
  {α : Type}
  [DecidableEq α]
  (xs ys : List α)
  (h1 : xs.length = ys.length)
  (h2 : xs.Nodup)
  (h3 : ys.Nodup) :
  ∃ (f : α ≃ α), xs.map f = ys :=

using

/--
  List.InjOn f xs := f is injective on xs if the restriction of f to xs is injective.
-/
def List.InjOn
  {α : Type}
  (f : α → α)
  (xs : List α) :
  Prop := ∀ ⦃x₁ : α⦄, x₁ ∈ xs → ∀ ⦃x₂ : α⦄, x₂ ∈ xs → f x₁ = f x₂ → x₁ = x₂


lemma List.nodup_eq_len_imp_exists_bijon
  {α : Type}
  [DecidableEq α]
  (xs ys : List α)
  (h1 : xs.length = ys.length)
  (h2 : xs.Nodup)
  (h3 : ys.Nodup) :
  ∃ (f : α → α), List.InjOn f xs ∧ xs.map f = ys :=

[Kim Morrison]

I think you want the following steps:

• An embedding { x : α // P x } ↪ β can be extended to an embedding α ↪ β as long as #α ≤ #β. (A Zorn argument, perhaps already available?)
• Easily from that, an embedding { x : α // P x } ↪ α can be extended to an autoequivalence α ≃ α.
• Now define f' : { x // x ∈ xs } → α by f' ⟨x, h⟩ := ys[xs.indexOf x], check that is an embedding using the Nodup hypotheses, and use the general machinery.

[Paige Thomas]

Thank you.

[Violeta Hernández]

This seems relevant: docs#Cardinal.extend_function

[Paige Thomas]

Thank you. Unfortunately a lot of this notation and terminology is over my head, and I'm fighting some kind of flu, so I probably can't think clearly enough to reason about it at the moment.

[Kim Morrison]

Those definitions are weird. Why do they have Nonempty (X \equiv Y) hypotheses instead of #X = #Y? It's in a file about cardinals!

[Mitchell Lee]

Can you do it as a product of transpositions by using induction on the list?

[Matt Diamond]

I wonder if there's a way to combine docs#List.Nodup.getEquiv and docs#Equiv.subtypeCongr here (i.e. constructing { x // x ∈ xs } ≃ { x // x ∈ ys } with List.Nodup.getEquiv and transitivity and then extending it with an equivalence of non-members)

[Yaël Dillies]

Kim Morrison said:

Those definitions are weird. Why do they have Nonempty (X \equiv Y) hypotheses instead of #X = #Y? It's in a file about cardinals!

That's because X and Y live in different universes, so #X = #Y doesn't typecheck. At least, that's my guess

[Kim Morrison]

Ah, okay. I guess with lifts in there it's even uglier.

[Paige Thomas]

Mitchell Lee said:

Can you do it as a product of transpositions by using induction on the list?

Perhaps? I have this as proven, but I'm not sure how to go about using it to do so, if this is what I would use

example
  {α β : Type}
  [DecidableEq α]
  [DecidableEq β]
  (f g : α → β)
  (a b : α)
  (h1 : Function.Injective f)
  (h2_left : g a = f b)
  (h2_right : g b = f a)
  (h3 : ∀ (x : α), (¬ x = a ∧ ¬ x = b) → f x = g x) :
  Function.Injective g :=

[Mitchell Lee]

Use Equiv.swap and composition of equivalences, as follows:

import Mathlib

def List.equivOfList {α : Type*} [DecidableEq α] (xs ys : List α) : α ≃ α :=
  match xs, ys with
  | .nil, _ | _, .nil => 1
  | x :: xs, y :: ys => let σ := equivOfList xs ys;
    (Equiv.swap (σ x) y) * σ

If xs and ys have the same length and no duplicates, then this equivalence satisfies the mapping property that you want. (This is a theorem that needs to be proved, but I suspect it isn't too hard. Note that it is better not to include the DecidableEq α hypothesis in the theorem statement, but instead to synthesize it using the classical tactic.)

[Paige Thomas]

I'm not sure I entirely follow the definition of List.equivOfList. Is 1 like Function.id? What is the *, some kind of composition? What does (Equiv.swap (σ x) y) * σ do?

[Aaron Liu]

1 and * come from the group structure on Equiv.Perm α, where multiplication is given by composition. (Equiv.swap (σ x) y) * σ says "the composition of σ followed by the equivalence that swaps σ x with y and leaves everything else unchanged"

[Paige Thomas]

So if xs and ys are both nil, then the resulting equiv function takes every value to itself? And if xs = [1] and ys = [3] then the result is a function that takes 1 to 3 and 3 to 1 and everything else to itself?

[Paige Thomas]

But then, I guess I don't see where it changes the y, ie, sets 3 -> 1? That is, why is it not (Equiv.swap (σ x) (σ y)) * σ?

[Eric Wieser]

Kim Morrison said:

Ah, okay. I guess with lifts in there it's even uglier.

I think in files about cardinals we tend to prefer lift, and let users translate to the Nonempty spelling when they need it

[Kim Morrison]

Any Cardinal enthusiasts want to rewrite Cardinal.extend_function to follow that rule (which seems good to me)?

[Violeta Hernández]

Kim Morrison said:

Those definitions are weird. Why do they have Nonempty (X \equiv Y) hypotheses instead of #X = #Y? It's in a file about cardinals!

I imagine the reasoning is that these can be types in distinct universes.

[Violeta Hernández]

Oh oops sorry, just noticed the reply.

[Violeta Hernández]

Yeah, I can do that refactor.

[Violeta Hernández]

Do note I made a thread explaining an idea for an alternate, simpler way of writing ordinal and cardinal equalities between different universes: #mathlib4 > Universe-heterogeneous ordinal and cardinal relations