-- Orthogonal 3 × 3 real matrices: the transpose transpose(M), the orthogonal
-- matrices transpose(M) M = 1 = M transpose(M), the determinant of a 3 × 3 matrix, the
-- group SO3 of orthogonal matrices of determinant one as a structure
-- value, and its actions on ℝ³ and on the unit sphere S²
-- 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.Rotation.Orthogonal
import Vectors
import Algebra.Group.Action

-- The transpose of a 3 × 3 real matrix.
defgraph transpose (M : Set) (p ∈ 3 × 3) : ℝ := M[snd(p), fst(p)]
requires matrix : M : realRing ^ 3 × 3
proof
  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with member
  rw [shape, fst.pair, snd.pair]
  exact Matrix.real_entry at M, j, i with *

theorem transpose.entry (M : realRing ^ 3 × 3) (i j : Set)
  requires row : i ∈ 3
  requires column : j ∈ 3
  shows transpose(M)[i, j] = M[j, i]
proof
  have pair := product.pair at i, j, 3, 3 with *
  have value := transpose.value at M, (i, j) with *
  rw [value, fst.pair, snd.pair]
  rfl

instance transpose.matrix (M : realRing ^ 3 × 3)
  shows transpose(M) : realRing ^ 3 × 3
proof
  have function := transpose.function with *
  rw ← realRing.carrierOf at function
  exact Matrix.of_function with function

theorem transpose.involutive (M : realRing ^ 3 × 3)
  shows transpose(transpose(M)) = M
proof
  have outer := transpose.matrix at transpose(M) with *
  apply Matrix.ext with outer, assumption
  intros i hi j hj
  have inner := transpose.entry at transpose(M), i, j with hi, hj
  have base := transpose.entry at M, j, i with hj, hi
  rw [inner, base]
  rfl

theorem transpose.mul (M N : realRing ^ 3 × 3)
  shows transpose(M * N) = transpose(N) * transpose(M)
proof
  have product := Matrix.mul_matrix at M, N with *
  have transposedM := transpose.matrix at M with *
  have transposedN := transpose.matrix at N with *
  have left := transpose.matrix at M * N with *
  have right := Matrix.mul_matrix at transpose(N), transpose(M) with *
  apply Matrix.ext with left, right
  intros i hi j hj
  have entry := transpose.entry at M * N, i, j with *
  have expandL := matrixRing.mul_entry_three at M, N, j, i with *
  have expandR := matrixRing.mul_entry_three at transpose(N), transpose(M), i, j with *
  have t0 := transpose.entry at N, i, 0 with *
  have t1 := transpose.entry at N, i, 1 with *
  have t2 := transpose.entry at N, i, 2 with *
  have u0 := transpose.entry at M, 0, j with *
  have u1 := transpose.entry at M, 1, j with *
  have u2 := transpose.entry at M, 2, j with *
  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, j with hj
  have n0 := Matrix.real_entry at N, 0, i with *
  have n1 := Matrix.real_entry at N, 1, i with *
  have n2 := Matrix.real_entry at N, 2, i with *
  rw [entry, expandL, expandR, t0, t1, t2, u0, u1, u2]
  ring

-- The symbol singleValue(ℝ, 0, 1, j, i) is symmetric in its indices.
theorem singleValue.symmetric (i j : Set)
  shows singleValue(Ring.carrier(realRing), Ring.zero(realRing), Ring.one(realRing), j, i) =
    singleValue(Ring.carrier(realRing), Ring.zero(realRing), Ring.one(realRing), i, j)
proof
  have comm := realRing.comm_ring
  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *
  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *
  have alternatives : i = j ∨ i ≠ j by tauto
  cases alternatives with same | different
  . have sameR : j = i by cc
    have first := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),
      Ring.one(realRing), j, i with zeroIn, oneIn, same
    have second := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),
      Ring.one(realRing), i, j with zeroIn, oneIn, sameR
    rw [first, second]
    rfl
  . have differentR : j ≠ i
      intro equal
      apply different
      cc
    have first := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
      Ring.one(realRing), j, i with zeroIn, oneIn, different
    have second := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
      Ring.one(realRing), i, j with zeroIn, oneIn, differentR
    rw [first, second]
    rfl

