mathlib documentation

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.

Main results #

pequiv.of_set: 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_is_some/injective_of_forall_is_some: If the domain of a pequiv is all of α (except possibly one point), its to_fun 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 semilattice_inf with an order_bot instance.

Tags #

pequiv, partial equivalence

structure pequiv (α : Type u) (β : Type v) :

Type (max u v)

to_fun : α → option β
inv_fun : β → option α
inv : ∀ (a : α) (b : β), a ∈ self.inv_fun b ↔ b ∈ self.to_fun a

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

pequiv.has_coe_to_fun = {coe := pequiv.to_fun β}

@[simp]

theorem pequiv.coe_mk_apply {α : Type u} {β : Type v} (f₁ : α → option β) (f₂ : β → option α) (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

pequiv.refl α = {to_fun := some α, inv_fun := some α, inv := _}

@[protected]

def pequiv.symm {α : Type u} {β : Type v} (f : α ≃. β) :

β ≃. α

The inverse partial equivalence.

Equations

f.symm = {to_fun := f.inv_fun, inv_fun := f.to_fun, inv := _}

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

f.trans g = {to_fun := λ (a : α), (⇑f a).bind ⇑g, inv_fun := λ (a : γ), (⇑(g.symm) a).bind ⇑(f.symm), inv := _}

@[simp]

theorem pequiv.refl_apply {α : Type u} (a : α) :

⇑(pequiv.refl α) a = some a

@[simp]

theorem pequiv.symm_refl {α : Type u} :

(pequiv.refl α).symm = pequiv.refl α

@[simp]

theorem pequiv.symm_symm {α : Type u} {β : Type v} (f : α ≃. β) :

f.symm.symm = f

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 ↔ ∃ (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 : α ≃. β) :

(pequiv.refl α).trans f = f

@[simp]

theorem pequiv.trans_refl {α : Type u} {β : Type v} (f : α ≃. β) :

f.trans (pequiv.refl β) = 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)) :

function.injective ⇑f

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)) :

function.injective ⇑f

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

pequiv.of_set s = {to_fun := λ (a : α), ite (a ∈ s) (some a) none, inv_fun := λ (a : α), ite (a ∈ s) (some a) none, inv := _}

theorem pequiv.mem_of_set_self_iff {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] {a : α} :

a ∈ ⇑(pequiv.of_set s) a ↔ a ∈ s

theorem pequiv.mem_of_set_iff {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] {a b : α} :

a ∈ ⇑(pequiv.of_set s) 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 : α} :

⇑(pequiv.of_set s) 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 : α} :

⇑(pequiv.of_set s) a = some a ↔ a ∈ s

@[simp]

theorem pequiv.of_set_symm {α : Type u} (s : set α) [decidable_pred (λ (_x : α), _x ∈ s)] :

(pequiv.of_set s).symm = pequiv.of_set s

@[simp]

theorem pequiv.of_set_univ {α : Type u} :

pequiv.of_set set.univ = pequiv.refl α

@[simp]

theorem pequiv.of_set_eq_refl {α : Type u} {s : set α} [decidable_pred (λ (_x : α), _x ∈ s)] :

pequiv.of_set s = pequiv.refl α ↔ 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.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 = pequiv.refl α ↔ ∀ (a : α), ↥((⇑f a).is_some)

@[protected, instance]

def pequiv.has_bot {α : Type u} {β : Type v} :

has_bot (α ≃. β)

Equations

pequiv.has_bot = {bot := {to_fun := λ (_x : α), none, inv_fun := λ (_x : β), none, inv := _}}

@[protected, instance]

def pequiv.inhabited {α : Type u} {β : Type v} :

inhabited (α ≃. β)

Equations

pequiv.inhabited = {default := ⊥}

@[simp]

theorem pequiv.bot_apply {α : Type u} {β : Type v} (a : α) :

⇑⊥ a = none

@[simp]

theorem pequiv.symm_bot {α : Type u} {β : Type v} :

