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 invFun toFun
- right_inv : Function.RightInverse invFun toFun
α ≃ β≃ β
is the type of functions from α → β→ β
with a two-sided inverse.
Instances For
Equations
- «term_≃_» = Lean.ParserDescr.trailingNode `term_≃_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ ") (Lean.ParserDescr.cat `term 26))
Turn an element of a type F
satisfying EquivLike F α β
into an actual
Equiv
. This is declared as the default coercion from F
to α ≃ β≃ β
.
Equations
- One or more equations did not get rendered due to their size.
Perm α
is the type of bijections from α
to itself.
Equations
- Equiv.Perm α = (α ≃ α)
Helper instance when inference gets stuck on following the normal chain
EquivLike → EmbeddingLike → FunLike → CoeFun→ EmbeddingLike → FunLike → CoeFun→ FunLike → CoeFun→ CoeFun
.
Equations
- Equiv.instFunLikeEquiv = EmbeddingLike.toFunLike
The map (r ≃ s) → (r → s)≃ s) → (r → s)→ (r → s)→ s)
is injective.
Equations
- Equiv.inhabited' = { default := Equiv.refl α }
Inverse of an equivalence e : α ≃ β≃ β
.
Equations
- Equiv.symm e = { toFun := e.invFun, invFun := e.toFun, left_inv := (_ : Function.RightInverse e.invFun e.toFun), right_inv := (_ : Function.LeftInverse e.invFun e.toFun) }
See Note [custom simps projection]
Equations
- Equiv.Simps.symm_apply e = ↑(Equiv.symm e)
Equations
- Equiv.instTransSortSortSortEquivEquivEquiv = { trans := fun {a} {b} {c} => Equiv.trans }
Equations
- Equiv.permUnique = uniqueOfSubsingleton (Equiv.refl α)
Transfer DecidableEq
across an equivalence.
Equations
If α ≃ β≃ β
and β
is inhabited, then so is α
.
Equations
- Equiv.inhabited e = { default := ↑(Equiv.symm e) default }
If α ≃ β≃ β
and β
is a singleton type, then so is α
.
Equations
- Equiv.unique e = Function.Surjective.unique ↑(Equiv.symm e) (_ : Function.Surjective ↑(Equiv.symm e))
Equivalence between equal types.
This cannot be a simp
lemmas as it incorrectly matches against e : α ≃ synonym α≃ synonym α
, when
synonym α
is semireducible. This makes a mess of multiplicative.of_add
etc.
If α
is equivalent to β
and γ
is equivalent to δ
, then the type of equivalences α ≃ γ≃ γ
is equivalent to the type of equivalences β ≃ δ≃ δ
.
Equations
- One or more equations did not get rendered due to their size.
If α
is equivalent to β
, then Perm α
is equivalent to Perm β
.
Equations
- Equiv.permCongr e = Equiv.equivCongr e e
If α
is an empty type, then it is equivalent to the Empty
type.
Equations
If α
is an empty type, then it is equivalent to the PEmpty
type in any universe.
Equations
The Sort
of proofs of a false proposition is equivalent to PEmpty
.
Equations
If α
has a unique element, then it is equivalent to any PUnit
.
Equations
The Sort
of proofs of a true proposition is equivalent to PUnit
.
Equations
If α₁
is equivalent to α₂
and β₁
is equivalent to β₂
, then the type of maps α₁ → β₁→ β₁
is equivalent to the type of maps α₂ → β₂→ β₂
.
Equations
- One or more equations did not get rendered due to their size.
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
- Equiv.arrowCongr' hα hβ = Equiv.arrowCongr hα hβ
Conjugate a map f : α → α→ α
by an equivalence α ≃ β≃ β
.
Equations
- Equiv.conj e = Equiv.arrowCongr e e
PUnit
sorts in any two universes are equivalent.
Equations
- Equiv.punitEquivPUnit = { toFun := fun x => PUnit.unit, invFun := fun x => PUnit.unit, left_inv := Equiv.punitEquivPUnit.proof_1, right_inv := Equiv.punitEquivPUnit.proof_2 }
Prop
is noncomputably equivalent to Bool
.
Equations
- Equiv.propEquivBool = { toFun := fun p => decide p, invFun := fun b => b = true, left_inv := Equiv.propEquivBool.proof_1, right_inv := Equiv.propEquivBool.proof_2 }
If α
is Subsingleton
and a : α
, then the type of dependent functions Π (i : α), β i
is equivalent to β a
.
Equations
- One or more equations did not get rendered due to their size.
If α
has a unique term, then the type of function α → β→ β
is equivalent to β
.
Equations
- Equiv.funUnique α β = Equiv.piSubsingleton (fun a => β) default
The sort of maps from PUnit
is equivalent to the codomain.
Equations
The sort of maps from True
is equivalent to the codomain.
Equations
A family of equivalences Π a, β₁ a ≃ β₂ a≃ β₂ a
generates an equivalence between Σ' a, β₁ a
and
Σ' a, β₂ a
.
Equations
- One or more equations did not get rendered due to their size.
A family of equivalences Π a, β₁ a ≃ β₂ a≃ β₂ a
generates an equivalence between Σ a, β₁ a
and
Σ a, β₂ a
.
Equations
- One or more equations did not get rendered due to their size.
A Sigma
with λ i, ULift (PLift (P i))
fibers is equivalent to { x // P x }
.
Variant of sigmaPLiftEquivSubtype
.
Equations
- Equiv.sigmaULiftPLiftEquivSubtype P = Equiv.trans (Equiv.sigmaCongrRight fun x => Equiv.ulift) (Equiv.sigmaPLiftEquivSubtype P)
A family of permutations Π a, Perm (β a)
generates a permuation Perm (Σ a, β₁ a)
.
Equations
Transporting a sigma type through an equivalence of the base
Equations
An equivalence e : α ≃ β≃ β
generates an equivalence between quotient spaces,
if `ra a₁ a₂ ↔ rb (e a₁) (e a₂).
Equations
- One or more equations did not get rendered due to their size.
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
- Quot.congrRight eq = Quot.congr (Equiv.refl α) eq
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
- Quot.congrLeft e = Quot.congr e (_ : ∀ (x x_1 : α), r x x_1 ↔ r (↑(Equiv.symm e) (↑e x)) (↑(Equiv.symm e) (↑e x_1)))
An equivalence e : α ≃ β≃ β
generates an equivalence between quotient spaces,
if `ra a₁ a₂ ↔ rb (e a₁) (e a₂).
Equations
- Quotient.congr e eq = Quot.congr e eq