Grace/Cumulus/Geometry/Absorption/Absorb.g17

Open in Workbench Download source

Imports

Algebra.Group.Action · Algebra.Group.Pow

Declarations

Source

1-- Absorbing a set into its forward orbit: for an action act : G ↷ X, a2-- set D ⊆ X, and ρ ∈ G whose positive powers carry D off itself, the3-- forward orbit U = ⋃ₙ ρⁿ(D) satisfies ρ(U) = U ∖ D, so X and X ∖ D are4-- equidecomposable with the two pieces U and X ∖ U5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Geometry.Absorption.Absorb11import Algebra.Group.Action12import Algebra.Group.Pow1314-- The image of a set under the action of one group element.15def actImage (act g A : Set) : Set := { call2(act, g, x) | x ∈ A }1617-- The stages ρⁿ(D) and their union, the forward orbit of D under ρ.18def orbitStages (act G ρ D : Set) : Set :=19  { actImage(act, groupPow(G, ρ, n), D) | n ∈ ℕ }20def forwardOrbit (act G ρ D : Set) : Set := ⋃(orbitStages(act, G, ρ, D))2122theorem forwardOrbit.graph (act G ρ D : Set)23  shows forwardOrbit(act, G, ρ, D) = ⋃(orbitStages(act, G, ρ, D))24proof25  simp [forwardOrbit]2627theorem forwardOrbit.membership (act G ρ D y : Set)28  shows y ∈ forwardOrbit(act, G, ρ, D) ↔29    ∃ n ∈ ℕ, y ∈ actImage(act, groupPow(G, ρ, n), D)30proof31  rw forwardOrbit.graph32  constructor33  . intro h34    obtain ⟨A, hA, inA⟩ := union.membership.forward with h35    obtain ⟨n, hn, shape⟩ := orbitStages.membership.forward with hA36    refine ⟨n, hn, ?_⟩37    rw shape38    exact inA39  . intro h40    obtain ⟨n, hn, inStage⟩ := h41    have stageIn : actImage(act, groupPow(G, ρ, n), D) ∈ orbitStages(act, G, ρ, D)42      apply orbitStages.membership.backward43      exact ⟨n, hn, rfl⟩44    exact union.contains with stageIn, inStage4546section Absorption47variable (act G X : Set)48hypothesis action : act : G ↷ X4950theorem actImage.subset (g : G) (A : Set)51  requires subset : A ⊆ X52  shows actImage(act, g, A) ⊆ X53proof54  intros y hy55  obtain ⟨x, hx, shape⟩ := actImage.membership.forward with hy56  have xIn := subset with x, hx57  have moved : g ·ₐ x ∈ X := Action.act_mem with action, xIn58  rw ← shape59  exact moved6061theorem actImage.contains (g : G) (A x : Set)62  requires hx : x ∈ A63  shows g ·ₐ x ∈ actImage(act, g, A)64proof65  exact actImage.membership.backward with ⟨x, hx, rfl⟩6667theorem forwardOrbit.subset (ρ : G) (D : Set)68  requires subset : D ⊆ X69  shows forwardOrbit(act, G, ρ, D) ⊆ X70proof71  have group := Action.group with action72  intros y hy73  obtain ⟨n, hn, inStage⟩ := forwardOrbit.membership.forward with hy74  have natural := omega.natural with hn75  have powerIn : ρ ^ n ∈ G := Group.pow_mem with group76  have bounded : actImage(act, ρ ^ n, D) ⊆ X := actImage.subset with *77  exact bounded with y, inStage7879theorem forwardOrbit.contains (ρ : G) (D : Set)80  requires subset : D ⊆ X81  shows D ⊆ forwardOrbit(act, G, ρ, D)82proof83  have group := Action.group with action84  intros d hd85  have dIn := subset with d, hd86  have unit : ρ ^ 0 = G.one := pow_zero with group87  have fixed : G.one ·ₐ d = d := one_act with action, dIn88  have zeroIn : 0 ∈ ℕ by typecheck89  apply forwardOrbit.membership.backward90  refine ⟨0, zeroIn, ?_⟩91  apply actImage.membership.backward92  refine ⟨d, hd, ?_⟩93  rw unit94  exact fixed9596-- The forward orbit is carried by ρ onto itself minus D: ρ(ρⁿ(D)) is97-- ρⁿ⁺¹(D), and the stages beyond the first are the ones off D.98theorem forwardOrbit.image (ρ : G) (D : Set)99  requires subset : D ⊆ X100  requires separated : ∀ n ∈ ℕ, Disjoint(actImage(act, ρ ^ (n + 1), D), D)101  shows actImage(act, ρ, forwardOrbit(act, G, ρ, D)) =102    forwardOrbit(act, G, ρ, D) ∖ D103proof104  have group := Action.group with action105  ext y106  constructor107  . intro hy108    apply difference.membership.backward109    obtain ⟨x, hx, shape⟩ := actImage.membership.forward with hy110    obtain ⟨n, hn, inStage⟩ := forwardOrbit.membership.forward with hx111    have natural := omega.natural with hn112    obtain ⟨d, hd, moved⟩ := actImage.membership.forward with inStage113    have dIn := subset with d, hd114    have powerIn : ρ ^ n ∈ G := Group.pow_mem with group115    have step : ρ ^ (n + 1) = ρ * ρ ^ n := pow_succ_left with group116    have composed : (ρ * ρ ^ n) ·ₐ d = ρ ·ₐ ρ ^ n ·ₐ d := mul_act with action, dIn117    have nextShape : y = ρ ^ (n + 1) ·ₐ d118      rw [step, composed, moved, shape]119      rfl120    have nextIn : y ∈ actImage(act, ρ ^ (n + 1), D)121      rw nextShape122      exact actImage.contains with hd123    have succIn : n + 1 ∈ ℕ by typecheck124    constructor125    . exact forwardOrbit.membership.backward with ⟨n + 1, succIn, nextIn⟩126    . have disjoint := separated with n, natural127      have apart := Disjoint.iff.forward with disjoint128      exact apart with y, nextIn129  . intro hy130    obtain ⟨inOrbit, notInD⟩ := difference.membership.forward with hy131    obtain ⟨n, hn, inStage⟩ := forwardOrbit.membership.forward with inOrbit132    have natural := omega.natural with hn133    obtain ⟨d, hd, moved⟩ := actImage.membership.forward with inStage134    have dIn := subset with d, hd135    have cases := natural.zero_or_successor at n with natural136    cases cases with zero | positive137    . exfalso138      have unit : ρ ^ 0 = G.one := pow_zero with group139      have fixed : G.one ·ₐ d = d := one_act with action, dIn140      rw [zero, unit, fixed] at moved141      rw ← moved at notInD142      exact notInD with hd143    . obtain ⟨k, naturalK, shape⟩ := positive144      have powerIn : ρ ^ k ∈ G := Group.pow_mem with group145      have step : ρ ^ (k + 1) = ρ * ρ ^ k := pow_succ_left with group146      have succForm : k + 1 = succ(k) := add.right_one at k147      rw succForm at step148      have composed : (ρ * ρ ^ k) ·ₐ d = ρ ·ₐ ρ ^ k ·ₐ d := mul_act with action, dIn149      have earlier : ρ ^ k ·ₐ d ∈ actImage(act, ρ ^ k, D) := actImage.contains with hd150      have kIn : k ∈ ℕ by typecheck151      have earlierInOrbit : ρ ^ k ·ₐ d ∈ forwardOrbit(act, G, ρ, D) :=152        forwardOrbit.membership.backward with ⟨k, kIn, earlier⟩153      have lifted : ρ ·ₐ ρ ^ k ·ₐ d ∈ actImage(act, ρ, forwardOrbit(act, G, ρ, D)) :=154        actImage.contains with earlierInOrbit155      have shapeY : y = ρ ·ₐ ρ ^ k ·ₐ d156        rw [← moved, shape, step, composed]157        rfl158      rw shapeY159      exact lifted160161-- The absorption theorem: X and X ∖ D are equidecomposable with two162-- pieces, U carried by ρ and X ∖ U carried by the identity.163theorem absorption (ρ : G) (D : Set)164  requires subset : D ⊆ X165  requires separated : ∀ n ∈ ℕ, Disjoint(actImage(act, ρ ^ (n + 1), D), D)166  shows ∃ U ∈ 𝒫(X), Disjoint(U, X ∖ U) ∧ U ∪ (X ∖ U) = X ∧167    Disjoint(actImage(act, ρ, U), X ∖ U) ∧168    actImage(act, ρ, U) ∪ (X ∖ U) = X ∖ D169proof170  have orbitSubset : forwardOrbit(act, G, ρ, D) ⊆ X := forwardOrbit.subset with *171  have orbitContains : D ⊆ forwardOrbit(act, G, ρ, D) := forwardOrbit.contains with *172  have carried := forwardOrbit.image with action, subset, separated173  have inPower := powerset.membership_iff.backward with orbitSubset174  refine ⟨forwardOrbit(act, G, ρ, D), inPower, ?_, ?_, ?_, ?_⟩175  . exact Disjoint.difference_right at X, forwardOrbit(act, G, ρ, D)176  . exact difference.union2_of_subset with orbitSubset177  . rw carried178    apply Disjoint.iff.backward179    intros y hy hy2180    obtain ⟨inOrbit, notInD⟩ := difference.membership.forward with hy181    obtain ⟨inX, notInOrbit⟩ := difference.membership.forward with hy2182    exact notInOrbit with inOrbit183  . rw carried184    ext y185    constructor186    . intro hy187      have sides := union2.membership.forward with hy188      cases sides with inLeft | inRight189      . obtain ⟨inOrbit, notInD⟩ := difference.membership.forward with inLeft190        have inX := orbitSubset with y, inOrbit191        exact difference.membership.backward with ⟨inX, notInD⟩192      . obtain ⟨inX, notInOrbit⟩ := difference.membership.forward with inRight193        have notInD : ¬(y ∈ D)194          intro inD195          exact notInOrbit with (orbitContains with y, inD)196        exact difference.membership.backward with ⟨inX, notInD⟩197    . intro hy198      obtain ⟨inX, notInD⟩ := difference.membership.forward with hy199      have cases : y ∈ forwardOrbit(act, G, ρ, D) ∨ ¬(y ∈ forwardOrbit(act, G, ρ, D)) by tauto200      apply union2.membership.backward201      cases cases with inOrbit | notInOrbit202      . left203        exact difference.membership.backward with ⟨inOrbit, notInD⟩204      . right205        exact difference.membership.backward with ⟨inX, notInOrbit⟩206207end Absorption208