Grace/Cumulus/Geometry/Absorption/Pieces.g17

Open in Workbench Download source

Imports

Absorb · Algebra.Group.Paradox · Rotation.Orthogonal

Declarations

Source

1-- The absorption theorem as an equidecomposability: for act : G ↷ X,2-- D ⊆ X, and ρ ∈ G with ρⁿ⁺¹(D) ∩ D = ∅ for every n, the sets X and X ∖ D3-- are equidecomposable under the action with the two pieces U = ⋃ₙ ρⁿ(D),4-- carried by ρ, and X ∖ U, carried by the unit; in particular the unit5-- sphere S² and S² ∖ D are equidecomposable under the rotation group SO36-- 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.Geometry.Absorption.Pieces12import Absorb13import Algebra.Group.Paradox14import Rotation.Orthogonal1516section Pieces17variable (act G X : Set)18hypothesis action : act : G ↷ X1920-- The image of a subset of X under g, in the two spellings.21theorem actImage.eq_translate (g : G) (A : Set)22  requires subset : A ⊆ X23  shows translate(act, X, g, A) = actImage(act, g, A)24proof25  ext y26  constructor27  . intro hy28    have data := translate.membership.forward with hy29    obtain ⟨inX, x, hx, shape⟩ := data30    apply actImage.membership.backward31    refine ⟨x, hx, ?_⟩32    symm33    exact shape34  . intro hy35    obtain ⟨x, hx, shape⟩ := actImage.membership.forward with hy36    have xIn := subset with x, hx37    have moved : g ·ₐ x ∈ X := Action.act_mem with action, xIn38    rw shape at moved39    symm at shape40    apply translate.membership.backward41    exact ⟨moved, x, hx, shape⟩4243theorem translate.unit (A : Set)44  requires subset : A ⊆ X45  shows translate(act, X, G.one, A) = A46proof47  have group := Action.group with action48  ext y49  constructor50  . intro hy51    obtain ⟨inX, x, hx, shape⟩ := translate.membership.forward with hy52    have fixed : G.one ·ₐ x = x := one_act with action, (subset with x, hx)53    rw [shape, fixed]54    exact hx55  . intro hy56    have yIn := subset with y, hy57    have fixed : G.one ·ₐ y = y := one_act with action, yIn58    apply translate.membership.backward59    refine ⟨yIn, y, hy, ?_⟩60    rw fixed61    rfl6263-- The absorption theorem: X and X ∖ D are equidecomposable.64theorem absorption.equidecomposable (ρ : G) (D : Set)65  requires subset : D ⊆ X66  requires separated : ∀ n ∈ ℕ, Disjoint(actImage(act, ρ ^ (n + 1), D), D)67  shows Equidecomposable(act, G, X, X, X ∖ D)68proof69  have group := Action.group with action70  have unitIn : G.one ∈ G := Group.one_mem with group71  have rhoIn : ρ ∈ G by assumption72  have orbitSubset : forwardOrbit(act, G, ρ, D) ⊆ X := forwardOrbit.subset with *73  have orbitContains : D ⊆ forwardOrbit(act, G, ρ, D) := forwardOrbit.contains with *74  have carried := forwardOrbit.image with action, subset, separated75  have restSubset := difference.subset_left at X, forwardOrbit(act, G, ρ, D)76  have disjoint := Disjoint.difference_right at X, forwardOrbit(act, G, ρ, D)77  have cover := difference.union2_of_subset with orbitSubset78  have movedOrbit : translate(act, X, ρ, forwardOrbit(act, G, ρ, D)) = actImage(act, ρ, forwardOrbit(act, G, ρ, D)) :=79    actImage.eq_translate with *80  have movedRest : translate(act, X, G.one, X ∖ forwardOrbit(act, G, ρ, D)) = X ∖ forwardOrbit(act, G, ρ, D) :=81    translate.unit with *82  have disjointImages : Disjoint(translate(act, X, ρ, forwardOrbit(act, G, ρ, D)),83      translate(act, X, G.one, X ∖ forwardOrbit(act, G, ρ, D)))84    rw [movedOrbit, movedRest, carried]85    apply Disjoint.iff.backward86    intros y hy hy287    obtain ⟨inOrbit, notInD⟩ := difference.membership.forward with hy88    obtain ⟨inX, notInOrbit⟩ := difference.membership.forward with hy289    exact notInOrbit with inOrbit90  have coverImages : translate(act, X, ρ, forwardOrbit(act, G, ρ, D)) ∪ translate(act, X, G.one, X ∖ forwardOrbit(act, G, ρ, D)) = X ∖ D91    rw [movedOrbit, movedRest, carried]92    ext y93    constructor94    . intro hy95      have sides := union2.membership.forward with hy96      cases sides with inLeft | inRight97      . obtain ⟨inOrbit, notInD⟩ := difference.membership.forward with inLeft98        have inX := orbitSubset with y, inOrbit99        exact difference.membership.backward with ⟨inX, notInD⟩100      . obtain ⟨inX, notInOrbit⟩ := difference.membership.forward with inRight101        have notInD : ¬(y ∈ D)102          intro inD103          exact notInOrbit with (orbitContains with y, inD)104        exact difference.membership.backward with ⟨inX, notInD⟩105    . intro hy106      obtain ⟨inX, notInD⟩ := difference.membership.forward with hy107      have alternatives : y ∈ forwardOrbit(act, G, ρ, D) ∨ ¬(y ∈ forwardOrbit(act, G, ρ, D)) by tauto108      apply union2.membership.backward109      cases alternatives with inOrbit | notInOrbit110      . left111        exact difference.membership.backward with ⟨inOrbit, notInD⟩112      . right113        exact difference.membership.backward with ⟨inX, notInOrbit⟩114  exact Equidecomposable.of_two_pieces at act, G, X, X, X ∖ D,115    forwardOrbit(act, G, ρ, D), X ∖ forwardOrbit(act, G, ρ, D), ρ, G.one with116    action, rhoIn, unitIn, orbitSubset, restSubset, disjoint, cover,117    disjointImages, coverImages118119end Pieces120121-- Absorbing a set into the sphere: for D ⊆ S² and a rotation ρ with122-- ρⁿ⁺¹(D) ∩ D = ∅ for every n, S² and S² ∖ D are SO3-equidecomposable.123theorem sphere.absorb (ρ D : Set)124  requires rotation : ρ ∈ Group.carrier(SO3)125  requires subset : D ⊆ S²126  requires separated : ∀ n ∈ ℕ,127    Disjoint(actImage(sphereAction, groupPow(SO3, ρ, n + 1), D), D)128  shows Equidecomposable(sphereAction, SO3, S², S², S² ∖ D)129proof130  have action := sphereAction.action131  exact absorption.equidecomposable with action, rotation, subset, separated132