theorem transpose.one
  shows transpose(matrixRing(realRing, 3)[1]) = matrixRing(realRing, 3)[1]
proof
  have comm := realRing.comm_ring
  have one := Matrix.one_matrix
  have transposed := transpose.matrix at matrixRing(realRing, 3)[1] with *
  apply Matrix.ext with transposed, one
  intros i hi j hj
  have entry := transpose.entry at matrixRing(realRing, 3)[1], i, j with *
  have first := matrixRing.one_entry at realRing, 3, j, i with *
  have second := matrixRing.one_entry at realRing, 3, i, j with *
  rw [entry, first, second]
  exact singleValue.symmetric at j, i

-- The monoid laws of the matrix ring under multiplication.
theorem matrixRing.mul_assoc (M N P : realRing ^ 3 × 3)
  shows M * N * P = M * (N * P)
proof
  have ring := matrixRing.real_ring
  have monoid := IsRing.multiplicative with (Ring.parts with ring)
  have associative := IsMonoid.associative with monoid
  exact Associative.law with associative, *

theorem matrixRing.one_mul (M : realRing ^ 3 × 3)
  shows matrixRing(realRing, 3)[1] * M = M
proof
  have ring := matrixRing.real_ring
  have monoid := IsRing.multiplicative with (Ring.parts with ring)
  exact IsMonoid.left_identity with monoid, *

theorem matrixRing.mul_one (M : realRing ^ 3 × 3)
  shows M * matrixRing(realRing, 3)[1] = M
proof
  have ring := matrixRing.real_ring
  have monoid := IsRing.multiplicative with (Ring.parts with ring)
  exact IsMonoid.right_identity with monoid, *

-- Orthogonal matrices: both products with the transpose are the identity.
predicate Orthogonal (M : Set) :=
  Matrix(M, realRing, 3, 3) ∧
  call2(Ring.mul(matrixRing(realRing, 3)), transpose(M), M) =
    Ring.one(matrixRing(realRing, 3)) ∧
  call2(Ring.mul(matrixRing(realRing, 3)), M, transpose(M)) =
    Ring.one(matrixRing(realRing, 3))

theorem Orthogonal.mk (M : realRing ^ 3 × 3)
  requires left : transpose(M) * M = matrixRing(realRing, 3)[1]
  requires right : M * transpose(M) = matrixRing(realRing, 3)[1]
  shows Orthogonal(M)
proof
  unfold Orthogonal
  exact ⟨assumption, left, right⟩

theorem Orthogonal.matrix (M : Set)
  requires orthogonal : Orthogonal(M)
  shows M : realRing ^ 3 × 3
proof
  obtain ⟨matrix, left, right⟩ := orthogonal
  exact matrix

theorem Orthogonal.left (M : realRing ^ 3 × 3)
  requires orthogonal : Orthogonal(M)
  shows transpose(M) * M = matrixRing(realRing, 3)[1]
proof
  obtain ⟨matrix, left, right⟩ := orthogonal
  exact left

theorem Orthogonal.right (M : realRing ^ 3 × 3)
  requires orthogonal : Orthogonal(M)
  shows M * transpose(M) = matrixRing(realRing, 3)[1]
proof
  obtain ⟨matrix, left, right⟩ := orthogonal
  exact right

theorem Orthogonal.one
  shows Orthogonal(matrixRing(realRing, 3)[1])
proof
  have one := Matrix.one_matrix
  have law := matrixRing.mul_one at matrixRing(realRing, 3)[1] with one
  apply Orthogonal.mk with one
  . rw transpose.one
    exact law
  . rw transpose.one
    exact law

theorem Orthogonal.transpose (M : realRing ^ 3 × 3)
  requires orthogonal : Orthogonal(M)
  shows Orthogonal(transpose(M))
proof
  have transposed := transpose.matrix at M with *
  have left := Orthogonal.left with orthogonal
  have right := Orthogonal.right with orthogonal
  apply Orthogonal.mk with transposed
  . rw transpose.involutive
    exact right
  . rw transpose.involutive
    exact left

theorem Orthogonal.mul (M N : realRing ^ 3 × 3)
  requires orthogonalM : Orthogonal(M)
  requires orthogonalN : Orthogonal(N)
  shows Orthogonal(M * N)
