# Documentation

Mathlib.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.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} [] [] (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.

Instances For
@[simp]
theorem Function.Embedding.toEquivRange_apply {α : Type u_1} {β : Type u_2} [] [] (f : α β) (a : α) :
= { val := f a, property := (_ : f a ) }
@[simp]
theorem Function.Embedding.toEquivRange_symm_apply_self {α : Type u_1} {β : Type u_2} [] [] (f : α β) (a : α) :
().symm { val := f a, property := (_ : f a ) } = a
theorem Function.Embedding.toEquivRange_eq_ofInjective {α : Type u_1} {β : Type u_2} [] [] (f : α β) :
def Equiv.Perm.viaFintypeEmbedding {α : Type u_1} {β : Type u_2} [] [] (e : ) (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.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.

Instances For
@[simp]
theorem Equiv.Perm.viaFintypeEmbedding_apply_image {α : Type u_1} {β : Type u_2} [] [] (e : ) (f : α β) (a : α) :
↑() (f a) = f (e a)
theorem Equiv.Perm.viaFintypeEmbedding_apply_mem_range {α : Type u_1} {β : Type u_2} [] [] (e : ) (f : α β) {b : β} (h : b ) :
↑() b = f (e (Function.Embedding.invOfMemRange f { val := b, property := h }))
theorem Equiv.Perm.viaFintypeEmbedding_apply_not_mem_range {α : Type u_1} {β : Type u_2} [] [] (e : ) (f : α β) {b : β} (h : ¬b ) :
↑() b = b
@[simp]
theorem Equiv.Perm.viaFintypeEmbedding_sign {α : Type u_1} {β : Type u_2} [] [] (e : ) (f : α β) [] [] :
Equiv.Perm.sign () = Equiv.Perm.sign e
noncomputable def Equiv.toCompl {α : Type u_1} [] {p : αProp} {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.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.

Instances For
@[inline, reducible]
noncomputable abbrev Equiv.extendSubtype {α : Type u_1} [] {p : αProp} {q : αProp} [] [] (e : { x // p x } { x // q x }) :

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

Instances For
theorem Equiv.extendSubtype_apply_of_mem {α : Type u_1} [] {p : αProp} {q : αProp} [] [] (e : { x // p x } { x // q x }) (x : α) (hx : p x) :
↑() x = ↑(e { val := x, property := hx })
theorem Equiv.extendSubtype_mem {α : Type u_1} [] {p : αProp} {q : αProp} [] [] (e : { x // p x } { x // q x }) (x : α) (hx : p x) :
q (↑() x)
theorem Equiv.extendSubtype_apply_of_not_mem {α : Type u_1} [] {p : αProp} {q : αProp} [] [] (e : { x // p x } { x // q x }) (x : α) (hx : ¬p x) :
↑() x = ↑(↑() { val := x, property := hx })
theorem Equiv.extendSubtype_not_mem {α : Type u_1} [] {p : αProp} {q : αProp} [] [] (e : { x // p x } { x // q x }) (x : α) (hx : ¬p x) :
¬q (↑() x)