doc-next-gen

Mathlib.Data.Fintype.Inv

Module docstring

{"# 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. "}
Function.Injective.invOfMemRange definition
: Set.range f → α
Full source 
/-- 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 α`.
-/
def invOfMemRange : Set.range f → α := fun b =>
  Finset.choose (fun a => f a = b) Finset.univ
    ((existsUnique_congr (by simp)).mp (hf.existsUnique_of_mem_range b.property))
Computable inverse of an injective function on its range
Informal description
Given an injective function \( f : \alpha \to \beta \) with finite domain \(\alpha\) and decidable equality on \(\beta\), the function \( \text{invOfMemRange} \) maps an element \( b \) in the range of \( f \) to the unique \( a \in \alpha \) such that \( f(a) = b \). This is a computable version of the inverse function restricted to the range of \( f \).
Function.Injective.left_inv_of_invOfMemRange theorem
(b : Set.range f) : f (hf.invOfMemRange b) = b
Full source 
theorem left_inv_of_invOfMemRange (b : Set.range f) : f (hf.invOfMemRange b) = b :=
  (Finset.choose_spec (fun a => f a = b) _ _).right
Left Inverse Property of Computable Inverse on Range
Informal description
For any injective function $f \colon \alpha \to \beta$ with finite domain $\alpha$ and decidable equality on $\beta$, and for any element $b$ in the range of $f$, the function `invOfMemRange` satisfies $f(\text{invOfMemRange}(b)) = b$.
Function.Injective.right_inv_of_invOfMemRange theorem
(a : α) : hf.invOfMemRange ⟨f a, Set.mem_range_self a⟩ = a
Full source 
@[simp]
theorem right_inv_of_invOfMemRange (a : α) : hf.invOfMemRange ⟨f a, Set.mem_range_self a⟩ = a :=
  hf (Finset.choose_spec (fun a' => f a' = f a) _ _).right
Right Inverse Property of Computable Inverse for Injective Functions
Informal description
For any injective function $f \colon \alpha \to \beta$ with finite domain $\alpha$ and decidable equality on $\beta$, the computable inverse function $\text{invOfMemRange}$ satisfies $\text{invOfMemRange}(f(a)) = a$ for all $a \in \alpha$.
Function.Injective.invFun_restrict theorem
[Nonempty α] : (Set.range f).restrict (invFun f) = hf.invOfMemRange
Full source 
theorem invFun_restrict [Nonempty α] : (Set.range f).restrict (invFun f) = hf.invOfMemRange := by
  ext ⟨b, h⟩
  apply hf
  simp [hf.left_inv_of_invOfMemRange, @invFun_eq _ _ _ f b (Set.mem_range.mp h)]
Restricted Inverse Function Equals Computable Inverse on Range for Injective Functions
Informal description
For any injective function $f \colon \alpha \to \beta$ with finite domain $\alpha$ and decidable equality on $\beta$, and assuming $\alpha$ is nonempty, the restriction of the inverse function $\text{invFun}\, f$ to the range of $f$ equals the computable inverse function $\text{invOfMemRange}$ on the range of $f$.
Function.Injective.invOfMemRange_surjective theorem
: Function.Surjective hf.invOfMemRange
Full source 
theorem invOfMemRange_surjective : Function.Surjective hf.invOfMemRange := fun a =>
  ⟨⟨f a, Set.mem_range_self a⟩, by simp⟩
Surjectivity of the Computable Inverse for Injective Functions on Finite Domains
Informal description
For any injective function $f \colon \alpha \to \beta$ with finite domain $\alpha$ and decidable equality on $\beta$, the computable inverse function $\mathrm{invOfMemRange} \colon \mathrm{range}(f) \to \alpha$ is surjective.
Function.Embedding.invOfMemRange definition
: α
Full source 
/-- 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 α`.
-/
def invOfMemRange : α :=
  f.injective.invOfMemRange b
Computable inverse of an injective embedding on its range
Informal description
Given an injective function embedding \( f : \alpha \hookrightarrow \beta \) with finite domain \(\alpha\) and decidable equality on \(\beta\), the function \( \text{invOfMemRange} \) maps an element \( b \) in the range of \( f \) to the unique \( a \in \alpha \) such that \( f(a) = b \). This is a computable version of the inverse function restricted to the range of \( f \).
Function.Embedding.left_inv_of_invOfMemRange theorem
: f (f.invOfMemRange b) = b
Full source 
@[simp]
theorem left_inv_of_invOfMemRange : f (f.invOfMemRange b) = b :=
  f.injective.left_inv_of_invOfMemRange b
Left Inverse Property of Computable Inverse on Range
Informal description
For any injective function embedding $f \colon \alpha \hookrightarrow \beta$ with finite domain $\alpha$ and decidable equality on $\beta$, and for any element $b$ in the range of $f$, the computable inverse function $\text{invOfMemRange}$ satisfies $f(\text{invOfMemRange}(b)) = b$.
Function.Embedding.right_inv_of_invOfMemRange theorem
(a : α) : f.invOfMemRange ⟨f a, Set.mem_range_self a⟩ = a
Full source 
@[simp]
theorem right_inv_of_invOfMemRange (a : α) : f.invOfMemRange ⟨f a, Set.mem_range_self a⟩ = a :=
  f.injective.right_inv_of_invOfMemRange a
