Equivalence between fintypes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

function.embedding.to_equiv_range: computably turn an embedding of a fintype into an equiv of the domain to its range
equiv.perm.via_fintype_embedding : perm α → (α ↪ β) → perm β extends the domain of a permutation, fixing everything outside the range of the embedding

Implementation details #

function.embedding.to_equiv_range uses a computable inverse, but one that has poor computational performance, since it operates by exhaustive search over the input fintypes.

source

def function.embedding.to_equiv_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (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.of_left_inverse' or equiv.of_left_inverse instead. This is the computable version of equiv.of_injective.

Equations

f.to_equiv_range = {to_fun := λ (a : α), ⟨⇑f a, _⟩, inv_fun := f.inv_of_mem_range, left_inv := _, right_inv := _}

source

@[simp]

theorem function.embedding.to_equiv_range_apply {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) (a : α) :

⇑(f.to_equiv_range) a = ⟨⇑f a, _⟩

source

@[simp]

theorem function.embedding.to_equiv_range_symm_apply_self {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) (a : α) :

⇑(f.to_equiv_range.symm) ⟨⇑f a, _⟩ = a

source

theorem function.embedding.to_equiv_range_eq_of_injective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α ↪ β) :

f.to_equiv_range = equiv.of_injective ⇑f _

source

def equiv.perm.via_fintype_embedding {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α ↪ β) :

equiv.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.to_equiv_range. When a better α ≃ set.range f is known, use equiv.perm.via_set_range. When [fintype α] is not available, a noncomputable version is available as equiv.perm.via_embedding.

Equations

e.via_fintype_embedding f = e.extend_domain f.to_equiv_range

source

@[simp]

theorem equiv.perm.via_fintype_embedding_apply_image {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α ↪ β) (a : α) :

⇑(e.via_fintype_embedding f) (⇑f a) = ⇑f (⇑e a)

source

theorem equiv.perm.via_fintype_embedding_apply_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α ↪ β) {b : β} (h : b ∈ set.range ⇑f) :

⇑(e.via_fintype_embedding f) b = ⇑f (⇑e (f.inv_of_mem_range ⟨b, h⟩))

source

theorem equiv.perm.via_fintype_embedding_apply_not_mem_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α ↪ β) {b : β} (h : b ∉ set.range ⇑f) :

⇑(e.via_fintype_embedding f) b = b

source

@[simp]

theorem equiv.perm.via_fintype_embedding_sign {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α ↪ β) [decidable_eq α] [fintype β] :

⇑equiv.perm.sign (e.via_fintype_embedding f) = ⇑equiv.perm.sign e

source

noncomputable def equiv.to_compl {α : Type u_1} [fintype α] {p q : α → Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} ≃ {x // q x}) :

{x // ¬p x} ≃ {x // ¬q x}

If e is an equivalence between two subtypes of a fintype α, e.to_compl 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

e.to_compl = classical.choice _

source

@[reducible]

noncomputable def equiv.extend_subtype {α : Type u_1} [fintype α] {p q : α → Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} ≃ {x // q x}) :

equiv.perm α

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

Note that when p = q, equiv.perm.subtype_congr e (equiv.refl _) can be used instead.

source

theorem equiv.extend_subtype_apply_of_mem {α : Type u_1} [fintype α] {p q : α → Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} ≃ {x // q x}) (x : α) (hx : p x) :

⇑(e.extend_subtype) x = ↑(⇑e ⟨x, hx⟩)

source

theorem equiv.extend_subtype_mem {α : Type u_1} [fintype α] {p q : α → Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} ≃ {x // q x}) (x : α) (hx : p x) :

q (⇑(e.extend_subtype) x)

source

theorem equiv.extend_subtype_apply_of_not_mem {α : Type u_1} [fintype α] {p q : α → Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} ≃ {x // q x}) (x : α) (hx : ¬p x) :

⇑(e.extend_subtype) x = ↑(⇑(e.to_compl) ⟨x, hx⟩)

source

theorem equiv.extend_subtype_not_mem {α : Type u_1} [fintype α] {p q : α → Prop} [decidable_pred p] [decidable_pred q] (e : {x // p x} ≃ {x // q x}) (x : α) (hx : ¬p x) :

¬q (⇑(e.extend_subtype) x)