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.sumEquivSigmaBoolis 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;
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/Algebra/Equiv/TransferInstance.leandoes it for many algebraic type classes likeGroup,Module, etc.
Tags #
equivalence, congruence, bijective map
Type product is associative up to an equivalence.
γ-valued functions on α × β are equivalent to functions α → β → γ.
Equations
- Equiv.curry α β γ = { toFun := Function.curry, invFun := Function.uncurry, left_inv := ⋯, right_inv := ⋯ }
PUnit is a right identity for type product up to an equivalence.
Equations
- Equiv.prodPUnit α = { toFun := fun (p : α × PUnit.{?u.14 + 1}) => p.1, invFun := fun (a : α) => (a, PUnit.unit), left_inv := ⋯, right_inv := ⋯ }
PUnit is a left identity for type product up to an equivalence.
Equations
PUnit is a right identity for dependent type product up to an equivalence.
Equations
- Equiv.sigmaPUnit α = { toFun := fun (p : (_ : α) × PUnit.{?u.16 + 1}) => p.fst, invFun := fun (a : α) => ⟨a, PUnit.unit⟩, left_inv := ⋯, right_inv := ⋯ }
Any Unique type is a right identity for type product up to equivalence.
Equations
- Equiv.prodUnique α β = ((Equiv.refl α).prodCongr (Equiv.equivPUnit β)).trans (Equiv.prodPUnit α)
Any Unique type is a left identity for type product up to equivalence.
Equations
- Equiv.uniqueProd α β = ((Equiv.equivPUnit β).prodCongr (Equiv.refl α)).trans (Equiv.punitProd α)
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 α)
Any Unique type is a left identity for type sigma up to equivalence. Compare with uniqueProd
which is non-dependent.
Empty type is a right absorbing element for type product up to an equivalence.
Equations
- Equiv.prodEmpty α = Equiv.equivEmpty (α × Empty)
Empty type is a left absorbing element for type product up to an equivalence.
Equations
- Equiv.emptyProd α = Equiv.equivEmpty (Empty × α)
PEmpty type is a right absorbing element for type product up to an equivalence.
Equations
PEmpty type is a left absorbing element for type product up to an equivalence.
Equations
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 := ⋯ }
The sum of IsEmpty with any type is equivalent to that type.
Equations
- Equiv.emptySum α β = (Equiv.sumComm α β).trans (Equiv.sumEmpty β α)
The set of x : Option α such that isSome x is equivalent to α.
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.
α ⊕ β 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.
sigmaFiberEquiv f for f : α → β is the natural equivalence between
the type of all fibres of f and the total space α.
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.
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 := ⋯ }
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))
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)
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.
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 := ⋯ }
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 := ⋯ }
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 := ⋯ }
A family of equivalences ∀ (a : α₁), β₁ ≃ β₂ generates an equivalence
between β₁ × α₁ and β₂ × α₁.
A family of equivalences ∀ (a : α₁), β₁ ≃ β₂ generates an equivalence
between α₁ × β₁ and α₁ × β₂.
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.
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.
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.
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.
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
The type of functions on a sum type α ⊕ β is equivalent to the type of pairs of functions
on α and on β.
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 γ α))
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.
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.
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.
The product Bool × α is equivalent to α ⊕ α.
The function type Bool → α is equivalent to α × α.
The set of natural numbers is equivalent to ℕ ⊕ PUnit.
Equations
- One or more equations did not get rendered due to their size.
ℕ ⊕ PUnit is equivalent to ℕ.
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.
If two predicates p and q are pointwise equivalent, then {x // p x} is equivalent to
{x // q x}.
Equations
If two predicates are equal, then the corresponding subtypes are equivalent.
Equations
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.
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 ⋯)
If the outer subtype has more restrictive predicate than the inner one, then we can drop the latter.
Equations
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 := ⋯ }
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
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)
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.
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'
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.
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.
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.
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.
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.
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.
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 : α) => β
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)
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 })
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.
A helper function for Equiv.swap.
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 := ⋯ }
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
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 := ⋯ }
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 := ⋯ }
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
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.
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₁)
If α is a subsingleton, then it is equivalent to α × α.
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 := ⋯ }
A nonempty subsingleton type is (noncomputably) equivalent to PUnit.
Equations
- Equiv.punitOfNonemptyOfSubsingleton = equivOfSubsingletonOfSubsingleton (fun (x : α) => PUnit.unit) fun (x : PUnit.{?u.25}) => h.some
If Unique β, then Unique α is equivalent to α ≃ β.
Equations
- uniqueEquivEquivUnique α β = equivOfSubsingletonOfSubsingleton (fun (x : Unique α) => Equiv.ofUnique α β) Equiv.unique