Equivalence between types #
In this file we continue the work on equivalences begun in Mathlib/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.,
Mathlib/Logic/Equiv/TransferInstance.lean
does it for many algebraic type classes likeGroup
,Module
, etc.
Tags #
equivalence, congruence, bijective map
Type product is commutative up to an equivalence: α × β ≃ β × α
. This is Prod.swap
as an
equivalence.
Equations
- Equiv.prodComm α β = { toFun := Prod.swap, invFun := Prod.swap, left_inv := ⋯, right_inv := ⋯ }
Instances For
Type product is associative up to an equivalence.
Equations
Instances For
γ
-valued functions on α × β
are equivalent to functions α → β → γ
.
Equations
- Equiv.curry α β γ = { toFun := Function.curry, invFun := Function.uncurry, left_inv := ⋯, right_inv := ⋯ }
Instances For
PUnit
is a right identity for type product up to an equivalence.
Equations
- Equiv.prodPUnit α = { toFun := fun (p : α × PUnit.{?u.13 + 1} ) => p.1, invFun := fun (a : α) => (a, PUnit.unit), left_inv := ⋯, right_inv := ⋯ }
Instances For
PUnit
is a right identity for dependent type product up to an equivalence.
Equations
- Equiv.sigmaPUnit α = { toFun := fun (p : (_ : α) × PUnit.{?u.15 + 1} ) => p.fst, invFun := fun (a : α) => ⟨a, PUnit.unit⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
Any Unique
type is a right identity for type product up to equivalence.
Equations
- Equiv.prodUnique α β = ((Equiv.refl α).prodCongr (Equiv.equivPUnit β)).trans (Equiv.prodPUnit α)
Instances For
Any Unique
type is a left identity for type product up to equivalence.
Equations
- Equiv.uniqueProd α β = ((Equiv.equivPUnit β).prodCongr (Equiv.refl α)).trans (Equiv.punitProd α)
Instances For
Any family of Unique
types is a right identity for dependent type product up to
equivalence.
Equations
- Equiv.sigmaUnique α β = (Equiv.sigmaCongrRight fun (a : α) => Equiv.equivPUnit (β a)).trans (Equiv.sigmaPUnit α)
Instances For
Empty
type is a right absorbing element for type product up to an equivalence.
Equations
- Equiv.prodEmpty α = Equiv.equivEmpty (α × Empty)
Instances For
Empty
type is a left absorbing element for type product up to an equivalence.
Equations
- Equiv.emptyProd α = Equiv.equivEmpty (Empty × α)
Instances For
PEmpty
type is a right absorbing element for type product up to an equivalence.
Equations
Instances For
PEmpty
type is a left absorbing element for type product up to an equivalence.
Equations
Instances For
Equations
- Equiv.psumEquivSum α β = { toFun := fun (s : α ⊕' β) => PSum.casesOn s Sum.inl Sum.inr, invFun := Sum.elim PSum.inl PSum.inr, left_inv := ⋯, right_inv := ⋯ }
Instances For
Combine a permutation of α
and of β
into a permutation of α ⊕ β
.
Equations
- ea.sumCongr eb = Equiv.sumCongr ea eb
Instances For
Sum of types is commutative up to an equivalence. This is Sum.swap
as an equivalence.
Equations
- Equiv.sumComm α β = { toFun := Sum.swap, invFun := Sum.swap, left_inv := ⋯, right_inv := ⋯ }
Instances For
Sum with IsEmpty
is equivalent to the original type.
Equations
- Equiv.sumEmpty α β = { toFun := Sum.elim id fun (a : β) => isEmptyElim a, invFun := Sum.inl, left_inv := ⋯, right_inv := ⋯ }
Instances For
The sum of IsEmpty
with any type is equivalent to that type.
Equations
- Equiv.emptySum α β = (Equiv.sumComm α β).trans (Equiv.sumEmpty β α)
Instances For
The product over Option α
of β a
is the binary product of the
product over α
of β (some α)
and β none
Equations
- One or more equations did not get rendered due to their size.
Instances For
α ⊕ β
is equivalent to a Sigma
-type over Bool
. Note that this definition assumes α
and
β
to be types from the same universe, so it cannot be used directly to transfer theorems about
sigma types to theorems about sum types. In many cases one can use ULift
to work around this
difficulty.
Equations
- One or more equations did not get rendered due to their size.
Instances For
sigmaFiberEquiv f
for f : α → β
is the natural equivalence between
the type of all fibres of f
and the total space α
.
Equations
- Equiv.sigmaFiberEquiv f = { toFun := fun (x : (y : β) × { x : α // f x = y }) => ↑x.snd, invFun := fun (x : α) => ⟨f x, ⟨x, ⋯⟩⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
Inhabited types are equivalent to Option β
for some β
by identifying default
with none
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- Equiv.sumCompl p = { toFun := Sum.elim Subtype.val Subtype.val, invFun := fun (a : α) => if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
Combines an Equiv
between two subtypes with an Equiv
between their complements to form a
permutation.
Equations
- e.subtypeCongr f = (Equiv.sumCompl p).symm.trans ((e.sumCongr f).trans (Equiv.sumCompl q))
Instances For
Combining permutations on ε
that permute only inside or outside the subtype
split induced by p : ε → Prop
constructs a permutation on ε
.
Equations
- ep.subtypeCongr en = (Equiv.sumCompl p).permCongr (ep.sumCongr en)
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
- One or more equations did not get rendered due to their size.
Instances For
A family of equivalences ∀ a, β₁ a ≃ β₂ a
generates an equivalence between ∀ a, β₁ a
and
∀ a, β₂ a
.
Equations
- Equiv.piCongrRight F = { toFun := Pi.map fun (a : α) => ⇑(F a), invFun := Pi.map fun (a : α) => ⇑(F a).symm, left_inv := ⋯, right_inv := ⋯ }
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
- Equiv.piComm φ = { toFun := Function.swap, invFun := Function.swap, left_inv := ⋯, right_inv := ⋯ }
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
- Equiv.piCurry γ = { toFun := Sigma.curry, invFun := Sigma.uncurry, left_inv := ⋯, right_inv := ⋯ }
Instances For
A family of equivalences ∀ (a : α₁), β₁ ≃ β₂
generates an equivalence
between β₁ × α₁
and β₂ × α₁
.
Equations
- Equiv.prodCongrLeft e = { toFun := fun (ab : β₁ × α₁) => ((e ab.2) ab.1, ab.2), invFun := fun (ab : β₂ × α₁) => ((e ab.2).symm ab.1, ab.2), left_inv := ⋯, right_inv := ⋯ }
Instances For
A family of equivalences ∀ (a : α₁), β₁ ≃ β₂
generates an equivalence
between α₁ × β₁
and α₁ × β₂
.
Equations
- Equiv.prodCongrRight e = { toFun := fun (ab : α₁ × β₁) => (ab.1, (e ab.1) ab.2), invFun := fun (ab : α₁ × β₂) => (ab.1, (e ab.1).symm ab.2), left_inv := ⋯, right_inv := ⋯ }
Instances For
A family of equivalences between fibers gives an equivalence between domains.
Equations
- Equiv.ofFiberEquiv e = (Equiv.sigmaFiberEquiv f).symm.trans ((Equiv.sigmaCongrRight e).trans (Equiv.sigmaFiberEquiv g))
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.
Equations
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The type of functions to a product α × β
is equivalent to the type of pairs of functions
γ → α
and γ → β
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The type of dependent functions on a sum type ι ⊕ ι'
is equivalent to the type of pairs of
functions on ι
and on ι'
. This is a dependent version of Equiv.sumArrowEquivProdArrow
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equivalence between a product of two dependent functions types and a single dependent
function type. Basically a symmetric version of Equiv.sumPiEquivProdPi
.
Equations
- Equiv.prodPiEquivSumPi π π' = (Equiv.sumPiEquivProdPi (Sum.elim π π')).symm
Instances For
The type of functions on a sum type α ⊕ β
is equivalent to the type of pairs of functions
on α
and on β
.
Equations
Instances For
Type product is left distributive with respect to type sum up to an equivalence.
Equations
- Equiv.prodSumDistrib α β γ = Trans.trans (Trans.trans (Equiv.prodComm α (β ⊕ γ)) (Equiv.sumProdDistrib β γ α)) ((Equiv.prodComm β α).sumCongr (Equiv.prodComm γ α))
Instances For
An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The product of an indexed sum of types (formally, a Sigma
-type Σ i, α i
) by a type β
is
equivalent to the sum of products Σ i, (α i × β)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The function type Bool → α
is equivalent to α × α
.
Equations
- Equiv.boolArrowEquivProd α = { toFun := fun (f : Bool → α) => (f false, f true), invFun := fun (p : α × α) (b : Bool) => Bool.casesOn b p.1 p.2, left_inv := ⋯, right_inv := ⋯ }
Instances For
The set of natural numbers is equivalent to ℕ ⊕ PUnit
.
Equations
- One or more equations did not get rendered due to their size.
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
- e.subtypeEquiv h = { toFun := fun (a : { a : α // p a }) => ⟨e ↑a, ⋯⟩, invFun := fun (b : { b : β // q b }) => ⟨e.symm ↑b, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
If two predicates p
and q
are pointwise equivalent, then {x // p x}
is equivalent to
{x // q x}
.
Equations
- Equiv.subtypeEquivRight e = (Equiv.refl α).subtypeEquiv e
Instances For
If α ≃ β
, then for any predicate p : β → Prop
the subtype {a // p (e a)}
is equivalent
to the subtype {b // p b}
.
Equations
- e.subtypeEquivOfSubtype = e.subtypeEquiv ⋯
Instances For
If α ≃ β
, then for any predicate p : α → Prop
the subtype {a // p a}
is equivalent
to the subtype {b // p (e.symm b)}
. This version is used by equiv_rw
.
Equations
- e.subtypeEquivOfSubtype' = e.symm.subtypeEquivOfSubtype.symm
Instances For
If two predicates are equal, then the corresponding subtypes are equivalent.
Equations
- Equiv.subtypeEquivProp h = (Equiv.refl α).subtypeEquiv ⋯
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
- Equiv.subtypeSubtypeEquivSubtypeExists p q = { toFun := fun (a : Subtype q) => ⟨↑↑a, ⋯⟩, invFun := fun (a : { a : α // ∃ (h : p a), q ⟨a, h⟩ }) => ⟨⟨↑a, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates.
Equations
- Equiv.subtypeSubtypeEquivSubtypeInter p q = (Equiv.subtypeSubtypeEquivSubtypeExists p fun (x : Subtype p) => q ↑x).trans (Equiv.subtypeEquivRight ⋯)
Instances For
If the outer subtype has more restrictive predicate than the inner one, then we can drop the latter.
Equations
Instances For
If a proposition holds for all elements, then the subtype is equivalent to the original type.
Equations
- Equiv.subtypeUnivEquiv h = { toFun := fun (x : Subtype p) => ↑x, invFun := fun (x : α) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
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
- Equiv.sigmaSubtypeEquivOfSubset p q h = (Equiv.subtypeSigmaEquiv p q).symm.trans (Equiv.subtypeUnivEquiv ⋯)
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
- Equiv.sigmaSubtypeFiberEquiv f p h = Trans.trans (Equiv.sigmaSubtypeEquivOfSubset (fun (y : β) => { x : α // f x = y }) p ⋯) (Equiv.sigmaFiberEquiv f)
Instances For
If for each x
we have p x ↔ q (f x)
, then Σ y : {y // q y}, f ⁻¹' {y}
is equivalent
to {x // p x}
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A sigma type over an Option
is equivalent to the sigma set over the original type,
if the fiber is empty at none.
Equations
- Equiv.sigmaOptionEquivOfSome p h = (Equiv.sigmaSubtypeEquivOfSubset p (fun (x : Option α) => x.isSome = true) ⋯).symm.trans (Equiv.optionIsSomeEquiv α).sigmaCongrLeft'
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Instances For
A subtype of a product defined by componentwise conditions is equivalent to a product of subtypes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A subtype of a Prod
that depends only on the first component is equivalent to the
corresponding subtype of the first type times the second type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A subtype of a Prod
is equivalent to a sigma type whose fibers are subtypes.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- Equiv.funSplitAt i β = Equiv.piSplitAt i fun (a : α) => β
Instances For
The type of all functions X → Y
with prescribed values for all x' ≠ x
is equivalent to the codomain Y
.
Equations
- Equiv.subtypeEquivCodomain f = (Equiv.subtypePreimage (fun (a : X) => a ≠ x) f).trans (Equiv.funUnique { x' : X // ¬x' ≠ x } Y)
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
- e.extendDomain f = (f.permCongr e).subtypeCongr (Equiv.refl { a : β' // ¬p a })
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
- One or more equations did not get rendered due to their size.
Instances For
A helper function for Equiv.swap
.
Equations
- Equiv.swapCore a b r = if r = a then b else if r = b then a else r
Instances For
swap a b
is the permutation that swaps a
and b
and
leaves other values as is.
Equations
- Equiv.swap a b = { toFun := Equiv.swapCore a b, invFun := Equiv.swapCore a b, left_inv := ⋯, right_inv := ⋯ }
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
- f.setValue a b = Equiv.trans (Equiv.swap a (f.symm b)) f
Instances For
Convert an involutive function f
to a permutation with toFun = invFun = f
.
Equations
- Function.Involutive.toPerm f h = { toFun := f, invFun := f, left_inv := ⋯, right_inv := ⋯ }
Instances For
Transport dependent functions through an equivalence of the base space.
Equations
- Equiv.piCongrLeft' P e = { toFun := fun (f : (a : α) → P a) (x : β) => f (e.symm x), invFun := fun (f : (b : β) → P (e.symm b)) (x : α) => ⋯ ▸ f (e x), left_inv := ⋯, right_inv := ⋯ }
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))
.
Transporting dependent functions through an equivalence of the base, expressed as a "simplification".
Equations
- Equiv.piCongrLeft P e = (Equiv.piCongrLeft' P e.symm).symm
Instances For
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 fibers.
Equations
- h₁.piCongr h₂ = (Equiv.piCongrRight h₂).trans (Equiv.piCongrLeft Z h₁)
Instances For
Transport dependent functions through an equivalence of the base spaces and a family of equivalences of the matching fibres.
Equations
- h₁.piCongr' h₂ = (h₁.symm.piCongr fun (b : β) => (h₂ b).symm).symm
Instances For
If α
is a subsingleton, then it is equivalent to α × α
.
Equations
Instances For
To give an equivalence between two subsingleton types, it is sufficient to give any two functions between them.
Equations
- equivOfSubsingletonOfSubsingleton f g = { toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ }
Instances For
A nonempty subsingleton type is (noncomputably) equivalent to PUnit
.
Equations
- Equiv.punitOfNonemptyOfSubsingleton = equivOfSubsingletonOfSubsingleton (fun (x : α) => PUnit.unit) fun (x : PUnit.{?u.22}) => h.some
Instances For
If Unique β
, then Unique α
is equivalent to α ≃ β
.
Equations
- uniqueEquivEquivUnique α β = equivOfSubsingletonOfSubsingleton (fun (x : Unique α) => Equiv.equivOfUnique α β) Equiv.unique