Grace/Cumulus/Geometry/Hausdorff/Paradox.g17

Open in Workbench Download source

Imports

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

Declarations

Source

1-- Hausdorff's paradox: the sphere minus the fixed points of the nontrivial2-- words is paradoxical under SO3, through a free action of the free group3-- 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.Geometry.Hausdorff.Paradox9import Countable10import Algebra.Group.Paradox11import Algebra.Group.Action.Restrict1213theorem wordFixedSet.complement_subset14  shows S² ∖ wordFixedSet ⊆ S²15proof16  intros v hv17  obtain ⟨vIn, rest⟩ := difference.membership.forward with hv18  exact vIn1920-- The rotation of a word carries the complement of the fixed set into21-- itself: a point whose image is fixed by h is fixed by the conjugate22-- w⁻¹ h w, a nontrivial word.23theorem wordFixedSet.invariant (w v : Set)24  requires hw : w ∈ reducedWords25  requires hv : v ∈ S² ∖ wordFixedSet26  shows call2(sphereAction, wordRotation(w), v) ∈ S² ∖ wordFixedSet27proof28  have action := sphereAction.action29  have group := SO3.group30  have free := freeGroup.group31  have hom := wordHom.hom32  obtain ⟨vIn, notFixed⟩ := difference.membership.forward with hv33  have wIn := hw34  rw ← freeGroup.carrierOf at wIn35  have rotationW : wordHom(w) ∈ Group.carrier(SO3) :=36    GroupHom.map_mem with hom37  have valueW := wordHom.apply with hw38  have moved : wordHom(w) ·ₐ v ∈ S² := Action.act_mem with action, vIn39  rw valueW at moved40  apply difference.membership.backward41  refine ⟨moved, ?_⟩42  intro fixedImage43  obtain ⟨imageIn, h, hh, nonempty, fixes⟩ :=44    wordFixedSet.membership.forward with fixedImage45  apply notFixed46  apply wordFixedSet.membership.backward47  refine ⟨vIn, ?_⟩48  have hIn := hh49  rw ← freeGroup.carrierOf at hIn50  have valueH := wordHom.apply with hh51  have rotationH : wordHom(h) ∈ Group.carrier(SO3) :=52    GroupHom.map_mem with hom53  rw valueW at rotationW54  rw valueH at rotationH55  have conjugateIn : w⁻¹ * (h * w) ∈ Group.carrier(freeGroup) by typecheck56  have conjugateWords := conjugateIn57  rw freeGroup.carrierOf at conjugateWords58  refine ⟨w⁻¹ * (h * w), conjugateWords, ?_, ?_⟩59  . intro trivial60    apply nonempty61    rw ← freeGroup.unit at trivial62    have criterion := inv_mul_eq_one at freeGroup, w, h * w with free63    have same := criterion.forward with trivial64    have unitW : Group.one(freeGroup) * w = w := one_mul with free65    have equal : h * w = Group.one(freeGroup) * w66      rw [unitW, ← same]67      rfl68    have cancelled := mul_right_cancel at freeGroup, h, w, Group.one(freeGroup)69      with free, equal70    rw freeGroup.unit at cancelled71    exact cancelled72  . have mapK : wordHom(w⁻¹ * (h * w)) = wordHom(w⁻¹) * wordHom(h * w) :=73      GroupHom.map_mul with *74    have mapHW : wordHom(h * w) = wordHom(h) * wordHom(w) :=75      GroupHom.map_mul with *76    have mapInv : wordHom(w⁻¹) = wordHom(w)⁻¹ := GroupHom.map_inv with *77    have valueK := wordHom.apply with conjugateWords78    rw [← valueK, mapK, mapHW, mapInv, valueH, valueW]79    have outer : (wordRotation(w)⁻¹ *80        (wordRotation(h) * wordRotation(w))) ·ₐ v =81        wordRotation(w)⁻¹ ·ₐ (wordRotation(h) * wordRotation(w)) ·ₐ v82      exact mul_act with *83    have inner : (wordRotation(h) * wordRotation(w)) ·ₐ v =84        wordRotation(h) ·ₐ wordRotation(w) ·ₐ v := mul_act with *85    rw [outer, inner, fixes]86    exact inv_act_cancel with action, vIn8788-- The free group acts on the complement of the fixed set: the word w89-- sends v to the rotation of w applied to v.90defgraph freeSphereAction (p ∈ reducedWords × (S² ∖ wordFixedSet)) :91    S² ∖ wordFixedSet := sphereAction(wordRotation(fst(p)), snd(p))92proof93  obtain ⟨bound, w, hw, v, hv, shape⟩ :=94    product.membership.forward with member95  rw [shape, fst.pair, snd.pair]96  exact wordFixedSet.invariant with hw, hv9798theorem freeSphereAction.apply (w v : Set)99  requires hw : w ∈ reducedWords100  requires hv : v ∈ S² ∖ wordFixedSet101  shows freeSphereAction(w, v) = sphereAction(wordRotation(w), v)102proof103  have pair := product.pair at w, v, reducedWords, S² ∖ wordFixedSet with *104  have value := freeSphereAction.value at (w, v) with pair105  simp [call2]106  rw [fst.pair, snd.pair]107  rfl108109theorem freeSphereAction.action110  shows freeSphereAction : freeGroup ↷ S² ∖ wordFixedSet111proof112  have group := freeGroup.group113  have sphere := sphereAction.action114  have so3 := SO3.group115  have hom := wordHom.hom116  have function := freeSphereAction.function117  have carrierFunction : FunctionBetween(freeSphereAction,118      Group.carrier(freeGroup) × (S² ∖ wordFixedSet), S² ∖ wordFixedSet)119    rw freeGroup.carrierOf120    exact function121  have complement := wordFixedSet.complement_subset122  apply Action.mk with group, carrierFunction123  . intros v hv124    have vIn := complement with v, hv125    have unitIn := reducedWords.nil_mem126    have value := freeSphereAction.apply with unitIn, hv127    rw [freeGroup.unit, value, wordRotation.nil, ← SO3.oneOf]128    exact one_act with sphere, vIn129  . intros u hu w hw v hv130    have vIn := complement with v, hv131    have uIn := hu132    have wIn := hw133    rw freeGroup.carrierOf at uIn134    rw freeGroup.carrierOf at wIn135    have productIn : u * w ∈ reducedWords136      rw freeGroup.operation137      exact freeMul.mem with uIn, wIn138    have mapMul : wordHom(u * w) = wordHom(u) * wordHom(w) :=139      GroupHom.map_mul with *140    have valueU := wordHom.apply with uIn141    have valueW := wordHom.apply with wIn142    have valueP := wordHom.apply with productIn143    rw [valueU, valueW, valueP] at mapMul144    have rotU := wordRotation.so3 with (reducedWords.list with uIn)145    have rotW := wordRotation.so3 with (reducedWords.list with wIn)146    rw ← SO3.carrierOf at rotU147    rw ← SO3.carrierOf at rotW148    have moved := wordFixedSet.invariant with wIn, hv149    have first := freeSphereAction.apply with wIn, hv150    have second := freeSphereAction.apply with uIn, moved151    have third := freeSphereAction.apply with productIn, hv152    have merged : (wordRotation(u) * wordRotation(w)) ·ₐ v =153        wordRotation(u) ·ₐ wordRotation(w) ·ₐ v := mul_act with *154    rw [third, mapMul, merged, first, second]155    rfl156157-- The action is free: a word fixing a point of the complement is empty.158theorem freeSphereAction.free159  shows FreeAction(freeSphereAction, freeGroup, S² ∖ wordFixedSet)160proof161  have sphere := sphereAction.action162  have complement := wordFixedSet.complement_subset163  have nilIn := reducedWords.nil_mem164  unfold FreeAction165  intros v hv166  have vIn := complement with v, hv167  obtain ⟨vInSphere, notFixed⟩ := difference.membership.forward with hv168  rw freeGroup.unit169  ext w170  constructor171  . intro hw172    obtain ⟨wIn, fixes⟩ := stabilizer.membership.forward with hw173    rw freeGroup.carrierOf at wIn174    have value := freeSphereAction.apply with wIn, hv175    rw value at fixes176    have empty : w = []177      by_contra178      apply notFixed179      apply wordFixedSet.membership.backward180      exact ⟨vInSphere, w, wIn, this, fixes⟩181    rw empty182    exact singleton.self183  . intro hw184    have equal := singleton.membership.forward with hw185    rw equal186    apply stabilizer.membership.backward187    constructor188    . rw freeGroup.carrierOf189      exact nilIn190    . have value := freeSphereAction.apply with nilIn, hv191      rw [value, wordRotation.nil, ← SO3.oneOf]192      exact one_act with sphere, vIn193194theorem freeSphere.paradoxical195  shows Paradoxical(freeSphereAction, freeGroup, S² ∖ wordFixedSet)196proof197  exact Paradoxical.of_free_freeGroup with freeSphereAction.action,198    freeSphereAction.free199200-- Transfer of a decomposition along a homomorphism, from an action of H201-- on Y to any graph act on the pairs of G and a set X ⊇ Y that agrees202-- with it: the pieces stay, the elements are mapped. The target graph203-- need not be an action of G.204section Transfer205variable (act act2 G H X Y φ : Set)206hypothesis action2 : act2 : H ↷ Y207hypothesis hom : φ : H →* G208hypothesis subset : Y ⊆ X209hypothesis compatible : ∀ h ∈ H.carrier, ∀ y ∈ Y, act2(h, y) = act(φ(h), y)210211theorem translate.transfer (S h : Set)212  requires bounded : S ⊆ Y213  requires hh : h ∈ H.carrier214  shows translate(act, X, φ(h), S) = translate(act2, Y, h, S)215proof216  ext y217  constructor218  . intro hy219    obtain ⟨yIn, x, hx, shape⟩ := translate.membership.forward with hy220    have xIn := bounded with x, hx221    have agree := compatible with h, hh, x, xIn222    have moved : act2(h, x) ∈ Y :=223      Action.act_mem at act2, H, Y, h, x with action2, xIn224    apply translate.membership.backward225    refine ⟨?_, x, hx, ?_⟩226    . rw [shape, ← agree]227      exact moved228    . rw [shape, agree]229      rfl230  . intro hy231    obtain ⟨yIn, x, hx, shape⟩ := translate.membership.forward with hy232    have xIn := bounded with x, hx233    have agree := compatible with h, hh, x, xIn234    have yInX := subset with y, yIn235    apply translate.membership.backward236    refine ⟨yInX, x, hx, ?_⟩237    rw [shape, agree]238    rfl239240theorem Equidecomposable.transfer (A B : Set)241  requires equidecomposable : Equidecomposable(act2, H, Y, A, B)242  shows Equidecomposable(act, G, X, A, B)243proof244  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := equidecomposable245  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces246  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces247  have function := pushPair.function at φ, H, G, Y with hom248  have finiteImage := Finite.function_image with function, finite, bounded249  have values : ∀ p ∈ F, pushPair(φ, H, G, Y)(p) = (fst(p), φ(snd(p)))250    intros p hp251    have pIn := bounded with p, hp252    exact pushPair.value at φ, H, G, Y, p with hom, pIn253  have members : ∀ q ∈ functionImage(pushPair(φ, H, G, Y), F,254      𝒫(Y) × G.carrier), ∃ p ∈ F, q = pushPair(φ, H, G, Y)(p)255    intros q hq256    obtain ⟨qIn, p, hp, equal⟩ := functionImage.membership.forward with hq257    exact ⟨p, hp, equal⟩258  have images : ∀ p ∈ F,259      pushPair(φ, H, G, Y)(p) ∈ functionImage(pushPair(φ, H, G, Y), F,260        𝒫(Y) × G.carrier)261    intros p hp262    have pIn := bounded with p, hp263    have qIn := FunctionBetween.apply_closed with function, pIn264    exact functionImage.membership.backward with ⟨qIn, p, hp, rfl⟩265  have firsts : ∀ p ∈ F, fst(pushPair(φ, H, G, Y)(p)) = fst(p)266    intros p hp267    have value := values with p, hp268    rw [value, fst.pair]269    rfl270  have moves : ∀ p ∈ F,271      moved(act, X, pushPair(φ, H, G, Y)(p)) = moved(act2, Y, p)272    intros p hp273    have pIn := bounded with p, hp274    obtain ⟨boundP, S, hS, h, hh, shape⟩ :=275      product.membership.forward with pIn276    have value := values with p, hp277    have pieceBounded := powerset.membership_iff.forward with hS278    have transfer := translate.transfer with action2, hom, subset, compatible,279      pieceBounded, hh280    rw [value, shape, fst.pair, snd.pair, moved.value, moved.value]281    exact transfer282  have distinct : ∀ p ∈ F, ∀ q ∈ F,283      pushPair(φ, H, G, Y)(p) ≠ pushPair(φ, H, G, Y)(q) → p ≠ q284    intros p hp q hq different same285    apply different286    rw same287    rfl288  have imageBounded : functionImage(pushPair(φ, H, G, Y), F,289      𝒫(Y) × G.carrier) ⊆ 𝒫(X) × G.carrier290    have inner := functionImage.subset at pushPair(φ, H, G, Y), F,291      𝒫(Y) × G.carrier292    have powers := powerset.monotone with subset293    have same := Subset.reflexive at G.carrier294    have outer : 𝒫(Y) × G.carrier ⊆ 𝒫(X) × G.carrier :=295      product.monotone with powers, same296    exact Subset.transitive with inner, outer297  witness functionImage(pushPair(φ, H, G, Y), F, 𝒫(Y) × G.carrier)298  refine ⟨finiteImage, imageBounded, ?_, ?_⟩299  . refine ⟨?_, ?_, ?_⟩300    . intros q hq301      obtain ⟨p, hp, equal⟩ := members with q, hq302      have first := firsts with p, hp303      rw [equal, first]304      exact piecesBounded with p, hp305    . intros x hx306      obtain ⟨p, hp, member⟩ := piecesCover with x, hx307      have first := firsts with p, hp308      have image := images with p, hp309      witness pushPair(φ, H, G, Y)(p)310      rw first311      exact ⟨image, member⟩312    . intros q hq r hr different313      obtain ⟨p, hp, qEq⟩ := members with q, hq314      obtain ⟨s, hs, rEq⟩ := members with r, hr315      rw [qEq, rEq] at different316      have apart := distinct with p, hp, s, hs, different317      have firstP := firsts with p, hp318      have firstS := firsts with s, hs319      rw [qEq, rEq, firstP, firstS]320      exact piecesDisjoint with p, hp, s, hs, apart321  . refine ⟨?_, ?_, ?_⟩322    . intros q hq323      obtain ⟨p, hp, equal⟩ := members with q, hq324      have move := moves with p, hp325      rw [equal, move]326      exact movedBounded with p, hp327    . intros y hy328      obtain ⟨p, hp, member⟩ := movedCover with y, hy329      have move := moves with p, hp330      have image := images with p, hp331      witness pushPair(φ, H, G, Y)(p)332      rw move333      exact ⟨image, member⟩334    . intros q hq r hr different335      obtain ⟨p, hp, qEq⟩ := members with q, hq336      obtain ⟨s, hs, rEq⟩ := members with r, hr337      rw [qEq, rEq] at different338      have apart := distinct with p, hp, s, hs, different339      have moveP := moves with p, hp340      have moveS := moves with s, hs341      rw [qEq, rEq, moveP, moveS]342      exact movedDisjoint with p, hp, s, hs, apart343344end Transfer345346-- Hausdorff's paradox for the restricted graph of the sphere action: the347-- complement of the fixed set is paradoxical with its decomposition read348-- through the restriction of sphereAction to the pairs over it.349theorem hausdorff350  shows Paradoxical(restrictAction(sphereAction, SO3, S² ∖ wordFixedSet),351    SO3, S² ∖ wordFixedSet)352proof353  have sphere := sphereAction.action354  have hom := wordHom.hom355  have free := freeSphereAction.action356  have complement := wordFixedSet.complement_subset357  have same := Subset.reflexive at S² ∖ wordFixedSet358  have compatible : ∀ w ∈ Group.carrier(freeGroup),359      ∀ y ∈ S² ∖ wordFixedSet,360      freeSphereAction(w, y) =361        restrictAction(sphereAction, SO3, S² ∖ wordFixedSet)(wordHom(w), y)362    intros w hw y hy363    have wIn := hw364    rw freeGroup.carrierOf at wIn365    have rotation : wordHom(w) ∈ Group.carrier(SO3) :=366      GroupHom.map_mem with hom367    have left := freeSphereAction.apply with wIn, hy368    have right := restrictAction.value with sphere, complement, rotation,369      hy370    have value := wordHom.apply with wIn371    rw [left, right, value]372    rfl373  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ :=374    freeSphere.paradoxical375  witness A376  witness B377  refine ⟨boundedA, boundedB, disjoint, ?_, ?_⟩378  . exact Equidecomposable.transfer with free, hom, same, compatible, firstA379  . exact Equidecomposable.transfer with free, hom, same, compatible, secondB380381-- Hausdorff's paradox under the action of SO3 on the whole sphere: two382-- disjoint pieces of the complement, each equidecomposable with the383-- complement inside S².384theorem hausdorff.pieces385  shows ∃ A, ∃ B, A ⊆ S² ∖ wordFixedSet ∧ B ⊆ S² ∖ wordFixedSet ∧386    Disjoint(A, B) ∧387    Equidecomposable(sphereAction, SO3, S², A, S² ∖ wordFixedSet) ∧388    Equidecomposable(sphereAction, SO3, S², B, S² ∖ wordFixedSet)389proof390  have sphere := sphereAction.action391  have hom := wordHom.hom392  have free := freeSphereAction.action393  have complement := wordFixedSet.complement_subset394  have compatible : ∀ w ∈ Group.carrier(freeGroup),395      ∀ y ∈ S² ∖ wordFixedSet,396      freeSphereAction(w, y) = sphereAction(wordHom(w), y)397    intros w hw y hy398    have wIn := hw399    rw freeGroup.carrierOf at wIn400    have left := freeSphereAction.apply with wIn, hy401    have value := wordHom.apply with wIn402    rw [left, value]403    rfl404  obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ :=405    freeSphere.paradoxical406  refine ⟨A, B, boundedA, boundedB, disjoint, ?_, ?_⟩407  . exact Equidecomposable.transfer with408      free, hom, complement, compatible, firstA409  . exact Equidecomposable.transfer with410      free, hom, complement, compatible, secondB411