proof
  have ring := matrixRing.real_ring
  have product := Matrix.mul_matrix at M, N with *
  have transposedM := transpose.matrix at M with *
  have transposedN := transpose.matrix at N with *
  have leftM := Orthogonal.left with orthogonalM
  have rightM := Orthogonal.right with orthogonalM
  have leftN := Orthogonal.left with orthogonalN
  have rightN := Orthogonal.right with orthogonalN
  have assocL := matrixRing.mul_assoc at transpose(N), transpose(M), M * N with *
  have assocL2 := matrixRing.mul_assoc at transpose(M), M, N with *
  have unitL := matrixRing.one_mul at N with *
  have assocR := matrixRing.mul_assoc at M, N, transpose(N) * transpose(M) with *
  have assocR2 := matrixRing.mul_assoc at N, transpose(N), transpose(M) with *
  have unitR := matrixRing.one_mul at transpose(M) with *
  apply Orthogonal.mk with product
  . rw transpose.mul
    calc
      transpose(N) * transpose(M) * (M * N) =
          transpose(N) * (transpose(M) * M * N) := by rw [assocL, assocL2]
      _ = transpose(N) * N := by rw [leftM, unitL]
      _ = matrixRing(realRing, 3)[1] := leftN
  . rw transpose.mul
    calc
      M * N * (transpose(N) * transpose(M)) =
          M * (N * transpose(N) * transpose(M)) := by rw [assocR, assocR2]
      _ = M * transpose(M) := by rw [rightN, unitR]
      _ = matrixRing(realRing, 3)[1] := rightM

-- The determinant of a 3 × 3 real matrix, expanded along the first row.
def determinant3 (M : Set) : Set :=
  (M[0, 0]:R) * ((M[1, 1]:R) * (M[2, 2]:R) - (M[1, 2]:R) * (M[2, 1]:R)) -
  (M[0, 1]:R) * ((M[1, 0]:R) * (M[2, 2]:R) - (M[1, 2]:R) * (M[2, 0]:R)) +
  (M[0, 2]:R) * ((M[1, 0]:R) * (M[2, 1]:R) - (M[1, 1]:R) * (M[2, 0]:R))

theorem determinant3.value (M : Set)
  shows determinant3(M) =
    (M[0, 0]:R) * ((M[1, 1]:R) * (M[2, 2]:R) - (M[1, 2]:R) * (M[2, 1]:R)) -
    (M[0, 1]:R) * ((M[1, 0]:R) * (M[2, 2]:R) - (M[1, 2]:R) * (M[2, 0]:R)) +
    (M[0, 2]:R) * ((M[1, 0]:R) * (M[2, 1]:R) - (M[1, 1]:R) * (M[2, 0]:R))
proof
  simp [determinant3]

theorem Matrix.entries_real (M : realRing ^ 3 × 3)
  shows M[0, 0] ∈ ℝ ∧ M[0, 1] ∈ ℝ ∧ M[0, 2] ∈ ℝ ∧ M[1, 0] ∈ ℝ ∧ M[1, 1] ∈ ℝ ∧
    M[1, 2] ∈ ℝ ∧ M[2, 0] ∈ ℝ ∧ M[2, 1] ∈ ℝ ∧ M[2, 2] ∈ ℝ
proof
  obtain ⟨m00, m01, m02⟩ := Matrix.row_real at M, 0 with index.zero_mem
  obtain ⟨m10, m11, m12⟩ := Matrix.row_real at M, 1 with index.one_mem
  obtain ⟨m20, m21, m22⟩ := Matrix.row_real at M, 2 with index.two_mem
  exact ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩

instance determinant3.real (M : realRing ^ 3 × 3)
  shows determinant3(M) ∈ ℝ
proof
  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real with *
  rw determinant3.value
  typecheck

theorem determinant3.transpose (M : realRing ^ 3 × 3)
  shows determinant3(transpose(M)) = determinant3(M)
