The group SO(3) #

source

def GroupTheory.SO3 :

Type

The group of 3×3 real matrices with determinant 1 and A * Aᵀ = 1.

Equations

Instances For

source

instance GroupTheory.SO3Group :

Group SO3

The instance of a group on SO3.

Equations

source

@[simp]

theorem GroupTheory.SO3Group_inv (A : SO3) :

A⁻¹ = ⟨(↑A).transpose, ⋯⟩

source

@[simp]

theorem GroupTheory.SO3Group_mul_coe (A B : SO3) :

↑(A * B) = ↑A * ↑B

source

@[simp]

theorem GroupTheory.SO3Group_div (a b : SO3) :

a / b = DivInvMonoid.div' a b

source

@[simp]

theorem GroupTheory.SO3Group_one_coe :

↑1 = 1

source

def GroupTheory.SO3_notation :

Lean.ParserDescr

Notation for the group SO3.

Equations

Instances For

source

instance GroupTheory.instTopologicalSpaceSO3 :

TopologicalSpace SO3

SO3 has the subtype topology.

Equations

source

theorem GroupTheory.SO3.coe_inv (A : SO3) :

↑A⁻¹ = (↑A)⁻¹

source

def GroupTheory.SO3.toGL :

SO3 →* GL (Fin 3) ℝ

The inclusion of SO(3) into GL (Fin 3) ℝ.

Equations

Instances For

source

theorem GroupTheory.SO3.subtype_val_eq_toGL :

Subtype.val = Units.val ∘ (↑toGL).toFun

source

theorem GroupTheory.SO3.toGL_injective :

Function.Injective ⇑toGL

The inclusion of SO(3) into GL(3,ℝ) is an injection.

source

def GroupTheory.SO3.toProd :

SO3 →* Matrix (Fin 3) (Fin 3) ℝ × (Matrix (Fin 3) (Fin 3) ℝ)ᵐᵒᵖ

The inclusion of SO(3) into the monoid of matrices times the opposite of the monoid of matrices.

Equations

Instances For

source

@[simp]

theorem GroupTheory.SO3.toProd_apply (a✝ : SO3) :

toProd a✝ = (↑(toGL a✝), (MulOpposite.op ↑(toGL a✝))⁻¹ )

source

theorem GroupTheory.SO3.toProd_eq_transpose {A : SO3} :

toProd A = (↑A, { unop' := (↑A).transpose })

source

theorem GroupTheory.SO3.toProd_injective :

Function.Injective ⇑toProd

source

theorem GroupTheory.SO3.toProd_continuous :

Continuous ⇑toProd

source

theorem GroupTheory.SO3.toProd_embedding :

Topology.IsEmbedding ⇑toProd

The embedding of SO(3) into the monoid of matrices times the opposite of the monoid of matrices.

source

theorem GroupTheory.SO3.toGL_embedding :

Topology.IsEmbedding (↑toGL).toFun

The embedding of SO(3) into GL (Fin 3) ℝ.

source

instance GroupTheory.SO3.instIsTopologicalGroup :

IsTopologicalGroup SO3

The instance of a topological group on SO(3), defined through the embedding of SO(3) into GL(n).

source

theorem GroupTheory.SO3.det_minus_id (A : SO3) :

(↑A - 1).det = 0

The determinant of an SO(3) matrix minus the identity is equal to zero.

source

@[simp]

theorem GroupTheory.SO3.det_id_minus (A : SO3) :

(1 - ↑A).det = 0

The determinant of the identity minus an SO(3) matrix is zero.

source

@[simp]

theorem GroupTheory.SO3.one_in_spectrum (A : SO3) :

1 ∈ spectrum ℝ ↑A

For every matrix in SO(3), the real number 1 is in its spectrum.

source

def GroupTheory.SO3.toEnd (A : SO3) :

Module.End ℝ (EuclideanSpace ℝ (Fin 3))

The endomorphism of EuclideanSpace ℝ (Fin 3) associated to a element of SO(3).

Equations

Instances For

source

@[simp]

theorem GroupTheory.SO3.toEnd_apply_ofLp (A : SO3) (a✝ : EuclideanSpace ℝ (Fin 3)) (a✝¹ : Fin 3) :

(A.toEnd a✝).ofLp a✝¹ = (↑A).mulVec (⇑((EuclideanSpace.basisFun (Fin 3) ℝ).toBasis.repr a✝)) a✝¹

source

theorem GroupTheory.SO3.one_is_eigenvalue (A : SO3) :

A.toEnd.HasEigenvalue 1

Every SO(3) matrix has an eigenvalue equal to 1.

source

theorem GroupTheory.SO3.exists_stationary_vec (A : SO3) :

∃ (v : EuclideanSpace ℝ (Fin 3)), Orthonormal ℝ ({0}.restrict fun (x : Fin 3) => v) ∧ A.toEnd v = v

For every element of SO(3) there exists a vector which remains unchanged under the action of that SO(3) element.

source

theorem GroupTheory.SO3.exists_basis_preserved (A : SO3) :

∃ (b : OrthonormalBasis (Fin 3) ℝ (EuclideanSpace ℝ (Fin 3))), A.toEnd (b 0) = b 0

For every element of SO(3) there exists a basis indexed by Fin 3 under which the first element remains invariant.

Documentation

PhysLean.Mathematics.SO3.Basic

The group SO(3) #