-
Notifications
You must be signed in to change notification settings - Fork 298
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(data/pequiv): partial equivalences (#1206)
* feat(data/pequiv): partial equivalences * Update src/data/pequiv.lean Co-Authored-By: Floris van Doorn <fpvdoorn@gmail.com> * use notation
- Loading branch information
1 parent
03e6d0e
commit dcf0130
Showing
1 changed file
with
327 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,327 @@ | ||
/- | ||
Copyright (c) 2019 Chris Hughes. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Chris Hughes | ||
-/ | ||
|
||
import data.equiv.basic data.set.lattice tactic.tauto | ||
|
||
universes u v w x | ||
|
||
/-- A `pequiv` is a partial equivalence, a representation of a bijection between a subset | ||
of `α` and a subset of `β` -/ | ||
structure pequiv (α : Type u) (β : Type v) := | ||
(to_fun : α → option β) | ||
(inv_fun : β → option α) | ||
(inv : ∀ (a : α) (b : β), a ∈ inv_fun b ↔ b ∈ to_fun a) | ||
|
||
infixr ` ≃. `:25 := pequiv | ||
|
||
namespace pequiv | ||
variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} | ||
open function option | ||
|
||
instance : has_coe_to_fun (α ≃. β) := ⟨_, to_fun⟩ | ||
|
||
@[simp] lemma coe_mk_apply (f₁ : α → option β) (f₂ : β → option α) (h) (x : α) : | ||
(pequiv.mk f₁ f₂ h : α → option β) x = f₁ x := rfl | ||
|
||
@[extensionality] lemma ext : ∀ {f g : α ≃. β} (h : ∀ x, f x = g x), f = g | ||
| ⟨f₁, f₂, hf⟩ ⟨g₁, g₂, hg⟩ h := | ||
have h : f₁ = g₁, from funext h, | ||
have ∀ b, f₂ b = g₂ b, | ||
begin | ||
subst h, | ||
assume b, | ||
have hf := λ a, hf a b, | ||
have hg := λ a, hg a b, | ||
cases h : g₂ b with a, | ||
{ simp only [h, option.not_mem_none, false_iff] at hg, | ||
simp only [hg, iff_false] at hf, | ||
rwa [option.eq_none_iff_forall_not_mem] }, | ||
{ rw [← option.mem_def, hf, ← hg, h, option.mem_def] } | ||
end, | ||
by simp [*, funext_iff] | ||
|
||
lemma ext_iff {f g : α ≃. β} : f = g ↔ ∀ x, f x = g x := | ||
⟨congr_fun ∘ congr_arg _, ext⟩ | ||
|
||
@[refl] protected def refl (α : Type*) : α ≃. α := | ||
{ to_fun := some, | ||
inv_fun := some, | ||
inv := λ _ _, eq_comm } | ||
|
||
@[symm] protected def symm (f : α ≃. β) : β ≃. α := | ||
{ to_fun := f.2, | ||
inv_fun := f.1, | ||
inv := λ _ _, (f.inv _ _).symm } | ||
|
||
lemma mem_iff_mem (f : α ≃. β) : ∀ {a : α} {b : β}, a ∈ f.symm b ↔ b ∈ f a := f.3 | ||
|
||
lemma eq_some_iff (f : α ≃. β) : ∀ {a : α} {b : β}, f.symm b = some a ↔ f a = some b := f.3 | ||
|
||
@[trans] protected def trans (f : α ≃. β) (g : β ≃. γ) : pequiv α γ := | ||
{ to_fun := λ a, (f a).bind g, | ||
inv_fun := λ a, (g.symm a).bind f.symm, | ||
inv := λ a b, by simp [*, and.comm, eq_some_iff f, eq_some_iff g] at * } | ||
|
||
@[simp] lemma refl_apply (a : α) : pequiv.refl α a = some a := rfl | ||
|
||
@[simp] lemma symm_refl : (pequiv.refl α).symm = pequiv.refl α := rfl | ||
|
||
@[simp] lemma symm_refl_apply (a : α) : (pequiv.refl α).symm a = some a := rfl | ||
|
||
@[simp] lemma symm_symm (f : α ≃. β) : f.symm.symm = f := by cases f; refl | ||
|
||
@[simp] lemma symm_symm_apply (f : α ≃. β) (a : α) : f.symm.symm a = f a := | ||
by rw symm_symm | ||
|
||
lemma symm_injective : function.injective (@pequiv.symm α β) := | ||
injective_of_has_left_inverse ⟨_, symm_symm⟩ | ||
|
||
lemma trans_assoc (f : α ≃. β) (g : β ≃. γ) (h : γ ≃. δ) : | ||
(f.trans g).trans h = f.trans (g.trans h) := | ||
ext (λ _, option.bind_assoc _ _ _) | ||
|
||
lemma mem_trans (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ) : | ||
c ∈ f.trans g a ↔ ∃ b, b ∈ f a ∧ c ∈ g b := option.bind_eq_some' | ||
|
||
lemma trans_eq_some (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ) : | ||
f.trans g a = some c ↔ ∃ b, f a = some b ∧ g b = some c := option.bind_eq_some' | ||
|
||
lemma trans_eq_none (f : α ≃. β) (g : β ≃. γ) (a : α) : | ||
f.trans g a = none ↔ (∀ b c, b ∉ f a ∨ c ∉ g b) := | ||
by simp only [eq_none_iff_forall_not_mem, mem_trans]; push_neg; tauto | ||
|
||
@[simp] lemma refl_trans (f : α ≃. β) : (pequiv.refl α).trans f = f := | ||
by ext; dsimp [pequiv.trans]; refl | ||
|
||
@[simp] lemma trans_refl (f : α ≃. β) : f.trans (pequiv.refl β) = f := | ||
by ext; dsimp [pequiv.trans]; simp | ||
|
||
@[simp] lemma refl_trans_apply (f : α ≃. β) (a : α) : (pequiv.refl α).trans f a = f a := | ||
by rw refl_trans | ||
|
||
@[simp] lemma trans_refl_apply (f : α ≃. β) (a : α) : f.trans (pequiv.refl β) a = f a := | ||
by rw trans_refl | ||
|
||
protected lemma inj (f : α ≃. β) {a₁ a₂ : α} {b : β} (h₁ : b ∈ f a₁) (h₂ : b ∈ f a₂) : a₁ = a₂ := | ||
by rw ← mem_iff_mem at *; cases h : f.symm b; simp * at * | ||
|
||
lemma injective_of_forall_ne_is_some (f : α ≃. β) (a₂ : α) | ||
(h : ∀ (a₁ : α), a₁ ≠ a₂ → is_some (f a₁)) : injective f := | ||
injective_of_has_left_inverse | ||
⟨λ b, option.rec_on b a₂ (λ b', option.rec_on (f.symm b') a₂ id), | ||
λ x, begin | ||
classical, | ||
cases hfx : f x, | ||
{ have : x = a₂, from not_imp_comm.1 (h x) (hfx.symm ▸ by simp), simp [this] }, | ||
{ simp only [hfx], rw [(eq_some_iff f).2 hfx], refl } | ||
end⟩ | ||
|
||
lemma injective_of_forall_is_some {f : α ≃. β} | ||
(h : ∀ (a : α), is_some (f a)) : injective f := | ||
(classical.em (nonempty α)).elim | ||
(λ hn, injective_of_forall_ne_is_some f (classical.choice hn) | ||
(λ a _, h a)) | ||
(λ hn x, (hn ⟨x⟩).elim) | ||
|
||
section of_set | ||
variables (s : set α) [decidable_pred s] | ||
|
||
def of_set (s : set α) [decidable_pred s] : α ≃. α := | ||
{ to_fun := λ a, if a ∈ s then some a else none, | ||
inv_fun := λ a, if a ∈ s then some a else none, | ||
inv := λ a b, by split_ifs; finish [eq_comm] } | ||
|
||
lemma mem_of_set_self_iff {s : set α} [decidable_pred s] {a : α} : a ∈ of_set s a ↔ a ∈ s := | ||
by dsimp [of_set]; split_ifs; simp * | ||
|
||
lemma mem_of_set_iff {s : set α} [decidable_pred s] {a b : α} : a ∈ of_set s b ↔ a = b ∧ a ∈ s := | ||
by dsimp [of_set]; split_ifs; split; finish | ||
|
||
@[simp] lemma of_set_eq_some_self_iff {s : set α} {h : decidable_pred s} {a : α} : | ||
of_set s a = some a ↔ a ∈ s := mem_of_set_self_iff | ||
|
||
@[simp] lemma of_set_eq_some_iff {s : set α} {h : decidable_pred s} {a b : α} : | ||
of_set s b = some a ↔ a = b ∧ a ∈ s := mem_of_set_iff | ||
|
||
@[simp] lemma of_set_symm : (of_set s).symm = of_set s := rfl | ||
|
||
@[simp] lemma of_set_univ : of_set set.univ = pequiv.refl α := | ||
by ext; dsimp [of_set]; simp [eq_comm] | ||
|
||
@[simp] lemma of_set_eq_refl {s : set α} [decidable_pred s] : | ||
of_set s = pequiv.refl α ↔ s = set.univ := | ||
⟨λ h, begin | ||
rw [set.eq_univ_iff_forall], | ||
intro, | ||
rw [← mem_of_set_self_iff, h], | ||
exact rfl | ||
end, λ h, by simp only [of_set_univ.symm, h]; congr⟩ | ||
|
||
end of_set | ||
|
||
lemma symm_trans_rev (f : α ≃. β) (g : β ≃. γ) : (f.trans g).symm = g.symm.trans f.symm := rfl | ||
|
||
lemma trans_symm (f : α ≃. β) : f.trans f.symm = of_set {a | (f a).is_some} := | ||
begin | ||
ext, | ||
dsimp [pequiv.trans], | ||
simp only [eq_some_iff f, option.is_some_iff_exists, option.mem_def, bind_eq_some', of_set_eq_some_iff], | ||
split, | ||
{ rintros ⟨b, hb₁, hb₂⟩, | ||
exact ⟨pequiv.inj _ hb₂ hb₁, b, hb₂⟩ }, | ||
{ simp {contextual := tt} } | ||
end | ||
|
||
lemma symm_trans (f : α ≃. β) : f.symm.trans f = of_set {b | (f.symm b).is_some} := | ||
symm_injective $ by simp [symm_trans_rev, trans_symm, -symm_symm] | ||
|
||
lemma trans_symm_eq_iff_forall_is_some {f : α ≃. β} : | ||
f.trans f.symm = pequiv.refl α ↔ ∀ a, is_some (f a) := | ||
by rw [trans_symm, of_set_eq_refl, set.eq_univ_iff_forall]; refl | ||
|
||
instance : lattice.has_bot (α ≃. β) := | ||
⟨{ to_fun := λ _, none, | ||
inv_fun := λ _, none, | ||
inv := by simp }⟩ | ||
|
||
@[simp] lemma bot_apply (a : α) : (⊥ : α ≃. β) a = none := rfl | ||
|
||
@[simp] lemma symm_bot : (⊥ : α ≃. β).symm = ⊥ := rfl | ||
|
||
@[simp] lemma trans_bot (f : α ≃. β) : f.trans (⊥ : β ≃. γ) = ⊥ := | ||
by ext; dsimp [pequiv.trans]; simp | ||
|
||
@[simp] lemma bot_trans (f : β ≃. γ) : (⊥ : α ≃. β).trans f = ⊥ := | ||
by ext; dsimp [pequiv.trans]; simp | ||
|
||
lemma is_some_symm_get (f : α ≃. β) {a : α} (h : is_some (f a)) : | ||
is_some (f.symm (option.get h)) := | ||
is_some_iff_exists.2 ⟨a, by rw [f.eq_some_iff, some_get]⟩ | ||
|
||
section single | ||
variables [decidable_eq α] [decidable_eq β] [decidable_eq γ] | ||
|
||
def single (a : α) (b : β) : α ≃. β := | ||
{ to_fun := λ x, if x = a then some b else none, | ||
inv_fun := λ x, if x = b then some a else none, | ||
inv := λ _ _, by simp; split_ifs; cc } | ||
|
||
lemma mem_single (a : α) (b : β) : b ∈ single a b a := if_pos rfl | ||
|
||
lemma mem_single_iff (a₁ a₂ : α) (b₁ b₂ : β) : b₁ ∈ single a₂ b₂ a₁ ↔ a₁ = a₂ ∧ b₁ = b₂ := | ||
by dsimp [single]; split_ifs; simp [*, eq_comm] | ||
|
||
@[simp] lemma symm_single (a : α) (b : β) : (single a b).symm = single b a := rfl | ||
|
||
@[simp] lemma single_apply (a : α) (b : β) : single a b a = some b := if_pos rfl | ||
|
||
lemma single_apply_of_ne {a₁ a₂ : α} (h : a₁ ≠ a₂) (b : β) : single a₁ b a₂ = none := if_neg h.symm | ||
|
||
lemma single_trans_of_mem (a : α) {b : β} {c : γ} {f : β ≃. γ} (h : c ∈ f b) : | ||
(single a b).trans f = single a c := | ||
begin | ||
ext, | ||
dsimp [single, pequiv.trans], | ||
split_ifs; simp * at * | ||
end | ||
|
||
lemma trans_single_of_mem {a : α} {b : β} (c : γ) {f : α ≃. β} (h : b ∈ f a) : | ||
f.trans (single b c) = single a c := | ||
symm_injective $ single_trans_of_mem _ ((mem_iff_mem f).2 h) | ||
|
||
@[simp] lemma single_trans_single (a : α) (b : β) (c : γ) : (single a b).trans (single b c) = single a c := | ||
single_trans_of_mem _ (mem_single _ _) | ||
|
||
@[simp] lemma single_subsingleton_eq_refl [subsingleton α] (a b : α) : single a b = pequiv.refl α := | ||
begin | ||
ext i j, | ||
dsimp [single], | ||
rw [if_pos (subsingleton.elim i a), subsingleton.elim i j, subsingleton.elim b j] | ||
end | ||
|
||
lemma trans_single_of_eq_none {b : β} (c : γ) {f : α ≃. β} (h : f.symm b = none) : | ||
f.trans (single b c) = ⊥ := | ||
begin | ||
ext, | ||
simp only [eq_none_iff_forall_not_mem, option.mem_def, f.eq_some_iff] at h, | ||
dsimp [pequiv.trans, single], | ||
simp, | ||
intros, | ||
split_ifs; | ||
simp * at * | ||
end | ||
|
||
lemma single_trans_of_eq_none (a : α) {b : β} {f : β ≃. γ} (h : f b = none) : | ||
(single a b).trans f = ⊥ := | ||
symm_injective $ trans_single_of_eq_none _ h | ||
|
||
lemma single_trans_single_of_ne {b₁ b₂ : β} (h : b₁ ≠ b₂) (a : α) (c : γ) : | ||
(single a b₁).trans (single b₂ c) = ⊥ := | ||
single_trans_of_eq_none _ (single_apply_of_ne h.symm _) | ||
|
||
end single | ||
|
||
section order | ||
open lattice | ||
|
||
instance : partial_order (α ≃. β) := | ||
{ le := λ f g, ∀ (a : α) (b : β), b ∈ f a → b ∈ g a, | ||
le_refl := λ _ _ _, id, | ||
le_trans := λ f g h fg gh a b, (gh a b) ∘ (fg a b), | ||
le_antisymm := λ f g fg gf, ext begin | ||
assume a, | ||
cases h : g a with b, | ||
{ exact eq_none_iff_forall_not_mem.2 | ||
(λ b hb, option.not_mem_none b $ h ▸ fg a b hb) }, | ||
{ exact gf _ _ h } | ||
end } | ||
|
||
lemma le_def {f g : α ≃. β} : f ≤ g ↔ (∀ (a : α) (b : β), b ∈ f a → b ∈ g a) := iff.rfl | ||
|
||
instance : order_bot (α ≃. β) := | ||
{ bot_le := λ _ _ _ h, (not_mem_none _ h).elim, | ||
..pequiv.partial_order, | ||
..pequiv.lattice.has_bot } | ||
|
||
instance [decidable_eq α] [decidable_eq β] : semilattice_inf_bot (α ≃. β) := | ||
{ inf := λ f g, | ||
{ to_fun := λ a, if f a = g a then f a else none, | ||
inv_fun := λ b, if f.symm b = g.symm b then f.symm b else none, | ||
inv := λ a b, begin | ||
have := @mem_iff_mem _ _ f a b, | ||
have := @mem_iff_mem _ _ g a b, | ||
split_ifs; finish | ||
end }, | ||
inf_le_left := λ _ _ _ _, by simp; split_ifs; cc, | ||
inf_le_right := λ _ _ _ _, by simp; split_ifs; cc, | ||
le_inf := λ f g h fg gh a b, begin | ||
have := fg a b, | ||
have := gh a b, | ||
simp [le_def], | ||
split_ifs; finish | ||
end, | ||
..pequiv.lattice.order_bot } | ||
|
||
end order | ||
|
||
end pequiv | ||
|
||
namespace equiv | ||
variables {α : Type*} {β : Type*} {γ : Type*} | ||
|
||
def to_pequiv (f : α ≃ β) : α ≃. β := | ||
{ to_fun := some ∘ f, | ||
inv_fun := some ∘ f.symm, | ||
inv := by simp [equiv.eq_symm_apply, eq_comm] } | ||
|
||
@[simp] lemma to_pequiv_refl : (equiv.refl α).to_pequiv = pequiv.refl α := rfl | ||
|
||
lemma to_pequiv_trans (f : α ≃ β) (g : β ≃ γ) : (f.trans g).to_pequiv = | ||
f.to_pequiv.trans g.to_pequiv := rfl | ||
|
||
lemma to_pequiv_symm (f : α ≃ β) : f.symm.to_pequiv = f.to_pequiv.symm := rfl | ||
|
||
end equiv |