Equivalence between fintypes

This file contains some basic results on equivalences where one or both sides of the equivalence are Fintypes.

Main definitions

• Function.Embedding.toEquivRange: computably turn an embedding of a fintype into an Equiv of the domain to its range
• Equiv.Perm.viaFintypeEmbedding : Perm α → (α ↪ β) → Perm β extends the domain of a permutation, fixing everything outside the range of the embedding

Implementation details

• Function.Embedding.toEquivRange uses a computable inverse, but one that has poor computational performance, since it operates by exhaustive search over the input Fintypes.

def Function.Embedding.toEquivRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) : α ≃ ↑(Set.range ⇑f)

Computably turn an embedding f : α ↪ β into an equiv α ≃ Set.range f, if α is a Fintype. Has poor computational performance, due to exhaustive searching in constructed inverse. When a better inverse is known, use Equiv.ofLeftInverse' or Equiv.ofLeftInverse instead. This is the computable version of Equiv.ofInjective.

Equations

• f.toEquivRange = { toFun := fun (a : α) => ⟨f a, ⋯⟩, invFun := f.invOfMemRange, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Function.Embedding.toEquivRange_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) (a : α) : f.toEquivRange a = ⟨f a, ⋯⟩

@[simp]

theorem Function.Embedding.toEquivRange_symm_apply_self {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) (a : α) : f.toEquivRange.symm ⟨f a, ⋯⟩ = a

theorem Function.Embedding.toEquivRange_eq_ofInjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) : f.toEquivRange = Equiv.ofInjective ⇑f ⋯

def Equiv.Perm.viaFintypeEmbedding {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (e : Perm α) (f : α ↪ β) : Perm β

Extend the domain of e : Equiv.Perm α, mapping it through f : α ↪ β. Everything outside of Set.range f is kept fixed. Has poor computational performance, due to exhaustive searching in constructed inverse due to using Function.Embedding.toEquivRange. When a better α ≃ Set.range f is known, use Equiv.Perm.viaSetRange. When [Fintype α] is not available, a noncomputable version is available as Equiv.Perm.viaEmbedding.

Equations

• e.viaFintypeEmbedding f = e.extendDomain f.toEquivRange

@[simp]

theorem Equiv.Perm.viaFintypeEmbedding_apply_image {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (e : Perm α) (f : α ↪ β) (a : α) : (e.viaFintypeEmbedding f) (f a) = f (e a)

theorem Equiv.Perm.viaFintypeEmbedding_apply_mem_range {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (e : Perm α) (f : α ↪ β) {b : β} (h : b ∈ Set.range ⇑f) : (e.viaFintypeEmbedding f) b = f (e (f.invOfMemRange ⟨b, h⟩))

theorem Equiv.Perm.viaFintypeEmbedding_apply_notMem_range {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (e : Perm α) (f : α ↪ β) {b : β} (h : b ∉ Set.range ⇑f) : (e.viaFintypeEmbedding f) b = b

noncomputable def Equiv.setDiffEquiv {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] (h : Fintype.card ↑s = Fintype.card ↑t) : ↑(s \ t) ≃ ↑(t \ s)

If two sets have the same finite cardinality, their set differences are equivalent.

Equations

• Equiv.setDiffEquiv h = ⋯.some

noncomputable def Equiv.toCompl {α : Type u_1} {p q : α → Prop} [Finite ↑{x : α | p x}] (e : ↑{x : α | p x} ≃ ↑{x : α | q x}) : ↑{x : α | ¬p x} ≃ ↑{x : α | ¬q x}

If e is an equivalence between two subtypes of a type α, e.toCompl is an equivalence between the complement of those subtypes.

See also Equiv.compl, for a computable version when a term of type {e' : α ≃ α // ∀ x : {x // p x}, e' x = e x} is known.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Equiv.extendSubtype {α : Type u_1} {p q : α → Prop} [DecidablePred p] [DecidablePred q] [Finite ↑{x : α | p x}] (e : { x : α // p x } ≃ { x : α // q x }) : Perm α

If e is an equivalence between two subtypes of a type α, e.extendSubtype is a permutation of α acting like e on the subtypes and doing something arbitrary outside.

Note that when p = q, Equiv.Perm.subtypeCongr e (Equiv.refl _) can be used instead.

Equations

• e.extendSubtype = e.subtypeCongr e.toCompl

theorem Equiv.extendSubtype_apply_of_mem {α : Type u_1} {p q : α → Prop} [DecidablePred p] [DecidablePred q] [Finite ↑{x : α | p x}] (e : { x : α // p x } ≃ { x : α // q x }) (x : α) (hx : p x) : e.extendSubtype x = ↑(e ⟨x, hx⟩)

theorem Equiv.extendSubtype_mem {α : Type u_1} {p q : α → Prop} [DecidablePred p] [DecidablePred q] [Finite ↑{x : α | p x}] (e : { x : α // p x } ≃ { x : α // q x }) (x : α) (hx : p x) : q (e.extendSubtype x)

theorem Equiv.extendSubtype_apply_of_not_mem {α : Type u_1} {p q : α → Prop} [DecidablePred p] [DecidablePred q] [Finite ↑{x : α | p x}] (e : { x : α // p x } ≃ { x : α // q x }) (x : α) (hx : ¬p x) : e.extendSubtype x = ↑(e.toCompl ⟨x, hx⟩)

theorem Equiv.extendSubtype_not_mem {α : Type u_1} {p q : α → Prop} [DecidablePred p] [DecidablePred q] [Finite ↑{x : α | p x}] (e : { x : α // p x } ≃ { x : α // q x }) (x : α) (hx : ¬p x) : ¬q (e.extendSubtype x)

theorem Equiv.Perm.exists_extending_pair {α : Type u_1} {β : Type u_2} [Finite α] (f g : α → β) (hf : Function.Injective f) (hg : Function.Injective g) : ∃ (σ : Perm β), ∀ (a : α), σ (f a) = g a

Given two injective functions f and g from a finite type α to any type β, there exists a permutation of β that maps f to g.

theorem Equiv.Perm.exists_map_finset_eq {β : Type u_2} (s t : Finset β) (h : s.card = t.card) : ∃ (σ : Perm β), Finset.map (Equiv.toEmbedding σ) s = t

Any two same-cardinality finsets are related by a permutation.