def M_s_Z : ZMAT

We define the Sato Subgroup of SO3 and show it is isomorphic to the free group on two generators.

Equations

• M_s_Z = !![6, 2, 3; 2, 3, -6; -3, 6, 2]

def M_t_Z : ZMAT

Equations

• M_t_Z = !![2, -6, 3; 6, 3, 2; -3, 2, 6]

def M_s_Z_trans : ZMAT

Equations

• M_s_Z_trans = !![6, 2, -3; 2, 3, 6; 3, -6, 2]

def M_t_Z_trans : ZMAT

Equations

• M_t_Z_trans = !![2, 6, -3; -6, 3, 2; 3, 2, 6]

theorem M_s_Z_transpose_def : Matrix.transpose M_s_Z = M_s_Z_trans

theorem M_t_Z_transpose_def : Matrix.transpose M_t_Z = M_t_Z_trans

theorem fnlem_s : M_s_Z * M_s_Z_trans = Matrix.diagonal 49

theorem fnlem_t : M_t_Z * M_t_Z_trans = Matrix.diagonal 49

def M_s : MAT

Equations

• M_s = to_MAT M_s_Z

def M_t : MAT

Equations

• M_t = to_MAT M_t_Z

theorem ms_def : M_s = to_MAT M_s_Z

theorem mt_def : M_t = to_MAT M_t_Z

noncomputable def M_s_normed : MAT

Equations

• M_s_normed = (1 / 7) • M_s

noncomputable def M_t_normed : MAT

Equations

• M_t_normed = (1 / 7) • M_t

theorem M_s_normed_transpose_def : Matrix.transpose M_s_normed = (1 / 7) • to_MAT M_s_Z_trans

theorem M_t_normed_transpose_def : Matrix.transpose M_t_normed = (1 / 7) • to_MAT M_t_Z_trans

theorem M_s_normed_is_special : M_s_normed ∈ SO3

theorem M_t_normed_is_special : M_t_normed ∈ SO3

noncomputable def s_op_n : ↥SO3

Equations

• s_op_n = ⟨M_s_normed, M_s_normed_is_special⟩

noncomputable def t_op_n : ↥SO3

Equations

• t_op_n = ⟨M_t_normed, M_t_normed_is_special⟩

noncomputable def s_i_op_n : ↥SO3

Equations

• s_i_op_n = s_op_n⁻¹

theorem s_i_op_n_def : s_i_op_n = s_op_n⁻¹

noncomputable def t_i_op_n : ↥SO3

Equations

• t_i_op_n = t_op_n⁻¹

theorem t_i_op_n_def : t_i_op_n = t_op_n⁻¹

def M_s_i_Z : ZMAT

Equations

• M_s_i_Z = !![6, 2, -3; 2, 3, 6; 3, -6, 2]

def M_s_i : MAT

Equations

• M_s_i = to_MAT M_s_i_Z

theorem msi_def : M_s_i = to_MAT M_s_i_Z

theorem msinv_lem : M_s_i * M_s = Matrix.diagonal fun (x : Fin 3) => 49

theorem msinv_lem2 : M_s * M_s_i = Matrix.diagonal fun (x : Fin 3) => 49

theorem s_i_op_n_equiv : ↑s_i_op_n = 7⁻¹ • M_s_i

theorem s_i_op_n_equiv_2 : 7 • ↑s_i_op_n = M_s_i

def M_t_i_Z : ZMAT

Equations

• M_t_i_Z = !![2, 6, -3; -6, 3, 2; 3, 2, 6]

def M_t_i : MAT

Equations

• M_t_i = to_MAT M_t_i_Z

theorem mti_def : M_t_i = to_MAT M_t_i_Z

theorem mtinv_lem : M_t_i * M_t = Matrix.diagonal fun (x : Fin 3) => 49

theorem mtinv_lem2 : M_t * M_t_i = Matrix.diagonal fun (x : Fin 3) => 49

theorem t_i_op_n_equiv : ↑t_i_op_n = 7⁻¹ • M_t_i

theorem t_i_op_n_equiv_2 : 7 • ↑t_i_op_n = M_t_i

def sato_generators : Set ↥SO3

Equations

• sato_generators = {s_op_n, t_op_n}

def SATO : Subgroup ↥SO3

Equations

• SATO = Subgroup.closure sato_generators

theorem s_mem : s_op_n ∈ SATO

theorem t_mem : t_op_n ∈ SATO

noncomputable def sato_s : ↥SATO

Equations

• sato_s = ⟨s_op_n, s_mem⟩

noncomputable def sato_t : ↥SATO

Equations

• sato_t = ⟨t_op_n, t_mem⟩

def sato_generators_ss : Set ↥SATO

Equations

• sato_generators_ss = {sato_s, sato_t}

noncomputable def sato_fg3_iso_seed : Fin 2 → ↥SATO

Equations

• sato_fg3_iso_seed = ![sato_s, sato_t]

noncomputable def to_sato : FG2 →* ↥SATO

Equations

• to_sato = FreeGroup.lift sato_fg3_iso_seed

theorem to_sato_range : to_sato.range = Subgroup.closure sato_generators_ss

theorem to_sato_is_surjective : Function.Surjective ⇑to_sato

def Vs : Set Z3_raw

Equations

• Vs = {![3, 1, 2], ![5, 4, 1], ![6, 2, 4]}

def Vt : Set Z3_raw

Equations

• Vt = {![3, 2, 6], ![5, 1, 3], ![6, 4, 5]}

def Vtinv : Set Z3_raw

Equations

• Vtinv = {![3, 5, 1], ![5, 6, 4], ![6, 3, 2]}

def Vsinv : Set Z3_raw

Equations

• Vsinv = {![1, 5, 4], ![2, 3, 1], ![4, 6, 2]}

theorem l1 (v : Z3_raw) : v ∈ Vs ∪ Vt ∪ Vtinv → mod7_Z (Matrix.mulVec M_s_Z v) ∈ Vs

theorem l2 (v : Z3_raw) : v ∈ Vsinv ∪ Vt ∪ Vtinv → mod7_Z (Matrix.mulVec M_s_i_Z v) ∈ Vsinv

theorem l3 (v : Z3_raw) : v ∈ Vt ∪ Vs ∪ Vsinv → mod7_Z (Matrix.mulVec M_t_Z v) ∈ Vt

theorem l4 (v : Z3_raw) : v ∈ Vtinv ∪ Vs ∪ Vsinv → mod7_Z (Matrix.mulVec M_t_i_Z v) ∈ Vtinv

theorem to_sato_is_injective : Function.Injective ⇑to_sato

theorem to_sato_is_bijective : Function.Bijective ⇑to_sato

noncomputable def iso_forward_equiv : FG2 ≃ ↥SATO

Equations

• iso_forward_equiv = Equiv.ofBijective (⇑to_sato) to_sato_is_bijective

noncomputable def sato_fg3_iso : FG2 ≃* ↥SATO

Equations

• sato_fg3_iso = MulEquiv.mk' iso_forward_equiv sato_fg3_iso._proof_1

instance SATO_smul_R3 : SMul (↥SATO) R3

Equations

• SATO_smul_R3 = { smul := fun (g : ↥SATO) (x : R3) => ↑g • x }

instance SATO_action_on_R3 : MulAction (↥SATO) R3

Equations

• SATO_action_on_R3 = inferInstance

theorem SATO_smul_def (g : ↥SATO) (v : R3) : g • v = to_R3 ((↑↑g).mulVec v.ofLp)