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
Combine two equivalences using PProd in the domain and Prod in the codomain.
Equations
- ea.pprodProd eb = (ea.pprodCongr eb).trans Equiv.pprodEquivProd
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.14 + 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.16 + 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
Any Unique type is a left identity for type sigma up to equivalence. Compare with uniqueProd
which is non-dependent.
Equations
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
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
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
Instances For
A family of equivalences ∀ (a : α₁), β₁ ≃ β₂ generates an equivalence
between α₁ × β₁ and α₁ × β₂.
Equations
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. 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.
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 set of natural numbers is equivalent to ℕ ⊕ PUnit.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
Instances For
If two predicates p and q are pointwise equivalent, then {x // p x} is equivalent to
{x // q x}.
Equations
Instances For
If α ≃ β, then for any predicate p : β → Prop the subtype {a // p (e a)} is equivalent
to the subtype {b // p b}.
Equations
Instances For
If two predicates are equal, then the corresponding subtypes are equivalent.
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 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
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.
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)).
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₁)
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.25}) => h.some
Instances For
If Unique β, then Unique α is equivalent to α ≃ β.
Equations
- uniqueEquivEquivUnique α β = equivOfSubsingletonOfSubsingleton (fun (x : Unique α) => Equiv.ofUnique α β) Equiv.unique