# Partial Equivalences #

In this file, we define partial equivalences PEquiv, which are a bijection between a subset of α and a subset of β. Notationally, a PEquiv is denoted by "≃." (note that the full stop is part of the notation). The way we store these internally is with two functions f : α → Option β and the reverse function g : β → Option α, with the condition that if f a is some b, then g b is some a.

## Main results #

• PEquiv.ofSet: creates a PEquiv from a set s, which sends an element to itself if it is in s.
• PEquiv.single: given two elements a : α and b : β, create a PEquiv that sends them to each other, and ignores all other elements.
• PEquiv.injective_of_forall_ne_isSome/injective_of_forall_isSome: If the domain of a PEquiv is all of α (except possibly one point), its toFun is injective.

## Canonical order #

PEquiv is canonically ordered by inclusion; that is, if a function f defined on a subset s is equal to g on that subset, but g is also defined on a larger set, then f ≤ g. We also have a definition of ⊥, which is the empty PEquiv (sends all to none), which in the end gives us a SemilatticeInf with an OrderBot instance.

## Tags #

pequiv, partial equivalence

structure PEquiv (α : Type u) (β : Type v) :
Type (max u v)

A PEquiv is a partial equivalence, a representation of a bijection between a subset of α and a subset of β. See also PartialEquiv for a version that requires toFun and invFun to be globally defined functions and has source and target sets as extra fields.

• toFun : α

The underlying partial function of a PEquiv

• invFun : β

The partial inverse of toFun

• inv : ∀ (a : α) (b : β), a self.invFun b b self.toFun a

invFun is the partial inverse of toFun

Instances For
theorem PEquiv.inv {α : Type u} {β : Type v} (self : α ≃. β) (a : α) (b : β) :
a self.invFun b b self.toFun a

invFun is the partial inverse of toFun

A PEquiv is a partial equivalence, a representation of a bijection between a subset of α and a subset of β. See also PartialEquiv for a version that requires toFun and invFun to be globally defined functions and has source and target sets as extra fields.

