data.pequiv

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 option.some b, then g b is option.some a.

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 semilattice_inf with an order_bot 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 local_equiv for a version that requires to_fun and inv_fun to be globally defined functions and has source and target sets as extra fields.

@[protected, instance]
def pequiv.has_coe_to_fun {α : Type u} {β : Type v} :
has_coe_to_fun ≃. β) (λ (_x : α ≃. β), α → option β)
Equations
@[simp]
theorem pequiv.coe_mk_apply {α : Type u} {β : Type v} (f₁ : α → ) (f₂ : β → ) (h : ∀ (a : α) (b : β), a f₂ b b f₁ a) (x : α) :
{to_fun := f₁, inv_fun := f₂, inv := h} x = f₁ x
@[ext]
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
@[protected]
def pequiv.refl (α : Type u_1) :
α ≃. α

The identity map as a partial equivalence.

Equations
@[protected]
def pequiv.symm {α : Type u} {β : Type v} (f : α ≃. β) :
β ≃. α

The inverse partial equivalence.

Equations
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
@[protected]
def pequiv.trans {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) :
α ≃. γ

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

Equations
@[simp]
theorem pequiv.refl_apply {α : Type u} (a : α) :
@[simp]
theorem pequiv.symm_refl {α : Type u} :
@[simp]
theorem pequiv.symm_symm {α : Type u} {β : Type v} (f : α ≃. β) :
f.symm.symm = f
theorem pequiv.symm_injective {α : Type u} {β : Type v} :
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 ∃ (b : β), b f 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 : γ), b f a c g b
@[simp]
theorem pequiv.refl_trans {α : Type u} {β : Type v} (f : α ≃. β) :
@[simp]
theorem pequiv.trans_refl {α : Type u} {β : Type v} (f : α ≃. β) :
@[protected]
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_is_some {α : Type u} {β : Type v} (f : α ≃. β) (a₂ : α) (h : ∀ (a₁ : α), a₁ a₂((f a₁).is_some)) :

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

theorem pequiv.injective_of_forall_is_some {α : Type u} {β : Type v} {f : α ≃. β} (h : ∀ (a : α), ((f a).is_some)) :

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

def pequiv.of_set {α : Type u} (s : set α) [decidable_pred (λ (_x : α), _x s)] :
α ≃. α

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

Equations
theorem pequiv.mem_of_set_self_iff {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x s)] {a : α} :
a a a s
theorem pequiv.mem_of_set_iff {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x s)] {a b : α} :
a b a = b a s
@[simp]
theorem pequiv.of_set_eq_some_iff {α : Type u} {s : set α} {h : decidable_pred (λ (_x : α), _x s)} {a b : α} :
b = some a a = b a s
@[simp]
theorem pequiv.of_set_eq_some_self_iff {α : Type u} {s : set α} {h : decidable_pred (λ (_x : α), _x s)} {a : α} :
a = some a a s
@[simp]
theorem pequiv.of_set_symm {α : Type u} (s : set α) [decidable_pred (λ (_x : α), _x s)] :
@[simp]
theorem pequiv.of_set_univ {α : Type u} :
@[simp]
theorem pequiv.of_set_eq_refl {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x s)] :
theorem pequiv.symm_trans_rev {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) :
theorem pequiv.self_trans_symm {α : Type u} {β : Type v} (f : α ≃. β) :
f.trans f.symm = pequiv.of_set {a : α | ((f a).is_some)}
theorem pequiv.symm_trans_self {α : Type u} {β : Type v} (f : α ≃. β) :
f.symm.trans f = pequiv.of_set {b : β | (((f.symm) b).is_some)}
theorem pequiv.trans_symm_eq_iff_forall_is_some {α : Type u} {β : Type v} {f : α ≃. β} :
f.trans f.symm = ∀ (a : α), ((f a).is_some)
@[protected, instance]
def pequiv.has_bot {α : Type u} {β : Type v} :
has_bot ≃. β)
Equations
@[protected, instance]
def pequiv.inhabited {α : Type u} {β : Type v} :
inhabited ≃. β)
Equations
@[simp]
theorem pequiv.bot_apply {α : Type u} {β : Type v} (a : α) :
@[simp]
theorem pequiv.symm_bot {α : Type u} {β : Type v} :
@[simp]
theorem pequiv.trans_bot {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) :
@[simp]
theorem pequiv.bot_trans {α : Type u} {β : Type v} {γ : Type w} (f : β ≃. γ) :
theorem pequiv.is_some_symm_get {α : Type u} {β : Type v} (f : α ≃. β) {a : α} (h : ((f a).is_some)) :
def pequiv.single {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] (a : α) (b : β) :
α ≃. β

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