proof
  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real with *
  have t00 := transpose.entry at M, 0, 0 with *
  have t01 := transpose.entry at M, 0, 1 with *
  have t02 := transpose.entry at M, 0, 2 with *
  have t10 := transpose.entry at M, 1, 0 with *
  have t11 := transpose.entry at M, 1, 1 with *
  have t12 := transpose.entry at M, 1, 2 with *
  have t20 := transpose.entry at M, 2, 0 with *
  have t21 := transpose.entry at M, 2, 1 with *
  have t22 := transpose.entry at M, 2, 2 with *
  rw [determinant3.value, determinant3.value, t00, t01, t02, t10, t11, t12, t20, t21, t22]
  ring

theorem determinant3.mul (M N : realRing ^ 3 × 3)
  shows determinant3(M * N) = determinant3(M) * determinant3(N)
proof
  have product := Matrix.mul_matrix at M, N with *
  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real at M with *
  obtain ⟨n00, n01, n02, n10, n11, n12, n20, n21, n22⟩ := Matrix.entries_real at N with *
  have p00 := matrixRing.mul_entry_three at M, N, 0, 0 with *
  have p01 := matrixRing.mul_entry_three at M, N, 0, 1 with *
  have p02 := matrixRing.mul_entry_three at M, N, 0, 2 with *
  have p10 := matrixRing.mul_entry_three at M, N, 1, 0 with *
  have p11 := matrixRing.mul_entry_three at M, N, 1, 1 with *
  have p12 := matrixRing.mul_entry_three at M, N, 1, 2 with *
  have p20 := matrixRing.mul_entry_three at M, N, 2, 0 with *
  have p21 := matrixRing.mul_entry_three at M, N, 2, 1 with *
  have p22 := matrixRing.mul_entry_three at M, N, 2, 2 with *
  rw [determinant3.value, determinant3.value, determinant3.value,
    p00, p01, p02, p10, p11, p12, p20, p21, p22]
  ring

theorem determinant3.one
  shows determinant3(matrixRing(realRing, 3)[1]) = (1:R)
proof
  have comm := realRing.comm_ring
  have one := Matrix.one_matrix
  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *
  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *
  have same0 : 0 = 0 by rfl
  have same1 : 1 = 1 by rfl
  have same2 : 2 = 2 by rfl
  have e00 := matrixRing.one_entry at realRing, 3, 0, 0 with *
  have e01 := matrixRing.one_entry at realRing, 3, 0, 1 with *
  have e02 := matrixRing.one_entry at realRing, 3, 0, 2 with *
  have e10 := matrixRing.one_entry at realRing, 3, 1, 0 with *
  have e11 := matrixRing.one_entry at realRing, 3, 1, 1 with *
  have e12 := matrixRing.one_entry at realRing, 3, 1, 2 with *
  have e20 := matrixRing.one_entry at realRing, 3, 2, 0 with *
  have e21 := matrixRing.one_entry at realRing, 3, 2, 1 with *
  have e22 := matrixRing.one_entry at realRing, 3, 2, 2 with *
  have s00 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 0, 0 with zeroIn, oneIn, same0
  have s11 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 1, 1 with zeroIn, oneIn, same1
  have s22 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 2, 2 with zeroIn, oneIn, same2
  have s10 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 1, 0 with zeroIn, oneIn, index.zero_ne_one
  have s20 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 2, 0 with zeroIn, oneIn, index.zero_ne_two
  have s01 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 0, 1 with zeroIn, oneIn, index.one_ne_zero
  have s21 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 2, 1 with zeroIn, oneIn, index.one_ne_two
  have s02 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 0, 2 with zeroIn, oneIn, index.two_ne_zero
  have s12 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), 1, 2 with zeroIn, oneIn, index.two_ne_one
  rw [determinant3.value, e00, e01, e02, e10, e11, e12, e20, e21, e22,
    s00, s11, s22, s10, s20, s01, s21, s02, s12, realRing.zero_value, realRing.one_value]
  ring

-- An orthogonal matrix preserves the dot products of columns, hence the
-- squared norm of every vector.
theorem Orthogonal.column (M : realRing ^ 3 × 3) (j k : Set)
  requires orthogonal : Orthogonal(M)
  requires hj : j ∈ 3
  requires hk : k ∈ 3
  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) =
    singleValue(Ring.carrier(realRing), Ring.zero(realRing), Ring.one(realRing), k, j)
