Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

The Pin group and the Spin group #

In this file we define lipschitzGroup, pinGroup and spinGroup and show they form a group.

Main definitions #

Implementation Notes #

The definition of the Lipschitz group $\{ x \in \mathop{\mathcal{C}\ell} | x \text{ is invertible and } x v x^{-1} ∈ V \}$ is given by:

But they presumably form a group only in finite dimensions. So we define lipschitzGroup with closure of all the invertible elements in the form of ι Q m, and we show this definition is at least as large as the other definition (See lipschitzGroup.conjAct_smul_range_ι and lipschitzGroup.involute_act_ι_mem_range_ι). The reverse statement presumably is true only in finite dimensions.

Here are some discussions about the latent ambiguity of definition : https://mathoverflow.net/q/427881/172242 and https://mathoverflow.net/q/251288/172242

TODO #

Try to show the reverse statement is true in finite dimensions.

def lipschitzGroup {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :

lipschitzGroup is the subgroup closure of all the invertible elements in the form of ι Q m where ι is the canonical linear map M →ₗ[R] CliffordAlgebra Q.

Equations
Instances For
    theorem lipschitzGroup.conjAct_smul_ι_mem_range_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} (hx : x lipschitzGroup Q) [Invertible 2] (m : M) :

    The conjugation action by elements of the Lipschitz group keeps vectors as vectors.

    theorem lipschitzGroup.involute_act_ι_mem_range_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} [Invertible 2] {x : (CliffordAlgebra Q)ˣ} (hx : x lipschitzGroup Q) (b : M) :
    CliffordAlgebra.involute x * (CliffordAlgebra.ι Q) b * x⁻¹ LinearMap.range (CliffordAlgebra.ι Q)

    This is another version of lipschitzGroup.conjAct_smul_ι_mem_range_ι which uses involute.

    If x is in lipschitzGroup Q, then (ι Q).range is closed under twisted conjugation. The reverse statement presumably is true only in finite dimensions.

    def pinGroup {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :

    pinGroup Q is defined as the infimum of lipschitzGroup Q and unitary (CliffordAlgebra Q). See mem_iff.

    Equations
    Instances For

      An element is in pinGroup Q if and only if it is in lipschitzGroup Q and unitary.

      theorem pinGroup.mem_lipschitzGroup {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x pinGroup Q) :
      theorem pinGroup.mem_unitary {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x pinGroup Q) :
      theorem pinGroup.units_mem_lipschitzGroup {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} (hx : x pinGroup Q) :
      theorem pinGroup.conjAct_smul_ι_mem_range_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} (hx : x pinGroup Q) [Invertible 2] (y : M) :

      The conjugation action by elements of the spin group keeps vectors as vectors.

      theorem pinGroup.involute_act_ι_mem_range_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} (hx : x pinGroup Q) [Invertible 2] (y : M) :
      CliffordAlgebra.involute x * (CliffordAlgebra.ι Q) y * x⁻¹ LinearMap.range (CliffordAlgebra.ι Q)

      This is another version of conjAct_smul_ι_mem_range_ι which uses involute.

      theorem pinGroup.conjAct_smul_range_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} (hx : x pinGroup Q) [Invertible 2] :

      If x is in pinGroup Q, then (ι Q).range is closed under twisted conjugation. The reverse statement presumably being true only in finite dimensions.

      @[simp]
      theorem pinGroup.star_mul_self_of_mem {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x pinGroup Q) :
      star x * x = 1
      @[simp]
      theorem pinGroup.mul_star_self_of_mem {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x pinGroup Q) :
      x * star x = 1
      theorem pinGroup.star_mem {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x pinGroup Q) :

      See star_mem_iff for both directions.

      @[simp]
      theorem pinGroup.star_mem_iff {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} :

      An element is in pinGroup Q if and only if star x is in pinGroup Q. See star_mem for only one direction.

      Equations
      • pinGroup.instStarSubtypeCliffordAlgebraMemSubmonoid = { star := fun (x : (pinGroup Q)) => star x, }
      @[simp]
      theorem pinGroup.coe_star {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (pinGroup Q)} :
      (star x) = star x
      theorem pinGroup.coe_star_mul_self {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (pinGroup Q)) :
      star x * x = 1
      theorem pinGroup.coe_mul_star_self {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (pinGroup Q)) :
      x * (star x) = 1
      @[simp]
      theorem pinGroup.star_mul_self {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (pinGroup Q)) :
      star x * x = 1
      @[simp]
      theorem pinGroup.mul_star_self {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (pinGroup Q)) :
      x * star x = 1

      pinGroup Q forms a group where the inverse is star.

      Equations
      • pinGroup.instGroupSubtypeCliffordAlgebraMemSubmonoid = Group.mk
      Equations
      • pinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid = StarMul.mk
      Equations
      • pinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid = { default := 1 }
      theorem pinGroup.star_eq_inv {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (pinGroup Q)) :
      theorem pinGroup.star_eq_inv' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
      star = Inv.inv
      @[simp]
      theorem pinGroup.val_toUnits_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (pinGroup Q)) :
      (pinGroup.toUnits x) = x
      @[simp]
      theorem pinGroup.val_inv_toUnits_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (pinGroup Q)) :
      (pinGroup.toUnits x)⁻¹ = x⁻¹
      def pinGroup.toUnits {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :

      The elements in pinGroup Q embed into (CliffordAlgebra Q)ˣ.

      Equations
      • pinGroup.toUnits = { toFun := fun (x : (pinGroup Q)) => { val := x, inv := x⁻¹, val_inv := , inv_val := }, map_one' := , map_mul' := }
      Instances For
        theorem pinGroup.toUnits_injective {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
        Function.Injective pinGroup.toUnits
        def spinGroup {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :

        spinGroup Q is defined as the infimum of pinGroup Q and CliffordAlgebra.even Q. See mem_iff.

        Equations
        Instances For
          theorem spinGroup.mem_iff {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} :

          An element is in spinGroup Q if and only if it is in pinGroup Q and even Q.

          theorem spinGroup.mem_pin {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x spinGroup Q) :
          theorem spinGroup.mem_even {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x spinGroup Q) :
          theorem spinGroup.units_mem_lipschitzGroup {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} (hx : x spinGroup Q) :
          theorem spinGroup.involute_eq {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x spinGroup Q) :
          CliffordAlgebra.involute x = x

          If x is in spinGroup Q, then involute x is equal to x.

          theorem spinGroup.units_involute_act_eq_conjAct {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} (hx : x spinGroup Q) (y : M) :
          CliffordAlgebra.involute x * (CliffordAlgebra.ι Q) y * x⁻¹ = ConjAct.toConjAct x (CliffordAlgebra.ι Q) y
          theorem spinGroup.conjAct_smul_ι_mem_range_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} (hx : x spinGroup Q) [Invertible 2] (y : M) :

          The conjugation action by elements of the spin group keeps vectors as vectors.

          theorem spinGroup.involute_act_ι_mem_range_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} (hx : x spinGroup Q) [Invertible 2] (y : M) :
          CliffordAlgebra.involute x * (CliffordAlgebra.ι Q) y * x⁻¹ LinearMap.range (CliffordAlgebra.ι Q)
          @[simp]
          theorem spinGroup.star_mul_self_of_mem {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x spinGroup Q) :
          star x * x = 1
          @[simp]
          theorem spinGroup.mul_star_self_of_mem {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x spinGroup Q) :
          x * star x = 1
          theorem spinGroup.star_mem {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x spinGroup Q) :

          See star_mem_iff for both directions.

          @[simp]
          theorem spinGroup.star_mem_iff {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} :

          An element is in spinGroup Q if and only if star x is in spinGroup Q. See star_mem for only one direction.

          Equations
          • spinGroup.instStarSubtypeCliffordAlgebraMemSubmonoid = { star := fun (x : (spinGroup Q)) => star x, }
          @[simp]
          theorem spinGroup.coe_star {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (spinGroup Q)} :
          (star x) = star x
          theorem spinGroup.coe_star_mul_self {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (spinGroup Q)) :
          star x * x = 1
          theorem spinGroup.coe_mul_star_self {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (spinGroup Q)) :
          x * (star x) = 1
          @[simp]
          theorem spinGroup.star_mul_self {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (spinGroup Q)) :
          star x * x = 1
          @[simp]
          theorem spinGroup.mul_star_self {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (spinGroup Q)) :
          x * star x = 1

          spinGroup Q forms a group where the inverse is star.

          Equations
          • spinGroup.instGroupSubtypeCliffordAlgebraMemSubmonoid = Group.mk
          Equations
          • spinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid = StarMul.mk
          Equations
          • spinGroup.instInhabitedSubtypeCliffordAlgebraMemSubmonoid = { default := 1 }
          theorem spinGroup.star_eq_inv {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (spinGroup Q)) :
          theorem spinGroup.star_eq_inv' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
          star = Inv.inv
          @[simp]
          theorem spinGroup.val_toUnits_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (spinGroup Q)) :
          (spinGroup.toUnits x) = x
          @[simp]
          theorem spinGroup.val_inv_toUnits_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : (spinGroup Q)) :
          (spinGroup.toUnits x)⁻¹ = x⁻¹
          def spinGroup.toUnits {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :

          The elements in spinGroup Q embed into (CliffordAlgebra Q)ˣ.

          Equations
          • spinGroup.toUnits = { toFun := fun (x : (spinGroup Q)) => { val := x, inv := x⁻¹, val_inv := , inv_val := }, map_one' := , map_mul' := }
          Instances For
            theorem spinGroup.toUnits_injective {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
            Function.Injective spinGroup.toUnits