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.
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
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
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
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