proof
  have comm := realRing.comm_ring
  have transposed := transpose.matrix at M with *
  have left := Orthogonal.left with orthogonal
  have entry := matrixRing.mul_entry_three at transpose(M), M, j, k with *
  have unit := matrixRing.one_entry at realRing, 3, j, k with *
  have t0 := transpose.entry at M, j, 0 with *
  have t1 := transpose.entry at M, j, 1 with *
  have t2 := transpose.entry at M, j, 2 with *
  rw [left, unit, t0, t1, t2] at entry
  symm at entry
  exact entry

theorem Orthogonal.column_same (M : realRing ^ 3 × 3) (j : Set)
  requires orthogonal : Orthogonal(M)
  requires hj : j ∈ 3
  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) = 1
proof
  have comm := realRing.comm_ring
  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *
  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *
  have same : j = j by rfl
  have column := Orthogonal.column at M, j, j with *
  have selected := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), j, j with zeroIn, oneIn, same
  rw [column, selected, realRing.one_value]
  rfl

theorem Orthogonal.column_other (M : realRing ^ 3 × 3) (j k : Set)
  requires orthogonal : Orthogonal(M)
  requires hj : j ∈ 3
  requires hk : k ∈ 3
  requires different : j ≠ k
  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) = 0
proof
  have comm := realRing.comm_ring
  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *
  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *
  have column := Orthogonal.column at M, j, k with *
  have selected := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),
    Ring.one(realRing), k, j with zeroIn, oneIn, different
  rw [column, selected, realRing.zero_value]
  rfl

theorem Orthogonal.normSq (M : realRing ^ 3 × 3) (v : Set)
  requires orthogonal : Orthogonal(M)
  requires vector : v : 3 → ℝ
  shows normSq(M · v) = normSq(v)
proof
  obtain ⟨m00, m01, m02, m10, m11, m12, m20, m21, m22⟩ := Matrix.entries_real with *
  have v0 := vector.component_real at v, 0 with *
  have v1 := vector.component_real at v, 1 with *
  have v2 := vector.component_real at v, 2 with *
  have c00 := Orthogonal.column_same at M, 0 with *
  have c11 := Orthogonal.column_same at M, 1 with *
  have c22 := Orthogonal.column_same at M, 2 with *
  have c01 := Orthogonal.column_other at M, 0, 1 with orthogonal, index.zero_mem,
    index.one_mem, index.zero_ne_one
  have c02 := Orthogonal.column_other at M, 0, 2 with orthogonal, index.zero_mem,
    index.two_mem, index.zero_ne_two
  have c12 := Orthogonal.column_other at M, 1, 2 with orthogonal, index.one_mem,
    index.two_mem, index.one_ne_two
  have e0 := matrixVector.entry at M, v, 0 with *
  have e1 := matrixVector.entry at M, v, 1 with *
  have e2 := matrixVector.entry at M, v, 2 with *
  have expand : normSq(M · v) =
      ((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)) +
      ((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)) +
      ((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)) +
      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)) +
      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)) +
      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))
    rw [normSq.value, e0, e1, e2]
    ring
  rw [expand, c00, c11, c22, c01, c02, c12, normSq.value]
  ring

-- The special orthogonal matrices: orthogonal, of determinant one.
def so3Matrices : Set :=
  { M ∈ Ring.carrier(matrixRing(realRing, 3)) | Orthogonal(M) ∧ determinant3(M) = (1:R) }

theorem so3Matrices.mk (M : realRing ^ 3 × 3)
  requires orthogonal : Orthogonal(M)
  requires unit : determinant3(M) = (1:R)
  shows M ∈ so3Matrices
proof
  have member := Matrix.mem_ring at M, realRing, 3 with assumption
  exact so3Matrices.membership.backward with ⟨member, orthogonal, unit⟩

theorem so3Matrices.matrix (M : Set)
  requires member : M ∈ so3Matrices
  shows M : realRing ^ 3 × 3
proof
  obtain ⟨ring, orthogonal, unit⟩ := so3Matrices.membership.forward with member
  exact Matrix.of_mem with ring

theorem so3Matrices.orthogonal (M : Set)
  requires member : M ∈ so3Matrices
  shows Orthogonal(M)
