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 inMathlib/GroupTheory/Perm.lean
.
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.,
Mathlib/Algebra/Equiv/TransferInstance.lean
does it for many algebraic type classes likeGroup
,Module
, etc.
Many more such isomorphisms and operations are defined in Mathlib/Logic/Equiv/Basic.lean
.
Tags #
equivalence, congruence, bijective map
α ≃ β
is the type of functions from α → β
with a two-sided inverse.
Equations
Instances For
The map (r ≃ s) → (r → s)
is injective.
See Note [custom simps projection]
Equations
Instances For
Restatement of Equiv.left_inv
in terms of Function.LeftInverse
.
Restatement of Equiv.right_inv
in terms of Function.RightInverse
.
Equivalence between equal types.
Equations
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.
Equations
Instances For
Alias of Equiv.ofUnique
.
If both α
and β
have a unique element, then α ≃ β
.
Equations
Instances For
equivalence of propositions is the same as iff
Equations
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)
.
Equations
Instances For
A Sigma
with fun i ↦ ULift (PLift (P i))
fibers is equivalent to { x // P x }
.
Variant of sigmaPLiftEquivSubtype
.
Equations
Instances For
Function.swap
as an equivalence.
Equations
Instances For
If f
is a bijective function, then its domain is equivalent to its codomain.
Equations
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.
Equations
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
.
Equations
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.