Grace/Cumulus/Rotation/Orthogonal.g17

Open in Workbench Download source

Imports

Vectors · Algebra.Group.Action

Declarations

Source

1-- Orthogonal 3 × 3 real matrices: the transpose transpose(M), the orthogonal2-- matrices transpose(M) M = 1 = M transpose(M), the determinant of a 3 × 3 matrix, the3-- group SO3 of orthogonal matrices of determinant one as a structure4-- value, and its actions on ℝ³ and on the unit sphere S²5-- 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.Rotation.Orthogonal11import Vectors12import Algebra.Group.Action1314-- The transpose of a 3 × 3 real matrix.15defgraph transpose (M : Set) (p ∈ 3 × 3) : ℝ := M[snd(p), fst(p)]16requires matrix : M : realRing ^ 3 × 317proof18  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with member19  rw [shape, fst.pair, snd.pair]20  exact Matrix.real_entry at M, j, i with *2122theorem transpose.entry (M : realRing ^ 3 × 3) (i j : Set)23  requires row : i ∈ 324  requires column : j ∈ 325  shows transpose(M)[i, j] = M[j, i]26proof27  have pair := product.pair at i, j, 3, 3 with *28  have value := transpose.value at M, (i, j) with *29  rw [value, fst.pair, snd.pair]30  rfl3132instance transpose.matrix (M : realRing ^ 3 × 3)33  shows transpose(M) : realRing ^ 3 × 334proof35  have function := transpose.function with *36  rw ← realRing.carrierOf at function37  exact Matrix.of_function with function3839theorem transpose.involutive (M : realRing ^ 3 × 3)40  shows transpose(transpose(M)) = M41proof42  have outer := transpose.matrix at transpose(M) with *43  apply Matrix.ext with outer, assumption44  intros i hi j hj45  have inner := transpose.entry at transpose(M), i, j with hi, hj46  have base := transpose.entry at M, j, i with hj, hi47  rw [inner, base]48  rfl4950theorem transpose.mul (M N : realRing ^ 3 × 3)51  shows transpose(M * N) = transpose(N) * transpose(M)52proof53  have product := Matrix.mul_matrix at M, N with *54  have transposedM := transpose.matrix at M with *55  have transposedN := transpose.matrix at N with *56  have left := transpose.matrix at M * N with *57  have right := Matrix.mul_matrix at transpose(N), transpose(M) with *58  apply Matrix.ext with left, right59  intros i hi j hj60  have entry := transpose.entry at M * N, i, j with *61  have expandL := matrixRing.mul_entry_three at M, N, j, i with *62  have expandR := matrixRing.mul_entry_three at transpose(N), transpose(M), i, j with *63  have t0 := transpose.entry at N, i, 0 with *64  have t1 := transpose.entry at N, i, 1 with *65  have t2 := transpose.entry at N, i, 2 with *66  have u0 := transpose.entry at M, 0, j with *67  have u1 := transpose.entry at M, 1, j with *68  have u2 := transpose.entry at M, 2, j with *69  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, j with hj70  have n0 := Matrix.real_entry at N, 0, i with *71  have n1 := Matrix.real_entry at N, 1, i with *72  have n2 := Matrix.real_entry at N, 2, i with *73  rw [entry, expandL, expandR, t0, t1, t2, u0, u1, u2]74  ring7576-- The symbol singleValue(ℝ, 0, 1, j, i) is symmetric in its indices.77theorem singleValue.symmetric (i j : Set)78  shows singleValue(Ring.carrier(realRing), Ring.zero(realRing), Ring.one(realRing), j, i) =79    singleValue(Ring.carrier(realRing), Ring.zero(realRing), Ring.one(realRing), i, j)80proof81  have comm := realRing.comm_ring82  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *83  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *84  have alternatives : i = j ∨ i ≠ j by tauto85  cases alternatives with same | different86  . have sameR : j = i by cc87    have first := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),88      Ring.one(realRing), j, i with zeroIn, oneIn, same89    have second := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),90      Ring.one(realRing), i, j with zeroIn, oneIn, sameR91    rw [first, second]92    rfl93  . have differentR : j ≠ i94      intro equal95      apply different96      cc97    have first := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),98      Ring.one(realRing), j, i with zeroIn, oneIn, different99    have second := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),100      Ring.one(realRing), i, j with zeroIn, oneIn, differentR101    rw [first, second]102    rfl103104theorem transpose.one105  shows transpose(matrixRing(realRing, 3)[1]) = matrixRing(realRing, 3)[1]106proof107  have comm := realRing.comm_ring108  have one := Matrix.one_matrix109  have transposed := transpose.matrix at matrixRing(realRing, 3)[1] with *110  apply Matrix.ext with transposed, one111  intros i hi j hj112  have entry := transpose.entry at matrixRing(realRing, 3)[1], i, j with *113  have first := matrixRing.one_entry at realRing, 3, j, i with *114  have second := matrixRing.one_entry at realRing, 3, i, j with *115  rw [entry, first, second]116  exact singleValue.symmetric at j, i117118-- The monoid laws of the matrix ring under multiplication.119theorem matrixRing.mul_assoc (M N P : realRing ^ 3 × 3)120  shows M * N * P = M * (N * P)121proof122  have ring := matrixRing.real_ring123  have monoid := IsRing.multiplicative with (Ring.parts with ring)124  have associative := IsMonoid.associative with monoid125  exact Associative.law with associative, *126127theorem matrixRing.one_mul (M : realRing ^ 3 × 3)128  shows matrixRing(realRing, 3)[1] * M = M129proof130  have ring := matrixRing.real_ring131  have monoid := IsRing.multiplicative with (Ring.parts with ring)132  exact IsMonoid.left_identity with monoid, *133134theorem matrixRing.mul_one (M : realRing ^ 3 × 3)135  shows M * matrixRing(realRing, 3)[1] = M136proof137  have ring := matrixRing.real_ring138  have monoid := IsRing.multiplicative with (Ring.parts with ring)139  exact IsMonoid.right_identity with monoid, *140141-- Orthogonal matrices: both products with the transpose are the identity.142predicate Orthogonal (M : Set) :=143  Matrix(M, realRing, 3, 3) ∧144  call2(Ring.mul(matrixRing(realRing, 3)), transpose(M), M) =145    Ring.one(matrixRing(realRing, 3)) ∧146  call2(Ring.mul(matrixRing(realRing, 3)), M, transpose(M)) =147    Ring.one(matrixRing(realRing, 3))148149theorem Orthogonal.mk (M : realRing ^ 3 × 3)150  requires left : transpose(M) * M = matrixRing(realRing, 3)[1]151  requires right : M * transpose(M) = matrixRing(realRing, 3)[1]152  shows Orthogonal(M)153proof154  unfold Orthogonal155  exact ⟨assumption, left, right⟩156157theorem Orthogonal.matrix (M : Set)158  requires orthogonal : Orthogonal(M)159  shows M : realRing ^ 3 × 3160proof161  obtain ⟨matrix, left, right⟩ := orthogonal162  exact matrix163164theorem Orthogonal.left (M : realRing ^ 3 × 3)165  requires orthogonal : Orthogonal(M)166  shows transpose(M) * M = matrixRing(realRing, 3)[1]167proof168  obtain ⟨matrix, left, right⟩ := orthogonal169  exact left170171theorem Orthogonal.right (M : realRing ^ 3 × 3)172  requires orthogonal : Orthogonal(M)173  shows M * transpose(M) = matrixRing(realRing, 3)[1]174proof175  obtain ⟨matrix, left, right⟩ := orthogonal176  exact right177178theorem Orthogonal.one179  shows Orthogonal(matrixRing(realRing, 3)[1])180proof181  have one := Matrix.one_matrix182  have law := matrixRing.mul_one at matrixRing(realRing, 3)[1] with one183  apply Orthogonal.mk with one184  . rw transpose.one185    exact law186  . rw transpose.one187    exact law188189theorem Orthogonal.transpose (M : realRing ^ 3 × 3)190  requires orthogonal : Orthogonal(M)191  shows Orthogonal(transpose(M))192proof193  have transposed := transpose.matrix at M with *194  have left := Orthogonal.left with orthogonal195  have right := Orthogonal.right with orthogonal196  apply Orthogonal.mk with transposed197  . rw transpose.involutive198    exact right199  . rw transpose.involutive200    exact left201202theorem Orthogonal.mul (M N : realRing ^ 3 × 3)203  requires orthogonalM : Orthogonal(M)204  requires orthogonalN : Orthogonal(N)205  shows Orthogonal(M * N)206proof207  have ring := matrixRing.real_ring208  have product := Matrix.mul_matrix at M, N with *209  have transposedM := transpose.matrix at M with *210  have transposedN := transpose.matrix at N with *211  have leftM := Orthogonal.left with orthogonalM212  have rightM := Orthogonal.right with orthogonalM213  have leftN := Orthogonal.left with orthogonalN214  have rightN := Orthogonal.right with orthogonalN215  have assocL := matrixRing.mul_assoc at transpose(N), transpose(M), M * N with *216  have assocL2 := matrixRing.mul_assoc at transpose(M), M, N with *217  have unitL := matrixRing.one_mul at N with *218  have assocR := matrixRing.mul_assoc at M, N, transpose(N) * transpose(M) with *219  have assocR2 := matrixRing.mul_assoc at N, transpose(N), transpose(M) with *220  have unitR := matrixRing.one_mul at transpose(M) with *221  apply Orthogonal.mk with product222  . rw transpose.mul223    calc224      transpose(N) * transpose(M) * (M * N) =225          transpose(N) * (transpose(M) * M * N) := by rw [assocL, assocL2]226      _ = transpose(N) * N := by rw [leftM, unitL]227      _ = matrixRing(realRing, 3)[1] := leftN228  . rw transpose.mul229    calc230      M * N * (transpose(N) * transpose(M)) =231          M * (N * transpose(N) * transpose(M)) := by rw [assocR, assocR2]232      _ = M * transpose(M) := by rw [rightN, unitR]233      _ = matrixRing(realRing, 3)[1] := rightM234235-- The determinant of a 3 × 3 real matrix, expanded along the first row.236def determinant3 (M : Set) : Set :=237  (M[0, 0]:R) * ((M[1, 1]:R) * (M[2, 2]:R) - (M[1, 2]:R) * (M[2, 1]:R)) -238  (M[0, 1]:R) * ((M[1, 0]:R) * (M[2, 2]:R) - (M[1, 2]:R) * (M[2, 0]:R)) +239  (M[0, 2]:R) * ((M[1, 0]:R) * (M[2, 1]:R) - (M[1, 1]:R) * (M[2, 0]:R))240241theorem determinant3.value (M : Set)242  shows determinant3(M) =243    (M[0, 0]:R) * ((M[1, 1]:R) * (M[2, 2]:R) - (M[1, 2]:R) * (M[2, 1]:R)) -244    (M[0, 1]:R) * ((M[1, 0]:R) * (M[2, 2]:R) - (M[1, 2]:R) * (M[2, 0]:R)) +245    (M[0, 2]:R) * ((M[1, 0]:R) * (M[2, 1]:R) - (M[1, 1]:R) * (M[2, 0]:R))246proof247  simp [determinant3]248249theorem Matrix.entries_real (M : realRing ^ 3 × 3)250  shows M[0, 0] ∈ ℝ ∧ M[0, 1] ∈ ℝ ∧ M[0, 2] ∈ ℝ ∧ M[1, 0] ∈ ℝ ∧ M[1, 1] ∈ ℝ ∧251    M[1, 2] ∈ ℝ ∧ M[2, 0] ∈ ℝ ∧ M[2, 1] ∈ ℝ ∧ M[2, 2] ∈ ℝ252proof253  obtain ⟨m00, m01, m02⟩ := Matrix.row_real at M, 0 with index.zero_mem254  obtain ⟨m10, m11, m12⟩ := Matrix.row_real at M, 1 with index.one_mem255  obtain ⟨m20, m21, m22⟩ := Matrix.row_real at M, 2 with index.two_mem256  exact ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩257258instance determinant3.real (M : realRing ^ 3 × 3)259  shows determinant3(M) ∈ ℝ260proof261  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real with *262  rw determinant3.value263  typecheck264265theorem determinant3.transpose (M : realRing ^ 3 × 3)266  shows determinant3(transpose(M)) = determinant3(M)267proof268  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real with *269  have t00 := transpose.entry at M, 0, 0 with *270  have t01 := transpose.entry at M, 0, 1 with *271  have t02 := transpose.entry at M, 0, 2 with *272  have t10 := transpose.entry at M, 1, 0 with *273  have t11 := transpose.entry at M, 1, 1 with *274  have t12 := transpose.entry at M, 1, 2 with *275  have t20 := transpose.entry at M, 2, 0 with *276  have t21 := transpose.entry at M, 2, 1 with *277  have t22 := transpose.entry at M, 2, 2 with *278  rw [determinant3.value, determinant3.value, t00, t01, t02, t10, t11, t12, t20, t21, t22]279  ring280281theorem determinant3.mul (M N : realRing ^ 3 × 3)282  shows determinant3(M * N) = determinant3(M) * determinant3(N)283proof284  have product := Matrix.mul_matrix at M, N with *285  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real at M with *286  obtain ⟨n00, n01, n02, n10, n11, n12, n20, n21, n22⟩ := Matrix.entries_real at N with *287  have p00 := matrixRing.mul_entry_three at M, N, 0, 0 with *288  have p01 := matrixRing.mul_entry_three at M, N, 0, 1 with *289  have p02 := matrixRing.mul_entry_three at M, N, 0, 2 with *290  have p10 := matrixRing.mul_entry_three at M, N, 1, 0 with *291  have p11 := matrixRing.mul_entry_three at M, N, 1, 1 with *292  have p12 := matrixRing.mul_entry_three at M, N, 1, 2 with *293  have p20 := matrixRing.mul_entry_three at M, N, 2, 0 with *294  have p21 := matrixRing.mul_entry_three at M, N, 2, 1 with *295  have p22 := matrixRing.mul_entry_three at M, N, 2, 2 with *296  rw [determinant3.value, determinant3.value, determinant3.value,297    p00, p01, p02, p10, p11, p12, p20, p21, p22]298  ring299300theorem determinant3.one301  shows determinant3(matrixRing(realRing, 3)[1]) = (1:R)302proof303  have comm := realRing.comm_ring304  have one := Matrix.one_matrix305  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *306  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *307  have same0 : 0 = 0 by rfl308  have same1 : 1 = 1 by rfl309  have same2 : 2 = 2 by rfl310  have e00 := matrixRing.one_entry at realRing, 3, 0, 0 with *311  have e01 := matrixRing.one_entry at realRing, 3, 0, 1 with *312  have e02 := matrixRing.one_entry at realRing, 3, 0, 2 with *313  have e10 := matrixRing.one_entry at realRing, 3, 1, 0 with *314  have e11 := matrixRing.one_entry at realRing, 3, 1, 1 with *315  have e12 := matrixRing.one_entry at realRing, 3, 1, 2 with *316  have e20 := matrixRing.one_entry at realRing, 3, 2, 0 with *317  have e21 := matrixRing.one_entry at realRing, 3, 2, 1 with *318  have e22 := matrixRing.one_entry at realRing, 3, 2, 2 with *319  have s00 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),320    Ring.one(realRing), 0, 0 with zeroIn, oneIn, same0321  have s11 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),322    Ring.one(realRing), 1, 1 with zeroIn, oneIn, same1323  have s22 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),324    Ring.one(realRing), 2, 2 with zeroIn, oneIn, same2325  have s10 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),326    Ring.one(realRing), 1, 0 with zeroIn, oneIn, index.zero_ne_one327  have s20 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),328    Ring.one(realRing), 2, 0 with zeroIn, oneIn, index.zero_ne_two329  have s01 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),330    Ring.one(realRing), 0, 1 with zeroIn, oneIn, index.one_ne_zero331  have s21 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),332    Ring.one(realRing), 2, 1 with zeroIn, oneIn, index.one_ne_two333  have s02 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),334    Ring.one(realRing), 0, 2 with zeroIn, oneIn, index.two_ne_zero335  have s12 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),336    Ring.one(realRing), 1, 2 with zeroIn, oneIn, index.two_ne_one337  rw [determinant3.value, e00, e01, e02, e10, e11, e12, e20, e21, e22,338    s00, s11, s22, s10, s20, s01, s21, s02, s12, realRing.zero_value, realRing.one_value]339  ring340341-- An orthogonal matrix preserves the dot products of columns, hence the342-- squared norm of every vector.343theorem Orthogonal.column (M : realRing ^ 3 × 3) (j k : Set)344  requires orthogonal : Orthogonal(M)345  requires hj : j ∈ 3346  requires hk : k ∈ 3347  shows (M[0, j]:R) * (M[0, k]:R) + (M[1, j]:R) * (M[1, k]:R) + (M[2, j]:R) * (M[2, k]:R) =348    singleValue(Ring.carrier(realRing), Ring.zero(realRing), Ring.one(realRing), k, j)349proof350  have comm := realRing.comm_ring351  have transposed := transpose.matrix at M with *352  have left := Orthogonal.left with orthogonal353  have entry := matrixRing.mul_entry_three at transpose(M), M, j, k with *354  have unit := matrixRing.one_entry at realRing, 3, j, k with *355  have t0 := transpose.entry at M, j, 0 with *356  have t1 := transpose.entry at M, j, 1 with *357  have t2 := transpose.entry at M, j, 2 with *358  rw [left, unit, t0, t1, t2] at entry359  symm at entry360  exact entry361362theorem Orthogonal.column_same (M : realRing ^ 3 × 3) (j : Set)363  requires orthogonal : Orthogonal(M)364  requires hj : j ∈ 3365  shows (M[0, j]:R) * (M[0, j]:R) + (M[1, j]:R) * (M[1, j]:R) + (M[2, j]:R) * (M[2, j]:R) = 1366proof367  have comm := realRing.comm_ring368  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *369  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *370  have same : j = j by rfl371  have column := Orthogonal.column at M, j, j with *372  have selected := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),373    Ring.one(realRing), j, j with zeroIn, oneIn, same374  rw [column, selected, realRing.one_value]375  rfl376377theorem Orthogonal.column_other (M : realRing ^ 3 × 3) (j k : Set)378  requires orthogonal : Orthogonal(M)379  requires hj : j ∈ 3380  requires hk : k ∈ 3381  requires different : j ≠ k382  shows (M[0, j]:R) * (M[0, k]:R) + (M[1, j]:R) * (M[1, k]:R) + (M[2, j]:R) * (M[2, k]:R) = 0383proof384  have comm := realRing.comm_ring385  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *386  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *387  have column := Orthogonal.column at M, j, k with *388  have selected := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),389    Ring.one(realRing), k, j with zeroIn, oneIn, different390  rw [column, selected, realRing.zero_value]391  rfl392393theorem Orthogonal.normSq (M : realRing ^ 3 × 3) (v : Set)394  requires orthogonal : Orthogonal(M)395  requires vector : v : 3 → ℝ396  shows normSq(M · v) = normSq(v)397proof398  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real with *399  have v0 := vector.component_real at v, 0 with *400  have v1 := vector.component_real at v, 1 with *401  have v2 := vector.component_real at v, 2 with *402  have c00 := Orthogonal.column_same at M, 0 with *403  have c11 := Orthogonal.column_same at M, 1 with *404  have c22 := Orthogonal.column_same at M, 2 with *405  have c01 := Orthogonal.column_other at M, 0, 1 with orthogonal, index.zero_mem,406    index.one_mem, index.zero_ne_one407  have c02 := Orthogonal.column_other at M, 0, 2 with orthogonal, index.zero_mem,408    index.two_mem, index.zero_ne_two409  have c12 := Orthogonal.column_other at M, 1, 2 with orthogonal, index.one_mem,410    index.two_mem, index.one_ne_two411  have e0 := matrixVector.entry at M, v, 0 with *412  have e1 := matrixVector.entry at M, v, 1 with *413  have e2 := matrixVector.entry at M, v, 2 with *414  have expand : normSq(M · v) =415      ((M[0, 0]:R) * (M[0, 0]:R) + (M[1, 0]:R) * (M[1, 0]:R) + (M[2, 0]:R) * (M[2, 0]:R)) * ((v(0):R) * (v(0):R)) +416      ((M[0, 1]:R) * (M[0, 1]:R) + (M[1, 1]:R) * (M[1, 1]:R) + (M[2, 1]:R) * (M[2, 1]:R)) * ((v(1):R) * (v(1):R)) +417      ((M[0, 2]:R) * (M[0, 2]:R) + (M[1, 2]:R) * (M[1, 2]:R) + (M[2, 2]:R) * (M[2, 2]:R)) * ((v(2):R) * (v(2):R)) +418      2 * ((M[0, 0]:R) * (M[0, 1]:R) + (M[1, 0]:R) * (M[1, 1]:R) + (M[2, 0]:R) * (M[2, 1]:R)) * ((v(0):R) * (v(1):R)) +419      2 * ((M[0, 0]:R) * (M[0, 2]:R) + (M[1, 0]:R) * (M[1, 2]:R) + (M[2, 0]:R) * (M[2, 2]:R)) * ((v(0):R) * (v(2):R)) +420      2 * ((M[0, 1]:R) * (M[0, 2]:R) + (M[1, 1]:R) * (M[1, 2]:R) + (M[2, 1]:R) * (M[2, 2]:R)) * ((v(1):R) * (v(2):R))421    rw [normSq.value, e0, e1, e2]422    ring423  rw [expand, c00, c11, c22, c01, c02, c12, normSq.value]424  ring425426-- The special orthogonal matrices: orthogonal, of determinant one.427def so3Matrices : Set :=428  { M ∈ Ring.carrier(matrixRing(realRing, 3)) | Orthogonal(M) ∧ determinant3(M) = (1:R) }429430theorem so3Matrices.mk (M : realRing ^ 3 × 3)431  requires orthogonal : Orthogonal(M)432  requires unit : determinant3(M) = (1:R)433  shows M ∈ so3Matrices434proof435  have member := Matrix.mem_ring at M, realRing, 3 with assumption436  exact so3Matrices.membership.backward with ⟨member, orthogonal, unit⟩437438theorem so3Matrices.matrix (M : Set)439  requires member : M ∈ so3Matrices440  shows M : realRing ^ 3 × 3441proof442  obtain ⟨ring, orthogonal, unit⟩ := so3Matrices.membership.forward with member443  exact Matrix.of_mem with ring444445theorem so3Matrices.orthogonal (M : Set)446  requires member : M ∈ so3Matrices447  shows Orthogonal(M)448proof449  obtain ⟨ring, orthogonal, unit⟩ := so3Matrices.membership.forward with member450  exact orthogonal451452theorem so3Matrices.determinant (M : Set)453  requires member : M ∈ so3Matrices454  shows determinant3(M) = (1:R)455proof456  obtain ⟨ring, orthogonal, unit⟩ := so3Matrices.membership.forward with member457  exact unit458459theorem so3Matrices.subset460  shows so3Matrices ⊆ Ring.carrier(matrixRing(realRing, 3))461proof462  intros M hM463  obtain ⟨ring, orthogonal, unit⟩ := so3Matrices.membership.forward with hM464  exact ring465466theorem so3Matrices.one_mem467  shows matrixRing(realRing, 3)[1] ∈ so3Matrices468proof469  have one := Matrix.one_matrix470  exact so3Matrices.mk with Orthogonal.one, determinant3.one471472theorem so3Matrices.mul_mem (M N : realRing ^ 3 × 3)473  requires hM : M ∈ so3Matrices474  requires hN : N ∈ so3Matrices475  shows M * N ∈ so3Matrices476proof477  have product := Matrix.mul_matrix at M, N with *478  have orthogonal := Orthogonal.mul with (so3Matrices.orthogonal with hM),479    (so3Matrices.orthogonal with hN)480  have unitM := so3Matrices.determinant with hM481  have unitN := so3Matrices.determinant with hN482  have unit : determinant3(M * N) = (1:R)483    rw [determinant3.mul, unitM, unitN]484    ring485  exact so3Matrices.mk with orthogonal, unit486487theorem so3Matrices.transpose_mem (M : realRing ^ 3 × 3)488  requires hM : M ∈ so3Matrices489  shows transpose(M) ∈ so3Matrices490proof491  have transposed := transpose.matrix at M with *492  have orthogonal := Orthogonal.transpose with (so3Matrices.orthogonal with hM)493  have unitM := so3Matrices.determinant with hM494  have unit : determinant3(transpose(M)) = (1:R)495    rw [determinant3.transpose, unitM]496    rfl497  exact so3Matrices.mk with orthogonal, unit498499-- The inverse of a special orthogonal matrix is its transpose.500defgraph so3Inverse (M ∈ so3Matrices) : so3Matrices := transpose(M)501proof502  have matrix := so3Matrices.matrix with member503  exact so3Matrices.transpose_mem with matrix, member504505-- The group SO3: the special orthogonal matrices under matrix506-- multiplication, with the identity and transposition.507def SO3 : Set :=508  Group.mk(so3Matrices,509    restrict(Ring.mul(matrixRing(realRing, 3)), so3Matrices × so3Matrices),510    Ring.one(matrixRing(realRing, 3)), so3Inverse)511512theorem SO3.carrierOf513  shows Group.carrier(SO3) = so3Matrices514proof515  simp [SO3, Group.mk.carrier]516517theorem SO3.mulOf518  shows Group.mul(SO3) = restrict(Ring.mul(matrixRing(realRing, 3)), so3Matrices × so3Matrices)519proof520  simp [SO3, Group.mk.mul]521522theorem SO3.oneOf523  shows Group.one(SO3) = matrixRing(realRing, 3)[1]524proof525  simp [SO3, Group.mk.one]526527theorem SO3.invOf528  shows Group.inv(SO3) = so3Inverse529proof530  simp [SO3, Group.mk.inv]531532theorem SO3.engine533  shows IsGroup(so3Matrices,534    restrict(Ring.mul(matrixRing(realRing, 3)), so3Matrices × so3Matrices),535    Ring.one(matrixRing(realRing, 3)), so3Inverse)536proof537  have ring := matrixRing.real_ring538  have monoid := IsRing.multiplicative with (Ring.parts with ring)539  have magma := IsSemigroup.magma with (IsMonoid.semigroup with monoid)540  have associative := IsMonoid.associative with monoid541  have identity := IsMonoid.identity with monoid542  have subset := so3Matrices.subset543  have closed : ClosedBinary(so3Matrices, Ring.mul(matrixRing(realRing, 3)))544    intros M hM N hN545    have matrixM := so3Matrices.matrix with hM546    have matrixN := so3Matrices.matrix with hN547    exact so3Matrices.mul_mem with *548  have unitIn := so3Matrices.one_mem549  have rFunction := restrictBinary.function with magma, subset, closed550  have rMagma : IsMagma(so3Matrices,551      restrict(Ring.mul(matrixRing(realRing, 3)), so3Matrices × so3Matrices))552    exact rFunction553  have rAssociative := restrictBinary.associative with magma, subset, closed, associative554  have rIdentity := restrictBinary.identity with magma, subset, closed, identity, unitIn555  have rInverse : Inverse(so3Matrices,556      restrict(Ring.mul(matrixRing(realRing, 3)), so3Matrices × so3Matrices),557      Ring.one(matrixRing(realRing, 3)), so3Inverse)558    constructor559    . exact so3Inverse.function560    . intros M hM561      have matrixM := so3Matrices.matrix with hM562      have transposed := so3Matrices.transpose_mem with matrixM, hM563      have value := so3Inverse.value with hM564      have transposedMatrix := transpose.matrix at M with *565      have leftValue := restrictBinary.value at Ring.carrier(matrixRing(realRing, 3)),566        so3Matrices, Ring.mul(matrixRing(realRing, 3)), transpose(M), M567        with magma, subset, closed, transposed, hM568      have rightValue := restrictBinary.value at Ring.carrier(matrixRing(realRing, 3)),569        so3Matrices, Ring.mul(matrixRing(realRing, 3)), M, transpose(M)570        with magma, subset, closed, hM, transposed571      have orthogonal := so3Matrices.orthogonal with hM572      have left := Orthogonal.left with orthogonal573      have right := Orthogonal.right with orthogonal574      rw value575      constructor576      . rw leftValue577        exact left578      . rw rightValue579        exact right580  unfold IsGroup581  exact ⟨⟨⟨rMagma, rAssociative⟩, rIdentity⟩, rInverse⟩582583instance SO3.group584  shows Group(SO3)585proof586  have engine := SO3.engine587  unfold SO3588  exact Group.of_parts with engine589590-- Sets of vectors carried into themselves by every special orthogonal591-- matrix: ℝ³ itself, and the unit sphere, since rotations preserve the592-- squared norm.593predicate Invariant (X : Set) :=594  X ⊆ ℝ³ ∧ ∀ M ∈ so3Matrices, ∀ v ∈ X, matrixVector(M, v) ∈ X595596theorem Invariant.space597  shows Invariant(ℝ³)598proof599  unfold Invariant600  constructor601  . exact Subset.reflexive at ℝ³602  . intros M hM v hv603    have matrix := so3Matrices.matrix with hM604    have vector := ℝ³.function with hv605    have image := matrixVector.vector with matrix, vector606    exact ℝ³.of_function with image607608theorem Invariant.sphere609  shows Invariant(S²)610proof611  unfold Invariant612  constructor613  . exact S².subset614  . intros M hM v hv615    have matrix := so3Matrices.matrix with hM616    have orthogonal := so3Matrices.orthogonal with hM617    obtain ⟨inSpace, unit⟩ := S².membership.forward with hv618    have vector := ℝ³.function with inSpace619    have image := matrixVector.vector with matrix, vector620    have imageInSpace := ℝ³.of_function with image621    have norm := Orthogonal.normSq with orthogonal, vector622    have imageUnit : normSq(M · v) = (1:R)623      rw norm624      exact unit625    exact S².membership.backward with ⟨imageInSpace, imageUnit⟩626627-- The action graph of SO3 on an invariant set X: the pair (M, v) is sent628-- to M · v.629defunique matrixActionValue (X q : Set) (w ∈ X) :=630  ∃ M ∈ so3Matrices, ∃ v ∈ X, q = (M, v) ∧ w = matrixVector(M, v)631requires invariant : Invariant(X)632requires pair : q ∈ so3Matrices × X633proof634  obtain ⟨bound, M, hM, v, hv, shape⟩ := product.membership.forward with pair635  obtain ⟨subset, closed⟩ := invariant636  have value := closed with M, hM, v, hv637  refine ⟨matrixVector(M, v), value, M, hM, v, hv, shape, rfl⟩638uniqueness639  intros u hu first w hw second640  obtain ⟨M, hM, x, hx, shapeU, valueU⟩ := first641  obtain ⟨N, hN, y, hy, shapeV, valueV⟩ := second642  have equal : (M, x) = (N, y)643    cc644  have coordinates := orderedPair.injective at M, x, N, y with equal645  cc646647defgraph matrixAction (X : Set) (q ∈ so3Matrices × X) : X := matrixActionValue(X, q)648requires invariant : Invariant(X)649proof650  have selected := matrixActionValue.selected at X, q with *651  exact selected.left652653theorem matrixAction.apply (X M v : Set)654  requires invariant : Invariant(X)655  requires hM : M ∈ so3Matrices656  requires hv : v ∈ X657  shows matrixAction(X)(M, v) = M · v658proof659  have pair := product.pair at M, v, so3Matrices, X with *660  have selected := matrixActionValue.selected at X, (M, v) with *661  obtain ⟨N, hN, w, hw, shape, result⟩ := selected.right662  have coordinates := orderedPair.injective with shape663  have value := matrixAction.value at X, (M, v) with *664  unfold call2665  cc666667theorem matrixAction.action (X : Set)668  requires invariant : Invariant(X)669  shows matrixAction(X) : SO3 ↷ X670proof671  have group := SO3.group672  have function := matrixAction.function at X with invariant673  rw ← SO3.carrierOf at function674  obtain ⟨subset, closed⟩ := invariant675  apply Action.mk with group, function676  . intros x hx677    have vector := ℝ³.function with (subset with x, hx)678    have unitIn := so3Matrices.one_mem679    rw SO3.oneOf680    have value := matrixAction.apply at X, matrixRing(realRing, 3)[1], x with *681    rw value682    exact matrixVector.one with vector683  . intros g hg h hh x hx684    rw SO3.carrierOf at hg685    rw SO3.carrierOf at hh686    have matrixG := so3Matrices.matrix with hg687    have matrixH := so3Matrices.matrix with hh688    have vector := ℝ³.function with (subset with x, hx)689    have ring := matrixRing.real_ring690    have magma := IsSemigroup.magma with691      (IsMonoid.semigroup with (IsRing.multiplicative with (Ring.parts with ring)))692    have closedMul : ClosedBinary(so3Matrices, Ring.mul(matrixRing(realRing, 3)))693      intros M hM N hN694      have matrixM := so3Matrices.matrix with hM695      have matrixN := so3Matrices.matrix with hN696      exact so3Matrices.mul_mem with *697    have productIn := so3Matrices.mul_mem at g, h with *698    have imageIn := closed with h, hh, x, hx699    have operation := restrictBinary.value at Ring.carrier(matrixRing(realRing, 3)),700      so3Matrices, Ring.mul(matrixRing(realRing, 3)), g, h701      with magma, so3Matrices.subset, closedMul, hg, hh702    have outer := matrixAction.apply at X,703      call2(Ring.mul(matrixRing(realRing, 3)), g, h), x with *704    have inner := matrixAction.apply at X, h, x with *705    have composed := matrixAction.apply at X, g, h · x with *706    rw [SO3.mulOf, operation, outer, inner, composed]707    exact matrixVector.mul with vector708709-- The actions of SO3 on ℝ³ and on the unit sphere.710def spaceAction : Set := matrixAction(ℝ³)711def sphereAction : Set := matrixAction(S²)712713theorem spaceAction.action714  shows spaceAction : SO3 ↷ ℝ³715proof716  unfold spaceAction717  exact matrixAction.action with Invariant.space718719theorem sphereAction.action720  shows sphereAction : SO3 ↷ S²721proof722  unfold sphereAction723  exact matrixAction.action with Invariant.sphere724725theorem spaceAction.apply (M v : Set)726  requires hM : M ∈ so3Matrices727  requires hv : v ∈ ℝ³728  shows spaceAction(M, v) = M · v729proof730  unfold spaceAction731  exact matrixAction.apply with Invariant.space, hM, hv732733theorem sphereAction.apply (M v : Set)734  requires hM : M ∈ so3Matrices735  requires hv : v ∈ S²736  shows sphereAction(M, v) = M · v737proof738  unfold sphereAction739  exact matrixAction.apply with Invariant.sphere, hM, hv740