Equivalence between fintypes #
This file contains some basic results on equivalences where one or both
sides of the equivalence are Fintype
s.
Main definitions #
Function.Embedding.toEquivRange
: computably turn an embedding of a fintype into anEquiv
of the domain to its rangeEquiv.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 inputFintype
s.
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
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
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.
Equations
- Equiv.toCompl e = Classical.choice (_ : Nonempty ({ x : α // ¬p x } ≃ { x : α // ¬q x }))
Instances For
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.