Grace/Cumulus/Algebra/Group/Paradox/Transfer.g17

Open in Workbench Download source

Imports

Algebra.Group.Paradox · Algebra.Group.Action.Restrict

Declarations

Source

1-- Decompositions transfer between a set and an invariant subset, so a set2-- equidecomposable with a paradoxical invariant subset is paradoxical3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Algebra.Group.Paradox.Transfer9import Algebra.Group.Paradox10import Algebra.Group.Action.Restrict1112section Transfer13variable (act G X : Set)14hypothesis action : act : G ↷ X1516-- The image of a subset of Y under g is the same under the restricted17-- action, and so is every moved piece.18theorem translate.restrict (Y g S : Set)19  requires subset : Y ⊆ X20  requires invariant : ∀ g ∈ G.carrier, ∀ y ∈ Y, g ·ₐ y ∈ Y21  requires hg : g ∈ G.carrier22  requires bounded : S ⊆ Y23  shows translate(act, X, g, S) = translate(restrictAction(act, G, Y), Y, g, S)24proof25  ext y26  constructor27  . intro hy28    obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with hy29    have xIn := bounded with x, hx30    have value := restrictAction.apply with action, subset, invariant, hg, xIn31    have moved := invariant with g, hg, x, xIn32    rw ← equal at moved33    rw ← value at equal34    exact translate.membership.backward with ⟨moved, x, hx, equal⟩35  . intro hy36    obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with hy37    have xIn := bounded with x, hx38    have value := restrictAction.apply with action, subset, invariant, hg, xIn39    rw value at equal40    have inX := subset with y, yIn41    exact translate.membership.backward with ⟨inX, x, hx, equal⟩4243theorem moved.restrict (Y p : Set)44  requires subset : Y ⊆ X45  requires invariant : ∀ g ∈ G.carrier, ∀ y ∈ Y, g ·ₐ y ∈ Y46  requires hp : p ∈ 𝒫(Y) × G.carrier47  shows moved(act, X, p) = moved(restrictAction(act, G, Y), Y, p)48proof49  obtain ⟨bound, S, hS, g, hg, shape⟩ := product.membership.forward with hp50  have bounded := powerset.membership_iff.forward with hS51  rw [shape, moved.value, moved.value]52  exact translate.restrict with action, subset, invariant, hg, bounded5354-- A decomposition under the restricted action is a decomposition under55-- the action on X.56theorem Equidecomposable.of_restrict (Y A B : Set)57  requires subset : Y ⊆ X58  requires invariant : ∀ g ∈ G.carrier, ∀ y ∈ Y, g ·ₐ y ∈ Y59  requires boundedA : A ⊆ Y60  requires boundedB : B ⊆ Y61  requires restricted : Equidecomposable(restrictAction(act, G, Y), G, Y, A, B)62  shows Equidecomposable(act, G, X, A, B)63proof64  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := restricted65  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces66  have powersets := powerset.monotone with subset67  have pairs : 𝒫(Y) × G.carrier ⊆ 𝒫(X) × G.carrier :=68    product.monotone with powersets, (Subset.reflexive at G.carrier)69  have boundedX := Subset.transitive with bounded, pairs70  have moves : ∀ p ∈ F,71      moved(act, X, p) = moved(restrictAction(act, G, Y), Y, p)72    intros p hp73    exact moved.restrict with action, subset, invariant, (bounded with p, hp)74  witness F75  refine ⟨finite, boundedX, pieces, ?_⟩76  refine ⟨?_, ?_, ?_⟩77  . intros p hp78    have move := moves with p, hp79    rw move80    exact movedBounded with p, hp81  . intros y hy82    obtain ⟨p, hp, member⟩ := movedCover with y, hy83    have move := moves with p, hp84    witness p85    rw move86    exact ⟨hp, member⟩87  . intros p hp q hq different88    have moveP := moves with p, hp89    have moveQ := moves with q, hq90    rw [moveP, moveQ]91    exact movedDisjoint with p, hp, q, hq, different9293-- A paradoxical invariant subset Y of X has two disjoint subsets each94-- equidecomposable with Y under the action on X.95theorem Paradoxical.of_restrict (Y : Set)96  requires subset : Y ⊆ X97  requires invariant : ∀ g ∈ G.carrier, ∀ y ∈ Y, g ·ₐ y ∈ Y98  requires paradoxical : Paradoxical(restrictAction(act, G, Y), G, Y)99  shows ∃ A, ∃ B, A ⊆ Y ∧ B ⊆ Y ∧ Disjoint(A, B) ∧100    Equidecomposable(act, G, X, A, Y) ∧ Equidecomposable(act, G, X, B, Y)101proof102  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ :=103    paradoxical104  have whole := Subset.reflexive at Y105  witness A106  witness B107  refine ⟨boundedA, boundedB, disjoint, ?_, ?_⟩108  . exact Equidecomposable.of_restrict with109      action, subset, invariant, boundedA, whole, firstA110  . exact Equidecomposable.of_restrict with111      action, subset, invariant, boundedB, whole, secondB112113-- A set equidecomposable with a subset carrying two disjoint pieces each114-- equidecomposable with that subset is paradoxical.115theorem Paradoxical.of_equidecomposable (Y : Set)116  requires subset : Y ⊆ X117  requires whole : Equidecomposable(act, G, X, X, Y)118  requires pieces : ∃ A, ∃ B, A ⊆ Y ∧ B ⊆ Y ∧ Disjoint(A, B) ∧119    Equidecomposable(act, G, X, A, Y) ∧ Equidecomposable(act, G, X, B, Y)120  shows Paradoxical(act, G, X)121proof122  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ := pieces123  have back : Equidecomposable(act, G, X, Y, X) :=124    Equidecomposable.symmetric with action, whole125  have inA := Subset.transitive with boundedA, subset126  have inB := Subset.transitive with boundedB, subset127  witness A128  witness B129  refine ⟨inA, inB, disjoint, ?_, ?_⟩130  . exact Equidecomposable.transitive with action, firstA, back131  . exact Equidecomposable.transitive with action, secondB, back132133-- Conversely, a decomposition in X of subsets of Y whose moved pieces134-- stay inside Y is a decomposition under the restricted action; the135-- restriction need not be an action for this (restrictAction.value).136theorem translate.restrict_of_bounded (Y g S : Set)137  requires subset : Y ⊆ X138  requires hg : g ∈ G.carrier139  requires bounded : S ⊆ Y140  requires image : translate(act, X, g, S) ⊆ Y141  shows translate(restrictAction(act, G, Y), Y, g, S) = translate(act, X, g, S)142proof143  ext y144  constructor145  . intro hy146    obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with hy147    have xIn := bounded with x, hx148    have value := restrictAction.value with action, subset, hg, xIn149    rw value at equal150    have inX := subset with y, yIn151    exact translate.membership.backward with ⟨inX, x, hx, equal⟩152  . intro hy153    have yIn := image with y, hy154    obtain ⟨inX, x, hx, equal⟩ := translate.membership.forward with hy155    have xIn := bounded with x, hx156    have value := restrictAction.value with action, subset, hg, xIn157    rw ← value at equal158    exact translate.membership.backward with ⟨yIn, x, hx, equal⟩159160theorem moved.restrict_of_bounded (Y p : Set)161  requires subset : Y ⊆ X162  requires hp : p ∈ 𝒫(X) × G.carrier163  requires piece : fst(p) ⊆ Y164  requires image : moved(act, X, p) ⊆ Y165  shows moved(restrictAction(act, G, Y), Y, p) = moved(act, X, p)166proof167  obtain ⟨bound, S, hS, g, hg, shape⟩ := product.membership.forward with hp168  rw [shape, fst.pair] at piece169  rw [shape, moved.value] at image170  rw [shape, moved.value, moved.value]171  exact translate.restrict_of_bounded with action, subset, hg, piece, image172173theorem Equidecomposable.to_restrict (Y A B : Set)174  requires subset : Y ⊆ X175  requires boundedA : A ⊆ Y176  requires boundedB : B ⊆ Y177  requires equidecomposable : Equidecomposable(act, G, X, A, B)178  shows Equidecomposable(restrictAction(act, G, Y), G, Y, A, B)179proof180  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := equidecomposable181  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces182  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces183  have boundedY : F ⊆ 𝒫(Y) × G.carrier184    intros p hp185    obtain ⟨bound, S, hS, g, hg, shape⟩ :=186        product.membership.forward with (bounded with p, hp)187    have piece := piecesBounded with p, hp188    rw [shape, fst.pair] at piece189    have inY := powerset.membership_iff.backward with (Subset.transitive190        with piece, boundedA)191    rw shape192    exact product.pair with inY, hg193  have moves : ∀ p ∈ F,194      moved(restrictAction(act, G, Y), Y, p) = moved(act, X, p)195    intros p hp196    have piece := Subset.transitive with (piecesBounded with p, hp), boundedA197    have image := Subset.transitive with (movedBounded with p, hp), boundedB198    exact moved.restrict_of_bounded with action, subset, (bounded with p, hp),199        piece, image200  witness F201  refine ⟨finite, boundedY, pieces, ?_⟩202  refine ⟨?_, ?_, ?_⟩203  . intros p hp204    have move := moves with p, hp205    rw move206    exact movedBounded with p, hp207  . intros y hy208    obtain ⟨p, hp, member⟩ := movedCover with y, hy209    have move := moves with p, hp210    witness p211    rw move212    exact ⟨hp, member⟩213  . intros p hp q hq different214    have moveP := moves with p, hp215    have moveQ := moves with q, hq216    rw [moveP, moveQ]217    exact movedDisjoint with p, hp, q, hq, different218219theorem Paradoxical.to_restrict (Y : Set)220  requires subset : Y ⊆ X221  requires pieces : ∃ A, ∃ B, A ⊆ Y ∧ B ⊆ Y ∧ Disjoint(A, B) ∧222    Equidecomposable(act, G, X, A, Y) ∧ Equidecomposable(act, G, X, B, Y)223  shows Paradoxical(restrictAction(act, G, Y), G, Y)224proof225  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ := pieces226  have whole := Subset.reflexive at Y227  witness A228  witness B229  refine ⟨boundedA, boundedB, disjoint, ?_, ?_⟩230  . exact Equidecomposable.to_restrict with action, subset, boundedA, whole,231      firstA232  . exact Equidecomposable.to_restrict with action, subset, boundedB, whole,233      secondB234235end Transfer236