proof
  obtain ⟨ring, orthogonal, unit⟩ := so3Matrices.membership.forward with member
  exact orthogonal

theorem so3Matrices.determinant (M : Set)
  requires member : M ∈ so3Matrices
  shows determinant3(M) = (1:R)
proof
  obtain ⟨ring, orthogonal, unit⟩ := so3Matrices.membership.forward with member
  exact unit

theorem so3Matrices.subset
  shows so3Matrices ⊆ Ring.carrier(matrixRing(realRing, 3))
proof
  intros M hM
  obtain ⟨ring, orthogonal, unit⟩ := so3Matrices.membership.forward with hM
  exact ring

theorem so3Matrices.one_mem
  shows matrixRing(realRing, 3)[1] ∈ so3Matrices
proof
  have one := Matrix.one_matrix
  exact so3Matrices.mk with Orthogonal.one, determinant3.one

theorem so3Matrices.mul_mem (M N : realRing ^ 3 × 3)
  requires hM : M ∈ so3Matrices
  requires hN : N ∈ so3Matrices
  shows M * N ∈ so3Matrices
proof
  have product := Matrix.mul_matrix at M, N with *
  have orthogonal := Orthogonal.mul with (so3Matrices.orthogonal with hM),
    (so3Matrices.orthogonal with hN)
  have unitM := so3Matrices.determinant with hM
  have unitN := so3Matrices.determinant with hN
  have unit : determinant3(M * N) = (1:R)
    rw [determinant3.mul, unitM, unitN]
    ring
  exact so3Matrices.mk with orthogonal, unit

theorem so3Matrices.transpose_mem (M : realRing ^ 3 × 3)
  requires hM : M ∈ so3Matrices
  shows transpose(M) ∈ so3Matrices
proof
  have transposed := transpose.matrix at M with *
  have orthogonal := Orthogonal.transpose with (so3Matrices.orthogonal with hM)
  have unitM := so3Matrices.determinant with hM
  have unit : determinant3(transpose(M)) = (1:R)
    rw [determinant3.transpose, unitM]
    rfl
  exact so3Matrices.mk with orthogonal, unit

-- The inverse of a special orthogonal matrix is its transpose.
defgraph so3Inverse (M ∈ so3Matrices) : so3Matrices := transpose(M)
proof
  have matrix := so3Matrices.matrix with member
  exact so3Matrices.transpose_mem with matrix, member

-- The group SO3: the special orthogonal matrices under matrix
-- multiplication, with the identity and transposition.
def SO3 : Set :=
  Group.mk(so3Matrices,
    restrict(Ring.mul(matrixRing(realRing, 3)), so3Matrices × so3Matrices),
    Ring.one(matrixRing(realRing, 3)), so3Inverse)

theorem SO3.carrierOf
  shows Group.carrier(SO3) = so3Matrices
proof
  simp [SO3, Group.mk.carrier]

theorem SO3.mulOf
  shows Group.mul(SO3) = restrict(Ring.mul(matrixRing(realRing, 3)), so3Matrices × so3Matrices)
proof
  simp [SO3, Group.mk.mul]

theorem SO3.oneOf
  shows Group.one(SO3) = matrixRing(realRing, 3)[1]
proof
  simp [SO3, Group.mk.one]

theorem SO3.invOf
  shows Group.inv(SO3) = so3Inverse
proof
  simp [SO3, Group.mk.inv]

theorem SO3.engine
  shows IsGroup(so3Matrices,
    restrict(Ring.mul(matrixRing(realRing, 3)), so3Matrices × so3Matrices),
    Ring.one(matrixRing(realRing, 3)), so3Inverse)
