Grace/Cumulus/Geometry/Hausdorff/Countable.g17

Open in Workbench Download source

Imports

Hom · FixedPoints · Geometry.Absorption.CountableUnion

Declarations

Source

1-- The points of the sphere fixed by some nontrivial reduced word form a2-- countable set, coded through the pairing of ℕ × ℕ3-- 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.Countable9import Hom10import FixedPoints11import Geometry.Absorption.CountableUnion1213-- The points of the sphere fixed by the rotation of some nontrivial14-- reduced word.15def wordFixedSet : Set :=16  { v ∈ S² | ∃ w ∈ reducedWords,17    w ≠ [] ∧ call2(sphereAction, wordRotation(w), v) = v }1819theorem wordFixedSet.subset20  shows wordFixedSet ⊆ S²21proof22  intros v hv23  have parts := wordFixedSet.membership.forward with hv24  exact parts.left2526-- Coding words by naturals: the empty word is 0, and a letter in front27-- is paired with the code of the rest.28def wordCode (w : List(4)) → Set29  | [] => 030  | x :: xs => succ(naturalPairing((x, wordCode(xs))))3132theorem wordCode.nil33  shows wordCode([]) = 034proof35  simp [wordCode]3637theorem wordCode.cons (x : Set) (xs : List(4))38  requires hx : x ∈ 439  shows wordCode(x :: xs) = succ(naturalPairing((x, wordCode(xs))))40proof41  simp [wordCode]4243theorem wordCode.natural (w : List(4))44  shows wordCode(w) ∈ ℕ45proof46  induction w47  | List.nil =>48    rw wordCode.nil49    typecheck50  | List.cons(x, xs) using ih =>51    have hx : x ∈ 4 by assumption52    have natural := letter.natural with hx53    have xIn : x ∈ ℕ := nat.omega.forward with natural54    have pair := product.pair at x, wordCode(xs), ℕ, ℕ with xIn, ih55    have function := naturalPairing.function56    have codeIn := FunctionBetween.apply_closed with function, pair57    have head := wordCode.cons at x, xs with hx58    rw head59    exact omega.successor with codeIn6061theorem wordCode.injective (u : List(4))62  shows ∀ v, List(4, v) → wordCode(u) = wordCode(v) → u = v63proof64  induction u65  | List.nil =>66    intros v listV same67    have shape := List.cases at 4, v with listV68    cases shape with nil | cons69    . rw nil70      rfl71    . obtain ⟨y, hy, ys, tailList, equal⟩ := cons72      exfalso73      have headY := wordCode.cons at y, ys with hy74      rw [equal, headY, wordCode.nil] at same75      exact Naturals.disjoint.zero.succ at naturalPairing((y, wordCode(ys)))76        with same77  | List.cons(x, xs) using ih =>78    intros v listV same79    have hx : x ∈ 4 by assumption80    have headX := wordCode.cons at x, xs with hx81    have shape := List.cases at 4, v with listV82    cases shape with nil | cons83    . exfalso84      rw [nil, headX, wordCode.nil] at same85      symm at same86      exact Naturals.disjoint.zero.succ at naturalPairing((x, wordCode(xs)))87        with same88    . obtain ⟨y, hy, ys, tailList, equal⟩ := cons89      have headY := wordCode.cons at y, ys with hy90      rw [equal, headX, headY] at same91      have codes := Naturals.injective.succ with same92      have naturalX := nat.omega.forward with (letter.natural with hx)93      have naturalY := nat.omega.forward with (letter.natural with hy)94      have codeX := wordCode.natural at xs with *95      have codeY := wordCode.natural at ys with *96      have pairX := product.pair at x, wordCode(xs), ℕ, ℕ with naturalX, codeX97      have pairY := product.pair at y, wordCode(ys), ℕ, ℕ with naturalY, codeY98      have injective := naturalPairing.injective99      have pairs := Injective.apply_cancel with injective, pairX, pairY, codes100      obtain ⟨sameHead, sameCode⟩ := orderedPair.injective with pairs101      have sameTail := ih with ys, tailList, sameCode102      rw [equal, sameHead, sameTail]103      rfl104105-- The code as a graph on the reduced words, so the reduced words are106-- countable.107defgraph wordIndex (w ∈ reducedWords) : ℕ := wordCode(w)108proof109  have list := reducedWords.list with member110  exact wordCode.natural with list111112theorem reducedWords.countable113  shows Countable(reducedWords)114proof115  have function := wordIndex.function116  witness wordIndex117  apply Injective.of_pointwise with function118  intros a ha b hb same119  have listA := reducedWords.list with ha120  have listB := reducedWords.list with hb121  have valueA := wordIndex.value with ha122  have valueB := wordIndex.value with hb123  rw [valueA, valueB] at same124  have cancel := wordCode.injective at a with listA125  exact cancel with listB, same126127-- The points fixed by the rotation of one word, empty for the empty word.128def fixedBy (w : Set) : Set :=129  { v ∈ S² | w ≠ [] ∧ call2(sphereAction, wordRotation(w), v) = v }130131theorem fixedBy.subset (w : Set)132  shows fixedBy(w) ⊆ S²133proof134  intros v hv135  have parts := fixedBy.membership.forward with hv136  exact parts.left137138-- A nontrivial word fixes at most a point and its opposite.139theorem fixedBy.countable (w : Set)140  requires hw : w ∈ reducedWords141  shows Countable(fixedBy(w))142proof143  have split : w = [] ∨ w ≠ [] by tauto144  cases split with empty | nonempty145  . have finiteEmpty := Finite.empty146    have countableEmpty := Countable.of_finite with finiteEmpty147    have subset : fixedBy(w) ⊆ ∅148      intros v hv149      obtain ⟨vIn, nonempty, fixed⟩ := fixedBy.membership.forward with hv150      exfalso151      exact nonempty with empty152    exact Countable.subset with countableEmpty, subset153  . have list := reducedWords.list with hw154    have reduced := reducedWords.reduced with hw155    have rotation := wordRotation.so3 with list156    have nontrivial := wordRotation.ne_one with list, reduced, nonempty157    obtain ⟨p, hp, bound⟩ := so3.fixed_points with rotation, nontrivial158    have finiteSingle := Finite.singleton at vectorNeg(p)159    have finitePair := Finite.insert at {vectorNeg(p)}, p with finiteSingle160    have countablePair := Countable.of_finite with finitePair161    have subset : fixedBy(w) ⊆ insert(p, {vectorNeg(p)})162      intros v hv163      obtain ⟨vIn, nonempty2, fixed⟩ := fixedBy.membership.forward with hv164      have applied := sphereAction.apply with rotation, vIn165      rw applied at fixed166      have alternatives := bound with v, vIn, fixed167      apply insert.membership.backward168      cases alternatives with same | opposite169      . left170        exact same171      . right172        rw opposite173        exact singleton.self174    exact Countable.subset with countablePair, subset175176-- The fixed sets as a family indexed by the reduced words.177defgraph fixedFamily (w ∈ reducedWords) : 𝒫(S²) := fixedBy(w)178proof179  have subset := fixedBy.subset at w180  exact powerset.membership_iff.backward with subset181182theorem wordFixedSet.countable183  shows Countable(wordFixedSet)184proof185  have function := fixedFamily.function186  have countable := reducedWords.countable187  have members : ∀ w ∈ reducedWords, Countable(fixedFamily(w))188    intros w hw189    have value := fixedFamily.value with hw190    rw value191    exact fixedBy.countable with hw192  have union := Countable.indexed_union with function, countable, members193  have subset : wordFixedSet ⊆194      ⋃(functionImage(fixedFamily, reducedWords, 𝒫(S²)))195    intros v hv196    obtain ⟨vIn, w, hw, nonempty, fixed⟩ :=197      wordFixedSet.membership.forward with hv198    have value := fixedFamily.value with hw199    have inFixed : v ∈ fixedBy(w) :=200      fixedBy.membership.backward with ⟨vIn, nonempty, fixed⟩201    have closed := FunctionBetween.apply_closed with function, hw202    have imageIn : fixedFamily(w) ∈ functionImage(fixedFamily,203        reducedWords, 𝒫(S²)) :=204      functionImage.membership.backward with ⟨closed, w, hw, rfl⟩205    rw ← value at inFixed206    exact union.membership.backward with ⟨fixedFamily(w), imageIn, inFixed⟩207  exact Countable.subset with union, subset208