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

Open in Workbench Download source

Imports

Algebra.Group.Paradox

Declarations

Source

1-- Piece maps: the function a decomposition realises, carrying each point2-- of a piece by the element of that piece. It is an injection of the3-- decomposed set whose image is the union of the moved pieces, and4-- cutting the pieces down to a subset decomposes the subset onto its5-- image under the piece map6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Algebra.Group.Paradox.PieceMaps12import Algebra.Group.Paradox1314-- The piece map of a family F: x is carried to act(g, x) when x lies in15-- the piece of (S, g).16def pieceMap (act X F : Set) : Set :=17  { q ∈ X × X | ∃ p ∈ F, fst(q) ∈ fst(p) ∧ snd(q) = act(snd(p), fst(q)) }1819-- Every piece cut down to C, carried by the same element.20defgraph cutPair (X G C : Set) (p ∈ 𝒫(X) × Group.carrier(G)) :21    𝒫(X) × Group.carrier(G) :=22  (fst(p) ∩ C, snd(p))23proof24  obtain ⟨bound, S, hS, g, hg, shape⟩ := product.membership.forward with member25  have subset := powerset.membership_iff.forward with hS26  have cut : S ∩ C ⊆ X :=27    Subset.transitive with (intersection.subset_left at S, C), subset28  have cutIn := powerset.membership_iff.backward with cut29  rw [shape, fst.pair, snd.pair]30  exact product.pair with cutIn, hg3132theorem pieceMap.relates (act X F x y : Set)33  shows relates(pieceMap(act, X, F), x, y) ↔34    (x, y) ∈ X × X ∧ ∃ p ∈ F, x ∈ fst(p) ∧ y = act(snd(p), x)35proof36  unfold relates37  constructor38  . intro h39    obtain ⟨pair, p, hp, inP, equal⟩ := pieceMap.membership.forward with h40    rw fst.pair at inP41    rw [fst.pair, snd.pair] at equal42    exact ⟨pair, p, hp, inP, equal⟩43  . intro h44    obtain ⟨pair, p, hp, inP, equal⟩ := h45    apply pieceMap.membership.backward46    refine ⟨pair, p, hp, ?_, ?_⟩47    . rw fst.pair48      exact inP49    . rw [fst.pair, snd.pair]50      exact equal5152-- The two coordinates of a piece: a subset of X and a group element.53theorem piece.parts (G X p : Set)54  requires hp : p ∈ 𝒫(X) × Group.carrier(G)55  shows fst(p) ⊆ X ∧ snd(p) ∈ Group.carrier(G)56proof57  obtain ⟨bound, S, hS, g, hg, shape⟩ := product.membership.forward with hp58  have subset := powerset.membership_iff.forward with hS59  rw [shape, fst.pair, snd.pair]60  exact ⟨subset, hg⟩6162theorem cutPair.shape (act G X C p : Set)63  requires hp : p ∈ 𝒫(X) × Group.carrier(G)64  shows fst(cutPair(X, G, C)(p)) = fst(p) ∩ C ∧65    moved(act, X, cutPair(X, G, C)(p)) = translate(act, X, snd(p), fst(p) ∩ C)66proof67  have value := cutPair.value at X, G, C, p with hp68  rw [value, fst.pair, moved.value]69  exact ⟨rfl, rfl⟩7071section PieceMaps72variable (act G X : Set)73hypothesis action : act : G ↷ X7475theorem pieceMap.relates_of (F p x : Set)76  requires bounded : F ⊆ 𝒫(X) × G.carrier77  requires hp : p ∈ F78  requires hx : x ∈ fst(p)79  shows relates(pieceMap(act, X, F), x, act(snd(p), x))80proof81  obtain ⟨subset, gIn⟩ := piece.parts with (bounded with p, hp)82  have xIn := subset with x, hx83  have moved : snd(p) ·ₐ x ∈ X := Action.act_mem with action, gIn, xIn84  have pair := product.pair with xIn, moved85  exact pieceMap.relates.backward with ⟨pair, p, hp, hx, rfl⟩8687-- The piece map is a function on the decomposed set.88theorem pieceMap.function (A F : Set)89  requires bounded : F ⊆ 𝒫(X) × G.carrier90  requires pieces : Pieces(A, F)91  shows pieceMap(act, X, F) : A → X92proof93  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces94  refine ⟨?_, ?_, ?_⟩95  . intros q hq96    obtain ⟨qIn, p, hp, inPiece, equal⟩ := pieceMap.membership.forward with hq97    obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with qIn98    rw [shape, fst.pair] at inPiece99    have xIn := piecesBounded with p, hp, x, inPiece100    rw shape101    exact product.pair with xIn, hy102  . intros x y hxy z hxz103    obtain ⟨pairY, p, hp, inP, yEq⟩ := pieceMap.relates.forward with hxy104    obtain ⟨pairZ, q, hq, inQ, zEq⟩ := pieceMap.relates.forward with hxz105    have split : p = q ∨ p ≠ q by tauto106    cases split with same | apart107    . rw [yEq, zEq, same]108      rfl109    . exfalso110      have disjoint := piecesDisjoint with p, hp, q, hq, apart111      have absent := Disjoint.iff.forward with disjoint112      exact absent with x, inP, inQ113  . intros x hx114    obtain ⟨p, hp, inP⟩ := piecesCover with x, hx115    obtain ⟨subset, gIn⟩ := piece.parts with (bounded with p, hp)116    have xIn := subset with x, inP117    have moved : snd(p) ·ₐ x ∈ X := Action.act_mem with action, gIn, xIn118    have related := pieceMap.relates_of with action, bounded, hp, inP119    witness act(snd(p), x)120    exact ⟨moved, related⟩121122theorem pieceMap.apply (A F p x : Set)123  requires bounded : F ⊆ 𝒫(X) × G.carrier124  requires pieces : Pieces(A, F)125  requires hp : p ∈ F126  requires hx : x ∈ fst(p)127  shows pieceMap(act, X, F)(x) = snd(p) ·ₐ x128proof129  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces130  have function := pieceMap.function with action, bounded, pieces131  have xIn := piecesBounded with p, hp, x, hx132  have related := pieceMap.relates_of with action, bounded, hp, hx133  exact FunctionBetween.apply_value with function, xIn, related134135-- The value at a point of a piece lies in the moved piece.136theorem pieceMap.apply_mem (A F p x : Set)137  requires bounded : F ⊆ 𝒫(X) × G.carrier138  requires pieces : Pieces(A, F)139  requires hp : p ∈ F140  requires hx : x ∈ fst(p)141  shows pieceMap(act, X, F)(x) ∈ moved(act, X, p)142proof143  obtain ⟨subset, gIn⟩ := piece.parts with (bounded with p, hp)144  have value := pieceMap.apply with action, bounded, pieces, hp, hx145  have member : snd(p) ·ₐ x ∈ translate(act, X, snd(p), fst(p)) :=146    translate.act_mem with action, subset, hx147  rw [value, moved.unfold]148  exact member149150-- With the moved pieces inside B, the piece map lands in B.151theorem pieceMap.codomain (A B F : Set)152  requires bounded : F ⊆ 𝒫(X) × G.carrier153  requires pieces : Pieces(A, F)154  requires movedBounded : ∀ p ∈ F, moved(act, X, p) ⊆ B155  shows pieceMap(act, X, F) : A → B156proof157  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces158  have function := pieceMap.function with action, bounded, pieces159  apply FunctionBetween.codomain_of_values with function160  intros x hx161  obtain ⟨p, hp, inP⟩ := piecesCover with x, hx162  have member := pieceMap.apply_mem with action, bounded, pieces, hp, inP163  exact movedBounded with p, hp, pieceMap(act, X, F)(x), member164165-- Disjoint moved pieces make the piece map injective.166theorem pieceMap.injective (A B F : Set)167  requires bounded : F ⊆ 𝒫(X) × G.carrier168  requires pieces : Pieces(A, F)169  requires movedBounded : ∀ p ∈ F, moved(act, X, p) ⊆ B170  requires movedDisjoint : ∀ p q ∈ F, p ≠ q →171    Disjoint(moved(act, X, p), moved(act, X, q))172  shows InjectiveBetween(pieceMap(act, X, F), A, B)173proof174  have group := Action.group with action175  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces176  have function := pieceMap.codomain with action, bounded, pieces, movedBounded177  apply Injective.of_pointwise with function178  intros x hx y hy same179  obtain ⟨p, hp, inP⟩ := piecesCover with x, hx180  obtain ⟨q, hq, inQ⟩ := piecesCover with y, hy181  have memberX := pieceMap.apply_mem with action, bounded, pieces, hp, inP182  have memberY := pieceMap.apply_mem with action, bounded, pieces, hq, inQ183  have valueX := pieceMap.apply with action, bounded, pieces, hp, inP184  have valueY := pieceMap.apply with action, bounded, pieces, hq, inQ185  have split : p = q ∨ p ≠ q by tauto186  cases split with equal | apart187  . obtain ⟨subset, gIn⟩ := piece.parts with (bounded with p, hp)188    have xIn := subset with x, inP189    rw ← equal at inQ190    have yIn := subset with y, inQ191    rw [valueX, valueY] at same192    rw ← equal at same193    have backX : snd(p)⁻¹ ·ₐ snd(p) ·ₐ x = x := inv_act_cancel with *194    have backY : snd(p)⁻¹ ·ₐ snd(p) ·ₐ y = y := inv_act_cancel with *195    have step : snd(p)⁻¹ ·ₐ snd(p) ·ₐ x = snd(p)⁻¹ ·ₐ snd(p) ·ₐ y196      rw same197      rfl198    rw [backX, backY] at step199    exact step200  . exfalso201    have disjoint := movedDisjoint with p, hp, q, hq, apart202    have absent := Disjoint.iff.forward with disjoint203    rw same at memberX204    exact absent with pieceMap(act, X, F)(y), memberX, memberY205206-- Moved pieces covering B make the piece map onto B.207theorem pieceMap.surjective (A B F : Set)208  requires bounded : F ⊆ 𝒫(X) × G.carrier209  requires pieces : Pieces(A, F)210  requires movedPieces : MovedPieces(act, X, B, F)211  shows SurjectiveBetween(pieceMap(act, X, F), A, B)212proof213  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces214  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces215  have function := pieceMap.codomain with action, bounded, pieces, movedBounded216  constructor217  . exact function218  . intros y hy219    obtain ⟨p, hp, member⟩ := movedCover with y, hy220    rw moved.unfold at member221    obtain ⟨yIn, x, hx, yEq⟩ := translate.membership.forward with member222    have xIn := piecesBounded with p, hp, x, hx223    have related := pieceMap.relates_of with action, bounded, hp, hx224    witness x225    rw yEq226    exact ⟨xIn, related⟩227228theorem pieceMap.bijective (A B F : Set)229  requires bounded : F ⊆ 𝒫(X) × G.carrier230  requires pieces : Pieces(A, F)231  requires movedPieces : MovedPieces(act, X, B, F)232  shows BijectiveBetween(pieceMap(act, X, F), A, B)233proof234  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces235  constructor236  . exact pieceMap.injective with action, bounded, pieces, movedBounded,237      movedDisjoint238  . exact pieceMap.surjective with action, bounded, pieces, movedPieces239240-- Restriction: cutting the pieces down to C ⊆ A decomposes C onto its241-- image under the piece map.242theorem Equidecomposable.restrict (A B C F : Set)243  requires finite : Finite(F)244  requires bounded : F ⊆ 𝒫(X) × G.carrier245  requires pieces : Pieces(A, F)246  requires movedBounded : ∀ p ∈ F, moved(act, X, p) ⊆ B247  requires movedDisjoint : ∀ p q ∈ F, p ≠ q →248    Disjoint(moved(act, X, p), moved(act, X, q))249  requires subset : C ⊆ A250  shows Equidecomposable(act, G, X, C, functionImage(pieceMap(act, X, F), C, B))251proof252  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces253  have cutFunction := cutPair.function at X, G, C254  have cuts : ∀ p ∈ F, fst(cutPair(X, G, C)(p)) = fst(p) ∩ C ∧255      moved(act, X, cutPair(X, G, C)(p)) = translate(act, X, snd(p), fst(p) ∩ C)256    intros p hp257    exact cutPair.shape at act, G, X, C, p with (bounded with p, hp)258  have movedCut : ∀ p ∈ F, moved(act, X, cutPair(X, G, C)(p)) ⊆ moved(act, X, p)259    intros p hp260    obtain ⟨first, second⟩ := cuts with p, hp261    have inner := intersection.subset_left at fst(p), C262    rw [second, moved.unfold]263    exact translate.monotone at act, X, snd(p), fst(p) ∩ C, fst(p) with inner264  apply Equidecomposable.of_reindex with cutFunction, finite, bounded265  . intros p hp266    obtain ⟨first, second⟩ := cuts with p, hp267    rw first268    exact intersection.subset_right at fst(p), C269  . intros x hx270    obtain ⟨p, hp, inP⟩ := piecesCover with x, (subset with x, hx)271    obtain ⟨first, second⟩ := cuts with p, hp272    have both := intersection.membership.backward at fst(p), C, x with ⟨inP, hx⟩273    witness p274    rw first275    exact ⟨hp, both⟩276  . intros p hp q hq different277    obtain ⟨firstP, secondP⟩ := cuts with p, hp278    obtain ⟨firstQ, secondQ⟩ := cuts with q, hq279    have disjoint := piecesDisjoint with p, hp, q, hq, different280    have innerP := intersection.subset_left at fst(p), C281    have innerQ := intersection.subset_left at fst(q), C282    have step := Disjoint.of_subset_left with disjoint, innerP283    rw [firstP, firstQ]284    exact Disjoint.of_subset_right with step, innerQ285  . intros p hp286    obtain ⟨first, second⟩ := cuts with p, hp287    rw second288    intros y hy289    obtain ⟨yIn, x, hx, yEq⟩ := translate.membership.forward with hy290    obtain ⟨inP, inC⟩ := intersection.membership.forward with hx291    have value := pieceMap.apply with action, bounded, pieces, hp, inP292    have member := pieceMap.apply_mem with action, bounded, pieces, hp, inP293    rw [value, ← yEq] at member294    have inB := movedBounded with p, hp, y, member295    apply functionImage.membership.backward296    refine ⟨inB, x, inC, ?_⟩297    rw [value, yEq]298    rfl299  . intros y hy300    obtain ⟨inB, x, hx, yEq⟩ := functionImage.membership.forward with hy301    obtain ⟨p, hp, inP⟩ := piecesCover with x, (subset with x, hx)302    obtain ⟨first, second⟩ := cuts with p, hp303    obtain ⟨subsetP, gIn⟩ := piece.parts with (bounded with p, hp)304    have value := pieceMap.apply with action, bounded, pieces, hp, inP305    have inner := intersection.subset_left at fst(p), C306    have cutBounded : fst(p) ∩ C ⊆ X := Subset.transitive with inner, subsetP307    have both := intersection.membership.backward at fst(p), C, x with ⟨inP, hx⟩308    have member : snd(p) ·ₐ x ∈ translate(act, X, snd(p), fst(p) ∩ C) :=309      translate.act_mem with action, cutBounded, both310    witness p311    rw [second, yEq, value]312    exact ⟨hp, member⟩313  . intros p hp q hq different314    have disjoint := movedDisjoint with p, hp, q, hq, different315    have step := Disjoint.of_subset_left with disjoint, (movedCut with p, hp)316    exact Disjoint.of_subset_right with step, (movedCut with q, hq)317318end PieceMaps319