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 : α → Option β

  The underlying partial function of a PEquiv

• invFun : β → Option α

  The partial inverse of toFun

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

  invFun is the partial inverse of toFun

def «term_≃._» : Lean.TrailingParserDescr

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

• «term_≃._» = Lean.ParserDescr.trailingNode `term_≃._ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃. ") (Lean.ParserDescr.cat `term 25))

instance PEquiv.instFunLikePEquivOption {α : Type u} {β : Type v} : FunLike (α ≃. β) α (Option β)

Equations

• PEquiv.instFunLikePEquivOption = { coe := PEquiv.toFun, coe_injective' := ⋯ }

@[simp]

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

• PEquiv.refl α = { toFun := some, invFun := some, inv := ⋯ }

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

The inverse partial equivalence.

Equations

• PEquiv.symm f = { toFun := f.invFun, invFun := f.toFun, inv := ⋯ }

theorem PEquiv.mem_iff_mem {α : Type u} {β : Type v} (f : α ≃. β) {a : α} {b : β} : a ∈ (PEquiv.symm f) b ↔ b ∈ f a

theorem PEquiv.eq_some_iff {α : Type u} {β : Type v} (f : α ≃. β) {a : α} {b : β} : (PEquiv.symm f) 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

• PEquiv.trans f g = { toFun := fun (a : α) => Option.bind (f a) ⇑g, invFun := fun (a : γ) => Option.bind ((PEquiv.symm g) a) ⇑(PEquiv.symm f), inv := ⋯ }

@[simp]

theorem PEquiv.refl_apply {α : Type u} (a : α) : (PEquiv.refl α) a = some a

@[simp]

theorem PEquiv.symm_refl {α : Type u} : PEquiv.symm (PEquiv.refl α) = PEquiv.refl α

@[simp]

theorem PEquiv.symm_symm {α : Type u} {β : Type v} (f : α ≃. β) : PEquiv.symm (PEquiv.symm f) = 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 : γ ≃. δ) : PEquiv.trans (PEquiv.trans f g) h = PEquiv.trans f (PEquiv.trans g h)

theorem PEquiv.mem_trans {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ) : c ∈ (PEquiv.trans f g) a ↔ ∃ b ∈ f a, c ∈ g b

theorem PEquiv.trans_eq_some {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ) : (PEquiv.trans f 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 : α) : (PEquiv.trans f g) a = none ↔ ∀ (b : β) (c : γ), b ∉ f a ∨ c ∉ g b

@[simp]

theorem PEquiv.refl_trans {α : Type u} {β : Type v} (f : α ≃. β) : PEquiv.trans (PEquiv.refl α) f = f

@[simp]

theorem PEquiv.trans_refl {α : Type u} {β : Type v} (f : α ≃. β) : PEquiv.trans f (PEquiv.refl β) = 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₂ → Option.isSome (f a₁) = true) : Function.Injective ⇑f

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 : α), Option.isSome (f a) = true) : Function.Injective ⇑f

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

• PEquiv.ofSet s = { toFun := fun (a : α) => if a ∈ s then some a else none, invFun := fun (a : α) => if a ∈ s then some a else none, inv := ⋯ }

theorem PEquiv.mem_ofSet_self_iff {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {a : α} : a ∈ (PEquiv.ofSet s) a ↔ a ∈ s

theorem PEquiv.mem_ofSet_iff {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] {a : α} {b : α} : a ∈ (PEquiv.ofSet s) b ↔ a = b ∧ a ∈ s

@[simp]

theorem PEquiv.ofSet_eq_some_iff {α : Type u} {s : Set α} : ∀ {x : DecidablePred fun (x : α) => x ∈ s} {a b : α}, (PEquiv.ofSet s) 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 : α}, (PEquiv.ofSet s) a = some a ↔ a ∈ s

@[simp]