proof
  have ring := matrixRing.real_ring
  have monoid := IsRing.multiplicative with (Ring.parts with ring)
  have magma := IsSemigroup.magma with (IsMonoid.semigroup with monoid)
  have associative := IsMonoid.associative with monoid
  have identity := IsMonoid.identity with monoid
  have subset := so3Matrices.subset
  have closed : ClosedBinary(so3Matrices, Ring.mul(matrixRing(realRing, 3)))
    intros M hM N hN
    have matrixM := so3Matrices.matrix with hM
    have matrixN := so3Matrices.matrix with hN
    exact so3Matrices.mul_mem with *
  have unitIn := so3Matrices.one_mem
  have rFunction := restrictBinary.function with magma, subset, closed
  have rMagma : IsMagma(so3Matrices,
      restrict(Ring.mul(matrixRing(realRing, 3)), so3Matrices × so3Matrices))
    exact rFunction
  have rAssociative := restrictBinary.associative with magma, subset, closed, associative
  have rIdentity := restrictBinary.identity with magma, subset, closed, identity, unitIn
  have rInverse : Inverse(so3Matrices,
      restrict(Ring.mul(matrixRing(realRing, 3)), so3Matrices × so3Matrices),
      Ring.one(matrixRing(realRing, 3)), so3Inverse)
    constructor
    . exact so3Inverse.function
    . intros M hM
      have matrixM := so3Matrices.matrix with hM
      have transposed := so3Matrices.transpose_mem with matrixM, hM
      have value := so3Inverse.value with hM
      have transposedMatrix := transpose.matrix at M with *
      have leftValue := restrictBinary.value at Ring.carrier(matrixRing(realRing, 3)),
        so3Matrices, Ring.mul(matrixRing(realRing, 3)), transpose(M), M
        with magma, subset, closed, transposed, hM
      have rightValue := restrictBinary.value at Ring.carrier(matrixRing(realRing, 3)),
        so3Matrices, Ring.mul(matrixRing(realRing, 3)), M, transpose(M)
        with magma, subset, closed, hM, transposed
      have orthogonal := so3Matrices.orthogonal with hM
      have left := Orthogonal.left with orthogonal
      have right := Orthogonal.right with orthogonal
      rw value
      constructor
      . rw leftValue
        exact left
      . rw rightValue
        exact right
  unfold IsGroup
  exact ⟨⟨⟨rMagma, rAssociative⟩, rIdentity⟩, rInverse⟩

instance SO3.group
  shows Group(SO3)
proof
  have engine := SO3.engine
  unfold SO3
  exact Group.of_parts with engine

-- Sets of vectors carried into themselves by every special orthogonal
-- matrix: ℝ³ itself, and the unit sphere, since rotations preserve the
-- squared norm.
predicate Invariant (X : Set) :=
  X ⊆ ℝ³ ∧ ∀ M ∈ so3Matrices, ∀ v ∈ X, matrixVector(M, v) ∈ X

theorem Invariant.space
  shows Invariant(ℝ³)
proof
  unfold Invariant
  constructor
  . exact Subset.reflexive at ℝ³
  . intros M hM v hv
    have matrix := so3Matrices.matrix with hM
    have vector := ℝ³.function with hv
    have image := matrixVector.vector with matrix, vector
    exact ℝ³.of_function with image

theorem Invariant.sphere
  shows Invariant(S²)
proof
  unfold Invariant
  constructor
  . exact S².subset
  . intros M hM v hv
    have matrix := so3Matrices.matrix with hM
    have orthogonal := so3Matrices.orthogonal with hM
    obtain ⟨inSpace, unit⟩ := S².membership.forward with hv
    have vector := ℝ³.function with inSpace
    have image := matrixVector.vector with matrix, vector
    have imageInSpace := ℝ³.of_function with image
    have norm := Orthogonal.normSq with orthogonal, vector
    have imageUnit : normSq(M · v) = (1:R)
      rw norm
      exact unit
    exact S².membership.backward with ⟨imageInSpace, imageUnit⟩

-- The action graph of SO3 on an invariant set X: the pair (M, v) is sent
-- to M · v.
defunique matrixActionValue (X q : Set) (w ∈ X) :=
  ∃ M ∈ so3Matrices, ∃ v ∈ X, q = (M, v) ∧ w = matrixVector(M, v)
requires invariant : Invariant(X)
requires pair : q ∈ so3Matrices × X
proof
  obtain ⟨bound, M, hM, v, hv, shape⟩ := product.membership.forward with pair
  obtain ⟨subset, closed⟩ := invariant
  have value := closed with M, hM, v, hv
  refine ⟨matrixVector(M, v), value, M, hM, v, hv, shape, rfl⟩