@[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.is_some_symm_get {α : Type u} {β : Type v} (f : α ≃. β) {a : α} (h : ↥((⇑f a).is_some)) :

↥((⇑(f.symm) (option.get h)).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

pequiv.single a b = {to_fun := λ (x : α), ite (x = a) (some b) none, inv_fun := λ (x : β), ite (x = b) (some a) none, inv := _}

theorem pequiv.mem_single {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] (a : α) (b : β) :

b ∈ ⇑(pequiv.single a b) a

theorem pequiv.mem_single_iff {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] (a₁ a₂ : α) (b₁ b₂ : β) :

b₁ ∈ ⇑(pequiv.single a₂ b₂) a₁ ↔ a₁ = a₂ ∧ b₁ = b₂

@[simp]

theorem pequiv.symm_single {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] (a : α) (b : β) :

(pequiv.single a b).symm = pequiv.single b a

@[simp]

theorem pequiv.single_apply {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] (a : α) (b : β) :

⇑(pequiv.single a b) a = some b

theorem pequiv.single_apply_of_ne {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] {a₁ a₂ : α} (h : a₁ ≠ a₂) (b : β) :

⇑(pequiv.single a₁ 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) :

(pequiv.single a b).trans f = pequiv.single a c

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 (pequiv.single b c) = pequiv.single a c

@[simp]

theorem pequiv.single_trans_single {α : Type u} {β : Type v} {γ : Type w} [decidable_eq α] [decidable_eq β] [decidable_eq γ] (a : α) (b : β) (c : γ) :

(pequiv.single a b).trans (pequiv.single b c) = pequiv.single a c

@[simp]

theorem pequiv.single_subsingleton_eq_refl {α : Type u} [decidable_eq α] [subsingleton α] (a b : α) :

pequiv.single a b = pequiv.refl α

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 (pequiv.single b 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) :

(pequiv.single a 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 : γ) :

(pequiv.single a b₁).trans (pequiv.single b₂ c) = ⊥

@[protected, instance]

def pequiv.partial_order {α : Type u} {β : Type v} :

partial_order (α ≃. β)

Equations

pequiv.partial_order = {le := λ (f g : α ≃. β), ∀ (a : α) (b : β), b ∈ ⇑f a → b ∈ ⇑g a, lt := preorder.lt._default (λ (f g : α ≃. β), ∀ (a : α) (b : β), b ∈ ⇑f a → b ∈ ⇑g a), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

theorem pequiv.le_def {α : Type u} {β : Type v} {f g : α ≃. β} :

f ≤ g ↔ ∀ (a : α) (b : β), b ∈ ⇑f a → b ∈ ⇑g a

@[protected, instance]

def pequiv.order_bot {α : Type u} {β : Type v} :

order_bot (α ≃. β)

Equations

pequiv.order_bot = {bot := ⊥, bot_le := _}

@[protected, instance]

def pequiv.semilattice_inf {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] :

semilattice_inf (α ≃. β)

Equations

pequiv.semilattice_inf = {inf := λ (f g : α ≃. β), {to_fun := λ (a : α), ite (⇑f a = ⇑g a) (⇑f a) none, inv_fun := λ (b : β), ite (⇑(f.symm) b = ⇑(g.symm) b) (⇑(f.symm) b) none, inv := _}, le := partial_order.le pequiv.partial_order, lt := partial_order.lt pequiv.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

def equiv.to_pequiv {α : Type u_1} {β : Type u_2} (f : α ≃ β) :

α ≃. β

Turns an equiv into a pequiv of the whole type.

Equations

f.to_pequiv = {to_fun := some ∘ ⇑f, inv_fun := some ∘ ⇑(f.symm), inv := _}

@[simp]

theorem equiv.to_pequiv_refl {α : Type u_1} :

(equiv.refl α).to_pequiv = pequiv.refl α

theorem equiv.to_pequiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ≃ β) (g : β ≃ γ) :

(f.trans g).to_pequiv = f.to_pequiv.trans g.to_pequiv

theorem equiv.to_pequiv_symm {α : Type u_1} {β : Type u_2} (f : α ≃ β) :

f.symm.to_pequiv = f.to_pequiv.symm

theorem equiv.to_pequiv_apply {α : Type u_1} {β : Type u_2} (f : α ≃ β) (x : α) :

⇑(f.to_pequiv) x = some (⇑f x)