Right inverse property of the computable inverse for injective embeddings
Informal description
For any injective function embedding $f \colon \alpha \hookrightarrow \beta$ with finite domain $\alpha$ and decidable equality on $\beta$, the computable inverse function $\text{invOfMemRange}$ satisfies $\text{invOfMemRange}(f(a)) = a$ for all $a \in \alpha$.
Function.Embedding.invFun_restrict theorem
[Nonempty α] : (Set.range f).restrict (invFun f) = f.invOfMemRange
Full source 
theorem invFun_restrict [Nonempty α] : (Set.range f).restrict (invFun f) = f.invOfMemRange := by
  ext ⟨b, h⟩
  apply f.injective
  simp [f.left_inv_of_invOfMemRange, @invFun_eq _ _ _ f b (Set.mem_range.mp h)]
Restricted Inverse Function Equals Computable Inverse on Range for Injective Embeddings
Informal description
For any nonempty type $\alpha$ and an injective function embedding $f \colon \alpha \hookrightarrow \beta$ with finite domain $\alpha$ and decidable equality on $\beta$, the restriction of the inverse function $\text{invFun}\, f$ to the range of $f$ is equal to the computable inverse function $\text{invOfMemRange}$ of $f$. That is: $$ \text{invFun}\, f \restriction \text{range}(f) = \text{invOfMemRange}\, f. $$
Function.Embedding.invOfMemRange_surjective theorem
: Function.Surjective f.invOfMemRange
Full source 
theorem invOfMemRange_surjective : Function.Surjective f.invOfMemRange := fun a =>
  ⟨⟨f a, Set.mem_range_self a⟩, by simp⟩
Surjectivity of the Computable Inverse for Injective Embeddings
Informal description
For any injective function embedding $f \colon \alpha \hookrightarrow \beta$ with finite domain $\alpha$ and decidable equality on $\beta$, the computable inverse function $\mathrm{invOfMemRange} \colon \mathrm{range}(f) \to \alpha$ is surjective. That is, for every $a \in \alpha$, there exists $b \in \mathrm{range}(f)$ such that $\mathrm{invOfMemRange}(b) = a$.
Fintype.chooseX definition
(hp : ∃! a : α, p a) : { a // p a }
Full source 
/-- 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 chooseX (hp : ∃! a : α, p a) : { a // p a } :=
  ⟨Finset.choose p univ (by simpa), Finset.choose_property _ _ _⟩
Unique element satisfying a predicate in a finite type
Informal description
Given a finite type $\alpha$ and a predicate $p$ on $\alpha$, if there exists a unique element $a$ in $\alpha$ satisfying $p(a)$, then `Fintype.chooseX` returns this unique element as a term of the subtype $\{a \mid p(a)\}$.
Fintype.choose definition
(hp : ∃! a, p a) : α
Full source 
/-- 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 `α`. -/
def choose (hp : ∃! a, p a) : α :=
  chooseX p hp
Unique element satisfying a predicate in a finite type
Informal description
Given a finite type $\alpha$ and a predicate $p$ on $\alpha$, if there exists a unique element $a$ in $\alpha$ satisfying $p(a)$, then `Fintype.choose` returns this unique element as a term of type $\alpha$.
Fintype.choose_spec theorem
(hp : ∃! a, p a) : p (choose p hp)
Full source 
theorem choose_spec (hp : ∃! a, p a) : p (choose p hp) :=
  (chooseX p hp).property
The chosen element satisfies the predicate in a finite type
Informal description
Given a finite type $\alpha$ and a predicate $p$ on $\alpha$, if there exists a unique element $a$ in $\alpha$ satisfying $p(a)$, then the element chosen by `Fintype.choose` satisfies the predicate $p$, i.e., $p(\text{choose}(p, \text{hp}))$ holds.
Fintype.bijInv definition
(f_bij : Bijective f) (b : β) : α
Full source 
/-- `bijInv f` is the unique inverse to a bijection `f`. This acts
  as a computable alternative to `Function.invFun`. -/
def bijInv (f_bij : Bijective f) (b : β) : α :=
  Fintype.choose (fun a => f a = b) (f_bij.existsUnique b)
Computable inverse of a bijective function on finite types
Informal description
For a bijective function \( f \colon \alpha \to \beta \) on finite types, `bijInv f` is the computable inverse function that maps each \( b \in \beta \) to the unique \( a \in \alpha \) such that \( f(a) = b \).
Fintype.leftInverse_bijInv theorem
(f_bij : Bijective f) : LeftInverse (bijInv f_bij) f
Full source 
theorem leftInverse_bijInv (f_bij : Bijective f) : LeftInverse (bijInv f_bij) f := fun a =>
  f_bij.left (choose_spec (fun a' => f a' = f a) _)
Left Inverse Property of Computable Bijective Inverse on Finite Types
Informal description
For any bijective function $f \colon \alpha \to \beta$ between finite types, the computable inverse function $\text{bijInv}(f)$ is a left inverse of $f$, meaning that for every $a \in \alpha$, we have $\text{bijInv}(f)(f(a)) = a$.
Fintype.rightInverse_bijInv theorem
(f_bij : Bijective f) : RightInverse (bijInv f_bij) f
Full source 
theorem rightInverse_bijInv (f_bij : Bijective f) : RightInverse (bijInv f_bij) f := fun b =>
  choose_spec (fun a' => f a' = b) _
Right Inverse Property of Computable Bijection Inverse on Finite Types
Informal description
For any bijective function $f \colon \alpha \to \beta$ between finite types, the computable inverse function $\text{bijInv}\ f$ is a right inverse of $f$, meaning that for every $b \in \beta$, we have $f(\text{bijInv}\ f\ b) = b$.