-- Hausdorff's paradox: the sphere minus the fixed points of the nontrivial -- words is paradoxical under SO3, through a free action of the free group -- Part of Cumulus, the Grace17 mathematics library. -- Copyright (c) 2026 Grant Passmore. -- Released under the Apache License 2.0. See LICENSE in the repository root. -- Authors: Grant Passmore module Grace.Cumulus.Geometry.Hausdorff.Paradox import Countable import Algebra.Group.Paradox import Algebra.Group.Action.Restrict theorem wordFixedSet.complement_subset shows S² ∖ wordFixedSet ⊆ S² proof intros v hv obtain ⟨vIn, rest⟩ := difference.membership.forward with hv exact vIn -- The rotation of a word carries the complement of the fixed set into -- itself: a point whose image is fixed by h is fixed by the conjugate -- w⁻¹ h w, a nontrivial word. theorem wordFixedSet.invariant (w v : Set) requires hw : w ∈ reducedWords requires hv : v ∈ S² ∖ wordFixedSet shows call2(sphereAction, wordRotation(w), v) ∈ S² ∖ wordFixedSet proof have action := sphereAction.action have group := SO3.group have free := freeGroup.group have hom := wordHom.hom obtain ⟨vIn, notFixed⟩ := difference.membership.forward with hv have wIn := hw rw ← freeGroup.carrierOf at wIn have rotationW : wordHom(w) ∈ Group.carrier(SO3) := GroupHom.map_mem with hom have valueW := wordHom.apply with hw have moved : wordHom(w) ·ₐ v ∈ S² := Action.act_mem with action, vIn rw valueW at moved apply difference.membership.backward refine ⟨moved, ?_⟩ intro fixedImage obtain ⟨imageIn, h, hh, nonempty, fixes⟩ := wordFixedSet.membership.forward with fixedImage apply notFixed apply wordFixedSet.membership.backward refine ⟨vIn, ?_⟩ have hIn := hh rw ← freeGroup.carrierOf at hIn have valueH := wordHom.apply with hh have rotationH : wordHom(h) ∈ Group.carrier(SO3) := GroupHom.map_mem with hom rw valueW at rotationW rw valueH at rotationH have conjugateIn : w⁻¹ * (h * w) ∈ Group.carrier(freeGroup) by typecheck have conjugateWords := conjugateIn rw freeGroup.carrierOf at conjugateWords refine ⟨w⁻¹ * (h * w), conjugateWords, ?_, ?_⟩ . intro trivial apply nonempty rw ← freeGroup.unit at trivial have criterion := inv_mul_eq_one at freeGroup, w, h * w with free have same := criterion.forward with trivial have unitW : Group.one(freeGroup) * w = w := one_mul with free have equal : h * w = Group.one(freeGroup) * w rw [unitW, ← same] rfl have cancelled := mul_right_cancel at freeGroup, h, w, Group.one(freeGroup) with free, equal rw freeGroup.unit at cancelled exact cancelled . have mapK : wordHom(w⁻¹ * (h * w)) = wordHom(w⁻¹) * wordHom(h * w) := GroupHom.map_mul with * have mapHW : wordHom(h * w) = wordHom(h) * wordHom(w) := GroupHom.map_mul with * have mapInv : wordHom(w⁻¹) = wordHom(w)⁻¹ := GroupHom.map_inv with * have valueK := wordHom.apply with conjugateWords rw [← valueK, mapK, mapHW, mapInv, valueH, valueW] have outer : (wordRotation(w)⁻¹ * (wordRotation(h) * wordRotation(w))) ·ₐ v = wordRotation(w)⁻¹ ·ₐ (wordRotation(h) * wordRotation(w)) ·ₐ v exact mul_act with * have inner : (wordRotation(h) * wordRotation(w)) ·ₐ v = wordRotation(h) ·ₐ wordRotation(w) ·ₐ v := mul_act with * rw [outer, inner, fixes] exact inv_act_cancel with action, vIn -- The free group acts on the complement of the fixed set: the word w -- sends v to the rotation of w applied to v. defgraph freeSphereAction (p ∈ reducedWords × (S² ∖ wordFixedSet)) : S² ∖ wordFixedSet := sphereAction(wordRotation(fst(p)), snd(p)) proof obtain ⟨bound, w, hw, v, hv, shape⟩ := product.membership.forward with member rw [shape, fst.pair, snd.pair] exact wordFixedSet.invariant with hw, hv theorem freeSphereAction.apply (w v : Set) requires hw : w ∈ reducedWords requires hv : v ∈ S² ∖ wordFixedSet shows freeSphereAction(w, v) = sphereAction(wordRotation(w), v) proof have pair := product.pair at w, v, reducedWords, S² ∖ wordFixedSet with * have value := freeSphereAction.value at (w, v) with pair simp [call2] rw [fst.pair, snd.pair] rfl theorem freeSphereAction.action shows freeSphereAction : freeGroup ↷ S² ∖ wordFixedSet proof have group := freeGroup.group have sphere := sphereAction.action have so3 := SO3.group have hom := wordHom.hom have function := freeSphereAction.function have carrierFunction : FunctionBetween(freeSphereAction, Group.carrier(freeGroup) × (S² ∖ wordFixedSet), S² ∖ wordFixedSet) rw freeGroup.carrierOf exact function have complement := wordFixedSet.complement_subset apply Action.mk with group, carrierFunction . intros v hv have vIn := complement with v, hv have unitIn := reducedWords.nil_mem have value := freeSphereAction.apply with unitIn, hv rw [freeGroup.unit, value, wordRotation.nil, ← SO3.oneOf] exact one_act with sphere, vIn . intros u hu w hw v hv have vIn := complement with v, hv have uIn := hu have wIn := hw rw freeGroup.carrierOf at uIn rw freeGroup.carrierOf at wIn have productIn : u * w ∈ reducedWords rw freeGroup.operation exact freeMul.mem with uIn, wIn have mapMul : wordHom(u * w) = wordHom(u) * wordHom(w) := GroupHom.map_mul with * have valueU := wordHom.apply with uIn have valueW := wordHom.apply with wIn have valueP := wordHom.apply with productIn rw [valueU, valueW, valueP] at mapMul have rotU := wordRotation.so3 with (reducedWords.list with uIn) have rotW := wordRotation.so3 with (reducedWords.list with wIn) rw ← SO3.carrierOf at rotU rw ← SO3.carrierOf at rotW have moved := wordFixedSet.invariant with wIn, hv have first := freeSphereAction.apply with wIn, hv have second := freeSphereAction.apply with uIn, moved have third := freeSphereAction.apply with productIn, hv have merged : (wordRotation(u) * wordRotation(w)) ·ₐ v = wordRotation(u) ·ₐ wordRotation(w) ·ₐ v := mul_act with * rw [third, mapMul, merged, first, second] rfl -- The action is free: a word fixing a point of the complement is empty. theorem freeSphereAction.free shows FreeAction(freeSphereAction, freeGroup, S² ∖ wordFixedSet) proof have sphere := sphereAction.action have complement := wordFixedSet.complement_subset have nilIn := reducedWords.nil_mem unfold FreeAction intros v hv have vIn := complement with v, hv obtain ⟨vInSphere, notFixed⟩ := difference.membership.forward with hv rw freeGroup.unit ext w constructor . intro hw obtain ⟨wIn, fixes⟩ := stabilizer.membership.forward with hw rw freeGroup.carrierOf at wIn have value := freeSphereAction.apply with wIn, hv rw value at fixes have empty : w = [] by_contra apply notFixed apply wordFixedSet.membership.backward exact ⟨vInSphere, w, wIn, this, fixes⟩ rw empty exact singleton.self . intro hw have equal := singleton.membership.forward with hw rw equal apply stabilizer.membership.backward constructor . rw freeGroup.carrierOf exact nilIn . have value := freeSphereAction.apply with nilIn, hv rw [value, wordRotation.nil, ← SO3.oneOf] exact one_act with sphere, vIn theorem freeSphere.paradoxical shows Paradoxical(freeSphereAction, freeGroup, S² ∖ wordFixedSet) proof exact Paradoxical.of_free_freeGroup with freeSphereAction.action, freeSphereAction.free -- Transfer of a decomposition along a homomorphism, from an action of H -- on Y to any graph act on the pairs of G and a set X ⊇ Y that agrees -- with it: the pieces stay, the elements are mapped. The target graph -- need not be an action of G. section Transfer variable (act act2 G H X Y φ : Set) hypothesis action2 : act2 : H ↷ Y hypothesis hom : φ : H →* G hypothesis subset : Y ⊆ X hypothesis compatible : ∀ h ∈ H.carrier, ∀ y ∈ Y, act2(h, y) = act(φ(h), y) theorem translate.transfer (S h : Set) requires bounded : S ⊆ Y requires hh : h ∈ H.carrier shows translate(act, X, φ(h), S) = translate(act2, Y, h, S) proof ext y constructor . intro hy obtain ⟨yIn, x, hx, shape⟩ := translate.membership.forward with hy have xIn := bounded with x, hx have agree := compatible with h, hh, x, xIn have moved : act2(h, x) ∈ Y := Action.act_mem at act2, H, Y, h, x with action2, xIn apply translate.membership.backward refine ⟨?_, x, hx, ?_⟩ . rw [shape, ← agree] exact moved . rw [shape, agree] rfl . intro hy obtain ⟨yIn, x, hx, shape⟩ := translate.membership.forward with hy have xIn := bounded with x, hx have agree := compatible with h, hh, x, xIn have yInX := subset with y, yIn apply translate.membership.backward refine ⟨yInX, x, hx, ?_⟩ rw [shape, agree] rfl theorem Equidecomposable.transfer (A B : Set) requires equidecomposable : Equidecomposable(act2, H, Y, A, B) shows Equidecomposable(act, G, X, A, B) proof obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := equidecomposable obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces have function := pushPair.function at φ, H, G, Y with hom have finiteImage := Finite.function_image with function, finite, bounded have values : ∀ p ∈ F, pushPair(φ, H, G, Y)(p) = (fst(p), φ(snd(p))) intros p hp have pIn := bounded with p, hp exact pushPair.value at φ, H, G, Y, p with hom, pIn have members : ∀ q ∈ functionImage(pushPair(φ, H, G, Y), F, 𝒫(Y) × G.carrier), ∃ p ∈ F, q = pushPair(φ, H, G, Y)(p) intros q hq obtain ⟨qIn, p, hp, equal⟩ := functionImage.membership.forward with hq exact ⟨p, hp, equal⟩ have images : ∀ p ∈ F, pushPair(φ, H, G, Y)(p) ∈ functionImage(pushPair(φ, H, G, Y), F, 𝒫(Y) × G.carrier) intros p hp have pIn := bounded with p, hp have qIn := FunctionBetween.apply_closed with function, pIn exact functionImage.membership.backward with ⟨qIn, p, hp, rfl⟩ have firsts : ∀ p ∈ F, fst(pushPair(φ, H, G, Y)(p)) = fst(p) intros p hp have value := values with p, hp rw [value, fst.pair] rfl have moves : ∀ p ∈ F, moved(act, X, pushPair(φ, H, G, Y)(p)) = moved(act2, Y, p) intros p hp have pIn := bounded with p, hp obtain ⟨boundP, S, hS, h, hh, shape⟩ := product.membership.forward with pIn have value := values with p, hp have pieceBounded := powerset.membership_iff.forward with hS have transfer := translate.transfer with action2, hom, subset, compatible, pieceBounded, hh rw [value, shape, fst.pair, snd.pair, moved.value, moved.value] exact transfer have distinct : ∀ p ∈ F, ∀ q ∈ F, pushPair(φ, H, G, Y)(p) ≠ pushPair(φ, H, G, Y)(q) → p ≠ q intros p hp q hq different same apply different rw same rfl have imageBounded : functionImage(pushPair(φ, H, G, Y), F, 𝒫(Y) × G.carrier) ⊆ 𝒫(X) × G.carrier have inner := functionImage.subset at pushPair(φ, H, G, Y), F, 𝒫(Y) × G.carrier have powers := powerset.monotone with subset have same := Subset.reflexive at G.carrier have outer : 𝒫(Y) × G.carrier ⊆ 𝒫(X) × G.carrier := product.monotone with powers, same exact Subset.transitive with inner, outer witness functionImage(pushPair(φ, H, G, Y), F, 𝒫(Y) × G.carrier) refine ⟨finiteImage, imageBounded, ?_, ?_⟩ . refine ⟨?_, ?_, ?_⟩ . intros q hq obtain ⟨p, hp, equal⟩ := members with q, hq have first := firsts with p, hp rw [equal, first] exact piecesBounded with p, hp . intros x hx obtain ⟨p, hp, member⟩ := piecesCover with x, hx have first := firsts with p, hp have image := images with p, hp witness pushPair(φ, H, G, Y)(p) rw first exact ⟨image, member⟩ . intros q hq r hr different obtain ⟨p, hp, qEq⟩ := members with q, hq obtain ⟨s, hs, rEq⟩ := members with r, hr rw [qEq, rEq] at different have apart := distinct with p, hp, s, hs, different have firstP := firsts with p, hp have firstS := firsts with s, hs rw [qEq, rEq, firstP, firstS] exact piecesDisjoint with p, hp, s, hs, apart . refine ⟨?_, ?_, ?_⟩ . intros q hq obtain ⟨p, hp, equal⟩ := members with q, hq have move := moves with p, hp rw [equal, move] exact movedBounded with p, hp . intros y hy obtain ⟨p, hp, member⟩ := movedCover with y, hy have move := moves with p, hp have image := images with p, hp witness pushPair(φ, H, G, Y)(p) rw move exact ⟨image, member⟩ . intros q hq r hr different obtain ⟨p, hp, qEq⟩ := members with q, hq obtain ⟨s, hs, rEq⟩ := members with r, hr rw [qEq, rEq] at different have apart := distinct with p, hp, s, hs, different have moveP := moves with p, hp have moveS := moves with s, hs rw [qEq, rEq, moveP, moveS] exact movedDisjoint with p, hp, s, hs, apart end Transfer -- Hausdorff's paradox for the restricted graph of the sphere action: the -- complement of the fixed set is paradoxical with its decomposition read -- through the restriction of sphereAction to the pairs over it. theorem hausdorff shows Paradoxical(restrictAction(sphereAction, SO3, S² ∖ wordFixedSet), SO3, S² ∖ wordFixedSet) proof have sphere := sphereAction.action have hom := wordHom.hom have free := freeSphereAction.action have complement := wordFixedSet.complement_subset have same := Subset.reflexive at S² ∖ wordFixedSet have compatible : ∀ w ∈ Group.carrier(freeGroup), ∀ y ∈ S² ∖ wordFixedSet, freeSphereAction(w, y) = restrictAction(sphereAction, SO3, S² ∖ wordFixedSet)(wordHom(w), y) intros w hw y hy have wIn := hw rw freeGroup.carrierOf at wIn have rotation : wordHom(w) ∈ Group.carrier(SO3) := GroupHom.map_mem with hom have left := freeSphereAction.apply with wIn, hy have right := restrictAction.value with sphere, complement, rotation, hy have value := wordHom.apply with wIn rw [left, right, value] rfl obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ := freeSphere.paradoxical witness A witness B refine ⟨boundedA, boundedB, disjoint, ?_, ?_⟩ . exact Equidecomposable.transfer with free, hom, same, compatible, firstA . exact Equidecomposable.transfer with free, hom, same, compatible, secondB -- Hausdorff's paradox under the action of SO3 on the whole sphere: two -- disjoint pieces of the complement, each equidecomposable with the -- complement inside S². theorem hausdorff.pieces shows ∃ A, ∃ B, A ⊆ S² ∖ wordFixedSet ∧ B ⊆ S² ∖ wordFixedSet ∧ Disjoint(A, B) ∧ Equidecomposable(sphereAction, SO3, S², A, S² ∖ wordFixedSet) ∧ Equidecomposable(sphereAction, SO3, S², B, S² ∖ wordFixedSet) proof have sphere := sphereAction.action have hom := wordHom.hom have free := freeSphereAction.action have complement := wordFixedSet.complement_subset have compatible : ∀ w ∈ Group.carrier(freeGroup), ∀ y ∈ S² ∖ wordFixedSet, freeSphereAction(w, y) = sphereAction(wordHom(w), y) intros w hw y hy have wIn := hw rw freeGroup.carrierOf at wIn have left := freeSphereAction.apply with wIn, hy have value := wordHom.apply with wIn rw [left, value] rfl obtain ⟨A, B, boundedA, boundedB, disjoint, firstA, secondB⟩ := freeSphere.paradoxical refine ⟨A, B, boundedA, boundedB, disjoint, ?_, ?_⟩ . exact Equidecomposable.transfer with free, hom, complement, compatible, firstA . exact Equidecomposable.transfer with free, hom, complement, compatible, secondB