Documentation

Mathlib.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 β→ Option β and the reverse function g : β → Option α→ Option α, with the condition that if f a is some b, then g b is some a.

Main results #

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≤ 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 (maxuv)
  • The underlying partial function of a PEquiv

    toFun : αOption β
  • The partial inverse of toFun

    invFun : βOption α
  • invFun is the partial inverse of toFun

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

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

Instances For

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

    Equations
    instance PEquiv.instFunLikePEquivOption {α : Type u} {β : Type v} :
    FunLike (α ≃. β) α fun x => Option β
    Equations
    • PEquiv.instFunLikePEquivOption = { coe := PEquiv.toFun, coe_injective' := (_ : ∀ ⦃a₁ a₂ : α ≃. β⦄, a₁.toFun = a₂.toFuna₁ = a₂) }
    @[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
    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 ↑(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
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem PEquiv.refl_apply {α : Type u} (a : α) :
    ↑(PEquiv.refl α) a = some a
    @[simp]
    theorem PEquiv.symm_symm {α : Type u} {β : Type v} (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 : γ ≃. δ) :
    theorem PEquiv.mem_trans {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ) :
    c ↑(PEquiv.trans f g) a b, 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 : α ≃. β) :
    @[simp]
    theorem PEquiv.trans_refl {α : Type u} {β : Type v} (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) :

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

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

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

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

    Equations
    • One or more equations did not get rendered due to their size.
    theorem PEquiv.mem_ofSet_self_iff {α : Type u} {s : Set α} [inst : DecidablePred fun x => x s] {a : α} :
    a ↑(PEquiv.ofSet s) a a s
    theorem PEquiv.mem_ofSet_iff {α : Type u} {s : Set α} [inst : 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 α) [inst : DecidablePred fun x => x s] :
    @[simp]
    theorem PEquiv.ofSet_univ {α : Type u} :
    @[simp]
    theorem PEquiv.ofSet_eq_refl {α : Type u} {s : Set α} [inst : 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 : β ≃. γ) :
    theorem PEquiv.self_trans_symm {α : Type u} {β : Type v} (f : α ≃. β) :
    theorem PEquiv.symm_trans_self {α : Type u} {β : Type v} (f : α ≃. β) :
    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 := (_ : ∀ (a : α) (a_1 : β), a none a_1 none) } }
    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} :
    @[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.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} [inst : DecidableEq α] [inst : DecidableEq β] (a : α) (b : β) :
    α ≃. β

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

    Equations
    • One or more equations did not get rendered due to their size.
    theorem PEquiv.mem_single {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] (a : α) (b : β) :
    b ↑(PEquiv.single a b) a
    theorem PEquiv.mem_single_iff {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
    b₁ ↑(PEquiv.single a₂ b₂) a₁ a₁ = a₂ b₁ = b₂
    @[simp]
    theorem PEquiv.symm_single {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] (a : α) (b : β) :
    @[simp]
    theorem PEquiv.single_apply {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] (a : α) (b : β) :
    ↑(PEquiv.single a b) a = some b
    theorem PEquiv.single_apply_of_ne {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : 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} [inst : DecidableEq α] [inst : DecidableEq β] [inst : DecidableEq γ] (a : α) {b : β} {c : γ} {f : β ≃. γ} (h : c f b) :
    theorem PEquiv.trans_single_of_mem {α : Type u} {β : Type v} {γ : Type w} [inst : DecidableEq α] [inst : DecidableEq β] [inst : DecidableEq γ] {a : α} {b : β} (c : γ) {f : α ≃. β} (h : b f a) :
    @[simp]
    theorem PEquiv.single_trans_single {α : Type u} {β : Type v} {γ : Type w} [inst : DecidableEq α] [inst : DecidableEq β] [inst : DecidableEq γ] (a : α) (b : β) (c : γ) :
    @[simp]
    theorem PEquiv.single_subsingleton_eq_refl {α : Type u} [inst : DecidableEq α] [inst : Subsingleton α] (a : α) (b : α) :
    theorem PEquiv.trans_single_of_eq_none {β : Type v} {γ : Type w} {δ : Type x} [inst : DecidableEq β] [inst : DecidableEq γ] {b : β} (c : γ) {f : δ ≃. β} (h : ↑(PEquiv.symm f) b = none) :
    theorem PEquiv.single_trans_of_eq_none {α : Type u} {β : Type v} {δ : Type x} [inst : DecidableEq α] [inst : DecidableEq β] (a : α) {b : β} {f : β ≃. δ} (h : f b = none) :
    theorem PEquiv.single_trans_single_of_ne {α : Type u} {β : Type v} {γ : Type w} [inst : DecidableEq α] [inst : DecidableEq β] [inst : DecidableEq γ] {b₁ : β} {b₂ : β} (h : b₁ b₂) (a : α) (c : γ) :
    instance PEquiv.instPartialOrderPEquiv {α : Type u} {β : Type v} :
    Equations
    theorem PEquiv.le_def {α : Type u} {β : Type v} {f : α ≃. β} {g : α ≃. β} :
    f g ∀ (a : α) (b : β), b f ab g a
    Equations
    • PEquiv.instOrderBotPEquivToLEToPreorderInstPartialOrderPEquiv = let src := PEquiv.instBotPEquiv; OrderBot.mk (_ : ∀ (x : α ≃. β) (x_1 : α) (x_2 : β), x_2 x_1x_2 x x_1)
    instance PEquiv.instSemilatticeInfPEquiv {α : Type u} {β : Type v} [inst : DecidableEq α] [inst : DecidableEq β] :
    Equations
    • One or more equations did not get rendered due to their size.
    def Equiv.toPEquiv {α : Type u_1} {β : Type u_2} (f : α β) :
    α ≃. β

    Turns an Equiv into a PEquiv of the whole type.

    Equations
    theorem Equiv.toPEquiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (g : β γ) :
    theorem Equiv.toPEquiv_apply {α : Type u_1} {β : Type u_2} (f : α β) (x : α) :
    ↑(Equiv.toPEquiv f) x = some (f x)