Equivalence between sum 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, bif b then β else α
;Equiv.prodSumDistrib : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ)
shows that type product and type sum satisfy the distributive law up to a canonical equivalence;
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
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
α ⊕ β
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
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
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. Compare
with Equiv.sumSigmaDistrib
which is indexed by sums.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A type indexed by disjoint sums of types is equivalent to the sum of the sums. Compare with
Equiv.sigmaSumDistrib
which has the sums as the output type.
Equations
- One or more equations did not get rendered due to their size.