Grace/Cumulus/Algebra/Group/Paradox.g17

Open in Workbench Download source

Imports

FreeGroup · Action · Set.ChoiceFunctions

Declarations

Source

1-- Paradoxical decompositions: two subsets of a set with a group action are2-- equidecomposable when finitely many pairwise disjoint pieces of the one3-- are carried by group elements onto pairwise disjoint pieces of the4-- other; a set is paradoxical when two disjoint subsets of it are each5-- equidecomposable with it. Equidecomposability is an equivalence relation6-- respecting disjoint unions, and the transfer theorem: a set with a free7-- action of a group containing the free group on two generators is8-- paradoxical, by choosing one point in each orbit9-- Part of Cumulus, the Grace17 mathematics library.10-- Copyright (c) 2026 Grant Passmore.11-- Released under the Apache License 2.0. See LICENSE in the repository root.12-- Authors: Grant Passmore1314module Grace.Cumulus.Algebra.Group.Paradox15import FreeGroup16import Action17import Set.ChoiceFunctions1819-- The image of a set S of points under a group element g, and the image20-- of a set M of points under a set H of group elements.21def translate (act X g S : Set) : Set := { y ∈ X | ∃ x ∈ S, y = act(g, x) }22def sweep (act X H M : Set) : Set :=23  { y ∈ X | ∃ g ∈ H, ∃ x ∈ M, y = act(g, x) }2425-- A decomposition is a finite family F of pairs (S, g) of a piece and a26-- group element. Pieces(A, F) says the pieces are pairwise disjoint and27-- cover A; moved(act, X, p) is the image of the piece of p under its28-- element, and MovedPieces(act, X, B, F) says the moved pieces are29-- pairwise disjoint and cover B.30def moved (act X p : Set) : Set := translate(act, X, snd(p), fst(p))3132predicate Pieces (A F : Set) :=33  (∀ p ∈ F, fst(p) ⊆ A) ∧ (∀ x ∈ A, ∃ p ∈ F, x ∈ fst(p)) ∧34  (∀ p q ∈ F, p ≠ q → Disjoint(fst(p), fst(q)))3536predicate MovedPieces (act X B F : Set) :=37  (∀ p ∈ F, moved(act, X, p) ⊆ B) ∧ (∀ y ∈ B, ∃ p ∈ F, y ∈ moved(act, X, p)) ∧38  (∀ p q ∈ F, p ≠ q → Disjoint(moved(act, X, p), moved(act, X, q)))3940-- A and B are equidecomposable under the action act of G on X; X is41-- paradoxical when two disjoint subsets are each equidecomposable with X;42-- the action is free when every stabilizer is trivial.43predicate Equidecomposable (act G X A B : Set) :=44  ∃ F, Finite(F) ∧ F ⊆ 𝒫(X) × Group.carrier(G) ∧ Pieces(A, F) ∧45    MovedPieces(act, X, B, F)4647predicate Paradoxical (act G X : Set) :=48  ∃ A, ∃ B, A ⊆ X ∧ B ⊆ X ∧ Disjoint(A, B) ∧49    Equidecomposable(act, G, X, A, X) ∧ Equidecomposable(act, G, X, B, X)5051predicate FreeAction (act G X : Set) :=52  ∀ x ∈ X, stabilizer(act, G, X, x) = {Group.one(G)}5354-- One chosen point in each orbit, through a choice function c on the55-- subsets of X.56def representatives (act G X c : Set) : Set := { c(O) | O ∈ orbits(act, G, X) }5758theorem moved.value (act X S g : Set)59  shows moved(act, X, (S, g)) = translate(act, X, g, S)60proof61  simp [moved, fst.pair, snd.pair]6263theorem moved.unfold (act X p : Set)64  shows moved(act, X, p) = translate(act, X, snd(p), fst(p))65proof66  simp [moved]6768theorem translate.subset (act X g S : Set)69  shows translate(act, X, g, S) ⊆ X70proof71  intros y hy72  have parts := translate.membership.forward with hy73  exact parts.left7475theorem sweep.subset (act X H M : Set)76  shows sweep(act, X, H, M) ⊆ X77proof78  intros y hy79  have parts := sweep.membership.forward with hy80  exact parts.left8182-- Translating by different elements or actions agreeing on S gives the83-- same image.84theorem translate.congr (act act2 X g h S : Set)85  requires agree : ∀ x ∈ S, act(g, x) = act2(h, x)86  shows translate(act, X, g, S) = translate(act2, X, h, S)87proof88  ext y89  constructor90  . intro hy91    obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with hy92    have same := agree with x, hx93    rw same at equal94    exact translate.membership.backward with ⟨yIn, x, hx, equal⟩95  . intro hy96    obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with hy97    have same := agree with x, hx98    rw ← same at equal99    exact translate.membership.backward with ⟨yIn, x, hx, equal⟩100101theorem translate.monotone (act X g S T : Set)102  requires subset : S ⊆ T103  shows translate(act, X, g, S) ⊆ translate(act, X, g, T)104proof105  intros y hy106  obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with hy107  exact translate.membership.backward with ⟨yIn, x, (subset with x, hx), equal⟩108109theorem translate.union2 (act X g S T : Set)110  shows translate(act, X, g, S ∪ T) = translate(act, X, g, S) ∪ translate(act, X, g, T)111proof112  ext y113  constructor114  . intro hy115    obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with hy116    have split := union2.membership.forward with hx117    cases split with inS | inT118    . apply union2.membership.backward119      left120      exact translate.membership.backward with ⟨yIn, x, inS, equal⟩121    . apply union2.membership.backward122      right123      exact translate.membership.backward with ⟨yIn, x, inT, equal⟩124  . intro hy125    have split := union2.membership.forward with hy126    cases split with inS | inT127    . obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with inS128      have member := union2.subset_left at S, T with x, hx129      exact translate.membership.backward with ⟨yIn, x, member, equal⟩130    . obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with inT131      have member := union2.subset_right at S, T with x, hx132      exact translate.membership.backward with ⟨yIn, x, member, equal⟩133134section TranslateLaws135variable (act G X : Set)136hypothesis action : act : G ↷ X137138instance translate.act_mem (g : G) (S x : Set)139  requires bounded : S ⊆ X140  requires hx : x ∈ S141  shows g ·ₐ x ∈ translate(act, X, g, S)142proof143  have xIn := bounded with x, hx144  have moved : g ·ₐ x ∈ X := Action.act_mem with *145  exact translate.membership.backward with ⟨moved, x, hx, rfl⟩146147theorem translate.one (S : Set)148  requires bounded : S ⊆ X149  shows translate(act, X, G.one, S) = S150proof151  have group := Action.group with action152  ext y153  constructor154  . intro hy155    obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with hy156    have xIn := bounded with x, hx157    have fixed : G.one ·ₐ x = x := one_act with *158    rw [equal, fixed]159    exact hx160  . intro hy161    have yIn := bounded with y, hy162    have fixed : G.one ·ₐ y = y := one_act with *163    have member : G.one ·ₐ y ∈ translate(act, X, G.one, S) := translate.act_mem with *164    rwa fixed at member165166theorem translate.mul (g h : G) (S : Set)167  requires bounded : S ⊆ X168  shows translate(act, X, g * h, S) = translate(act, X, g, translate(act, X, h, S))169proof170  have group := Action.group with action171  have inner := translate.subset at act, X, h, S172  ext y173  constructor174  . intro hy175    obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with hy176    have xIn := bounded with x, hx177    have merged : (g * h) ·ₐ x = g ·ₐ h ·ₐ x := mul_act with *178    have step : h ·ₐ x ∈ translate(act, X, h, S) := translate.act_mem with *179    have member : g ·ₐ h ·ₐ x ∈ translate(act, X, g, translate(act, X, h, S)) :=180      translate.act_mem with *181    rw [equal, merged]182    exact member183  . intro hy184    obtain ⟨yIn, z, hz, equal⟩ := translate.membership.forward with hy185    obtain ⟨zIn, x, hx, zEq⟩ := translate.membership.forward with hz186    have xIn := bounded with x, hx187    have merged : (g * h) ·ₐ x = g ·ₐ h ·ₐ x := mul_act with *188    rw [equal, zEq, ← merged]189    exact translate.act_mem with *190191theorem translate.inv_translate (g : G) (S : Set)192  requires bounded : S ⊆ X193  shows translate(act, X, g⁻¹, translate(act, X, g, S)) = S194proof195  have group := Action.group with action196  have merged := translate.mul at act, G, X, g⁻¹, g, S with *197  rw [← merged, Group.inv_mul]198  exact translate.one with *199200theorem translate.translate_inv (g : G) (S : Set)201  requires bounded : S ⊆ X202  shows translate(act, X, g, translate(act, X, g⁻¹, S)) = S203proof204  have group := Action.group with action205  have merged := translate.mul at act, G, X, g, g⁻¹, S with *206  rw [← merged, Group.mul_inv]207  exact translate.one with *208209theorem translate.mem_iff (g : G) (S y : Set)210  requires bounded : S ⊆ X211  requires hy : y ∈ X212  shows y ∈ translate(act, X, g, S) ↔ g⁻¹ ·ₐ y ∈ S213proof214  have group := Action.group with action215  constructor216  . intro member217    obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with member218    have xIn := bounded with x, hx219    have back : g⁻¹ ·ₐ g ·ₐ x = x := inv_act_cancel with *220    rw [equal, back]221    exact hx222  . intro member223    have moved : g ·ₐ g⁻¹ ·ₐ y ∈ translate(act, X, g, S) := translate.act_mem with *224    have cancel : g ·ₐ g⁻¹ ·ₐ y = y := act_inv_cancel with *225    rwa cancel at moved226227theorem translate.disjoint (g : G) (S T : Set)228  requires boundedS : S ⊆ X229  requires boundedT : T ⊆ X230  requires disjoint : Disjoint(S, T)231  shows Disjoint(translate(act, X, g, S), translate(act, X, g, T))232proof233  have group := Action.group with action234  have apart := Disjoint.iff.forward with disjoint235  apply Disjoint.iff.backward236  intros y hyS hyT237  have yIn := translate.subset at act, X, g, S with y, hyS238  have inS := translate.mem_iff.forward with action, boundedS, yIn, hyS239  have inT := translate.mem_iff.forward with action, boundedT, yIn, hyT240  exact apart with g⁻¹ ·ₐ y, inS, inT241242theorem translate.intersection (g : G) (S T : Set)243  requires boundedS : S ⊆ X244  requires boundedT : T ⊆ X245  shows translate(act, X, g, S ∩ T) = translate(act, X, g, S) ∩ translate(act, X, g, T)246proof247  have group := Action.group with action248  have boundedST := Subset.transitive with (intersection.subset_left at S, T), boundedS249  ext y250  constructor251  . intro hy252    have yIn := translate.subset at act, X, g, S ∩ T with y, hy253    have inST := translate.mem_iff.forward with action, boundedST, yIn, hy254    obtain ⟨inS, inT⟩ := intersection.membership.forward with inST255    have left := translate.mem_iff.backward with action, boundedS, yIn, inS256    have right := translate.mem_iff.backward with action, boundedT, yIn, inT257    exact intersection.membership.backward with ⟨left, right⟩258  . intro hy259    obtain ⟨hyS, hyT⟩ := intersection.membership.forward with hy260    have yIn := translate.subset at act, X, g, S with y, hyS261    have inS := translate.mem_iff.forward with action, boundedS, yIn, hyS262    have inT := translate.mem_iff.forward with action, boundedT, yIn, hyT263    have inST := intersection.membership.backward at264      S, T, g⁻¹ ·ₐ y with ⟨inS, inT⟩265    exact translate.mem_iff.backward with action, boundedST, yIn, inST266267end TranslateLaws268269-- A decomposition with two pieces.270theorem Equidecomposable.of_two_pieces (act G X A B S T g h : Set)271  requires action : act : G ↷ X272  requires hg : g ∈ Group.carrier(G)273  requires hh : h ∈ Group.carrier(G)274  requires boundedS : S ⊆ X275  requires boundedT : T ⊆ X276  requires disjoint : Disjoint(S, T)277  requires cover : S ∪ T = A278  requires disjointImages : Disjoint(translate(act, X, g, S), translate(act, X, h, T))279  requires coverImages : translate(act, X, g, S) ∪ translate(act, X, h, T) = B280  shows Equidecomposable(act, G, X, A, B)281proof282  have first : (S, g) ∈ 𝒫(X) × G.carrier :=283    product.pair with (powerset.membership_iff.backward with boundedS), hg284  have second : (T, h) ∈ 𝒫(X) × G.carrier :=285    product.pair with (powerset.membership_iff.backward with boundedT), hh286  have movedS := moved.value at act, X, S, g287  have movedT := moved.value at act, X, T, h288  have members : ∀ p ∈ insert((S, g), {(T, h)}), p = (S, g) ∨ p = (T, h)289    intros p hp290    have split := insert.membership.forward with hp291    cases split with left | right292    . left293      exact left294    . right295      exact singleton.membership.forward with right296  have firstIn : (S, g) ∈ insert((S, g), {(T, h)}) := insert.self297  have secondIn : (T, h) ∈ insert((S, g), {(T, h)}) :=298    insert.contains with (singleton.self at (T, h))299  witness insert((S, g), {(T, h)})300  refine ⟨?_, ?_, ?_, ?_⟩301  . exact Finite.insert with (Finite.singleton at (T, h))302  . intros p hp303    have split := members with p, hp304    cases split with left | right305    . rw left306      exact first307    . rw right308      exact second309  . refine ⟨?_, ?_, ?_⟩310    . intros p hp311      have split := members with p, hp312      cases split with left | right313      . rw [left, fst.pair, ← cover]314        exact union2.subset_left at S, T315      . rw [right, fst.pair, ← cover]316        exact union2.subset_right at S, T317    . intros x hx318      rw ← cover at hx319      have split := union2.membership.forward with hx320      cases split with inS | inT321      . witness (S, g)322        rw fst.pair323        exact ⟨firstIn, inS⟩324      . witness (T, h)325        rw fst.pair326        exact ⟨secondIn, inT⟩327    . intros p hp q hq different328      have splitP := members with p, hp329      have splitQ := members with q, hq330      cases splitP with pFirst | pSecond331      . cases splitQ with qFirst | qSecond332        . exfalso333          apply different334          rw [pFirst, qFirst]335          rfl336        . rw [pFirst, qSecond, fst.pair, fst.pair]337          exact disjoint338      . cases splitQ with qFirst | qSecond339        . rw [pSecond, qFirst, fst.pair, fst.pair]340          exact Disjoint.symmetric with disjoint341        . exfalso342          apply different343          rw [pSecond, qSecond]344          rfl345  . refine ⟨?_, ?_, ?_⟩346    . intros p hp347      have split := members with p, hp348      cases split with left | right349      . rw [left, movedS, ← coverImages]350        exact union2.subset_left at translate(act, X, g, S), translate(act, X, h, T)351      . rw [right, movedT, ← coverImages]352        exact union2.subset_right at translate(act, X, g, S), translate(act, X, h, T)353    . intros y hy354      rw ← coverImages at hy355      have split := union2.membership.forward with hy356      cases split with inS | inT357      . witness (S, g)358        rw movedS359        exact ⟨firstIn, inS⟩360      . witness (T, h)361        rw movedT362        exact ⟨secondIn, inT⟩363    . intros p hp q hq different364      have splitP := members with p, hp365      have splitQ := members with q, hq366      cases splitP with pFirst | pSecond367      . cases splitQ with qFirst | qSecond368        . exfalso369          apply different370          rw [pFirst, qFirst]371          rfl372        . rw [pFirst, qSecond, movedS, movedT]373          exact disjointImages374      . cases splitQ with qFirst | qSecond375        . rw [pSecond, qFirst, movedS, movedT]376          exact Disjoint.symmetric with disjointImages377        . exfalso378          apply different379          rw [pSecond, qSecond]380          rfl381382section Equivalence383variable (act G X : Set)384hypothesis action : act : G ↷ X385386-- Equidecomposability is reflexive.387theorem Equidecomposable.reflexive (A : Set)388  requires bounded : A ⊆ X389  shows Equidecomposable(act, G, X, A, A)390proof391  have group := Action.group with action392  have unitIn : G.one ∈ G := Group.one_mem with *393  have pair : (A, G.one) ∈ 𝒫(X) × G.carrier :=394    product.pair with (powerset.membership_iff.backward with bounded), unitIn395  have movedA := moved.value at act, X, A, G.one396  have fixed := translate.one with action, bounded397  rw fixed at movedA398  have members : ∀ p ∈ {(A, G.one)}, p = (A, G.one)399    intros p hp400    exact singleton.membership.forward with hp401  witness {(A, G.one)}402  refine ⟨Finite.singleton at (A, G.one), ?_, ?_, ?_⟩403  . intros p hp404    have equal := members with p, hp405    rw equal406    exact pair407  . refine ⟨?_, ?_, ?_⟩408    . intros p hp409      have equal := members with p, hp410      rw [equal, fst.pair]411      exact Subset.reflexive at A412    . intros x hx413      witness (A, G.one)414      rw fst.pair415      exact ⟨singleton.self, hx⟩416    . intros p hp q hq different417      have equalP := members with p, hp418      have equalQ := members with q, hq419      exfalso420      apply different421      rw [equalP, equalQ]422      rfl423  . refine ⟨?_, ?_, ?_⟩424    . intros p hp425      have equal := members with p, hp426      rw [equal, movedA]427      exact Subset.reflexive at A428    . intros x hx429      witness (A, G.one)430      rw movedA431      exact ⟨singleton.self, hx⟩432    . intros p hp q hq different433      have equalP := members with p, hp434      have equalQ := members with q, hq435      exfalso436      apply different437      rw [equalP, equalQ]438      rfl439440end Equivalence441442-- Reindexing: a finite family F of indices, each mapped by f to a piece443-- and an element, with the piece and moved-piece conditions read through f.444theorem Equidecomposable.of_reindex (act G X A B D F f : Set)445  requires function : f : D → 𝒫(X) × Group.carrier(G)446  requires finite : Finite(F)447  requires bounded : F ⊆ D448  requires piecesBounded : ∀ p ∈ F, fst(f(p)) ⊆ A449  requires piecesCover : ∀ x ∈ A, ∃ p ∈ F, x ∈ fst(f(p))450  requires piecesDisjoint : ∀ p q ∈ F, p ≠ q → Disjoint(fst(f(p)), fst(f(q)))451  requires movedBounded : ∀ p ∈ F, moved(act, X, f(p)) ⊆ B452  requires movedCover : ∀ y ∈ B, ∃ p ∈ F, y ∈ moved(act, X, f(p))453  requires movedDisjoint : ∀ p q ∈ F, p ≠ q → Disjoint(moved(act, X, f(p)), moved(act, X, f(q)))454  shows Equidecomposable(act, G, X, A, B)455proof456  have finiteImage := Finite.function_image with function, finite, bounded457  have boundedImage := functionImage.subset at f, F, 𝒫(X) × Group.carrier(G)458  have members : ∀ q ∈ functionImage(f, F, 𝒫(X) × Group.carrier(G)), ∃ p ∈ F, q = f(p)459    intros q hq460    obtain ⟨qIn, p, hp, equal⟩ := functionImage.membership.forward with hq461    exact ⟨p, hp, equal⟩462  have images : ∀ p ∈ F, f(p) ∈ functionImage(f, F, 𝒫(X) × Group.carrier(G))463    intros p hp464    have pIn := bounded with p, hp465    have qIn := FunctionBetween.apply_closed with function, pIn466    exact functionImage.membership.backward with ⟨qIn, p, hp, rfl⟩467  have distinct : ∀ p ∈ F, ∀ q ∈ F, f(p) ≠ f(q) → p ≠ q468    intros p hp q hq different same469    apply different470    rw same471    rfl472  witness functionImage(f, F, 𝒫(X) × Group.carrier(G))473  refine ⟨finiteImage, boundedImage, ?_, ?_⟩474  . refine ⟨?_, ?_, ?_⟩475    . intros q hq476      obtain ⟨p, hp, equal⟩ := members with q, hq477      rw equal478      exact piecesBounded with p, hp479    . intros x hx480      obtain ⟨p, hp, member⟩ := piecesCover with x, hx481      have image := images with p, hp482      witness f(p)483      exact ⟨image, member⟩484    . intros q hq r hr different485      obtain ⟨p, hp, qEq⟩ := members with q, hq486      obtain ⟨s, hs, rEq⟩ := members with r, hr487      rw [qEq, rEq] at different488      have apart := distinct with p, hp, s, hs, different489      rw [qEq, rEq]490      exact piecesDisjoint with p, hp, s, hs, apart491  . refine ⟨?_, ?_, ?_⟩492    . intros q hq493      obtain ⟨p, hp, equal⟩ := members with q, hq494      rw equal495      exact movedBounded with p, hp496    . intros y hy497      obtain ⟨p, hp, member⟩ := movedCover with y, hy498      have image := images with p, hp499      witness f(p)500      exact ⟨image, member⟩501    . intros q hq r hr different502      obtain ⟨p, hp, qEq⟩ := members with q, hq503      obtain ⟨s, hs, rEq⟩ := members with r, hr504      rw [qEq, rEq] at different505      have apart := distinct with p, hp, s, hs, different506      rw [qEq, rEq]507      exact movedDisjoint with p, hp, s, hs, apart508509-- Symmetry: each moved piece is carried back by the inverse element.510defgraph flipPair (act G X : Set) (p ∈ 𝒫(X) × Group.carrier(G)) : 𝒫(X) × Group.carrier(G) :=511  (moved(act, X, p), Group.inv(G)(snd(p)))512requires action : act : G ↷ X513proof514  obtain ⟨bound, S, hS, g, hg, shape⟩ := product.membership.forward with member515  have group := Action.group with action516  have invIn : g⁻¹ ∈ G := Group.inv_mem with *517  have movedBounded := powerset.membership_iff.backward with (translate.subset at act, X, g, S)518  rw [shape, moved.value, snd.pair]519  exact product.pair with movedBounded, invIn520521-- Transitivity: the piece of (S, g) followed by (T, h) is S ∩ g⁻¹T,522-- carried by h * g.523defgraph composePair (act G X : Set)524    (r ∈ (𝒫(X) × Group.carrier(G)) × (𝒫(X) × Group.carrier(G))) :525    𝒫(X) × Group.carrier(G) :=526  (fst(fst(r)) ∩ translate(act, X, Group.inv(G)(snd(fst(r))), fst(snd(r))),527    Group.mul(G)(snd(snd(r)), snd(fst(r))))528requires action : act : G ↷ X529proof530  obtain ⟨bound, p, hp, q, hq, shape⟩ := product.membership.forward with member531  obtain ⟨boundP, S, hS, g, hg, pShape⟩ := product.membership.forward with hp532  obtain ⟨boundQ, T, hT, h, hh, qShape⟩ := product.membership.forward with hq533  have group := Action.group with action534  have subsetS := powerset.membership_iff.forward with hS535  have product : h * g ∈ G := Group.mul_mem with *536  have pieceBounded : S ∩ translate(act, X, g⁻¹, T) ⊆ X :=537    Subset.transitive with (intersection.subset_left at S, translate(act, X, g⁻¹, T)), subsetS538  have pieceIn := powerset.membership_iff.backward with pieceBounded539  have outerFirst := fst.pair at (S, g), (T, h)540  have outerSecond := snd.pair at (S, g), (T, h)541  have firstP := fst.pair at S, g542  have secondP := snd.pair at S, g543  have firstQ := fst.pair at T, h544  have secondQ := snd.pair at T, h545  rw [shape, pShape, qShape, outerFirst, outerSecond, firstP, secondP, firstQ, secondQ]546  exact product.pair with pieceIn, product547548section Equivalence2549variable (act G X : Set)550hypothesis action : act : G ↷ X551552theorem flipPair.apply (S g : Set)553  requires hS : S ⊆ X554  requires hg : g ∈ G.carrier555  shows flipPair(act, G, X)((S, g)) = (translate(act, X, g, S), g⁻¹)556proof557  have boundS := powerset.membership_iff.backward with hS558  have pair := product.pair at S, g, 𝒫(X), Group.carrier(G) with boundS, hg559  have value := flipPair.value at act, G, X, (S, g) with action, pair560  rw [value, moved.value, snd.pair]561  rfl562563theorem Equidecomposable.symmetric (A B : Set)564  requires equidecomposable : Equidecomposable(act, G, X, A, B)565  shows Equidecomposable(act, G, X, B, A)566proof567  have group := Action.group with action568  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := equidecomposable569  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces570  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces571  have function := flipPair.function at act, G, X with action572  have firsts : ∀ p ∈ F, fst(flipPair(act, G, X)(p)) = moved(act, X, p)573    intros p hp574    obtain ⟨boundP, S, hS, g, hg, shape⟩ := product.membership.forward with (bounded with p, hp)575    have subset := powerset.membership_iff.forward with hS576    have value := flipPair.apply with action, subset, hg577    rw [shape, value, fst.pair, moved.value]578    rfl579  have moves : ∀ p ∈ F, moved(act, X, flipPair(act, G, X)(p)) = fst(p)580    intros p hp581    obtain ⟨boundP, S, hS, g, hg, shape⟩ := product.membership.forward with (bounded with p, hp)582    have subset := powerset.membership_iff.forward with hS583    have value := flipPair.apply with action, subset, hg584    have back := translate.inv_translate with action, subset585    have movedValue := moved.value at act, X, translate(act, X, g, S), g⁻¹586    rw [shape, value, movedValue, back, fst.pair]587    rfl588  apply Equidecomposable.of_reindex with function, finite, bounded589  . intros p hp590    have first := firsts with p, hp591    rw first592    exact movedBounded with p, hp593  . intros y hy594    obtain ⟨p, hp, member⟩ := movedCover with y, hy595    have first := firsts with p, hp596    witness p597    rw first598    exact ⟨hp, member⟩599  . intros p hp q hq different600    have firstP := firsts with p, hp601    have firstQ := firsts with q, hq602    rw [firstP, firstQ]603    exact movedDisjoint with p, hp, q, hq, different604  . intros p hp605    have move := moves with p, hp606    rw move607    exact piecesBounded with p, hp608  . intros x hx609    obtain ⟨p, hp, member⟩ := piecesCover with x, hx610    have move := moves with p, hp611    witness p612    rw move613    exact ⟨hp, member⟩614  . intros p hp q hq different615    have moveP := moves with p, hp616    have moveQ := moves with q, hq617    rw [moveP, moveQ]618    exact piecesDisjoint with p, hp, q, hq, different619620theorem composePair.apply (S T : Set) (g h : G)621  requires hS : S ⊆ X622  requires hT : T ⊆ X623  shows composePair(act, G, X)(((S, g), (T, h))) = (S ∩ translate(act, X, g⁻¹, T), h * g)624proof625  have gIn : g ∈ G.carrier by assumption626  have hIn : h ∈ G.carrier by assumption627  have boundS := powerset.membership_iff.backward with hS628  have boundT := powerset.membership_iff.backward with hT629  have first := product.pair at S, g, 𝒫(X), Group.carrier(G) with boundS, gIn630  have second := product.pair at T, h, 𝒫(X), Group.carrier(G) with boundT, hIn631  have pair := product.pair at (S, g), (T, h), 𝒫(X) × Group.carrier(G),632    𝒫(X) × Group.carrier(G) with first, second633  have value := composePair.value at act, G, X, ((S, g), (T, h)) with action, pair634  have outerFirst := fst.pair at (S, g), (T, h)635  have outerSecond := snd.pair at (S, g), (T, h)636  have firstP := fst.pair at S, g637  have secondP := snd.pair at S, g638  have firstQ := fst.pair at T, h639  have secondQ := snd.pair at T, h640  rw [value, outerFirst, outerSecond, firstP, secondP, firstQ, secondQ]641  rfl642643theorem composePair.shape (F F2 p q : Set)644  requires bounded : F ⊆ 𝒫(X) × G.carrier645  requires bounded2 : F2 ⊆ 𝒫(X) × G.carrier646  requires hp : p ∈ F647  requires hq : q ∈ F2648  shows fst(p) ⊆ X ∧ fst(q) ⊆ X ∧ snd(p) ∈ G.carrier ∧ snd(q) ∈ G.carrier ∧ fst(composePair(act, G, X)((p, q))) = fst(p) ∩ translate(act, X, G.inv(snd(p)), fst(q)) ∧ moved(act, X, composePair(act, G, X)((p, q))) = translate(act, X, snd(q), moved(act, X, p) ∩ fst(q))649proof650  obtain ⟨boundP, S, hS, g, hg, pShape⟩ := product.membership.forward with (bounded with p, hp)651  obtain ⟨boundQ, T, hT, h, hh, qShape⟩ := product.membership.forward with (bounded2 with q, hq)652  have group := Action.group with action653  have subsetS := powerset.membership_iff.forward with hS654  have subsetT := powerset.membership_iff.forward with hT655  have value : composePair(act, G, X)(((S, g), (T, h))) =656    (S ∩ translate(act, X, g⁻¹, T), h * g) := composePair.apply with *657  have invT := translate.subset at act, X, g⁻¹, T658  have pieceBounded : S ∩ translate(act, X, g⁻¹, T) ⊆ X :=659    Subset.transitive with (intersection.subset_left at S, translate(act, X, g⁻¹, T)), subsetS660  have mulLaw : translate(act, X, h * g, S ∩ translate(act, X, g⁻¹, T)) =661    translate(act, X, h, translate(act, X, g, S ∩ translate(act, X, g⁻¹, T))) :=662    translate.mul with *663  have meet : translate(act, X, g, S ∩ translate(act, X, g⁻¹, T)) =664    translate(act, X, g, S) ∩ translate(act, X, g, translate(act, X, g⁻¹, T)) :=665    translate.intersection with action, subsetS, invT666  have back : translate(act, X, g, translate(act, X, g⁻¹, T)) = T :=667    translate.translate_inv with action, subsetT668  have movedComposite := moved.value at act, X, S ∩ translate(act, X, g⁻¹, T), h * g669  have movedP := moved.value at act, X, S, g670  have firstP := fst.pair at S, g671  have secondP := snd.pair at S, g672  have firstQ := fst.pair at T, h673  have secondQ := snd.pair at T, h674  have firstComposite := fst.pair at S ∩ translate(act, X, g⁻¹, T), h * g675  rw [pShape, qShape, value]676  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩677  . rw firstP678    exact subsetS679  . rw firstQ680    exact subsetT681  . rw secondP682    exact hg683  . rw secondQ684    exact hh685  . rw [firstComposite, firstP, secondP, firstQ]686    rfl687  . rw [movedComposite, movedP, mulLaw, meet, back, secondQ, firstQ]688    rfl689690theorem Equidecomposable.transitive (A B C : Set)691  requires first : Equidecomposable(act, G, X, A, B)692  requires second : Equidecomposable(act, G, X, B, C)693  shows Equidecomposable(act, G, X, A, C)694proof695  have group := Action.group with action696  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := first697  obtain ⟨F2, finite2, bounded2, pieces2, movedPieces2⟩ := second698  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces699  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces700  obtain ⟨piecesBounded2, piecesCover2, piecesDisjoint2⟩ := pieces2701  obtain ⟨movedBounded2, movedCover2, movedDisjoint2⟩ := movedPieces2702  have function := composePair.function at act, G, X with action703  have finiteProduct := Finite.product with finite, finite2704  have boundedProduct := product.monotone with bounded, bounded2705  apply Equidecomposable.of_reindex with function, finiteProduct, boundedProduct706  . intros r hr707    obtain ⟨bound, p, hp, q, hq, rShape⟩ := product.membership.forward with hr708    obtain ⟨subsetP, subsetQ, gIn, hIn, firstEq, movedEq⟩ :=709      composePair.shape with action, bounded, bounded2, hp, hq710    rw [rShape, firstEq]711    have inner := intersection.subset_left at fst(p), translate(act, X, G.inv(snd(p)), fst(q))712    exact Subset.transitive with inner, (piecesBounded with p, hp)713  . intros x hx714    obtain ⟨p, hp, xInP⟩ := piecesCover with x, hx715    obtain ⟨boundP, S, hS, g, hg, pShape⟩ := product.membership.forward with (bounded with p, hp)716    have subsetS := powerset.membership_iff.forward with hS717    rw [pShape, fst.pair] at xInP718    have moved : g ·ₐ x ∈ translate(act, X, g, S) := translate.act_mem with *719    have movedValue := moved.value at act, X, S, g720    rw [← movedValue, ← pShape] at moved721    have inB := movedBounded with p, hp, g ·ₐ x, moved722    obtain ⟨q, hq, inQ⟩ := piecesCover2 with g ·ₐ x, inB723    obtain ⟨subsetP, subsetQ, gIn, hIn, firstEq, movedEq⟩ :=724      composePair.shape with action, bounded, bounded2, hp, hq725    have xIn := subsetS with x, xInP726    have twice : (g⁻¹)⁻¹ = g := inv_inv with *727    have pulled : x ∈ translate(act, X, g⁻¹, fst(q))728      apply translate.mem_iff.backward with action, subsetQ, xIn729      rw twice730      exact inQ731    have pair := product.pair at p, q, F, F2 with hp, hq732    witness (p, q)733    refine ⟨pair, ?_⟩734    rw [firstEq, pShape, fst.pair, snd.pair]735    exact intersection.membership.backward at736      S, translate(act, X, g⁻¹, fst(q)), x with ⟨xInP, pulled⟩737  . intros r hr s hs different738    obtain ⟨bound, p, hp, q, hq, rShape⟩ := product.membership.forward with hr739    obtain ⟨bound2, p2, hp2, q2, hq2, sShape⟩ := product.membership.forward with hs740    obtain ⟨subsetP, subsetQ, gIn, hIn, firstEq, movedEq⟩ :=741      composePair.shape with action, bounded, bounded2, hp, hq742    obtain ⟨subsetP2, subsetQ2, gIn2, hIn2, firstEq2, movedEq2⟩ :=743      composePair.shape with action, bounded, bounded2, hp2, hq2744    rw [rShape, sShape] at different745    rw [rShape, sShape, firstEq, firstEq2]746    have splitP : p = p2 ∨ p ≠ p2 by tauto747    cases splitP with same | apart748    . have apartQ : q ≠ q2749        intro sameQ750        apply different751        rw [same, sameQ]752        rfl753      have disjointQ := piecesDisjoint2 with q, hq, q2, hq2, apartQ754      rw same755      have invIn : G.inv(snd(p2)) ∈ G.carrier := Group.inv_mem with *756      have disjointPulled : Disjoint(translate(act, X, G.inv(snd(p2)), fst(q)),757        translate(act, X, G.inv(snd(p2)), fst(q2))) := translate.disjoint with *758      have left := intersection.subset_right at fst(p2), translate(act, X, G.inv(snd(p2)), fst(q))759      have right := intersection.subset_right at fst(p2), translate(act, X, G.inv(snd(p2)), fst(q2))760      have step := Disjoint.of_subset_left with disjointPulled, left761      exact Disjoint.of_subset_right with step, right762    . have disjointP := piecesDisjoint with p, hp, p2, hp2, apart763      have left := intersection.subset_left at fst(p), translate(act, X, G.inv(snd(p)), fst(q))764      have right := intersection.subset_left at fst(p2), translate(act, X, G.inv(snd(p2)), fst(q2))765      have step := Disjoint.of_subset_left with disjointP, left766      exact Disjoint.of_subset_right with step, right767  . intros r hr768    obtain ⟨bound, p, hp, q, hq, rShape⟩ := product.membership.forward with hr769    obtain ⟨subsetP, subsetQ, gIn, hIn, firstEq, movedEq⟩ :=770      composePair.shape with action, bounded, bounded2, hp, hq771    rw [rShape, movedEq]772    have inner := intersection.subset_right at moved(act, X, p), fst(q)773    have mono := translate.monotone at act, X, snd(q), moved(act, X, p) ∩ fst(q), fst(q) with inner774    have unfolded := moved.unfold at act, X, q775    rw ← unfolded at mono776    exact Subset.transitive with mono, (movedBounded2 with q, hq)777  . intros y hy778    obtain ⟨q, hq, yInQ⟩ := movedCover2 with y, hy779    have unfolded := moved.unfold at act, X, q780    rw unfolded at yInQ781    obtain ⟨yIn, t, ht, yEq⟩ := translate.membership.forward with yInQ782    have inB := piecesBounded2 with q, hq, t, ht783    obtain ⟨p, hp, tInP⟩ := movedCover with t, inB784    obtain ⟨subsetP, subsetQ, gIn, hIn, firstEq, movedEq⟩ :=785      composePair.shape with action, bounded, bounded2, hp, hq786    have both := intersection.membership.backward at787      moved(act, X, p), fst(q), t with ⟨tInP, ht⟩788    have meetBounded : moved(act, X, p) ∩ fst(q) ⊆ X :=789      Subset.transitive with (intersection.subset_right at moved(act, X, p), fst(q)), subsetQ790    have pair := product.pair at p, q, F, F2 with hp, hq791    witness (p, q)792    refine ⟨pair, ?_⟩793    rw [movedEq, yEq]794    exact translate.act_mem with action, meetBounded, both795  . intros r hr s hs different796    obtain ⟨bound, p, hp, q, hq, rShape⟩ := product.membership.forward with hr797    obtain ⟨bound2, p2, hp2, q2, hq2, sShape⟩ := product.membership.forward with hs798    obtain ⟨subsetP, subsetQ, gIn, hIn, firstEq, movedEq⟩ :=799      composePair.shape with action, bounded, bounded2, hp, hq800    obtain ⟨subsetP2, subsetQ2, gIn2, hIn2, firstEq2, movedEq2⟩ :=801      composePair.shape with action, bounded, bounded2, hp2, hq2802    rw [rShape, sShape] at different803    rw [rShape, sShape, movedEq, movedEq2]804    have splitQ : q = q2 ∨ q ≠ q2 by tauto805    cases splitQ with same | apart806    . have apartP : p ≠ p2807        intro sameP808        apply different809        rw [same, sameP]810        rfl811      have disjointP := movedDisjoint with p, hp, p2, hp2, apartP812      rw same813      have left := intersection.subset_left at moved(act, X, p), fst(q2)814      have right := intersection.subset_left at moved(act, X, p2), fst(q2)815      have step := Disjoint.of_subset_left with disjointP, left816      have inner := Disjoint.of_subset_right with step, right817      have innerLeft := intersection.subset_right at moved(act, X, p), fst(q2)818      have innerRight := intersection.subset_right at moved(act, X, p2), fst(q2)819      have meetBounded : moved(act, X, p) ∩ fst(q2) ⊆ X :=820        Subset.transitive with innerLeft, subsetQ2821      have meetBounded2 : moved(act, X, p2) ∩ fst(q2) ⊆ X :=822        Subset.transitive with innerRight, subsetQ2823      exact translate.disjoint with action, meetBounded, meetBounded2, inner824    . have disjointQ := movedDisjoint2 with q, hq, q2, hq2, apart825      have unfoldedQ := moved.unfold at act, X, q826      have unfoldedQ2 := moved.unfold at act, X, q2827      have innerQ := intersection.subset_right at moved(act, X, p), fst(q)828      have innerQ2 := intersection.subset_right at moved(act, X, p2), fst(q2)829      have monoQ := translate.monotone at act, X, snd(q), moved(act, X, p) ∩ fst(q), fst(q)830        with innerQ831      have monoQ2 := translate.monotone at act, X, snd(q2), moved(act, X, p2) ∩ fst(q2), fst(q2)832        with innerQ2833      rw ← unfoldedQ at monoQ834      rw ← unfoldedQ2 at monoQ2835      have step := Disjoint.of_subset_left with disjointQ, monoQ836      exact Disjoint.of_subset_right with step, monoQ2837838-- Disjoint unions of equidecomposable sets are equidecomposable.839theorem Equidecomposable.disjoint_union (A B C D : Set)840  requires first : Equidecomposable(act, G, X, A, C)841  requires second : Equidecomposable(act, G, X, B, D)842  requires disjointSource : Disjoint(A, B)843  requires disjointTarget : Disjoint(C, D)844  shows Equidecomposable(act, G, X, A ∪ B, C ∪ D)845proof846  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := first847  obtain ⟨F2, finite2, bounded2, pieces2, movedPieces2⟩ := second848  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces849  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces850  obtain ⟨piecesBounded2, piecesCover2, piecesDisjoint2⟩ := pieces2851  obtain ⟨movedBounded2, movedCover2, movedDisjoint2⟩ := movedPieces2852  have finiteUnion := Finite.union with finite, finite2853  have boundedUnion := union2.subset with bounded, bounded2854  have leftA := union2.subset_left at A, B855  have rightB := union2.subset_right at A, B856  have leftC := union2.subset_left at C, D857  have rightD := union2.subset_right at C, D858  have leftF := union2.subset_left at F, F2859  have rightF := union2.subset_right at F, F2860  have flippedSource := Disjoint.symmetric with disjointSource861  have flippedTarget := Disjoint.symmetric with disjointTarget862  witness F ∪ F2863  refine ⟨finiteUnion, boundedUnion, ?_, ?_⟩864  . refine ⟨?_, ?_, ?_⟩865    . intros p hp866      have split := union2.membership.forward with hp867      cases split with inF | inF2868      . exact Subset.transitive with (piecesBounded with p, inF), leftA869      . exact Subset.transitive with (piecesBounded2 with p, inF2), rightB870    . intros x hx871      have split := union2.membership.forward with hx872      cases split with inA | inB873      . obtain ⟨p, hp, member⟩ := piecesCover with x, inA874        have pIn := leftF with p, hp875        exact ⟨p, pIn, member⟩876      . obtain ⟨p, hp, member⟩ := piecesCover2 with x, inB877        have pIn := rightF with p, hp878        exact ⟨p, pIn, member⟩879    . intros p hp q hq different880      have splitP := union2.membership.forward with hp881      have splitQ := union2.membership.forward with hq882      cases splitP with pF | pF2883      . cases splitQ with qF | qF2884        . exact piecesDisjoint with p, pF, q, qF, different885        . have step := Disjoint.of_subset_left with disjointSource, (piecesBounded with p, pF)886          exact Disjoint.of_subset_right with step, (piecesBounded2 with q, qF2)887      . cases splitQ with qF | qF2888        . have step := Disjoint.of_subset_left with flippedSource, (piecesBounded2 with p, pF2)889          exact Disjoint.of_subset_right with step, (piecesBounded with q, qF)890        . exact piecesDisjoint2 with p, pF2, q, qF2, different891  . refine ⟨?_, ?_, ?_⟩892    . intros p hp893      have split := union2.membership.forward with hp894      cases split with inF | inF2895      . exact Subset.transitive with (movedBounded with p, inF), leftC896      . exact Subset.transitive with (movedBounded2 with p, inF2), rightD897    . intros y hy898      have split := union2.membership.forward with hy899      cases split with inC | inD900      . obtain ⟨p, hp, member⟩ := movedCover with y, inC901        have pIn := leftF with p, hp902        exact ⟨p, pIn, member⟩903      . obtain ⟨p, hp, member⟩ := movedCover2 with y, inD904        have pIn := rightF with p, hp905        exact ⟨p, pIn, member⟩906    . intros p hp q hq different907      have splitP := union2.membership.forward with hp908      have splitQ := union2.membership.forward with hq909      cases splitP with pF | pF2910      . cases splitQ with qF | qF2911        . exact movedDisjoint with p, pF, q, qF, different912        . have step := Disjoint.of_subset_left with disjointTarget, (movedBounded with p, pF)913          exact Disjoint.of_subset_right with step, (movedBounded2 with q, qF2)914      . cases splitQ with qF | qF2915        . have step := Disjoint.of_subset_left with flippedTarget, (movedBounded2 with p, pF2)916          exact Disjoint.of_subset_right with step, (movedBounded with q, qF)917        . exact movedDisjoint2 with p, pF2, q, qF2, different918919end Equivalence2920921-- The action of the free group pulled back along a homomorphism into G:922-- the word w acts as φ(w).923defgraph pullback (act G X φ : Set) (p ∈ reducedWords × X) : X := act(φ(fst(p)), snd(p))924requires action : act : G ↷ X925requires hom : φ : freeGroup →* G926proof927  obtain ⟨bound, w, hw, x, hx, shape⟩ := product.membership.forward with member928  have function := GroupHom.function with hom929  have carrier := freeGroup.carrierOf930  rw ← carrier at hw931  have image := FunctionBetween.apply_closed with function, hw932  rw [shape, fst.pair, snd.pair]933  exact Action.act_mem with action, image, hx934935section Pullback936variable (act G X φ : Set)937hypothesis action : act : G ↷ X938hypothesis hom : φ : freeGroup →* G939940theorem pullback.apply (w x : Set)941  requires hw : w ∈ reducedWords942  requires hx : x ∈ X943  shows pullback(act, G, X, φ)(w, x) = act(φ(w), x)944proof945  have pair := product.pair at w, x, reducedWords, X with *946  have value := pullback.value at act, G, X, φ, (w, x) with action, hom, pair947  simp [call2]948  rw [fst.pair, snd.pair]949  rfl950951theorem pullback.image_mem (w : Set)952  requires hw : w ∈ reducedWords953  shows φ(w) ∈ G.carrier954proof955  have function := GroupHom.function with hom956  have carrier := freeGroup.carrierOf957  rw ← carrier at hw958  exact FunctionBetween.apply_closed with function, hw959960theorem pullback.map_nil961  shows φ([]) = G.one962proof963  have mapOne := GroupHom.map_one with hom964  rwa freeGroup.unit at mapOne965966theorem pullback.action967  shows pullback(act, G, X, φ) : freeGroup ↷ X968proof969  have group := freeGroup.group970  have function := pullback.function at act, G, X, φ with action, hom971  have carrierFunction : pullback(act, G, X, φ) : Group.carrier(freeGroup) × X → X972    rw freeGroup.carrierOf973    exact function974  apply Action.mk with group, carrierFunction975  . intros x hx976    have unitIn := reducedWords.nil_mem977    have value := pullback.apply with action, hom, unitIn, hx978    have mapOne := pullback.map_nil with hom979    rw [freeGroup.unit, value, mapOne]980    exact one_act with action, hx981  . intros u hu v hv x hx982    have uIn := hu983    have vIn := hv984    rw freeGroup.carrierOf at uIn985    rw freeGroup.carrierOf at vIn986    have mapMul : φ(u * v) = φ(u) * φ(v) := GroupHom.map_mul with *987    have productIn : u * v ∈ reducedWords988      rw freeGroup.operation989      exact freeMul.mem with uIn, vIn990    have imageU := pullback.image_mem with hom, uIn991    have imageV := pullback.image_mem with hom, vIn992    have moved : φ(v) ·ₐ x ∈ X := Action.act_mem with *993    have first := pullback.apply with action, hom, vIn, hx994    have second := pullback.apply with action, hom, uIn, moved995    have third := pullback.apply with action, hom, productIn, hx996    have merged : (φ(u) * φ(v)) ·ₐ x = φ(u) ·ₐ φ(v) ·ₐ x := mul_act with *997    rw [third, mapMul, merged, first, second]998    rfl9991000theorem pullback.free1001  requires free : FreeAction(act, G, X)1002  requires injective : InjectiveBetween(φ, reducedWords, G.carrier)1003  shows FreeAction(pullback(act, G, X, φ), freeGroup, X)1004proof1005  have group := Action.group with action1006  have function := GroupHom.function with hom1007  rw freeGroup.carrierOf at function1008  have mapOne := pullback.map_nil with hom1009  have nilIn := reducedWords.nil_mem1010  have oneIn : G.one ∈ G := Group.one_mem with *1011  unfold FreeAction1012  intros x hx1013  have trivial := free with x, hx1014  rw freeGroup.unit1015  ext w1016  constructor1017  . intro hw1018    obtain ⟨wIn, fixes⟩ := stabilizer.membership.forward with hw1019    rw freeGroup.carrierOf at wIn1020    have value := pullback.apply with action, hom, wIn, hx1021    rw value at fixes1022    have imageIn := pullback.image_mem with hom, wIn1023    have inStabilizer : φ(w) ∈ stabilizer(act, G, X, x) :=1024      stabilizer.membership.backward with ⟨imageIn, fixes⟩1025    rw trivial at inStabilizer1026    have equal := singleton.membership.forward with inStabilizer1027    have relatesW := FunctionBetween.relates_apply with function, wIn1028    have relatesNil := FunctionBetween.relates_apply with function, nilIn1029    rw equal at relatesW1030    rw mapOne at relatesNil1031    have same := Injective.cancel with injective, wIn, nilIn, oneIn, relatesW, relatesNil1032    rw same1033    exact singleton.self1034  . intro hw1035    have equal := singleton.membership.forward with hw1036    rw equal1037    apply stabilizer.membership.backward1038    constructor1039    . rw freeGroup.carrierOf1040      exact nilIn1041    . have value := pullback.apply with action, hom, nilIn, hx1042      rw [value, mapOne]1043      exact one_act with action, hx10441045end Pullback10461047section Representatives1048variable (act G X c : Set)1049hypothesis action : act : G ↷ X1050hypothesis choice : SubsetChoice(c, X)10511052-- The chosen point of an orbit lies in it, so the representatives lie in1053-- X, every point is carried from a representative, and two1054-- representatives with the same orbit coincide.1055theorem representatives.chosen (O : Set)1056  requires hO : O ∈ orbits(act, G, X)1057  shows c(O) ∈ O1058proof1059  obtain ⟨bound, x, hx, OEq⟩ := orbits.membership.forward with hO1060  have subset := powerset.membership_iff.forward with bound1061  have self : x ∈ orbit(x) := orbit.self with *1062  have inhabited : Nonempty(O)1063    rw OEq1064    exact ⟨x, self⟩1065  exact SubsetChoice.member with choice, subset, inhabited10661067theorem representatives.subset1068  shows representatives(act, G, X, c) ⊆ X1069proof1070  intros m hm1071  obtain ⟨O, hO, equal⟩ := representatives.membership.forward with hm1072  have bound := orbits.subset_powerset at act, G, X with O, hO1073  have subset := powerset.membership_iff.forward with bound1074  have chosen := representatives.chosen with action, choice, hO1075  rw ← equal1076  exact subset with c(O), chosen10771078theorem representatives.orbit (m : Set)1079  requires hm : m ∈ representatives(act, G, X, c)1080  shows ∃ O ∈ orbits(act, G, X), O = orbit(m) ∧ c(O) = m1081proof1082  obtain ⟨O, hO, equal⟩ := representatives.membership.forward with hm1083  obtain ⟨bound, x, hx, OEq⟩ := orbits.membership.forward with hO1084  have chosen := representatives.chosen with action, choice, hO1085  rw equal at chosen1086  witness O1087  refine ⟨hO, ?_, equal⟩1088  rw OEq at chosen1089  have same : orbit(m) = orbit(x) := orbit.of_member with action, hx, chosen1090  rw [OEq, same]1091  rfl10921093theorem representatives.cover (x : Set)1094  requires hx : x ∈ X1095  shows ∃ m ∈ representatives(act, G, X, c), ∃ g ∈ G.carrier, x = g ·ₐ m1096proof1097  have group := Action.group with action1098  have hO := orbits.orbit_member at act, G, X, x with hx1099  have chosen := representatives.chosen with action, choice, hO1100  have member : c(orbit(x)) ∈ representatives(act, G, X, c) :=1101    representatives.membership.backward with ⟨orbit(x), hO, rfl⟩1102  obtain ⟨mIn, h, hIn, mEq⟩ := orbit.membership.forward with chosen1103  witness c(orbit(x))1104  refine ⟨member, h⁻¹, ?_, ?_⟩1105  . typecheck1106  . rw [mEq, inv_act_cancel]1107    rfl11081109theorem representatives.unique (m n : Set)1110  requires hm : m ∈ representatives(act, G, X, c)1111  requires hn : n ∈ representatives(act, G, X, c)1112  requires same : orbit(m) = orbit(n)1113  shows m = n1114proof1115  obtain ⟨O, hO, OEq, chosenO⟩ := representatives.orbit with action, choice, hm1116  obtain ⟨P, hP, PEq, chosenP⟩ := representatives.orbit with action, choice, hn1117  have equal : O = P by cc1118  rw [← chosenO, ← chosenP, equal]1119  rfl11201121-- Under a free action, a point of X is carried from a representative by1122-- exactly one group element.1123theorem representatives.injective (m n : Set) (g h : G)1124  requires free : FreeAction(act, G, X)1125  requires hm : m ∈ representatives(act, G, X, c)1126  requires hn : n ∈ representatives(act, G, X, c)1127  requires equal : g ·ₐ m = h ·ₐ n1128  shows m = n ∧ g = h1129proof1130  have group := Action.group with action1131  have bounded := representatives.subset with action, choice1132  have mIn := bounded with m, hm1133  have nIn := bounded with n, hn1134  have moved : h⁻¹ ·ₐ g ·ₐ m = n1135    rw [equal, inv_act_cancel]1136    rfl1137  have merged : (h⁻¹ * g) ·ₐ m = h⁻¹ ·ₐ g ·ₐ m := mul_act with *1138  have nInOrbit : n ∈ orbit(m)1139    rw [← moved, ← merged]1140    exact orbit.act_mem with *1141  have sameOrbit : orbit(n) = orbit(m) := orbit.of_member with action, mIn, nInOrbit1142  symm at sameOrbit1143  have mn := representatives.unique with action, choice, hm, hn, sameOrbit1144  refine ⟨mn, ?_⟩1145  rw ← mn at moved1146  rw ← merged at moved1147  have trivial := free with m, mIn1148  have inStabilizer : h⁻¹ * g ∈ stabilizer(act, G, X, m) := stabilizer.of_fixes with *1149  rw trivial at inStabilizer1150  have unit := singleton.membership.forward with inStabilizer1151  have criterion : h⁻¹ * g = G.one ↔ h = g := inv_mul_eq_one with *1152  symm1153  exact criterion.forward with unit11541155end Representatives11561157section Sweep1158variable (act G X : Set)1159hypothesis action : act : G ↷ X11601161-- Sweeping a set of representatives by a set of group elements: the1162-- images of distinct elements on representatives are disjoint under a1163-- free action, the whole group sweeps everything, and translating a1164-- sweep translates the elements.1165theorem sweep.act_mem (H M g x : Set)1166  requires boundedH : H ⊆ G.carrier1167  requires boundedM : M ⊆ X1168  requires hg : g ∈ H1169  requires hx : x ∈ M1170  shows act(g, x) ∈ sweep(act, X, H, M)1171proof1172  have xIn := boundedM with x, hx1173  have gIn := boundedH with g, hg1174  have moved : g ·ₐ x ∈ X := Action.act_mem with *1175  exact sweep.membership.backward with ⟨moved, g, hg, x, hx, rfl⟩11761177theorem sweep.monotone (H K M : Set)1178  requires subset : H ⊆ K1179  shows sweep(act, X, H, M) ⊆ sweep(act, X, K, M)1180proof1181  intros y hy1182  obtain ⟨yIn, g, hg, x, hx, equal⟩ := sweep.membership.forward with hy1183  exact sweep.membership.backward with ⟨yIn, g, (subset with g, hg), x, hx, equal⟩11841185theorem sweep.union2 (H K M : Set)1186  shows sweep(act, X, H ∪ K, M) = sweep(act, X, H, M) ∪ sweep(act, X, K, M)1187proof1188  ext y1189  constructor1190  . intro hy1191    obtain ⟨yIn, g, hg, x, hx, equal⟩ := sweep.membership.forward with hy1192    have split := union2.membership.forward with hg1193    cases split with inH | inK1194    . apply union2.membership.backward1195      left1196      exact sweep.membership.backward with ⟨yIn, g, inH, x, hx, equal⟩1197    . apply union2.membership.backward1198      right1199      exact sweep.membership.backward with ⟨yIn, g, inK, x, hx, equal⟩1200  . intro hy1201    have split := union2.membership.forward with hy1202    cases split with inH | inK1203    . have leftIn := union2.subset_left at H, K1204      have mono : sweep(act, X, H, M) ⊆ sweep(act, X, H ∪ K, M) :=1205        sweep.monotone with leftIn1206      exact mono with y, inH1207    . have rightIn := union2.subset_right at H, K1208      have mono : sweep(act, X, K, M) ⊆ sweep(act, X, H ∪ K, M) :=1209        sweep.monotone with rightIn1210      exact mono with y, inK12111212theorem sweep.disjoint (c H K : Set)1213  requires choice : SubsetChoice(c, X)1214  requires free : FreeAction(act, G, X)1215  requires boundedH : H ⊆ G.carrier1216  requires boundedK : K ⊆ G.carrier1217  requires disjoint : Disjoint(H, K)1218  shows Disjoint(sweep(act, X, H, representatives(act, G, X, c)),1219    sweep(act, X, K, representatives(act, G, X, c)))1220proof1221  have apart := Disjoint.iff.forward with disjoint1222  apply Disjoint.iff.backward1223  intros y hyH hyK1224  obtain ⟨yIn, g, hg, m, hm, gEq⟩ := sweep.membership.forward with hyH1225  obtain ⟨yIn2, h, hh, n, hn, hEq⟩ := sweep.membership.forward with hyK1226  have gIn := boundedH with g, hg1227  have hIn := boundedK with h, hh1228  have equal : g ·ₐ m = h ·ₐ n by cc1229  have both := representatives.injective with action, choice, free, hm, hn, equal1230  rw both.right at hg1231  exact apart with h, hg, hh12321233theorem sweep.whole (c : Set)1234  requires choice : SubsetChoice(c, X)1235  shows sweep(act, X, G.carrier, representatives(act, G, X, c)) = X1236proof1237  have boundedM := representatives.subset with action, choice1238  apply Subset.antisymmetric1239  . exact sweep.subset at act, X, G.carrier, representatives(act, G, X, c)1240  . intros x hx1241    obtain ⟨m, hm, g, hg, equal⟩ := representatives.cover with action, choice, hx1242    rw equal1243    exact sweep.act_mem with action, (Subset.reflexive at G.carrier), boundedM, hg, hm12441245theorem sweep.translate (g : G) (H M : Set)1246  requires boundedH : H ⊆ G.carrier1247  requires boundedM : M ⊆ X1248  shows translate(act, X, g, sweep(act, X, H, M)) = sweep(act, X, leftCoset(G, g, H), M)1249proof1250  have group := Action.group with action1251  ext y1252  constructor1253  . intro hy1254    obtain ⟨yIn, z, hz, equal⟩ := translate.membership.forward with hy1255    obtain ⟨zIn, h, hh, x, hx, zEq⟩ := sweep.membership.forward with hz1256    have hIn := boundedH with h, hh1257    have xIn := boundedM with x, hx1258    have merged : (g * h) ·ₐ x = g ·ₐ h ·ₐ x := mul_act with *1259    have product : g * h ∈ G by typecheck1260    have inCoset : g * h ∈ leftCoset(G, g, H) :=1261      leftCoset.membership.backward with ⟨product, h, hh, rfl⟩1262    rw [equal, zEq, ← merged]1263    exact sweep.act_mem with action, (leftCoset.subset at G, g, H), boundedM, inCoset, hx1264  . intro hy1265    obtain ⟨yIn, k, hk, x, hx, equal⟩ := sweep.membership.forward with hy1266    obtain ⟨kIn, h, hh, kEq⟩ := leftCoset.membership.forward with hk1267    have hIn := boundedH with h, hh1268    have xIn := boundedM with x, hx1269    have merged : (g * h) ·ₐ x = g ·ₐ h ·ₐ x := mul_act with *1270    have inner : h ·ₐ x ∈ sweep(act, X, H, M) :=1271      sweep.act_mem with action, boundedH, boundedM, hh, hx1272    rw [equal, kEq, merged]1273    exact translate.act_mem with action, (sweep.subset at act, X, H, M), inner12741275end Sweep12761277-- A set with a free action of the free group is paradoxical: with M one1278-- chosen point in each orbit, the words starting with a and with a⁻¹1279-- sweep M onto two pieces whose union is carried onto X by the unit and1280-- by a, and likewise for b.1281theorem Paradoxical.of_free_freeGroup (act X : Set)1282  requires action : act : freeGroup ↷ X1283  requires free : FreeAction(act, freeGroup, X)1284  shows Paradoxical(act, freeGroup, X)1285proof1286  obtain ⟨c, choice⟩ := SubsetChoice.exists at X1287  have group := freeGroup.group1288  have carrier := freeGroup.carrierOf1289  have boundedM := representatives.subset with action, choice1290  have zero := letter.zero_mem1291  have one := letter.one_mem1292  have two := letter.two_mem1293  have three := letter.three_mem1294  have inverseA : 1 = inverseLetter(0)1295    symm1296    exact inverseLetter.zero1297  have inverseB : 3 = inverseLetter(2)1298    symm1299    exact inverseLetter.two1300  have translateA := leftCoset.letter with zero, one, inverseA1301  have translateB := leftCoset.letter with two, three, inverseB1302  have subset0 := startsWith.subset at 01303  have subset1 := startsWith.subset at 11304  have subset2 := startsWith.subset at 21305  have subset3 := startsWith.subset at 31306  have bounded0 : startsWith(0) ⊆ Group.carrier(freeGroup)1307    rw carrier1308    exact subset01309  have bounded1 : startsWith(1) ⊆ Group.carrier(freeGroup)1310    rw carrier1311    exact subset11312  have bounded2 : startsWith(2) ⊆ Group.carrier(freeGroup)1313    rw carrier1314    exact subset21315  have bounded3 : startsWith(3) ⊆ Group.carrier(freeGroup)1316    rw carrier1317    exact subset31318  have rest0 : reducedWords ∖ startsWith(0) ⊆ Group.carrier(freeGroup)1319    rw carrier1320    exact difference.subset_left at reducedWords, startsWith(0)1321  have rest2 : reducedWords ∖ startsWith(2) ⊆ Group.carrier(freeGroup)1322    rw carrier1323    exact difference.subset_left at reducedWords, startsWith(2)1324  have unitIn : [] ∈ Group.carrier(freeGroup)1325    rw carrier1326    exact reducedWords.nil_mem1327  have valueA : freeA = 0 :: [] by simp [freeA]1328  have valueB : freeB = 2 :: [] by simp [freeB]1329  have singleA : 0 :: [] ∈ Group.carrier(freeGroup)1330    rw [carrier, ← valueA]1331    exact freeA.mem1332  have singleB : 2 :: [] ∈ Group.carrier(freeGroup)1333    rw [carrier, ← valueB]1334    exact freeB.mem1335  have whole := sweep.whole with action, choice1336  rw carrier at whole1337  have piece0 := sweep.subset at act, X, startsWith(0), representatives(act, freeGroup, X, c)1338  have piece1 := sweep.subset at act, X, startsWith(1), representatives(act, freeGroup, X, c)1339  have piece2 := sweep.subset at act, X, startsWith(2), representatives(act, freeGroup, X, c)1340  have piece3 := sweep.subset at act, X, startsWith(3), representatives(act, freeGroup, X, c)1341  have apart01 : 0 ≠ 1 by settle with Naturals.disjoint.zero.succ, Naturals.injective.succ1342  have apart02 : 0 ≠ 2 by settle with Naturals.disjoint.zero.succ, Naturals.injective.succ1343  have apart03 : 0 ≠ 3 by settle with Naturals.disjoint.zero.succ, Naturals.injective.succ1344  have apart12 : 1 ≠ 2 by settle with Naturals.disjoint.zero.succ, Naturals.injective.succ1345  have apart13 : 1 ≠ 3 by settle with Naturals.disjoint.zero.succ, Naturals.injective.succ1346  have apart23 : 2 ≠ 3 by settle with Naturals.disjoint.zero.succ, Naturals.injective.succ1347  have words01 := startsWith.disjoint with zero, one, apart011348  have words02 := startsWith.disjoint with zero, two, apart021349  have words03 := startsWith.disjoint with zero, three, apart031350  have words12 := startsWith.disjoint with one, two, apart121351  have words13 := startsWith.disjoint with one, three, apart131352  have words23 := startsWith.disjoint with two, three, apart231353  have disjoint01 := sweep.disjoint with action, choice, free, bounded0, bounded1, words011354  have disjoint23 := sweep.disjoint with action, choice, free, bounded2, bounded3, words231355  have union01 : sweep(act, X, startsWith(0) ∪ startsWith(1), representatives(act, freeGroup, X, c)) =1356    sweep(act, X, startsWith(0), representatives(act, freeGroup, X, c)) ∪ sweep(act, X, startsWith(1), representatives(act, freeGroup, X, c)) := sweep.union2 with *1357  have union23 : sweep(act, X, startsWith(2) ∪ startsWith(3), representatives(act, freeGroup, X, c)) =1358    sweep(act, X, startsWith(2), representatives(act, freeGroup, X, c)) ∪ sweep(act, X, startsWith(3), representatives(act, freeGroup, X, c)) := sweep.union2 with *1359  witness sweep(act, X, startsWith(0), representatives(act, freeGroup, X, c)) ∪ sweep(act, X, startsWith(1), representatives(act, freeGroup, X, c))1360  witness sweep(act, X, startsWith(2), representatives(act, freeGroup, X, c)) ∪ sweep(act, X, startsWith(3), representatives(act, freeGroup, X, c))1361  refine ⟨?_, ?_, ?_, ?_, ?_⟩1362  . exact union2.subset with piece0, piece11363  . exact union2.subset with piece2, piece31364  . rw [← union01, ← union23]1365    have bounded01 : startsWith(0) ∪ startsWith(1) ⊆ Group.carrier(freeGroup) :=1366      union2.subset with bounded0, bounded11367    have bounded23 : startsWith(2) ∪ startsWith(3) ⊆ Group.carrier(freeGroup) :=1368      union2.subset with bounded2, bounded31369    have apart : Disjoint(startsWith(0) ∪ startsWith(1), startsWith(2) ∪ startsWith(3))1370      apply Disjoint.iff.backward1371      intros w hwA hwB1372      have splitA := union2.membership.forward with hwA1373      have splitB := union2.membership.forward with hwB1374      cases splitA with in0 | in11375      . cases splitB with in2 | in31376        . have apartWords02 := Disjoint.iff.forward with words021377          exact apartWords02 with w, in0, in21378        . have apartWords03 := Disjoint.iff.forward with words031379          exact apartWords03 with w, in0, in31380      . cases splitB with in2 | in31381        . have apartWords12 := Disjoint.iff.forward with words121382          exact apartWords12 with w, in1, in21383        . have apartWords13 := Disjoint.iff.forward with words131384          exact apartWords13 with w, in1, in31385    exact sweep.disjoint with action, choice, free, bounded01, bounded23, apart1386  . have fixed := translate.one with action, piece01387    rw freeGroup.unit at fixed1388    have shifted : translate(act, X, 0 :: [], sweep(act, X, startsWith(1), representatives(act, freeGroup, X, c))) =1389      sweep(act, X, leftCoset(freeGroup, 0 :: [], startsWith(1)), representatives(act, freeGroup, X, c)) := sweep.translate with *1390    rw translateA at shifted1391    have apartRest := Disjoint.symmetric with (difference.disjoint at reducedWords, startsWith(0))1392    have disjointImages := sweep.disjoint with action, choice, free, bounded0, rest0, apartRest1393    have coverImages : sweep(act, X, startsWith(0) ∪ (reducedWords ∖ startsWith(0)), representatives(act, freeGroup, X, c)) =1394      sweep(act, X, startsWith(0), representatives(act, freeGroup, X, c)) ∪ sweep(act, X, reducedWords ∖ startsWith(0), representatives(act, freeGroup, X, c)) := sweep.union2 with *1395    have restore := difference.union2_of_subset with subset01396    rw restore at coverImages1397    rw [← fixed, ← shifted] at disjointImages1398    rw [whole, ← fixed, ← shifted] at coverImages1399    symm at coverImages1400    have coverPieces : sweep(act, X, startsWith(0), representatives(act, freeGroup, X, c)) ∪ sweep(act, X, startsWith(1), representatives(act, freeGroup, X, c)) =1401      sweep(act, X, startsWith(0), representatives(act, freeGroup, X, c)) ∪ sweep(act, X, startsWith(1), representatives(act, freeGroup, X, c)) by rfl1402    exact Equidecomposable.of_two_pieces with action, unitIn, singleA, piece0, piece1,1403      disjoint01, coverPieces, disjointImages, coverImages1404  . have fixed := translate.one with action, piece21405    rw freeGroup.unit at fixed1406    have shifted : translate(act, X, 2 :: [], sweep(act, X, startsWith(3), representatives(act, freeGroup, X, c))) =1407      sweep(act, X, leftCoset(freeGroup, 2 :: [], startsWith(3)), representatives(act, freeGroup, X, c)) := sweep.translate with *1408    rw translateB at shifted1409    have apartRest := Disjoint.symmetric with (difference.disjoint at reducedWords, startsWith(2))1410    have disjointImages := sweep.disjoint with action, choice, free, bounded2, rest2, apartRest1411    have coverImages : sweep(act, X, startsWith(2) ∪ (reducedWords ∖ startsWith(2)), representatives(act, freeGroup, X, c)) =1412      sweep(act, X, startsWith(2), representatives(act, freeGroup, X, c)) ∪ sweep(act, X, reducedWords ∖ startsWith(2), representatives(act, freeGroup, X, c)) := sweep.union2 with *1413    have restore := difference.union2_of_subset with subset21414    rw restore at coverImages1415    rw [← fixed, ← shifted] at disjointImages1416    rw [whole, ← fixed, ← shifted] at coverImages1417    symm at coverImages1418    have coverPieces : sweep(act, X, startsWith(2), representatives(act, freeGroup, X, c)) ∪ sweep(act, X, startsWith(3), representatives(act, freeGroup, X, c)) =1419      sweep(act, X, startsWith(2), representatives(act, freeGroup, X, c)) ∪ sweep(act, X, startsWith(3), representatives(act, freeGroup, X, c)) by rfl1420    exact Equidecomposable.of_two_pieces with action, unitIn, singleB, piece2, piece3,1421      disjoint23, coverPieces, disjointImages, coverImages14221423-- A decomposition under an action pulled back along a homomorphism is a1424-- decomposition under the original action, with the elements mapped.1425defgraph pushPair (φ H G X : Set) (p ∈ 𝒫(X) × H.carrier) : 𝒫(X) × G.carrier :=1426  (fst(p), φ(snd(p)))1427requires hom : φ : H →* G1428proof1429  obtain ⟨bound, S, hS, h, hh, shape⟩ := product.membership.forward with member1430  have function := GroupHom.function with hom1431  have image := FunctionBetween.apply_closed with function, hh1432  rw [shape, fst.pair, snd.pair]1433  exact product.pair with hS, image14341435section Transfer1436variable (act act2 G H X φ : Set)1437hypothesis action : act : G ↷ X1438hypothesis action2 : act2 : H ↷ X1439hypothesis hom : φ : H →* G1440hypothesis compatible : ∀ h ∈ H.carrier, ∀ x ∈ X, act2(h, x) = act(φ(h), x)14411442theorem pushPair.apply (S h : Set)1443  requires hS : S ∈ 𝒫(X)1444  requires hh : h ∈ H.carrier1445  shows pushPair(φ, H, G, X)((S, h)) = (S, φ(h))1446proof1447  have pair := product.pair at S, h, 𝒫(X), H.carrier with *1448  have value := pushPair.value at φ, H, G, X, (S, h) with hom, pair1449  rw [value, fst.pair, snd.pair]1450  rfl14511452theorem pushPair.moved (p : Set)1453  requires hp : p ∈ 𝒫(X) × H.carrier1454  shows moved(act, X, pushPair(φ, H, G, X)(p)) = moved(act2, X, p)1455proof1456  obtain ⟨bound, S, hS, h, hh, shape⟩ := product.membership.forward with hp1457  have bounded := powerset.membership_iff.forward with hS1458  have value := pushPair.apply with hom, hS, hh1459  have agree : ∀ x ∈ S, act(φ(h), x) = act2(h, x)1460    intros x hx1461    have xIn := bounded with x, hx1462    symm1463    exact compatible with h, hh, x, xIn1464  rw [shape, value, moved.value, moved.value]1465  exact translate.congr with agree14661467theorem Equidecomposable.of_hom (A B : Set)1468  requires equidecomposable : Equidecomposable(act2, H, X, A, B)1469  shows Equidecomposable(act, G, X, A, B)1470proof1471  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := equidecomposable1472  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces1473  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces1474  have function := pushPair.function at φ, H, G, X with hom1475  have finiteImage := Finite.function_image with function, finite, bounded1476  have members : ∀ q ∈ functionImage(pushPair(φ, H, G, X), F, 𝒫(X) × G.carrier), ∃ p ∈ F, q = pushPair(φ, H, G, X)(p)1477    intros q hq1478    obtain ⟨qIn, p, hp, equal⟩ := functionImage.membership.forward with hq1479    exact ⟨p, hp, equal⟩1480  have images : ∀ p ∈ F, pushPair(φ, H, G, X)(p) ∈ functionImage(pushPair(φ, H, G, X), F, 𝒫(X) × G.carrier)1481    intros p hp1482    have pIn := bounded with p, hp1483    have qIn := FunctionBetween.apply_closed with function, pIn1484    exact functionImage.membership.backward with ⟨qIn, p, hp, rfl⟩1485  have firsts : ∀ p ∈ F, fst(pushPair(φ, H, G, X)(p)) = fst(p)1486    intros p hp1487    have pIn := bounded with p, hp1488    obtain ⟨boundP, S, hS, h, hh, shape⟩ := product.membership.forward with pIn1489    have value := pushPair.apply with hom, hS, hh1490    rw [shape, value, fst.pair, fst.pair]1491    rfl1492  have moves : ∀ p ∈ F, moved(act, X, pushPair(φ, H, G, X)(p)) = moved(act2, X, p)1493    intros p hp1494    exact pushPair.moved with action, action2, hom, compatible, (bounded with p, hp)1495  have distinct : ∀ p ∈ F, ∀ q ∈ F, pushPair(φ, H, G, X)(p) ≠ pushPair(φ, H, G, X)(q) → p ≠ q1496    intros p hp q hq different same1497    apply different1498    rw same1499    rfl1500  have boundedImage := functionImage.subset at pushPair(φ, H, G, X), F, 𝒫(X) × G.carrier1501  witness functionImage(pushPair(φ, H, G, X), F, 𝒫(X) × G.carrier)1502  refine ⟨finiteImage, boundedImage, ?_, ?_⟩1503  . refine ⟨?_, ?_, ?_⟩1504    . intros q hq1505      obtain ⟨p, hp, equal⟩ := members with q, hq1506      have first := firsts with p, hp1507      rw [equal, first]1508      exact piecesBounded with p, hp1509    . intros x hx1510      obtain ⟨p, hp, member⟩ := piecesCover with x, hx1511      have first := firsts with p, hp1512      have image := images with p, hp1513      witness pushPair(φ, H, G, X)(p)1514      rw first1515      exact ⟨image, member⟩1516    . intros q hq r hr different1517      obtain ⟨p, hp, qEq⟩ := members with q, hq1518      obtain ⟨s, hs, rEq⟩ := members with r, hr1519      rw [qEq, rEq] at different1520      have apart := distinct with p, hp, s, hs, different1521      have firstP := firsts with p, hp1522      have firstS := firsts with s, hs1523      rw [qEq, rEq, firstP, firstS]1524      exact piecesDisjoint with p, hp, s, hs, apart1525  . refine ⟨?_, ?_, ?_⟩1526    . intros q hq1527      obtain ⟨p, hp, equal⟩ := members with q, hq1528      have move := moves with p, hp1529      rw [equal, move]1530      exact movedBounded with p, hp1531    . intros y hy1532      obtain ⟨p, hp, member⟩ := movedCover with y, hy1533      have move := moves with p, hp1534      have image := images with p, hp1535      witness pushPair(φ, H, G, X)(p)1536      rw move1537      exact ⟨image, member⟩1538    . intros q hq r hr different1539      obtain ⟨p, hp, qEq⟩ := members with q, hq1540      obtain ⟨s, hs, rEq⟩ := members with r, hr1541      rw [qEq, rEq] at different1542      have apart := distinct with p, hp, s, hs, different1543      have moveP := moves with p, hp1544      have moveS := moves with s, hs1545      rw [qEq, rEq, moveP, moveS]1546      exact movedDisjoint with p, hp, s, hs, apart15471548theorem Paradoxical.of_hom1549  requires paradoxical : Paradoxical(act2, H, X)1550  shows Paradoxical(act, G, X)1551proof1552  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ := paradoxical1553  witness A1554  witness B1555  refine ⟨boundedA, boundedB, disjoint, ?_, ?_⟩1556  . exact Equidecomposable.of_hom with action, action2, hom, compatible, firstA1557  . exact Equidecomposable.of_hom with action, action2, hom, compatible, secondB15581559end Transfer15601561-- The transfer theorem: a set with a free action of a group that contains1562-- the free group on two generators is paradoxical.1563theorem Paradoxical.of_free_action (act G X φ : Set)1564  requires action : act : G ↷ X1565  requires free : FreeAction(act, G, X)1566  requires hom : φ : freeGroup →* G1567  requires injective : InjectiveBetween(φ, reducedWords, G.carrier)1568  shows Paradoxical(act, G, X)1569proof1570  have pulled := pullback.action with action, hom1571  have pulledFree := pullback.free with action, hom, free, injective1572  have paradoxical := Paradoxical.of_free_freeGroup with pulled, pulledFree1573  have compatible : ∀ w ∈ Group.carrier(freeGroup), ∀ x ∈ X, pullback(act, G, X, φ)(w, x) = act(φ(w), x)1574    intros w hw x hx1575    rw freeGroup.carrierOf at hw1576    exact pullback.apply with action, hom, hw, hx1577  exact Paradoxical.of_hom with action, pulled, hom, compatible, paradoxical1578