theorem PEquiv.ofSet_symm {α : Type u} (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : PEquiv.symm (PEquiv.ofSet s) = PEquiv.ofSet s

@[simp]

theorem PEquiv.ofSet_univ {α : Type u} : PEquiv.ofSet Set.univ = PEquiv.refl α

@[simp]

theorem PEquiv.ofSet_eq_refl {α : Type u} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] : PEquiv.ofSet s = PEquiv.refl α ↔ s = Set.univ

theorem PEquiv.symm_trans_rev {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) : PEquiv.symm (PEquiv.trans f g) = PEquiv.trans (PEquiv.symm g) (PEquiv.symm f)

theorem PEquiv.self_trans_symm {α : Type u} {β : Type v} (f : α ≃. β) : PEquiv.trans f (PEquiv.symm f) = PEquiv.ofSet {a : α | Option.isSome (f a) = true}

theorem PEquiv.symm_trans_self {α : Type u} {β : Type v} (f : α ≃. β) : PEquiv.trans (PEquiv.symm f) f = PEquiv.ofSet {b : β | Option.isSome ((PEquiv.symm f) b) = true}

theorem PEquiv.trans_symm_eq_iff_forall_isSome {α : Type u} {β : Type v} {f : α ≃. β} : PEquiv.trans f (PEquiv.symm f) = PEquiv.refl α ↔ ∀ (a : α), Option.isSome (f a) = true

instance PEquiv.instBotPEquiv {α : Type u} {β : Type v} : Bot (α ≃. β)

Equations

• PEquiv.instBotPEquiv = { bot := { toFun := fun (x : α) => none, invFun := fun (x : β) => none, inv := ⋯ } }

instance PEquiv.instInhabitedPEquiv {α : Type u} {β : Type v} : Inhabited (α ≃. β)

Equations

• PEquiv.instInhabitedPEquiv = { default := ⊥ }

@[simp]

theorem PEquiv.bot_apply {α : Type u} {β : Type v} (a : α) : ⊥ a = none

@[simp]

theorem PEquiv.symm_bot {α : Type u} {β : Type v} : PEquiv.symm ⊥ = ⊥

@[simp]

theorem PEquiv.trans_bot {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) : PEquiv.trans f ⊥ = ⊥

@[simp]

theorem PEquiv.bot_trans {α : Type u} {β : Type v} {γ : Type w} (f : β ≃. γ) : PEquiv.trans ⊥ f = ⊥

theorem PEquiv.isSome_symm_get {α : Type u} {β : Type v} (f : α ≃. β) {a : α} (h : Option.isSome (f a) = true) : Option.isSome ((PEquiv.symm f) (Option.get (f a) h)) = true

