Equivalence between types #
In this file we continue the work on equivalences begun in Logic/Equiv/Defs.lean
, defining
-
canonical isomorphisms between various types: e.g.,
-
Equiv.sumEquivSigmaBool
is the canonical equivalence between the sum of two typesα ⊕ β
and the sigma-typeΣ b : Bool, b.casesOn α β
; -
Equiv.prodSumDistrib : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ)
shows that type product and type sum satisfy the distributive law up to a canonical equivalence;
-
-
operations on equivalences: e.g.,
Equiv.prodCongr ea eb : α₁ × β₁ ≃ α₂ × β₂
: combine two equivalencesea : α₁ ≃ α₂
andeb : β₁ ≃ β₂
usingProd.map
.
More definitions of this kind can be found in other files. E.g.,
Data/Equiv/TransferInstance.lean
does it for many algebraic type classes likeGroup
,Module
, etc.
Tags #
equivalence, congruence, bijective map
PUnit
is a right identity for type product up to an equivalence.
Instances For
PUnit
is a left identity for type product up to an equivalence.
Instances For
PUnit
is a right identity for dependent type product up to an equivalence.
Instances For
PEmpty
type is a right absorbing element for type product up to an equivalence.
Instances For
PEmpty
type is a left absorbing element for type product up to an equivalence.
Instances For
Combine a permutation of α
and of β
into a permutation of α ⊕ β
.
Instances For
The set of x : Option α
such that isSome x
is equivalent to α
.
Instances For
sigmaFiberEquiv f
for f : α → β
is the natural equivalence between
the type of all fibres of f
and the total space α
.
Instances For
For any predicate p
on α
,
the sum of the two subtypes {a // p a}
and its complement {a // ¬ p a}
is naturally equivalent to α
.
See subtypeOrEquiv
for sum types over subtypes {x // p x}
and {x // q x}
that are not necessarily IsCompl p q
.
Instances For
Combines an Equiv
between two subtypes with an Equiv
between their complements to form a
permutation.
Instances For
Combining permutations on ε
that permute only inside or outside the subtype
split induced by p : ε → Prop
constructs a permutation on ε
.
Instances For
For a fixed function x₀ : {a // p a} → β
defined on a subtype of α
,
the subtype of functions x : α → β
that agree with x₀
on the subtype {a // p a}
is naturally equivalent to the type of functions {a // ¬ p a} → β
.
Instances For
Given φ : α → β → Sort*
, we have an equivalence between ∀ a b, φ a b
and ∀ b a, φ a b
.
This is Function.swap
as an Equiv
.
Instances For
Dependent curry
equivalence: the type of dependent functions on Σ i, β i
is equivalent
to the type of dependent functions of two arguments (i.e., functions to the space of functions).
This is Sigma.curry
and Sigma.uncurry
together as an equiv.
Instances For
A variation on Equiv.prodCongr
where the equivalence in the second component can depend
on the first component. A typical example is a shear mapping, explaining the name of this
declaration.
Instances For
prodExtendRight a e
extends e : Perm β
to Perm (α × β)
by sending (a, b)
to
(a, e b)
and keeping the other (a', b)
fixed.
Instances For
The set of natural numbers is equivalent to ℕ ⊕ PUnit
.
Instances For
ℕ ⊕ PUnit
is equivalent to ℕ
.
Instances For
If α
is equivalent to β
and the predicates p : α → Prop
and q : β → Prop
are equivalent
at corresponding points, then {a // p a}
is equivalent to {b // q b}
.
For the statement where α = β
, that is, e : perm α
, see Perm.subtypePerm
.
Instances For
A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. This
version allows the “inner” predicate to depend on h : p a
.
Instances For
The type ∀ (i : α), β i
can be split as a product by separating the indices in α
depending on whether they satisfy a predicate p
or not.
Instances For
A product of types can be split as the binary product of one of the types and the product of all the remaining types.
Instances For
A product of copies of a type can be split as the binary product of one copy and the product of all the remaining copies.
Instances For
The type of all functions X → Y
with prescribed values for all x' ≠ x
is equivalent to the codomain Y
.
Instances For
If f
is a bijective function, then its domain is equivalent to its codomain.
Instances For
Extend the domain of e : Equiv.Perm α
to one that is over β
via f : α → Subtype p
,
where p : β → Prop
, permuting only the b : β
that satisfy p b
.
This can be used to extend the domain across a function f : α → β
,
keeping everything outside of Set.range f
fixed. For this use-case Equiv
given by f
can
be constructed by Equiv.of_leftInverse'
or Equiv.of_leftInverse
when there is a known
inverse, or Equiv.ofInjective
in the general case.
Instances For
Subtype of the quotient is equivalent to the quotient of the subtype. Let α
be a setoid with
equivalence relation ~
. Let p₂
be a predicate on the quotient type α/~
, and p₁
be the lift
of this predicate to α
: p₁ a ↔ p₂ ⟦a⟧
. Let ~₂
be the restriction of ~
to {x // p₁ x}
.
Then {x // p₂ x}
is equivalent to the quotient of {x // p₁ x}
by ~₂
.
Instances For
A helper function for Equiv.swap
.
Instances For
swap a b
is the permutation that swaps a
and b
and
leaves other values as is.
Instances For
A function is invariant to a swap if it is equal at both elements
Augment an equivalence with a prescribed mapping f a = b
Instances For
Convert an involutive function f
to a permutation with toFun = invFun = f
.
Instances For
Note: the "obvious" statement (piCongrLeft' P e).symm g a = g (e a)
doesn't typecheck: the
LHS would have type P a
while the RHS would have type P (e.symm (e a))
. For that reason,
we have to explicitly substitute along e.symm (e a) = a
in the statement of this lemma.
Note: the "obvious" statement (piCongrLeft' P e).symm g a = g (e a)
doesn't typecheck: the
LHS would have type P a
while the RHS would have type P (e.symm (e a))
. This lemma is a way
around it in the case where a
is of the form e.symm b
, so we can use g b
instead of
g (e (e.symm b))
.
Note: the "obvious" statement (piCongrLeft P e) f b = f (e.symm b)
doesn't typecheck: the
LHS would have type P b
while the RHS would have type P (e (e.symm b))
. For that reason,
we have to explicitly substitute along e (e.symm b) = b
in the statement of this lemma.
Note: the "obvious" statement (piCongrLeft P e) f b = f (e.symm b)
doesn't typecheck: the
LHS would have type P b
while the RHS would have type P (e (e.symm b))
. This lemma is a way
around it in the case where b
is of the form e a
, so we can use f a
instead of
f (e.symm (e a))
.
Transport dependent functions through an equivalence of the base spaces and a family of equivalences of the matching fibres.
Instances For
If α
is a subsingleton, then it is equivalent to α × α
.
Instances For
To give an equivalence between two subsingleton types, it is sufficient to give any two functions between them.
Instances For
A nonempty subsingleton type is (noncomputably) equivalent to PUnit
.