Mathlib.Logic.Equiv.Fintype

Function.Embedding.toEquivRange definition

: α ≃ Set.range f

Full source

/-- 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`.
-/
def Function.Embedding.toEquivRange : α ≃ Set.range f :=
  ⟨fun a => ⟨f a, Set.mem_range_self a⟩, f.invOfMemRange, fun _ => by simp, fun _ => by simp⟩

Equivalence between finite type and range of embedding

Informal description

Given a finite type $\alpha$ and an injective function embedding $f : \alpha \hookrightarrow \beta$, this definition constructs an equivalence (bijection) between $\alpha$ and the range of $f$, denoted as $\alpha \simeq \text{range } f$. The inverse is computed by exhaustive search over the finite domain $\alpha$, which may have poor computational performance. For better computational performance when an explicit inverse is known, use `Equiv.ofLeftInverse'` or `Equiv.ofLeftInverse` instead. This is the computable version of `Equiv.ofInjective`. The equivalence maps any element $a \in \alpha$ to $\langle f(a), \text{mem\_range\_self } a \rangle \in \text{range } f$, and its inverse satisfies $f.\text{toEquivRange}^{-1}(\langle f(a), \text{mem\_range\_self } a \rangle) = a$ for all $a \in \alpha$.

Function.Embedding.toEquivRange_apply theorem

(a : α) : f.toEquivRange a = ⟨f a, Set.mem_range_self a⟩

Full source

@[simp]
theorem Function.Embedding.toEquivRange_apply (a : α) :
    f.toEquivRange a = ⟨f a, Set.mem_range_self a⟩ :=
  rfl

Application of Equivalence from Finite Type to Range of Embedding

Informal description

For any element $a$ in a finite type $\alpha$ and an injective function embedding $f : \alpha \hookrightarrow \beta$, the equivalence $f.\text{toEquivRange}$ maps $a$ to the pair $\langle f(a), \text{mem\_range\_self } a \rangle$ in the range of $f$.

Function.Embedding.toEquivRange_symm_apply_self theorem

(a : α) : f.toEquivRange.symm ⟨f a, Set.mem_range_self a⟩ = a

Full source

@[simp]
theorem Function.Embedding.toEquivRange_symm_apply_self (a : α) :
    f.toEquivRange.symm ⟨f a, Set.mem_range_self a⟩ = a := by simp [Equiv.symm_apply_eq]

Inverse of Equivalence from Finite Type to Range Maps Back to Original Element

Informal description

For any element $a$ in a finite type $\alpha$ and an injective function embedding $f : \alpha \hookrightarrow \beta$, the inverse of the equivalence $f.\text{toEquivRange}$ maps the pair $\langle f(a), \text{mem\_range\_self } a \rangle$ back to $a$. That is, $f.\text{toEquivRange}^{-1}(\langle f(a), \text{mem\_range\_self } a \rangle) = a$.

Function.Embedding.toEquivRange_eq_ofInjective theorem

: f.toEquivRange = Equiv.ofInjective f f.injective

Full source

theorem Function.Embedding.toEquivRange_eq_ofInjective :
    f.toEquivRange = Equiv.ofInjective f f.injective := by
  ext
  simp

Equivalence from Finite Type to Range of Embedding Matches Noncomputable Version

Informal description

For any injective function embedding $f \colon \alpha \hookrightarrow \beta$ where $\alpha$ is a finite type, the equivalence $f.\text{toEquivRange}$ between $\alpha$ and the range of $f$ is equal to the noncomputable equivalence $\text{Equiv.ofInjective}\,f\,f.\text{injective}$.

Equiv.Perm.viaFintypeEmbedding definition

: Equiv.Perm β

Full source