Equations
theorem pequiv.mem_single {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] (a : α) (b : β) :
b b) a
theorem pequiv.mem_single_iff {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] (a₁ a₂ : α) (b₁ b₂ : β) :
b₁ b₂) a₁ a₁ = a₂ b₁ = b₂
@[simp]
theorem pequiv.symm_single {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] (a : α) (b : β) :
b).symm =
@[simp]
theorem pequiv.single_apply {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] (a : α) (b : β) :
b) a = some b
theorem pequiv.single_apply_of_ne {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] {a₁ a₂ : α} (h : a₁ a₂) (b : β) :
b) a₂ = none
theorem pequiv.single_trans_of_mem {α : Type u} {β : Type v} {γ : Type w} [decidable_eq α] [decidable_eq β] [decidable_eq γ] (a : α) {b : β} {c : γ} {f : β ≃. γ} (h : c f b) :
b).trans f =
theorem pequiv.trans_single_of_mem {α : Type u} {β : Type v} {γ : Type w} [decidable_eq α] [decidable_eq β] [decidable_eq γ] {a : α} {b : β} (c : γ) {f : α ≃. β} (h : b f a) :
f.trans c) =
@[simp]
theorem pequiv.single_trans_single {α : Type u} {β : Type v} {γ : Type w} [decidable_eq α] [decidable_eq β] [decidable_eq γ] (a : α) (b : β) (c : γ) :
b).trans c) =
@[simp]
theorem pequiv.single_subsingleton_eq_refl {α : Type u} [decidable_eq α] [subsingleton α] (a b : α) :
theorem pequiv.trans_single_of_eq_none {β : Type v} {γ : Type w} {δ : Type x} [decidable_eq β] [decidable_eq γ] {b : β} (c : γ) {f : δ ≃. β} (h : (f.symm) b = none) :
f.trans c) =
theorem pequiv.single_trans_of_eq_none {α : Type u} {β : Type v} {δ : Type x} [decidable_eq α] [decidable_eq β] (a : α) {b : β} {f : β ≃. δ} (h : f b = none) :
b).trans f =
theorem pequiv.single_trans_single_of_ne {α : Type u} {β : Type v} {γ : Type w} [decidable_eq α] [decidable_eq β] [decidable_eq γ] {b₁ b₂ : β} (h : b₁ b₂) (a : α) (c : γ) :
b₁).trans c) =
@[protected, instance]
def pequiv.partial_order {α : Type u} {β : Type v} :
Equations
theorem pequiv.le_def {α : Type u} {β : Type v} {f g : α ≃. β} :
f g ∀ (a : α) (b : β), b f ab g a
@[protected, instance]
def pequiv.order_bot {α : Type u} {β : Type v} :
order_bot ≃. β)
Equations
@[protected, instance]
def pequiv.semilattice_inf {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] :
Equations
def equiv.to_pequiv {α : Type u_1} {β : Type u_2} (f : α β) :
α ≃. β

Turns an equiv into a pequiv of the whole type.

Equations
@[simp]
theorem equiv.to_pequiv_refl {α : Type u_1} :
theorem equiv.to_pequiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (g : β γ) :
theorem equiv.to_pequiv_symm {α : Type u_1} {β : Type u_2} (f : α β) :
theorem equiv.to_pequiv_apply {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
(f.to_pequiv) x = some (f x)