# mathlibdocumentation

logic.equiv.fintype

# 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.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.
def function.embedding.to_equiv_range {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (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
@[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, _⟩
@[simp]
theorem function.embedding.to_equiv_range_symm_apply_self {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α β) (a : α) :
theorem function.embedding.to_equiv_range_eq_of_injective {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (f : α β) :
def equiv.perm.via_fintype_embedding {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α β) :

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
@[simp]
theorem equiv.perm.via_fintype_embedding_apply_image {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α β) (a : α) :
(f a) = f (e a)
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 ) :
b = f (e (f.inv_of_mem_range b, h⟩))
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 ) :
b = b
@[simp]
theorem equiv.perm.via_fintype_embedding_sign {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq β] (e : equiv.perm α) (f : α β) [decidable_eq α] [fintype β] :
noncomputable def equiv.to_compl {α : Type u_1} [fintype α] {p q : α → Prop} (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
noncomputable def equiv.extend_subtype {α : Type u_1} [fintype α] {p q : α → Prop} (e : {x // p x} {x // q x}) :

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.

theorem equiv.extend_subtype_apply_of_mem {α : Type u_1} [fintype α] {p q : α → Prop} (e : {x // p x} {x // q x}) (x : α) (hx : p x) :
(e.extend_subtype) x = (e x, hx⟩)
theorem equiv.extend_subtype_mem {α : Type u_1} [fintype α] {p q : α → Prop} (e : {x // p x} {x // q x}) (x : α) (hx : p x) :
theorem equiv.extend_subtype_apply_of_not_mem {α : Type u_1} [fintype α] {p q : α → Prop} (e : {x // p x} {x // q x}) (x : α) (hx : ¬p x) :
theorem equiv.extend_subtype_not_mem {α : Type u_1} [fintype α] {p q : α → Prop} (e : {x // p x} {x // q x}) (x : α) (hx : ¬p x) :