Theory Paradoxical_Decomposition
theory Paradoxical_Decomposition
imports BT_Prelim
begin
section ‹Group actions on a set›
text ‹
An action of a (carrier) group @{term G} on a set @{term X} is a function
@{term "act :: 'g ⇒ 'a ⇒ 'a"} respecting the unit and multiplication
on @{term X}. We do not fix the group structure here; rather, we record
the algebraic laws that an action must satisfy. Concrete instances will
be given in later theories (the action of ‹F⇩2› on itself by
left translation; the action of ‹SO(3)› on ‹S⇧2›).
›
locale group_action =
fixes carrier :: "'g set"
and unit :: "'g"
and mult :: "'g ⇒ 'g ⇒ 'g" (infixl ‹⋅› 70)
and act :: "'g ⇒ 'a ⇒ 'a"
and ground :: "'a set"
assumes unit_carrier [simp]: "unit ∈ carrier"
and mult_closed [intro]: "⟦g ∈ carrier; h ∈ carrier⟧ ⟹ g ⋅ h ∈ carrier"
and act_closed [intro]: "⟦g ∈ carrier; x ∈ ground⟧ ⟹ act g x ∈ ground"
and act_unit [simp]: "x ∈ ground ⟹ act unit x = x"
and act_mult: "⟦g ∈ carrier; h ∈ carrier; x ∈ ground⟧
⟹ act (g ⋅ h) x = act g (act h x)"
context group_action
begin
definition orbit :: "'a ⇒ 'a set" where
"orbit x = {y. ∃g ∈ carrier. y = act g x}"
definition image_set :: "'g ⇒ 'a set ⇒ 'a set" where
"image_set g A = act g ` A"
lemma image_set_unit:
assumes "A ⊆ ground"
shows "image_set unit A = A"
using assms unfolding image_set_def by force
lemma orbit_self:
assumes "x ∈ ground"
shows "x ∈ orbit x"
using assms by (simp add: orbit_def) (metis act_unit unit_carrier)
end
section ‹Paradoxical decomposition›
text ‹
A subset @{term X} of the underlying set of a group action is
∗‹paradoxical› when it admits two finite collections of
pairwise disjoint pieces, all contained in @{term X}, such that each
collection can be translated (by group elements) so that the resulting
∗‹disjoint› union is the whole of @{term X}.
This is the standard Banach-Tarski definition. We will instantiate it
twice: once for ‹F⇩2› acting on itself, and once for the
rotation group acting on ‹S⇧2› (and ultimately the ball).
›
context group_action
begin
definition paradoxical :: "'a set ⇒ bool" where
"paradoxical X ⟷
(∃P Q :: 'a set list. ∃gP gQ :: 'g list.
length P = length gP ∧ length Q = length gQ ∧
set gP ⊆ carrier ∧ set gQ ⊆ carrier ∧
pairwise_disjoint (P @ Q) ∧
pairwise_disjoint (map2 image_set gP P) ∧
pairwise_disjoint (map2 image_set gQ Q) ∧
(⋃i<length P. P ! i) ∪ (⋃i<length Q. Q ! i) ⊆ X ∧
X = (⋃i<length P. image_set (gP ! i) (P ! i)) ∧
X = (⋃i<length Q. image_set (gQ ! i) (Q ! i)))"
text ‹
A specialised constructor for the most common case: each of @{term P}
and @{term Q} has exactly two pieces. This matches the ‹F⇩2›
decomposition (split into the ‹a› / ‹a⇧-⇧1› classes and
the ‹b› / ‹b⇧-⇧1› classes).
›
lemma paradoxical_two_two:
assumes "p1 ∈ carrier" "p2 ∈ carrier" "q1 ∈ carrier" "q2 ∈ carrier"
and disj_P12: "P1 ∩ P2 = {}"
and disj_Q12: "Q1 ∩ Q2 = {}"
and disj_PQ: "(P1 ∪ P2) ∩ (Q1 ∪ Q2) = {}"
and sub: "P1 ∪ P2 ∪ Q1 ∪ Q2 ⊆ X"
and disj_imgP: "image_set p1 P1 ∩ image_set p2 P2 = {}"
and disj_imgQ: "image_set q1 Q1 ∩ image_set q2 Q2 = {}"
and cover_P: "X = image_set p1 P1 ∪ image_set p2 P2"
and cover_Q: "X = image_set q1 Q1 ∪ image_set q2 Q2"
shows "paradoxical X"
proof -
let ?P = "[P1, P2]" and ?Q = "[Q1, Q2]"
let ?gP = "[p1, p2]" and ?gQ = "[q1, q2]"
have lens: "length ?P = length ?gP" "length ?Q = length ?gQ" by simp_all
have closed: "set ?gP ⊆ carrier" "set ?gQ ⊆ carrier"
using assms(1-4) by auto
have disj_all: "pairwise_disjoint (?P @ ?Q)"
using disj_P12 disj_Q12 disj_PQ
by (auto simp: pairwise_disjoint_def nth_Cons' nth_append Int_commute Int_Un_distrib)
have map2_P: "map2 image_set ?gP ?P = [image_set p1 P1, image_set p2 P2]" by simp
have map2_Q: "map2 image_set ?gQ ?Q = [image_set q1 Q1, image_set q2 Q2]" by simp
have disj_map_P: "pairwise_disjoint (map2 image_set ?gP ?P)"
using disj_imgP unfolding map2_P
by (auto simp: pairwise_disjoint_def nth_Cons' Int_commute)
have disj_map_Q: "pairwise_disjoint (map2 image_set ?gQ ?Q)"
using disj_imgQ unfolding map2_Q
by (auto simp: pairwise_disjoint_def nth_Cons' Int_commute)
have sub_un: "(⋃i<length ?P. ?P ! i) ∪ (⋃i<length ?Q. ?Q ! i) ⊆ X"
using sub by (auto simp: lessThan_Suc)
have cov_P': "X = (⋃i<length ?P. image_set (?gP ! i) (?P ! i))"
using cover_P by (auto simp: lessThan_Suc)
have cov_Q': "X = (⋃i<length ?Q. image_set (?gQ ! i) (?Q ! i))"
using cover_Q by (auto simp: lessThan_Suc)
show ?thesis
unfolding paradoxical_def
using lens closed disj_all disj_map_P disj_map_Q sub_un cov_P' cov_Q'
by blast
qed
text ‹
With the finite-list convention used above, the empty set is
paradoxical: take both families of pieces to be empty. The two
translated indexed unions are then both the empty union, hence both
equal to ‹{}›. This degenerate case is harmless in the later
non-empty geometric applications, but recording it keeps the abstract
definition honest about empty indexed unions.
›
lemma paradoxical_empty: "paradoxical {}"
unfolding paradoxical_def
by (intro exI[where x="[]"])
(auto simp: pairwise_disjoint_def image_set_def)
end
section ‹Equidecomposability›
text ‹
Two subsets @{term X} and @{term Y} are ∗‹equidecomposable›
under a group action when they admit congruent partitions: the
‹i›-th piece of @{term X} maps onto the ‹i›-th piece of
@{term Y} via some group element.
›
context group_action
begin
definition equidecomposable :: "'a set ⇒ 'a set ⇒ bool" where
"equidecomposable X Y ⟷
(∃P Q :: 'a set list. ∃gs :: 'g list.
length P = length Q ∧ length P = length gs ∧
set gs ⊆ carrier ∧
pairwise_disjoint P ∧ pairwise_disjoint Q ∧
X = (⋃i<length P. P ! i) ∧
Y = (⋃i<length Q. Q ! i) ∧
(∀i < length P. Q ! i = image_set (gs ! i) (P ! i)))"
text ‹
The main development uses this relation only as background notation:
the sphere and ball arguments below work directly with explicit finite
lists of pieces and transformations, so the needed partition data is
visible at each transfer step.
›
end
end