Equations
Instances For
instance PEquiv.instFunLikeOption {α : Type u} {β : Type v} :
FunLike (α ≃. β) α ()
Equations
• PEquiv.instFunLikeOption = { coe := PEquiv.toFun, coe_injective' := }
@[simp]
theorem PEquiv.coe_mk {α : Type u} {β : Type v} (f₁ : α) (f₂ : β) (h : ∀ (a : α) (b : β), a f₂ b b f₁ a) :
{ toFun := f₁, invFun := f₂, inv := h } = f₁
theorem PEquiv.coe_mk_apply {α : Type u} {β : Type v} (f₁ : α) (f₂ : β) (h : ∀ (a : α) (b : β), a f₂ b b f₁ a) (x : α) :
{ toFun := f₁, invFun := f₂, inv := h } x = f₁ x
theorem PEquiv.ext {α : Type u} {β : Type v} {f : α ≃. β} {g : α ≃. β} (h : ∀ (x : α), f x = g x) :
f = g
theorem PEquiv.ext_iff {α : Type u} {β : Type v} {f : α ≃. β} {g : α ≃. β} :
f = g ∀ (x : α), f x = g x
def PEquiv.refl (α : Type u_1) :
α ≃. α

The identity map as a partial equivalence.

Equations
• = { toFun := some, invFun := some, inv := }
Instances For
def PEquiv.symm {α : Type u} {β : Type v} (f : α ≃. β) :
β ≃. α

The inverse partial equivalence.

Equations
• f.symm = { toFun := f.invFun, invFun := f.toFun, inv := }
Instances For
theorem PEquiv.mem_iff_mem {α : Type u} {β : Type v} (f : α ≃. β) {a : α} {b : β} :
a f.symm b b f a
theorem PEquiv.eq_some_iff {α : Type u} {β : Type v} (f : α ≃. β) {a : α} {b : β} :
f.symm b = some a f a = some b
def PEquiv.trans {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) :
α ≃. γ

Composition of partial equivalences f : α ≃. β and g : β ≃. γ.

Equations
• f.trans g = { toFun := fun (a : α) => (f a).bind g, invFun := fun (a : γ) => (g.symm a).bind f.symm, inv := }
Instances For
@[simp]
theorem PEquiv.refl_apply {α : Type u} (a : α) :
() a = some a
@[simp]
theorem PEquiv.symm_refl {α : Type u} :
().symm =
@[simp]
theorem PEquiv.symm_symm {α : Type u} {β : Type v} (f : α ≃. β) :
f.symm.symm = f
theorem PEquiv.symm_bijective {α : Type u} {β : Type v} :
Function.Bijective PEquiv.symm
theorem PEquiv.symm_injective {α : Type u} {β : Type v} :
Function.Injective PEquiv.symm
theorem PEquiv.trans_assoc {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} (f : α ≃. β) (g : β ≃. γ) (h : γ ≃. δ) :
(f.trans g).trans h = f.trans (g.trans h)
theorem PEquiv.mem_trans {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ) :
c (f.trans g) a bf a, c g b
theorem PEquiv.trans_eq_some {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ) :
(f.trans g) a = some c ∃ (b : β), f a = some b g b = some c
theorem PEquiv.trans_eq_none {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α) :
(f.trans g) a = none ∀ (b : β) (c : γ), bf a cg b
@[simp]
theorem PEquiv.refl_trans {α : Type u} {β : Type v} (f : α ≃. β) :
().trans f = f
@[simp]
theorem PEquiv.trans_refl {α : Type u} {β : Type v} (f : α ≃. β) :
f.trans () = f
theorem PEquiv.inj {α : Type u} {β : Type v} (f : α ≃. β) {a₁ : α} {a₂ : α} {b : β} (h₁ : b f a₁) (h₂ : b f a₂) :
a₁ = a₂
theorem PEquiv.injective_of_forall_ne_isSome {α : Type u} {β : Type v} (f : α ≃. β) (a₂ : α) (h : ∀ (a₁ : α), a₁ a₂(f a₁).isSome = true) :

If the domain of a PEquiv is α except a point, its forward direction is injective.

theorem PEquiv.injective_of_forall_isSome {α : Type u} {β : Type v} {f : α ≃. β} (h : ∀ (a : α), (f a).isSome = true) :

If the domain of a PEquiv is all of α, its forward direction is injective.

def PEquiv.ofSet {α : Type u} (s : Set α) [DecidablePred fun (x : α) => x s] :
α ≃. α

Creates a PEquiv that is the identity on s, and none outside of it.

Equations
• = { toFun := fun (a : α) => if a s then some a else none, invFun := fun (a : α) => if a s then some a else none, inv := }
Instances For
theorem PEquiv.mem_ofSet_self_iff {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x s] {a : α} :
a () a a s
theorem PEquiv.mem_ofSet_iff {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x s] {a : α} {b : α} :
a () b a = b a s
@[simp]
theorem PEquiv.ofSet_eq_some_iff {α : Type u} {s : Set α} :
∀ {x : DecidablePred fun (x : α) => x s} {a b : α}, () b = some a a = b a s
theorem PEquiv.ofSet_eq_some_self_iff {α : Type u} {s : Set α} :
∀ {x : DecidablePred fun (x : α) => x s} {a : α}, () a = some a a s
@[simp]
theorem PEquiv.ofSet_symm {α : Type u} (s : Set α) [DecidablePred fun (x : α) => x s] :
().symm =
@[simp]
theorem PEquiv.ofSet_univ {α : Type u} :
PEquiv.ofSet Set.univ =
@[simp]
theorem PEquiv.ofSet_eq_refl {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x s] :
s = Set.univ
theorem PEquiv.symm_trans_rev {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) :
(f.trans g).symm = g.symm.trans f.symm
theorem PEquiv.self_trans_symm {α : Type u} {β : Type v} (f : α ≃. β) :
f.trans f.symm = PEquiv.ofSet {a : α | (f a).isSome = true}
theorem PEquiv.symm_trans_self {α : Type u} {β : Type v} (f : α ≃. β) :
f.symm.trans f = PEquiv.ofSet {b : β | (f.symm b).isSome = true}
theorem PEquiv.trans_symm_eq_iff_forall_isSome {α : Type u} {β : Type v} {f : α ≃. β} :
f.trans f.symm = ∀ (a : α), (f a).isSome = true
instance PEquiv.instBotPEquiv {α : Type u} {β : Type v} :
Bot (α ≃. β)
Equations
• PEquiv.instBotPEquiv = { bot := { toFun := fun (x : α) => none, invFun := fun (x : β) => none, inv := } }
instance PEquiv.instInhabited {α : Type u} {β : Type v} :
Inhabited (α ≃. β)
Equations
• PEquiv.instInhabited = { default := }
@[simp]
theorem PEquiv.bot_apply {α : Type u} {β : Type v} (a : α) :
a = none
@[simp]
theorem PEquiv.symm_bot {α : Type u} {β : Type v} :
.symm =
@[simp]
theorem PEquiv.trans_bot {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) :
f.trans =
@[simp]
theorem PEquiv.bot_trans {α : Type u} {β : Type v} {γ : Type w} (f : β ≃. γ) :
.trans f =
theorem PEquiv.isSome_symm_get {α : Type u} {β : Type v} (f : α ≃. β) {a : α} (h : (f a).isSome = true) :
(f.symm ((f a).get h)).isSome = true
def PEquiv.single {α : Type u} {β : Type v} [] [] (a : α) (b : β) :
α ≃. β

Create a PEquiv which sends a to b and b to a, but is otherwise none.

Equations
• = { toFun := fun (x : α) => if x = a then some b else none, invFun := fun (x : β) => if x = b then some a else none, inv := }
Instances For
theorem PEquiv.mem_single {α : Type u} {β : Type v} [] [] (a : α) (b : β) :
b () a
theorem PEquiv.mem_single_iff {α : Type u} {β : Type v} [] [] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
b₁ (PEquiv.single a₂ b₂) a₁ a₁ = a₂ b₁ = b₂
@[simp]
theorem PEquiv.symm_single {α : Type u} {β : Type v} [] [] (a : α) (b : β) :
().symm =
@[simp]
theorem PEquiv.single_apply {α : Type u} {β : Type v} [] [] (a : α) (b : β) :
() a = some b
theorem PEquiv.single_apply_of_ne {α : Type u} {β : Type v} [] [] {a₁ : α} {a₂ : α} (h : a₁ a₂) (b : β) :
() a₂ = none
theorem PEquiv.single_trans_of_mem {α : Type u} {β : Type v} {γ : Type w} [] [] [] (a : α) {b : β} {c : γ} {f : β ≃. γ} (h : c f b) :
().trans f =
theorem PEquiv.trans_single_of_mem {α : Type u} {β : Type v} {γ : Type w} [] [] [] {a : α} {b : β} (c : γ) {f : α ≃. β} (h : b f a) :
f.trans () =
@[simp]
theorem PEquiv.single_trans_single {α : Type u} {β : Type v} {γ : Type w} [] [] [] (a : α) (b : β) (c : γ) :
().trans () =
@[simp]
theorem PEquiv.single_subsingleton_eq_refl {α : Type u} [] [] (a : α) (b : α) :
theorem PEquiv.trans_single_of_eq_none {β : Type v} {γ : Type w} {δ : Type x} [] [] {b : β} (c : γ) {f : δ ≃. β} (h : f.symm b = none) :
f.trans () =
theorem PEquiv.single_trans_of_eq_none {α : Type u} {β : Type v} {δ : Type x} [] [] (a : α) {b : β} {f : β ≃. δ} (h : f b = none) :
().trans f =
theorem PEquiv.single_trans_single_of_ne {α : Type u} {β : Type v} {γ : Type w} [] [] [] {b₁ : β} {b₂ : β} (h : b₁ b₂) (a : α) (c : γ) :
().trans () =
instance PEquiv.instPartialOrderPEquiv {α : Type u} {β : Type v} :
Equations
• PEquiv.instPartialOrderPEquiv =
theorem PEquiv.le_def {α : Type u} {β : Type v} {f : α ≃. β} {g : α ≃. β} :
f g ∀ (a : α), bf a, b g a
instance PEquiv.instOrderBot {α : Type u} {β : Type v} :
OrderBot (α ≃. β)
Equations
• PEquiv.instOrderBot = let __src := PEquiv.instBotPEquiv;
instance PEquiv.instSemilatticeInfOfDecidableEq {α : Type u} {β : Type v} [] [] :
Equations
• PEquiv.instSemilatticeInfOfDecidableEq = let __src := PEquiv.instPartialOrderPEquiv;
def Equiv.toPEquiv {α : Type u_1} {β : Type u_2} (f : α β) :
α ≃. β

Turns an Equiv into a PEquiv of the whole type.

Equations
• f.toPEquiv = { toFun := some f, invFun := some f.symm, inv := }
Instances For
@[simp]
theorem Equiv.toPEquiv_refl {α : Type u_1} :
().toPEquiv =
theorem Equiv.toPEquiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (g : β γ) :
(f.trans g).toPEquiv = f.toPEquiv.trans g.toPEquiv
theorem Equiv.toPEquiv_symm {α : Type u_1} {β : Type u_2} (f : α β) :
f.symm.toPEquiv = f.toPEquiv.symm
theorem Equiv.toPEquiv_apply {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
f.toPEquiv x = some (f x)