uniqueness
  intros u hu first w hw second
  obtain ⟨M, hM, x, hx, shapeU, valueU⟩ := first
  obtain ⟨N, hN, y, hy, shapeV, valueV⟩ := second
  have equal : (M, x) = (N, y)
    cc
  have coordinates := orderedPair.injective at M, x, N, y with equal
  cc

defgraph matrixAction (X : Set) (q ∈ so3Matrices × X) : X := matrixActionValue(X, q)
requires invariant : Invariant(X)
proof
  have selected := matrixActionValue.selected at X, q with *
  exact selected.left

theorem matrixAction.apply (X M v : Set)
  requires invariant : Invariant(X)
  requires hM : M ∈ so3Matrices
  requires hv : v ∈ X
  shows matrixAction(X)(M, v) = M · v
proof
  have pair := product.pair at M, v, so3Matrices, X with *
  have selected := matrixActionValue.selected at X, (M, v) with *
  obtain ⟨N, hN, w, hw, shape, result⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := matrixAction.value at X, (M, v) with *
  unfold call2
  cc

theorem matrixAction.action (X : Set)
  requires invariant : Invariant(X)
  shows matrixAction(X) : SO3 ↷ X
proof
  have group := SO3.group
  have function := matrixAction.function at X with invariant
  rw ← SO3.carrierOf at function
  obtain ⟨subset, closed⟩ := invariant
  apply Action.mk with group, function
  . intros x hx
    have vector := ℝ³.function with (subset with x, hx)
    have unitIn := so3Matrices.one_mem
    rw SO3.oneOf
    have value := matrixAction.apply at X, matrixRing(realRing, 3)[1], x with *
    rw value
    exact matrixVector.one with vector
  . intros g hg h hh x hx
    rw SO3.carrierOf at hg
    rw SO3.carrierOf at hh
    have matrixG := so3Matrices.matrix with hg
    have matrixH := so3Matrices.matrix with hh
    have vector := ℝ³.function with (subset with x, hx)
    have ring := matrixRing.real_ring
    have magma := IsSemigroup.magma with
      (IsMonoid.semigroup with (IsRing.multiplicative with (Ring.parts with ring)))
    have closedMul : ClosedBinary(so3Matrices, Ring.mul(matrixRing(realRing, 3)))
      intros M hM N hN
      have matrixM := so3Matrices.matrix with hM
      have matrixN := so3Matrices.matrix with hN
      exact so3Matrices.mul_mem with *
    have productIn := so3Matrices.mul_mem at g, h with *
    have imageIn := closed with h, hh, x, hx
    have operation := restrictBinary.value at Ring.carrier(matrixRing(realRing, 3)),
      so3Matrices, Ring.mul(matrixRing(realRing, 3)), g, h
      with magma, so3Matrices.subset, closedMul, hg, hh
    have outer := matrixAction.apply at X,
      call2(Ring.mul(matrixRing(realRing, 3)), g, h), x with *
    have inner := matrixAction.apply at X, h, x with *
    have composed := matrixAction.apply at X, g, h · x with *
    rw [SO3.mulOf, operation, outer, inner, composed]
    exact matrixVector.mul with vector

-- The actions of SO3 on ℝ³ and on the unit sphere.
def spaceAction : Set := matrixAction(ℝ³)
def sphereAction : Set := matrixAction(S²)

theorem spaceAction.action
  shows spaceAction : SO3 ↷ ℝ³
proof
  unfold spaceAction
  exact matrixAction.action with Invariant.space

theorem sphereAction.action
  shows sphereAction : SO3 ↷ S²
proof
  unfold sphereAction
  exact matrixAction.action with Invariant.sphere

theorem spaceAction.apply (M v : Set)
  requires hM : M ∈ so3Matrices
  requires hv : v ∈ ℝ³
  shows spaceAction(M, v) = M · v
proof
  unfold spaceAction
  exact matrixAction.apply with Invariant.space, hM, hv

theorem sphereAction.apply (M v : Set)
  requires hM : M ∈ so3Matrices
  requires hv : v ∈ S²
  shows sphereAction(M, v) = M · v
proof
  unfold sphereAction
  exact matrixAction.apply with Invariant.sphere, hM, hv