Grace/Cumulus/Geometry/Hausdorff/Hom.g17

Open in Workbench Download source

Imports

Rotation.Freeness · Algebra.Group.FreeGroup · Algebra.Group.Homomorphism

Declarations

Source

1-- The rotation of a word is an injective homomorphism of the free group2-- into SO3, by the freeness theorem3-- 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.Hom9import Rotation.Freeness10import Algebra.Group.FreeGroup11import Algebra.Group.Homomorphism1213-- The product in SO3 is the matrix product.14theorem SO3.mul_apply (M N : Set)15  requires hM : M ∈ so3Matrices16  requires hN : N ∈ so3Matrices17  shows Group.mul(SO3)(M, N) = Ring.mul(matrixRing(realRing, 3))(M, N)18proof19  have ring := matrixRing.real_ring20  have multiplicative := IsRing.multiplicative with (Ring.parts with ring)21  have semigroup := IsMonoid.semigroup with multiplicative22  have magma := IsSemigroup.magma with semigroup23  have closed : ClosedBinary(so3Matrices, Ring.mul(matrixRing(realRing, 3)))24    intros A hA B hB25    have matrixA := so3Matrices.matrix with hA26    have matrixB := so3Matrices.matrix with hB27    exact so3Matrices.mul_mem with *28  rw SO3.mulOf29  exact restrictBinary.value with magma, so3Matrices.subset, closed, hM, hN3031-- A letter and its inverse letter multiply to the identity.32theorem letterMatrix.cancel (ℓ : Set)33  requires letter : ℓ ∈ 434  shows letterMatrix(ℓ) * letterMatrix(inverseLetter(ℓ)) =35    Ring.one(matrixRing(realRing, 3))36proof37  have alternatives := letter.cases with letter38  rcases alternatives with at0 | at1 | at2 | at339  . rw [at0, inverseLetter.zero, letterMatrix.zero, letterMatrix.one]40    exact rotA.mul_transpose41  . rw [at1, inverseLetter.one, letterMatrix.one, letterMatrix.zero]42    exact rotA.transpose_mul43  . rw [at2, inverseLetter.two, letterMatrix.two, letterMatrix.three]44    exact rotB.mul_transpose45  . rw [at3, inverseLetter.three, letterMatrix.three, letterMatrix.two]46    exact rotB.transpose_mul4748-- The rotation of a concatenation is the product of the rotations.49theorem wordRotation.concat (u v : List(4))50  shows wordRotation(concat(u, v)) = wordRotation(u) * wordRotation(v)51proof52  induction u53  | List.nil =>54    have matrix := wordRotation.matrix at v with *55    rw [concat.nil_left, wordRotation.nil]56    symm57    exact matrixRing.one_mul with matrix58  | List.cons(x, xs) using ih =>59    have hx : x ∈ 4 by assumption60    have head := letterMatrix.matrix with hx61    have rest := wordRotation.matrix at xs with *62    have tail := wordRotation.matrix at v with *63    have joined := concat.cons at x, xs, v with hx64    have left := wordRotation.cons at x, concat(xs, v) with hx65    have right := wordRotation.cons at x, xs with hx66    rw [joined, left, ih, right]67    symm68    exact matrixRing.mul_assoc with head, rest, tail6970-- Pushing a letter onto a word multiplies the rotation by the letter.71theorem wordRotation.pushLetter (x : Set) (r : List(4))72  requires hx : x ∈ 473  shows wordRotation(pushLetter(x, r)) = letterMatrix(x) * wordRotation(r)74proof75  have shape := List.cases at 4, r with *76  cases shape with nil | cons77  . have single := wordRotation.cons at x, [] with hx78    rw [nil, pushLetter.nil, single]79    rfl80  . obtain ⟨y, hy, ys, tailList, equal⟩ := cons81    have boolean := cancels.boolean at x, y82    have split : cancels(x, y) = Bool.false ∨ cancels(x, y) = Bool.true :=83      boolean.cases with boolean84    have headY := wordRotation.cons at y, ys with hy85    cases split with keep | cancel86    . have kept := pushLetter.keep at x, y, ys with hx, hy, keep87      have headX := wordRotation.cons at x, y :: ys with hx88      rw [equal, kept, headX]89      rfl90    . have cancelled := pushLetter.cancel at x, y, ys with hx, hy, cancel91      have inverse := cancels.true_iff.forward with cancel92      have matrixX := letterMatrix.matrix with hx93      have matrixY := letterMatrix.matrix with hy94      have rest := wordRotation.matrix at ys with *95      have assoc := matrixRing.mul_assoc with matrixX, matrixY, rest96      have unit := matrixRing.one_mul with rest97      have pair : letterMatrix(x) * letterMatrix(y) =98          Ring.one(matrixRing(realRing, 3))99        rw inverse100        exact letterMatrix.cancel with hx101      rw [equal, cancelled, headY, ← assoc, pair, unit]102      rfl103104-- Reduction does not change the rotation.105theorem wordRotation.reduce (w : List(4))106  shows wordRotation(reduce(w)) = wordRotation(w)107proof108  induction w109  | List.nil =>110    rw reduce.nil111    rfl112  | List.cons(x, xs) using ih =>113    have hx : x ∈ 4 by assumption114    have closed := reduce.closed at xs with *115    have pushed := wordRotation.pushLetter at x, reduce(xs) with hx116    have step := reduce.cons at x, xs with hx117    have head := wordRotation.cons at x, xs with hx118    rw [step, pushed, ih, head]119    rfl120121-- The rotation of the inverse word is a left inverse of the rotation.122theorem wordRotation.inverseWord (w : List(4))123  shows wordRotation(inverseWord(w)) * wordRotation(w) =124    Ring.one(matrixRing(realRing, 3))125proof126  induction w127  | List.nil =>128    have one := Matrix.one_matrix129    rw [inverseWord.nil, wordRotation.nil]130    exact matrixRing.one_mul with one131  | List.cons(x, xs) using ih =>132    have hx : x ∈ 4 by assumption133    have letter := inverseLetter.letter with hx134    have single : List(4, inverseLetter(x) :: []) by typecheck135    have inverseList := inverseWord.closed at xs with *136    have matrixX := letterMatrix.matrix with hx137    have matrixI := letterMatrix.matrix with letter138    have rest := wordRotation.matrix at xs with *139    have front := wordRotation.matrix at inverseWord(xs) with *140    have one := Matrix.one_matrix141    have split := wordRotation.concat at inverseWord(xs),142      inverseLetter(x) :: [] with *143    have head := wordRotation.cons at inverseLetter(x), [] with letter144    have headX := wordRotation.cons at x, xs with hx145    have involutive := inverseLetter.involutive with hx146    have pair : letterMatrix(inverseLetter(x)) * letterMatrix(x) =147        Ring.one(matrixRing(realRing, 3))148      have cancel := letterMatrix.cancel with letter149      rw involutive at cancel150      exact cancel151    have unitR := matrixRing.mul_one with matrixI152    have unitF := matrixRing.mul_one with front153    have assoc1 := matrixRing.mul_assoc with front, matrixI, matrixX154    have product := Matrix.mul_matrix with front, matrixI155    have assoc2 := matrixRing.mul_assoc with product, matrixX, rest156    rw [inverseWord.cons, split, head, wordRotation.nil, unitR, headX]157    calc158      wordRotation(inverseWord(xs)) * letterMatrix(inverseLetter(x)) *159          (letterMatrix(x) * wordRotation(xs)) =160          wordRotation(inverseWord(xs)) * letterMatrix(inverseLetter(x)) *161          letterMatrix(x) * wordRotation(xs) := by rw assoc2162      _ = wordRotation(inverseWord(xs)) *163          (letterMatrix(inverseLetter(x)) * letterMatrix(x)) *164          wordRotation(xs) := by rw assoc1165      _ = wordRotation(inverseWord(xs)) *166          wordRotation(xs) := by rw [pair, unitF]167      _ = Ring.one(matrixRing(realRing, 3)) := ih168169-- The homomorphism: a reduced word goes to its rotation.170defgraph wordHom (w ∈ reducedWords) : so3Matrices := wordRotation(w)171proof172  have list := reducedWords.list with member173  exact wordRotation.so3 with list174175theorem wordHom.apply (w : Set)176  requires hw : w ∈ reducedWords177  shows wordHom(w) = wordRotation(w)178proof179  exact wordHom.value with hw180181theorem wordHom.carrier_function182  shows wordHom : Group.carrier(freeGroup) → Group.carrier(SO3)183proof184  have function := wordHom.function185  rw [freeGroup.carrierOf, SO3.carrierOf]186  exact function187188theorem wordHom.hom189  shows wordHom : freeGroup →* SO3190proof191  have group := freeGroup.group192  have target := SO3.group193  have function := wordHom.carrier_function194  apply GroupHom.mk with group, target, function195  intros u hu v hv196  have uIn := hu197  have vIn := hv198  rw freeGroup.carrierOf at uIn199  rw freeGroup.carrierOf at vIn200  have productIn : u * v ∈ reducedWords201    rw freeGroup.operation202    exact freeMul.mem with uIn, vIn203  have productValue : u * v = reduce(concat(u, v))204    rw freeGroup.operation205    exact freeMul.apply with uIn, vIn206  have listU := reducedWords.list with uIn207  have listV := reducedWords.list with vIn208  have joined := concat.closed at u, v with *209  have reduced := wordRotation.reduce at concat(u, v) with joined210  have split := wordRotation.concat with listU, listV211  have so3U := wordRotation.so3 with listU212  have so3V := wordRotation.so3 with listV213  have operation := SO3.mul_apply with so3U, so3V214  have first := wordHom.apply with uIn215  have second := wordHom.apply with vIn216  have third := wordHom.apply with productIn217  rw [third, first, second, productValue, reduced, split, operation]218  rfl219220-- Injectivity: equal rotations give a reduced word u⁻¹v with rotation221-- the identity, which is the empty word by the freeness theorem.222theorem wordHom.injective223  shows InjectiveBetween(wordHom, reducedWords, Group.carrier(SO3))224proof225  have group := freeGroup.group226  have function := wordHom.function227  rw SO3.carrierOf228  apply Injective.of_pointwise with function229  intros u hu v hv same230  have first := wordHom.apply with hu231  have second := wordHom.apply with hv232  rw [first, second] at same233  have listU := reducedWords.list with hu234  have listV := reducedWords.list with hv235  have inverseList := inverseWord.closed at u with *236  have joined := concat.closed at inverseWord(u), v with *237  have reducedK := reduce.reduced at concat(inverseWord(u), v) with joined238  have listK := reduce.closed at concat(inverseWord(u), v) with joined239  have rotation : wordRotation(reduce(concat(inverseWord(u), v))) =240      Ring.one(matrixRing(realRing, 3))241    have split := wordRotation.concat with inverseList, listV242    have cancel := wordRotation.inverseWord with listU243    rw [wordRotation.reduce, split, ← same]244    exact cancel245  have empty : reduce(concat(inverseWord(u), v)) = []246    by_contra247    have nonzero := wordRotation.ne_one with listK, reducedK, this248    exact nonzero with rotation249  have fixedV := reducedWords.fixed with hv250  have shift := reduce.concat with inverseList, listV251  rw [fixedV, empty] at shift252  have uIn := hu253  have vIn := hv254  rw ← freeGroup.carrierOf at uIn255  rw ← freeGroup.carrierOf at vIn256  have criterion := inv_mul_eq_one at freeGroup, u, v with group257  rw [freeGroup.operation, freeGroup.inverse, freeGroup.unit] at criterion258  have inverseIn := freeInv.mem with hu259  have inverseValue := freeInv.apply with hu260  have productValue := freeMul.apply with inverseIn, hv261  rw [productValue, inverseValue] at criterion262  symm at shift263  exact criterion.forward with shift264