Imports
module
public import Mathlib.LinearAlgebra.Eigenspace.Basic
public import Mathlib.Analysis.InnerProductSpace.PiL2
The group SO(3)
@[ expose ] public section
The group of 3×3 real matrices with determinant 1 and A * Aᵀ = 1.
def SO3 : Type := { A : Matrix ( Fin 3 ) ( Fin 3 ) ℝ // A . det = 1 ∧ A * A ᵀ = 1 }
The instance of a group on SO3.
@[ simps! mul_coe one_coe inv div ]
instance SO3Group : Group SO3 where
mul A B := ⟨ A . 1 * B . 1 ,
by A : SO3 B : SO3 ⊢ ( ↑ A * ↑ B ) . det = 1
simp only [ det_mul , A . 2 . 1 , B . 2 . 1 , mul_one ] All goals completed! 🐙 ,
by A : SO3 B : SO3 ⊢ ↑ A * ↑ B * ( ↑ A * ↑ B ) ᵀ = 1
simp only [ transpose_mul , Matrix.mul_assoc ] A : SO3 B : SO3 ⊢ ↑ A * ( ↑ B * ( (↑ B ) ᵀ * (↑ A ) ᵀ ) ) = 1
trans A . 1 * ( ( B . 1 * ( B . 1 ) ᵀ ) * ( A . 1 ) ᵀ ) A : SO3 B : SO3 ⊢ ↑ A * ( ↑ B * ( (↑ B ) ᵀ * (↑ A ) ᵀ ) ) = ↑ A * ( ↑ B * (↑ B ) ᵀ * (↑ A ) ᵀ ) A : SO3 B : SO3 ⊢ ↑ A * ( ↑ B * (↑ B ) ᵀ * (↑ A ) ᵀ ) = 1
· A : SO3 B : SO3 ⊢ ↑ A * ( ↑ B * ( (↑ B ) ᵀ * (↑ A ) ᵀ ) ) = ↑ A * ( ↑ B * (↑ B ) ᵀ * (↑ A ) ᵀ ) noncomm_ring All goals completed! 🐙
· A : SO3 B : SO3 ⊢ ↑ A * ( ↑ B * (↑ B ) ᵀ * (↑ A ) ᵀ ) = 1 simp [ B . 2 . 2 , A . 2 . 2 ] All goals completed! 🐙 ⟩
mul_assoc A B C := Subtype.ext ( Matrix.mul_assoc A . 1 B . 1 C . 1 )
one := ⟨ 1 , det_one , by ⊢ 1 * 1 ᵀ = 1 rw [ transpose_one , ⊢ 1 * 1 = 1 All goals completed! 🐙 mul_one ⊢ 1 = 1 All goals completed! 🐙 ] All goals completed! 🐙 ⟩
one_mul A := Subtype.ext ( Matrix.one_mul A . 1 )
mul_one A := Subtype.ext ( Matrix.mul_one A . 1 )
inv A := ⟨ A . 1 ᵀ , by A : SO3 ⊢ (↑ A ) ᵀ . det = 1 simp only [ det_transpose , A . 2 ] All goals completed! 🐙 ,
by A : SO3 ⊢ (↑ A ) ᵀ * (↑ A ) ᵀ ᵀ = 1 simp only [ transpose_transpose , mul_eq_one_comm . mpr A . 2 . 2 ] All goals completed! 🐙 ⟩
inv_mul_cancel A := Subtype.ext ( mul_eq_one_comm . mpr A . 2 . 2 )
Notation for the group SO3.
scoped [ GroupTheory ] notation ( name := SO3_notation ) "SO(3)" => SO3
SO3 has the subtype topology.
instance : TopologicalSpace SO3 := instTopologicalSpaceSubtype
lemma coe_inv ( A : SO3 ) : ( A ⁻¹ ) . 1 = A . 1 ⁻¹ :=
( inv_eq_left_inv ( mul_eq_one_comm . mpr A . 2 . 2 ) ) . symm
The inclusion of SO(3) into GL (Fin 3) ℝ.
def toGL : SO(3) →* GL ( Fin 3 ) ℝ where
toFun A := ⟨ A . 1 , ( A ⁻¹ ) . 1 , A . 2 . 2 , mul_eq_one_comm . mpr A . 2 . 2 ⟩
map_one' := ( GeneralLinearGroup.ext_iff _ 1 ) . mpr fun _ => congrFun rfl
map_mul' _ _ := ( GeneralLinearGroup.ext_iff _ _ ) . mpr fun _ => congrFun rfl
lemma subtype_val_eq_toGL : ( Subtype.val : SO3 → Matrix ( Fin 3 ) ( Fin 3 ) ℝ ) =
Units.val ∘ toGL . toFun :=
rfl
The inclusion of SO(3) into GL(3,ℝ) is an injection.
The inclusion of SO(3) into the monoid of matrices times the opposite of
the monoid of matrices.
@[ simps! ]
def toProd : SO(3) →* ( Matrix ( Fin 3 ) ( Fin 3 ) ℝ ) × ( Matrix ( Fin 3 ) ( Fin 3 ) ℝ ) ᵐᵒᵖ :=
MonoidHom.comp ( Units.embedProduct _ ) toGL
The embedding of SO(3) into the monoid of matrices times the opposite of
the monoid of matrices.
The embedding of SO(3) into GL (Fin 3) ℝ.
set_option backward.isDefEq.respectTransparency false in
lemma toGL_embedding : IsEmbedding toGL . toFun where
injective := toGL_injective
eq_induced := by ⊢ instTopologicalSpaceSO3 = TopologicalSpace.induced (↑ toGL ) . toFun Units.instTopologicalSpaceUnits
refine ( ( fun { X } { t t' } => TopologicalSpace.ext_iff . mpr ) ? _ ) . symm ⊢ ∀ ( s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ),
IsOpen[ TopologicalSpace.induced (↑ toGL ) . toFun Units.instTopologicalSpaceUnits ] s ↔ IsOpen s
intro s s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ IsOpen[ TopologicalSpace.induced (↑ toGL ) . toFun Units.instTopologicalSpaceUnits ] s ↔ IsOpen s
rw [ TopologicalSpace.ext_iff . mp toProd_embedding . eq_induced s s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ IsOpen[ TopologicalSpace.induced (↑ toGL ) . toFun Units.instTopologicalSpaceUnits ] s ↔
IsOpen[ TopologicalSpace.induced (⇑ toProd ) instTopologicalSpaceProd ] s s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ IsOpen[ TopologicalSpace.induced (↑ toGL ) . toFun Units.instTopologicalSpaceUnits ] s ↔
IsOpen[ TopologicalSpace.induced (⇑ toProd ) instTopologicalSpaceProd ] s ] s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ IsOpen[ TopologicalSpace.induced (↑ toGL ) . toFun Units.instTopologicalSpaceUnits ] s ↔
IsOpen[ TopologicalSpace.induced (⇑ toProd ) instTopologicalSpaceProd ] s
rw [ isOpen_induced_iff , s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ (∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s ) ↔ IsOpen[ TopologicalSpace.induced (⇑ toProd ) instTopologicalSpaceProd ] s s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ (∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s ) ↔ ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s isOpen_induced_iff s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ (∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s ) ↔ ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ (∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s ) ↔ ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s ] s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ (∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s ) ↔ ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s
constructor mp s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ (∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s ) → ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s mpr s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ (∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s ) → ∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s <;> mp s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ (∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s ) → ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s mpr s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } ⊢ (∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s ) → ∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s intro h mpr s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } h : ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s ⊢ ∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s <;> mp s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } h : ∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s ⊢ ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s mpr s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } h : ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s ⊢ ∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s obtain ⟨ U , hU1 , hU2 ⟩ := h mpr s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } U : Set ( Matrix ( Fin 3 ) ( Fin 3 ) ℝ × ( Matrix ( Fin 3 ) ( Fin 3 ) ℝ ) ᵐᵒᵖ ) hU1 : IsOpen U hU2 : ⇑ toProd ⁻¹' U = s ⊢ ∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s
· mp s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } U : Set ( GL ( Fin 3 ) ℝ ) hU1 : IsOpen U hU2 : (↑ toGL ) . toFun ⁻¹' U = s ⊢ ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s rw [ isOpen_induced_iff mp s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } U : Set ( GL ( Fin 3 ) ℝ ) hU1 : ∃ t , IsOpen t ∧ ⇑ ( Units.embedProduct ( Matrix ( Fin 3 ) ( Fin 3 ) ℝ ) ) ⁻¹' t = U hU2 : (↑ toGL ) . toFun ⁻¹' U = s ⊢ ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s mp s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } U : Set ( GL ( Fin 3 ) ℝ ) hU1 : ∃ t , IsOpen t ∧ ⇑ ( Units.embedProduct ( Matrix ( Fin 3 ) ( Fin 3 ) ℝ ) ) ⁻¹' t = U hU2 : (↑ toGL ) . toFun ⁻¹' U = s ⊢ ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s ] at hU1 mp s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } U : Set ( GL ( Fin 3 ) ℝ ) hU1 : ∃ t , IsOpen t ∧ ⇑ ( Units.embedProduct ( Matrix ( Fin 3 ) ( Fin 3 ) ℝ ) ) ⁻¹' t = U hU2 : (↑ toGL ) . toFun ⁻¹' U = s ⊢ ∃ t , IsOpen t ∧ ⇑ toProd ⁻¹' t = s
aesop All goals completed! 🐙
· mpr s : Set { A // A . det = 1 ∧ A * A ᵀ = 1 } U : Set ( Matrix ( Fin 3 ) ( Fin 3 ) ℝ × ( Matrix ( Fin 3 ) ( Fin 3 ) ℝ ) ᵐᵒᵖ ) hU1 : IsOpen U hU2 : ⇑ toProd ⁻¹' U = s ⊢ ∃ t , IsOpen t ∧ (↑ toGL ) . toFun ⁻¹' t = s exact ⟨ ( Units.embedProduct _ ) ⁻¹' U , And.intro ( isOpen_induced hU1 ) hU2 ⟩ All goals completed! 🐙
The instance of a topological group on SO(3), defined through the embedding of SO(3)
into GL(n).
instance : IsTopologicalGroup SO(3) :=
IsInducing.topologicalGroup toGL toGL_embedding . toIsInducing
The determinant of an SO(3) matrix minus the identity is equal to zero.
The determinant of the identity minus an SO(3) matrix is zero.
For every matrix in SO(3), the real number 1 is in its spectrum.
The endomorphism of EuclideanSpace ℝ (Fin 3) associated to a element of SO(3).
@[ simps! ]
def toEnd ( A : SO(3) ) : End ℝ ( EuclideanSpace ℝ ( Fin 3 ) ) :=
Matrix.toLin ( EuclideanSpace.basisFun ( Fin 3 ) ℝ ) . toBasis
( EuclideanSpace.basisFun ( Fin 3 ) ℝ ) . toBasis A . 1
Every SO(3) matrix has an eigenvalue equal to 1.
For every element of SO(3) there exists a vector which remains unchanged under the
action of that SO(3) element.
lemma exists_stationary_vec ( A : SO(3) ) :
∃ ( v : EuclideanSpace ℝ ( Fin 3 ) ) ,
Orthonormal ℝ ( ( { 0 } : Set ( Fin 3 ) ) . restrict ( fun _ => v ) )
∧ A . toEnd v = v := by A : SO(3) ⊢ ∃ v , Orthonormal ℝ ( { 0 } . restrict fun x => v ) ∧ A . toEnd v = v
obtain ⟨ v , hv ⟩ := End.HasEigenvalue.exists_hasEigenvector $ one_is_eigenvalue A A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v ⊢ ∃ v , Orthonormal ℝ ( { 0 } . restrict fun x => v ) ∧ A . toEnd v = v
have hvn : ‖ v ‖ ≠ 0 := norm_ne_zero_iff . mpr hv . 2 A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 ⊢ ∃ v , Orthonormal ℝ ( { 0 } . restrict fun x => v ) ∧ A . toEnd v = v
use ( 1 / ‖ v ‖ ) • v h A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 ⊢ Orthonormal ℝ ( { 0 } . restrict fun x => ( 1 / ‖ v ‖ ) • v ) ∧ A . toEnd ( ( 1 / ‖ v ‖ ) • v ) = ( 1 / ‖ v ‖ ) • v
constructor h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 ⊢ Orthonormal ℝ ( { 0 } . restrict fun x => ( 1 / ‖ v ‖ ) • v ) h.right A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 ⊢ A . toEnd ( ( 1 / ‖ v ‖ ) • v ) = ( 1 / ‖ v ‖ ) • v
· h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 ⊢ Orthonormal ℝ ( { 0 } . restrict fun x => ( 1 / ‖ v ‖ ) • v ) rw [ @ orthonormal_iff_ite h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 ⊢ ∀ ( i j : ↑ { 0 } ),
inner ℝ ( { 0 } . restrict (fun x => ( 1 / ‖ v ‖ ) • v ) i ) ( { 0 } . restrict (fun x => ( 1 / ‖ v ‖ ) • v ) j ) = if i = j then 1 else 0 h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 ⊢ ∀ ( i j : ↑ { 0 } ),
inner ℝ ( { 0 } . restrict (fun x => ( 1 / ‖ v ‖ ) • v ) i ) ( { 0 } . restrict (fun x => ( 1 / ‖ v ‖ ) • v ) j ) = if i = j then 1 else 0 ] h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 ⊢ ∀ ( i j : ↑ { 0 } ),
inner ℝ ( { 0 } . restrict (fun x => ( 1 / ‖ v ‖ ) • v ) i ) ( { 0 } . restrict (fun x => ( 1 / ‖ v ‖ ) • v ) j ) = if i = j then 1 else 0
intro v1 v2 h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } v2 : ↑ { 0 } ⊢ inner ℝ ( { 0 } . restrict (fun x => ( 1 / ‖ v ‖ ) • v ) v1 ) ( { 0 } . restrict (fun x => ( 1 / ‖ v ‖ ) • v ) v2 ) = if v1 = v2 then 1 else 0
simp only [ one_div ] h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } v2 : ↑ { 0 } ⊢ inner ℝ ( { 0 } . restrict (fun x => ‖ v ‖ ⁻¹ • v ) v1 ) ( { 0 } . restrict (fun x => ‖ v ‖ ⁻¹ • v ) v2 ) = if v1 = v2 then 1 else 0
have hveq : v1 = v2 := by A : SO(3) ⊢ ∃ v , Orthonormal ℝ ( { 0 } . restrict fun x => v ) ∧ A . toEnd v = v h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } v2 : ↑ { 0 } hveq : v1 = v2 ⊢ inner ℝ ( { 0 } . restrict (fun x => ‖ v ‖ ⁻¹ • v ) v1 ) ( { 0 } . restrict (fun x => ‖ v ‖ ⁻¹ • v ) v2 ) = if v1 = v2 then 1 else 0 aesop h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } v2 : ↑ { 0 } hveq : v1 = v2 ⊢ inner ℝ ( { 0 } . restrict (fun x => ‖ v ‖ ⁻¹ • v ) v1 ) ( { 0 } . restrict (fun x => ‖ v ‖ ⁻¹ • v ) v2 ) = if v1 = v2 then 1 else 0 h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } v2 : ↑ { 0 } hveq : v1 = v2 ⊢ inner ℝ ( { 0 } . restrict (fun x => ‖ v ‖ ⁻¹ • v ) v1 ) ( { 0 } . restrict (fun x => ‖ v ‖ ⁻¹ • v ) v2 ) = if v1 = v2 then 1 else 0
subst hveq h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } ⊢ inner ℝ ( { 0 } . restrict (fun x => ‖ v ‖ ⁻¹ • v ) v1 ) ( { 0 } . restrict (fun x => ‖ v ‖ ⁻¹ • v ) v1 ) = if v1 = v1 then 1 else 0
rw [ Set.restrict_apply , h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } ⊢ inner ℝ ( ‖ v ‖ ⁻¹ • v ) ( ‖ v ‖ ⁻¹ • v ) = if v1 = v1 then 1 else 0 h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } ⊢ ‖ v ‖ ⁻¹ * ( ( starRingEnd ℝ ) ‖ v ‖ ⁻¹ * ‖ v ‖ ^ 2 ) = if v1 = v1 then 1 else 0 inner_smul_right , h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } ⊢ ‖ v ‖ ⁻¹ * inner ℝ ( ‖ v ‖ ⁻¹ • v ) v = if v1 = v1 then 1 else 0 h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } ⊢ ‖ v ‖ ⁻¹ * ( ( starRingEnd ℝ ) ‖ v ‖ ⁻¹ * ‖ v ‖ ^ 2 ) = if v1 = v1 then 1 else 0 inner_smul_left , h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } ⊢ ‖ v ‖ ⁻¹ * ( ( starRingEnd ℝ ) ‖ v ‖ ⁻¹ * inner ℝ v v ) = if v1 = v1 then 1 else 0 h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } ⊢ ‖ v ‖ ⁻¹ * ( ( starRingEnd ℝ ) ‖ v ‖ ⁻¹ * ‖ v ‖ ^ 2 ) = if v1 = v1 then 1 else 0 real_inner_self_eq_norm_sq v h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } ⊢ ‖ v ‖ ⁻¹ * ( ( starRingEnd ℝ ) ‖ v ‖ ⁻¹ * ‖ v ‖ ^ 2 ) = if v1 = v1 then 1 else 0 h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } ⊢ ‖ v ‖ ⁻¹ * ( ( starRingEnd ℝ ) ‖ v ‖ ⁻¹ * ‖ v ‖ ^ 2 ) = if v1 = v1 then 1 else 0 ] h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } ⊢ ‖ v ‖ ⁻¹ * ( ( starRingEnd ℝ ) ‖ v ‖ ⁻¹ * ‖ v ‖ ^ 2 ) = if v1 = v1 then 1 else 0
simp only [ map_inv₀ , conj_trivial , Fin.isValue , ↓ reduceIte ] h.left A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 v1 : ↑ { 0 } ⊢ ‖ v ‖ ⁻¹ * ( ‖ v ‖ ⁻¹ * ‖ v ‖ ^ 2 ) = 1
field_simp All goals completed! 🐙
· h.right A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : A . toEnd . HasEigenvector 1 v hvn : ‖ v ‖ ≠ 0 ⊢ A . toEnd ( ( 1 / ‖ v ‖ ) • v ) = ( 1 / ‖ v ‖ ) • v simp [ End.mem_eigenspace_iff . mp hv . 1 ] All goals completed! 🐙
For every element of SO(3) there exists a basis indexed by Fin 3 under which the first
element remains invariant.
lemma exists_basis_preserved ( A : SO(3) ) :
∃ ( b : OrthonormalBasis ( Fin 3 ) ℝ ( EuclideanSpace ℝ ( Fin 3 ) ) ) , A . toEnd ( b 0 ) = b 0 := by A : SO(3) ⊢ ∃ b , A . toEnd ( b 0 ) = b 0
obtain ⟨ v , hv ⟩ := exists_stationary_vec A A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : Orthonormal ℝ ( { 0 } . restrict fun x => v ) ∧ A . toEnd v = v ⊢ ∃ b , A . toEnd ( b 0 ) = b 0
obtain ⟨ b , hb ⟩ := Orthonormal.exists_orthonormalBasis_extension_of_card_eq ( by A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : Orthonormal ℝ ( { 0 } . restrict fun x => v ) ∧ A . toEnd v = v ⊢ finrank ℝ ( EuclideanSpace ℝ ( Fin 3 ) ) = Fintype.card ( Fin 3 ) A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : Orthonormal ℝ ( { 0 } . restrict fun x => v ) ∧ A . toEnd v = v b : OrthonormalBasis ( Fin 3 ) ℝ ( EuclideanSpace ℝ ( Fin 3 ) ) hb : ∀ i ∈ { 0 } , b i = v ⊢ ∃ b , A . toEnd ( b 0 ) = b 0 aesop All goals completed! 🐙 A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : Orthonormal ℝ ( { 0 } . restrict fun x => v ) ∧ A . toEnd v = v b : OrthonormalBasis ( Fin 3 ) ℝ ( EuclideanSpace ℝ ( Fin 3 ) ) hb : ∀ i ∈ { 0 } , b i = v ⊢ ∃ b , A . toEnd ( b 0 ) = b 0 ) hv . 1 A : SO(3) v : EuclideanSpace ℝ ( Fin 3 ) hv : Orthonormal ℝ ( { 0 } . restrict fun x => v ) ∧ A . toEnd v = v b : OrthonormalBasis ( Fin 3 ) ℝ ( EuclideanSpace ℝ ( Fin 3 ) ) hb : ∀ i ∈ { 0 } , b i = v ⊢ ∃ b , A . toEnd ( b 0 ) = b 0
aesop All goals completed! 🐙