Equivalence between types #
In this file we define two types:
-
Equiv α β
a.k.a.α ≃ β
: a bijective mapα → β
bundled with its inverse map; we use this (and not equality!) to express that variousType
s orSort
s are equivalent. -
Equiv.Perm α
: the group of permutationsα ≃ α
. More lemmas aboutEquiv.Perm
can be found inGroupTheory.Perm
.
Then we define
-
canonical isomorphisms between various types: e.g.,
Equiv.refl α
is the identity map interpreted asα ≃ α
;
-
operations on equivalences: e.g.,
-
Equiv.symm e : β ≃ α
is the inverse ofe : α ≃ β
; -
Equiv.trans e₁ e₂ : α ≃ γ
is the composition ofe₁ : α ≃ β
ande₂ : β ≃ γ
(note the order of the arguments!);
-
-
definitions that transfer some instances along an equivalence. By convention, we transfer instances from right to left.
Equiv.inhabited
takese : α ≃ β
and[Inhabited β]
and returnsInhabited α
;Equiv.unique
takese : α ≃ β
and[Unique β]
and returnsUnique α
;Equiv.decidableEq
takese : α ≃ β
and[DecidableEq β]
and returnsDecidableEq α
.
More definitions of this kind can be found in other files. E.g.,
Data.Equiv.TransferInstance
does it for many algebraic type classes likeGroup
,Module
, etc.
Many more such isomorphisms and operations are defined in Logic.Equiv.Basic
.
Tags #
equivalence, congruence, bijective map
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
α ≃ β
is the type of functions from α → β
with a two-sided inverse.
Instances For
Helper instance when inference gets stuck on following the normal chain
EquivLike → EmbeddingLike → FunLike → CoeFun
.
The map (r ≃ s) → (r → s)
is injective.
See Note [custom simps projection]
Instances For
Transfer DecidableEq
across an equivalence.
Instances For
This cannot be a simp
lemmas as it incorrectly matches against e : α ≃ synonym α
, when
synonym α
is semireducible. This makes a mess of Multiplicative.ofAdd
etc.
If α
is an empty type, then it is equivalent to the PEmpty
type in any universe.
Instances For
The Sort
of proofs of a false proposition is equivalent to PEmpty
.
Instances For
A version of Equiv.arrowCongr
in Type
, rather than Sort
.
The equiv_rw
tactic is not able to use the default Sort
level Equiv.arrowCongr
,
because Lean's universe rules will not unify ?l_1
with imax (1 ?m_1)
.
Instances For
If α
is Subsingleton
and a : α
, then the type of dependent functions Π (i : α), β i
is equivalent to β a
.
Instances For
A Sigma
with fun i ↦ ULift (PLift (P i))
fibers is equivalent to { x // P x }
.
Variant of sigmaPLiftEquivSubtype
.
Instances For
A family of permutations Π a, Perm (β a)
generates a permutation Perm (Σ a, β₁ a)
.
Instances For
Quotients are congruent on equivalences under equality of their relation.
An alternative is just to use rewriting with eq
, but then computational proofs get stuck.
Instances For
An equivalence e : α ≃ β
generates an equivalence between the quotient space of α
by a relation ra
and the quotient space of β
by the image of this relation under e
.