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 #

Implementation details #

def Function.Embedding.toEquivRange {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α β) :
α (Set.range 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.

Equations
  • f.toEquivRange = { toFun := fun (a : α) => f a, , invFun := f.invOfMemRange, left_inv := , right_inv := }
Instances For
    @[simp]
    theorem Function.Embedding.toEquivRange_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α β) (a : α) :
    f.toEquivRange a = f a,
    @[simp]
    theorem Function.Embedding.toEquivRange_symm_apply_self {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α β) (a : α) :
    f.toEquivRange.symm f a, = a
    theorem Function.Embedding.toEquivRange_eq_ofInjective {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (f : α β) :
    f.toEquivRange = Equiv.ofInjective f
    def Equiv.Perm.viaFintypeEmbedding {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (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.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.

    Equations
    • e.viaFintypeEmbedding f = e.extendDomain f.toEquivRange
    Instances For
      @[simp]
      theorem Equiv.Perm.viaFintypeEmbedding_apply_image {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (e : Equiv.Perm α) (f : α β) (a : α) :
      (e.viaFintypeEmbedding f) (f a) = f (e a)
      theorem Equiv.Perm.viaFintypeEmbedding_apply_mem_range {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (e : Equiv.Perm α) (f : α β) {b : β} (h : b Set.range f) :
      (e.viaFintypeEmbedding f) b = f (e (f.invOfMemRange b, h))
      theorem Equiv.Perm.viaFintypeEmbedding_apply_not_mem_range {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (e : Equiv.Perm α) (f : α β) {b : β} (h : bSet.range f) :
      (e.viaFintypeEmbedding f) b = b
      @[simp]
      theorem Equiv.Perm.viaFintypeEmbedding_sign {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (e : Equiv.Perm α) (f : α β) [DecidableEq α] [Fintype β] :
      Equiv.Perm.sign (e.viaFintypeEmbedding f) = Equiv.Perm.sign e
      noncomputable def Equiv.toCompl {α : Type u_1} [Finite α] {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 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.

      Equations
      Instances For
        @[reducible, inline]
        noncomputable abbrev Equiv.extendSubtype {α : Type u_1} [Finite α] {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] (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.

        Equations
        • e.extendSubtype = e.subtypeCongr e.toCompl
        Instances For
          theorem Equiv.extendSubtype_apply_of_mem {α : Type u_1} [Finite α] {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] (e : { x : α // p x } { x : α // q x }) (x : α) (hx : p x) :
          e.extendSubtype x = (e x, hx)
          theorem Equiv.extendSubtype_mem {α : Type u_1} [Finite α] {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] (e : { x : α // p x } { x : α // q x }) (x : α) (hx : p x) :
          q (e.extendSubtype x)
          theorem Equiv.extendSubtype_apply_of_not_mem {α : Type u_1} [Finite α] {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] (e : { x : α // p x } { x : α // q x }) (x : α) (hx : ¬p x) :
          e.extendSubtype x = (e.toCompl x, hx)
          theorem Equiv.extendSubtype_not_mem {α : Type u_1} [Finite α] {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] (e : { x : α // p x } { x : α // q x }) (x : α) (hx : ¬p x) :
          ¬q (e.extendSubtype x)