Computable inverses for injective/surjective functions on finite types

Main results

• Function.Injective.invOfMemRange, Embedding.invOfMemRange, Fintype.bijInv: computable versions of Function.invFun.
• Fintype.choose: computably obtain a witness for ExistsUnique.

def Function.Injective.invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Injective f) : ↑(Set.range f) → α

The inverse of an hf : injective function f : α → β, of the type ↥(Set.range f) → α. This is the computable version of Function.invFun that requires Fintype α and DecidableEq β, or the function version of applying (Equiv.ofInjective f hf).symm. This function should not usually be used for actual computation because for most cases, an explicit inverse can be stated that has better computational properties. This function computes by checking all terms a : α to find the f a = b, so it is O(N) where N = Fintype.card α.

theorem Function.Injective.left_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Injective f) (b : ↑(Set.range f)) : f (hf.invOfMemRange b) = ↑b

@[simp]

theorem Function.Injective.right_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Injective f) (a : α) : hf.invOfMemRange ⟨f a, ⋯⟩ = a

theorem Function.Injective.invFun_restrict {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Injective f) [Nonempty α] : (Set.range f).restrict (invFun f) = hf.invOfMemRange

theorem Function.Injective.invOfMemRange_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (hf : Injective f) : Surjective hf.invOfMemRange

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

The inverse of an embedding f : α ↪ β, of the type ↥(Set.range f) → α. This is the computable version of Function.invFun that requires Fintype α and DecidableEq β, or the function version of applying (Equiv.ofInjective f f.injective).symm. This function should not usually be used for actual computation because for most cases, an explicit inverse can be stated that has better computational properties. This function computes by checking all terms a : α to find the f a = b, so it is O(N) where N = Fintype.card α.

@[simp]

theorem Function.Embedding.left_inv_of_invOfMemRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) (b : ↑(Set.range ⇑f)) : f (f.invOfMemRange b) = ↑b

@[simp]

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

theorem Function.Embedding.invFun_restrict {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) [Nonempty α] : (Set.range ⇑f).restrict (invFun ⇑f) = f.invOfMemRange

theorem Function.Embedding.invOfMemRange_surjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α ↪ β) : Surjective f.invOfMemRange

def Fintype.chooseX {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] (hp : ∃! a : α, p a) : { a : α // p a }

Given a fintype α and a predicate p, associate to a proof that there is a unique element of α satisfying p this unique element, as an element of the corresponding subtype.

def Fintype.choose {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] (hp : ∃! a : α, p a) : α

Given a fintype α and a predicate p, associate to a proof that there is a unique element of α satisfying p this unique element, as an element of α.

theorem Fintype.choose_spec {α : Type u_1} [Fintype α] (p : α → Prop) [DecidablePred p] (hp : ∃! a : α, p a) : p (choose p hp)

theorem Fintype.choose_subtype_eq {α : Type u_4} (p : α → Prop) [Fintype { a : α // p a }] [DecidableEq α] (x : { a : α // p a }) (h : ∃! a : { a : α // p a }, ↑a = ↑x := ⋯) : choose (fun (y : { a : α // p a }) => ↑y = ↑x) h = x

def Fintype.bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (f_bij : Function.Bijective f) (b : β) : α

bijInv f is the unique inverse to a bijection f. This acts as a computable alternative to Function.invFun.

theorem Fintype.leftInverse_bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (f_bij : Function.Bijective f) : Function.LeftInverse (bijInv f_bij) f

theorem Fintype.rightInverse_bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (f_bij : Function.Bijective f) : Function.RightInverse (bijInv f_bij) f

theorem Fintype.bijective_bijInv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {f : α → β} (f_bij : Function.Bijective f) : Function.Bijective (bijInv f_bij)