PhysLean Documentation

PhysLean.Mathematics.SO3.Basic

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
      • One or more equations did not get rendered due to their size.
      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 (A : SO3) (a✝ : EuclideanSpace ℝ (Fin 3)) :
            A.toEnd a✝ = (EuclideanSpace.basisFun (Fin 3) ℝ).repr.symm ((↑A).mulVec ⇑((EuclideanSpace.basisFun (Fin 3) ℝ).toBasis.repr 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.