Equivalence between types #
In this file we continue the work on equivalences begun in Mathlib/Logic/Equiv/Defs.lean
, defining
a lot of equivalences between various types and operations on these equivalences.
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 like
Group
, Module
, etc.
Tags #
equivalence, congruence, bijective map
Combines an Equiv
between two subtypes with an Equiv
between their complements to form a
permutation.
Equations
Instances For
Combining permutations on ε
that permute only inside or outside the subtype
split induced by p : ε → Prop
constructs a permutation on ε
.
Equations
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} → β
.
Equations
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
.
Equations
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.
Equations
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
.
Equations
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
.
Equations
Instances For
A sigma type over a subtype is equivalent to the sigma set over the original type, if the fiber is empty outside of the subset
Equations
Instances For
If a predicate p : β → Prop
is true on the range of a map f : α → β
, then
Σ y : {y // p y}, {x // f x = y}
is equivalent to α
.
Equations
Instances For
The Pi
-type ∀ i, π i
is equivalent to the type of sections f : ι → Σ i, π i
of the
Sigma
type such that for all i
we have (f i).fst = i
.
Equations
Instances For
The type of functions f : ∀ a, β a
such that for all a
we have p a (f a)
is equivalent
to the type of functions ∀ a, {b : β a // p a b}
.
Equations
Instances For
A subtype of a dependent triple which pins down both bases is equivalent to the respective fiber.
Equations
Instances For
A specialization of sigmaSigmaSubtype
to the case where the second base
does not depend on the first, and the property being checked for is simple
equality. Useful e.g. when γ
is Hom
inside a category.
Equations
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.
Equations
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 ~₂
.
Equations
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
Equations
Instances For
Convert an involutive function f
to a permutation with toFun = invFun = f
.
Equations
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.
This lemma is impractical to state in the dependent case.
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))
.
Alias of Equiv.piCongrLeft_sumInl
.
Alias of Equiv.piCongrLeft_sumInr
.
To give an equivalence between two subsingleton types, it is sufficient to give any two functions between them.
Equations
Instances For
A nonempty subsingleton type is (noncomputably) equivalent to PUnit
.