/-- 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`.
-/
def Equiv.Perm.viaFintypeEmbedding : Equiv.Perm β :=
  e.extendDomain f.toEquivRange

Permutation extension via finite type embedding

Informal description

Given a permutation $e$ of a finite type $\alpha$ and an injective function embedding $f : \alpha \hookrightarrow \beta$, this definition extends $e$ to a permutation of $\beta$ by applying $e$ to elements in the range of $f$ and leaving all other elements fixed. More precisely: - For any $a \in \alpha$, the permutation maps $f(a)$ to $f(e(a))$. - For any $b \in \beta$ not in the range of $f$, the permutation leaves $b$ unchanged. The extension is computed using the equivalence between $\alpha$ and the range of $f$ provided by `Function.Embedding.toEquivRange`, which may have poor computational performance due to exhaustive search over the finite domain $\alpha$.

Equiv.Perm.viaFintypeEmbedding_apply_image theorem

(a : α) : e.viaFintypeEmbedding f (f a) = f (e a)

Full source

@[simp]
theorem Equiv.Perm.viaFintypeEmbedding_apply_image (a : α) :
    e.viaFintypeEmbedding f (f a) = f (e a) := by
  rw [Equiv.Perm.viaFintypeEmbedding]
  convert Equiv.Perm.extendDomain_apply_image e (Function.Embedding.toEquivRange f) a

Action of Extended Permutation on Embedded Elements: $(e.\text{ext}\,f)(f(a)) = f(e(a))$

Informal description

For any permutation $e$ of a finite type $\alpha$ and any injective embedding $f \colon \alpha \hookrightarrow \beta$, the extended permutation $e.\text{viaFintypeEmbedding}\,f$ satisfies $(e.\text{viaFintypeEmbedding}\,f)(f(a)) = f(e(a))$ for all $a \in \alpha$.

Equiv.Perm.viaFintypeEmbedding_apply_mem_range theorem

{b : β} (h : b ∈ Set.range f) : e.viaFintypeEmbedding f b = f (e (f.invOfMemRange ⟨b, h⟩))

Full source

theorem Equiv.Perm.viaFintypeEmbedding_apply_mem_range {b : β} (h : b ∈ Set.range f) :
    e.viaFintypeEmbedding f b = f (e (f.invOfMemRange ⟨b, h⟩)) := by
  simp only [viaFintypeEmbedding, Function.Embedding.invOfMemRange]
  rw [Equiv.Perm.extendDomain_apply_subtype]
  congr

Action of Extended Permutation on Elements in the Range of an Embedding

Informal description

For any element $b \in \beta$ in the range of an injective embedding $f \colon \alpha \hookrightarrow \beta$, the permutation $e.\text{viaFintypeEmbedding}\ f$ maps $b$ to $f(e(f^{-1}(b)))$, where $f^{-1}(b)$ denotes the unique preimage of $b$ under $f$.

Equiv.Perm.viaFintypeEmbedding_apply_not_mem_range theorem

{b : β} (h : b ∉ Set.range f) : e.viaFintypeEmbedding f b = b

Full source

theorem Equiv.Perm.viaFintypeEmbedding_apply_not_mem_range {b : β} (h : b ∉ Set.range f) :
    e.viaFintypeEmbedding f b = b := by
  rwa [Equiv.Perm.viaFintypeEmbedding, Equiv.Perm.extendDomain_apply_not_subtype]

Fixed Points of Extended Permutation Outside Embedding Range

Informal description

For any element $b \in \beta$ not in the range of the embedding $f : \alpha \hookrightarrow \beta$, the permutation obtained by extending $e$ via $f$ leaves $b$ unchanged, i.e., $e.\text{viaFintypeEmbedding}\,f\,b = b$.

Equiv.toCompl definition

{p q : α → Prop} (e : { x // p x } ≃ { x // q x }) : { x // ¬p x } ≃ { x // ¬q x }

Full source

/-- If `e` is an equivalence between two subtypes of a finite type `α`, `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. -/
noncomputable def toCompl {p q : α → Prop} (e : { x // p x }{ x // p x } ≃ { x // q x }) :
    { x // ¬p x }{ x // ¬p x } ≃ { x // ¬q x } := by
  apply Classical.choice
  cases nonempty_fintype α
  classical
  exact Fintype.card_eq.mp <| Fintype.card_compl_eq_card_compl _ _ <| Fintype.card_congr e

Equivalence between complements of equivalent subtypes

Informal description

Given an equivalence $e$ between two subtypes $\{x \mid p x\}$ and $\{x \mid q x\}$ of a finite type $\alpha$, the function `Equiv.toCompl` constructs an equivalence between the complements $\{x \mid \neg p x\}$ and $\{x \mid \neg q x\}$ of these subtypes.

Equiv.extendSubtype abbrev

(e : { x // p x } ≃ { x // q x }) : Perm α

Full source

/-- 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. -/
noncomputable abbrev extendSubtype (e : { x // p x }{ x // p x } ≃ { x // q x }) : Perm α :=
  subtypeCongr e e.toCompl

Permutation Extension of Subtype Equivalence to Full Type

Informal description

Given an equivalence $e$ between two subtypes $\{x \mid p\ x\}$ and $\{x \mid q\ x\}$ of a finite type $\alpha$, the function `extendSubtype` constructs a permutation of $\alpha$ that acts as $e$ on the first subtype and behaves arbitrarily on its complement.

Equiv.extendSubtype_apply_of_mem theorem

(e : { x // p x } ≃ { x // q x }) (x) (hx : p x) : e.extendSubtype x = e ⟨x, hx⟩

Full source

theorem extendSubtype_apply_of_mem (e : { x // p x }{ x // p x } ≃ { x // q x }) (x) (hx : p x) :
    e.extendSubtype x = e ⟨x, hx⟩ := by
  dsimp only [extendSubtype]
  simp only [subtypeCongr, Equiv.trans_apply, Equiv.sumCongr_apply]
  rw [sumCompl_apply_symm_of_pos _ _ hx, Sum.map_inl, sumCompl_apply_inl]

Action of Extended Permutation on Subtype Elements

Informal description

For any equivalence $e$ between the subtypes $\{x \mid p(x)\}$ and $\{x \mid q(x)\}$ of a type $\alpha$, and for any element $x \in \alpha$ such that $p(x)$ holds, the permutation `e.extendSubtype` applied to $x$ equals the application of $e$ to the subtype element $\langle x, hx \rangle$, where $hx$ is the proof that $p(x)$ holds.

Equiv.extendSubtype_mem theorem

(e : { x // p x } ≃ { x // q x }) (x) (hx : p x) : q (e.extendSubtype x)

Full source

theorem extendSubtype_mem (e : { x // p x }{ x // p x } ≃ { x // q x }) (x) (hx : p x) :
    q (e.extendSubtype x) := by
  convert (e ⟨x, hx⟩).2
  rw [e.extendSubtype_apply_of_mem _ hx]

Image of Subtype Element under Extended Permutation Satisfies Target Predicate

Informal description

For any equivalence $e$ between the subtypes $\{x \mid p(x)\}$ and $\{x \mid q(x)\}$ of a type $\alpha$, and for any element $x \in \alpha$ such that $p(x)$ holds, the image of $x$ under the permutation `e.extendSubtype` satisfies $q$.

Equiv.extendSubtype_apply_of_not_mem theorem

(e : { x // p x } ≃ { x // q x }) (x) (hx : ¬p x) : e.extendSubtype x = e.toCompl ⟨x, hx⟩

Full source

theorem extendSubtype_apply_of_not_mem (e : { x // p x }{ x // p x } ≃ { x // q x }) (x) (hx : ¬p x) :
    e.extendSubtype x = e.toCompl ⟨x, hx⟩ := by
  dsimp only [extendSubtype]
  simp only [subtypeCongr, Equiv.trans_apply, Equiv.sumCongr_apply]
  rw [sumCompl_apply_symm_of_neg _ _ hx, Sum.map_inr, sumCompl_apply_inr]

Behavior of Extended Permutation on Complement Subtype

Informal description

Given an equivalence $e$ between the subtypes $\{x \mid p\ x\}$ and $\{x \mid q\ x\}$ of a type $\alpha$, and an element $x \in \alpha$ such that $\neg p\ x$ holds, the permutation `e.extendSubtype` applied to $x$ equals the application of the equivalence `e.toCompl` to the element $\langle x, hx \rangle$ of the complement subtype $\{x \mid \neg p\ x\}$.

Equiv.extendSubtype_not_mem theorem

(e : { x // p x } ≃ { x // q x }) (x) (hx : ¬p x) : ¬q (e.extendSubtype x)

Full source

theorem extendSubtype_not_mem (e : { x // p x }{ x // p x } ≃ { x // q x }) (x) (hx : ¬p x) :
    ¬q (e.extendSubtype x) := by
  convert (e.toCompl ⟨x, hx⟩).2
  rw [e.extendSubtype_apply_of_not_mem _ hx]

Permutation Extension Preserves Complement Membership

Informal description

Given an equivalence $e$ between the subtypes $\{x \mid p(x)\}$ and $\{x \mid q(x)\}$ of a type $\alpha$, and an element $x \in \alpha$ such that $\neg p(x)$ holds, the permutation `e.extendSubtype` applied to $x$ satisfies $\neg q(e.extendSubtype\ x)$.

Mathlib.Logic.Equiv.Fintype

Main definitions

Implementation details