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
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.
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 := ⋯ }
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.
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₁)
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