Completion of orbits #
Utilities to complete orbits of functions into local permutations.
Suppose we have a function f : α → α, and a set s on which f is injective.
We will construct a pair of functions toFun and invFun that agree with f and its inverse
on s, in such a way that forms a local permutation of α. In particular, consider the diagram
... → l 2 → l 1 → l 0 → s \ f '' s → ... → f '' s \ s → r 0 → r 1 → r 2 → ...
To fill in orbits of f, we construct a sequence of disjoint subsets of α called l i and r i
for each i : ℕ, where #(l i) = #(s \ f '' s) and #(r i) = #(f '' s \ s).
There are natural bijections along this diagram, mapping l (n + 1) to l n and r n to
r (n + 1), and there are also bijections f '' s \ s → r 0 and l 0 → s \ f '' s.
This yields a local permutation defined on s, f '' s \ s, the l i, and the r i.
Main declarations #
PartialPerm.complete: A completion of an injective function into a partial permutation.
theorem
PartialPerm.exists_sandbox_subset
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
:
def
PartialPerm.sandboxSubset
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
:
Set α
Creates a "sandbox" subset of t on which we will define an extension of f.
Equations
- PartialPerm.sandboxSubset hs ht = ⋯.choose
Instances For
theorem
PartialPerm.sandboxSubset_subset
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
:
PartialPerm.sandboxSubset hs ht ⊆ t
noncomputable def
PartialPerm.sandboxSubsetEquiv
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
:
Equations
- PartialPerm.sandboxSubsetEquiv hs ht = ⋯.some
Instances For
noncomputable def
PartialPerm.shiftRight
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
:
Considered an implementation detail; use lemmas about complete instead.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
PartialPerm.completeToFun
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
(a : α)
:
α
Considered an implementation detail; use lemmas about complete instead.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
PartialPerm.shiftLeft
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
:
Considered an implementation detail; use lemmas about complete instead.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
PartialPerm.completeInvFun
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
[Nonempty α]
(a : α)
:
α
Considered an implementation detail; use lemmas about complete instead.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
PartialPerm.completeDomain
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
:
Set α
The domain on which we will define the completion of a function to a local permutation.
Equations
- PartialPerm.completeDomain hs ht = s ∪ f '' s ∪ PartialPerm.sandboxSubset hs ht
Instances For
theorem
PartialPerm.completeToFun_domain
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
(x : α)
(h : x ∈ PartialPerm.completeDomain hs ht)
:
PartialPerm.completeToFun hs ht x ∈ PartialPerm.completeDomain hs ht
theorem
PartialPerm.completeInvFun_domain
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
[Nonempty α]
(x : α)
(h : x ∈ PartialPerm.completeDomain hs ht)
:
PartialPerm.completeInvFun hs ht x ∈ PartialPerm.completeDomain hs ht
theorem
PartialPerm.complete_left_inv
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
[Nonempty α]
(hst : Disjoint (s ∪ f '' s) t)
(hf : Set.InjOn f s)
(x : α)
(h : x ∈ PartialPerm.completeDomain hs ht)
:
PartialPerm.completeInvFun hs ht (PartialPerm.completeToFun hs ht x) = x
theorem
PartialPerm.complete_right_inv
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
[Nonempty α]
(hst : Disjoint (s ∪ f '' s) t)
(hf : Set.InjOn f s)
(x : α)
(h : x ∈ PartialPerm.completeDomain hs ht)
:
PartialPerm.completeToFun hs ht (PartialPerm.completeInvFun hs ht x) = x
noncomputable def
PartialPerm.complete
{α : Type u_1}
[Nonempty α]
(f : α → α)
(s : Set α)
(t : Set α)
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
(hst : Disjoint (s ∪ f '' s) t)
(hf : Set.InjOn f s)
:
Completes a function f on a domain s into a local permutation that agrees with f on s,
with domain contained in s ∪ (f '' s) ∪ t.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
PartialPerm.completeDomain_eq
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
[Nonempty α]
{hst : Disjoint (s ∪ f '' s) t}
{hf : Set.InjOn f s}
:
(PartialPerm.complete f s t hs ht hst hf).domain = PartialPerm.completeDomain hs ht
theorem
PartialPerm.mem_completeDomain_of_mem
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
(x : α)
(hx : x ∈ s)
:
x ∈ PartialPerm.completeDomain hs ht
theorem
PartialPerm.mem_completeDomain_of_mem_image
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
(x : α)
(hx : x ∈ f '' s)
:
x ∈ PartialPerm.completeDomain hs ht
theorem
PartialPerm.not_mem_sandbox_of_mem
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
(hst : Disjoint (s ∪ f '' s) t)
(x : α)
(hx : x ∈ s)
:
x ∉ PartialPerm.sandboxSubset hs ht
theorem
PartialPerm.not_mem_sandbox_of_mem_image
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
(hst : Disjoint (s ∪ f '' s) t)
(x : α)
(hx : x ∈ f '' s)
:
x ∉ PartialPerm.sandboxSubset hs ht
@[simp]
theorem
PartialPerm.complete_apply_eq
{α : Type u_1}
{f : α → α}
{s : Set α}
{t : Set α}
(hs : Cardinal.mk ↑(symmDiff s (f '' s)) ≤ Cardinal.mk ↑t)
(ht : Cardinal.aleph0 ≤ Cardinal.mk ↑t)
[Nonempty α]
{hst : Disjoint (s ∪ f '' s) t}
{hf : Set.InjOn f s}
(x : α)
(hx : x ∈ s)
:
(PartialPerm.complete f s t hs ht hst hf).toFun x = f x