def PEquiv.single {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (a : α) (b : β) : α ≃. β

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

Equations

• PEquiv.single a b = { toFun := fun (x : α) => if x = a then some b else none, invFun := fun (x : β) => if x = b then some a else none, inv := ⋯ }

theorem PEquiv.mem_single {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (a : α) (b : β) : b ∈ (PEquiv.single a b) a

theorem PEquiv.mem_single_iff {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) : b₁ ∈ (PEquiv.single a₂ b₂) a₁ ↔ a₁ = a₂ ∧ b₁ = b₂

@[simp]

theorem PEquiv.symm_single {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (a : α) (b : β) : PEquiv.symm (PEquiv.single a b) = PEquiv.single b a

@[simp]

theorem PEquiv.single_apply {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (a : α) (b : β) : (PEquiv.single a b) a = some b

theorem PEquiv.single_apply_of_ne {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {a₁ : α} {a₂ : α} (h : a₁ ≠ a₂) (b : β) : (PEquiv.single a₁ b) a₂ = none

theorem PEquiv.single_trans_of_mem {α : Type u} {β : Type v} {γ : Type w} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (a : α) {b : β} {c : γ} {f : β ≃. γ} (h : c ∈ f b) : PEquiv.trans (PEquiv.single a b) f = PEquiv.single a c

theorem PEquiv.trans_single_of_mem {α : Type u} {β : Type v} {γ : Type w} [DecidableEq α] [DecidableEq β] [DecidableEq γ] {a : α} {b : β} (c : γ) {f : α ≃. β} (h : b ∈ f a) : PEquiv.trans f (PEquiv.single b c) = PEquiv.single a c

@[simp]

theorem PEquiv.single_trans_single {α : Type u} {β : Type v} {γ : Type w} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (a : α) (b : β) (c : γ) : PEquiv.trans (PEquiv.single a b) (PEquiv.single b c) = PEquiv.single a c

@[simp]

theorem PEquiv.single_subsingleton_eq_refl {α : Type u} [DecidableEq α] [Subsingleton α] (a : α) (b : α) : PEquiv.single a b = PEquiv.refl α

theorem PEquiv.trans_single_of_eq_none {β : Type v} {γ : Type w} {δ : Type x} [DecidableEq β] [DecidableEq γ] {b : β} (c : γ) {f : δ ≃. β} (h : (PEquiv.symm f) b = none) : PEquiv.trans f (PEquiv.single b c) = ⊥

theorem PEquiv.single_trans_of_eq_none {α : Type u} {β : Type v} {δ : Type x} [DecidableEq α] [DecidableEq β] (a : α) {b : β} {f : β ≃. δ} (h : f b = none) : PEquiv.trans (PEquiv.single a b) f = ⊥

theorem PEquiv.single_trans_single_of_ne {α : Type u} {β : Type v} {γ : Type w} [DecidableEq α] [DecidableEq β] [DecidableEq γ] {b₁ : β} {b₂ : β} (h : b₁ ≠ b₂) (a : α) (c : γ) : PEquiv.trans (PEquiv.single a b₁) (PEquiv.single b₂ c) = ⊥

instance PEquiv.instPartialOrderPEquiv {α : Type u} {β : Type v} : PartialOrder (α ≃. β)

Equations

• PEquiv.instPartialOrderPEquiv = PartialOrder.mk ⋯

theorem PEquiv.le_def {α : Type u} {β : Type v} {f : α ≃. β} {g : α ≃. β} : f ≤ g ↔ ∀ (a : α), ∀ b ∈ f a, b ∈ g a

instance PEquiv.instOrderBotPEquivToLEToPreorderInstPartialOrderPEquiv {α : Type u} {β : Type v} : OrderBot (α ≃. β)

Equations

• PEquiv.instOrderBotPEquivToLEToPreorderInstPartialOrderPEquiv = let __src := PEquiv.instBotPEquiv; OrderBot.mk ⋯

instance PEquiv.instSemilatticeInfPEquiv {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : SemilatticeInf (α ≃. β)

Equations

• PEquiv.instSemilatticeInfPEquiv = let __src := PEquiv.instPartialOrderPEquiv; SemilatticeInf.mk ⋯ ⋯ ⋯

def Equiv.toPEquiv {α : Type u_1} {β : Type u_2} (f : α ≃ β) : α ≃. β

Turns an Equiv into a PEquiv of the whole type.

Equations

• Equiv.toPEquiv f = { toFun := some ∘ ⇑f, invFun := some ∘ ⇑f.symm, inv := ⋯ }

@[simp]

theorem Equiv.toPEquiv_refl {α : Type u_1} : Equiv.toPEquiv (Equiv.refl α) = PEquiv.refl α

theorem Equiv.toPEquiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ≃ β) (g : β ≃ γ) : Equiv.toPEquiv (f.trans g) = PEquiv.trans (Equiv.toPEquiv f) (Equiv.toPEquiv g)

theorem Equiv.toPEquiv_symm {α : Type u_1} {β : Type u_2} (f : α ≃ β) : Equiv.toPEquiv f.symm = PEquiv.symm (Equiv.toPEquiv f)

theorem Equiv.toPEquiv_apply {α : Type u_1} {β : Type u_2} (f : α ≃ β) (x : α) : (Equiv.toPEquiv f) x = some (f x)