Orthogonal and spin groups

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremCliffordAlgebra.range_spinToSpecialOrthogonal_eq_ker_spinorNorm#

The image of the Spin action on SO(Q) is exactly the kernel of the spinor norm.

CliffordAlgebra.range_spinToSpecialOrthogonal_eq_ker_spinorNorm.{u, v} {K : Type u} {V : Type v}
  [Field K] [AddCommGroup V] [_root_.Module K V] [FiniteDimensional K V] [Invertible 2]
  (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) :
  (CliffordAlgebra.spinToSpecialOrthogonal Q).range = (CliffordAlgebra.spinorNorm Q hQ).ker
Lean

Formalized in Tau Ceti as CliffordAlgebra.range_spinToSpecialOrthogonal_eq_ker_spinorNorm.

Sources
LeanCliffordAlgebra.range_spinToSpecialOrthogonal_eq_ker_spinorNorm

TheoremSpin is the even unitary group in dimensions one to five#

For a nondegenerate quadratic space of dimension between one and five, the even unitary carrier lies in the Lipschitz group. Dimension zero is excluded, and the exclusion is not decoration: there the Lipschitz group is trivial while the even unitary carrier is μ₂. The bound five is sharp, by CliffordAlgebra.not_evenUnitaryGroup_le_lipschitzGroup_of_six_le_finrank.

CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup.{u, v} {K : Type u} {V : Type v} [Field K]
  [AddCommGroup V] [_root_.Module K V] [Invertible 2] (Q : QuadraticForm K V)
  (hQ : QuadraticMap.Nondegenerate) (hV0 : 0 < Module.finrank K V) (hV : Module.finrank K V ≤ 5) :
  CliffordAlgebra.evenUnitaryGroup Q ≤ lipschitzGroup Q
Lean

Formalized in Tau Ceti as CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup.

Sources
LeanCliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup
Used by 2
Used bySpin₅ is a twisted form of Sp₄ · Split Spin₅ is Sp₄

AbbreviationThe Spin group of three hyperbolic planes is SL₄(K)#

This is TauCeti.spinGroupEquivSpecialLinearGroupOfFinrankEqSix for the canonical split polarization, so a Spin element goes to the matrix of its even half-spin action in TauCeti.spinSixHalfSpinStandardBasis. By TauCeti.coe_hyperbolicSixSpinEquivSpecialLinear_apply it is the restriction of TauCeti.hyperbolicSixEvenUnitaryEquivGeneralLinear to Spin, so Spin(Q) is the determinant-one subgroup of the reverse-unitary group U(C₀, σ) ≅ GL₄(K). Over ℚ, three hyperbolic planes give the split rational six-dimensional form, with U(C₀, σ) ≅ GL₄(ℚ) and Spin(Q) ≅ SL₄(ℚ).

TauCeti.hyperbolicSixSpinEquivSpecialLinear.{u_1} (K : Type u_1) [Field K] [NeZero 2] :
  ↥(spinGroup (TauCeti.splitEvenForm K 3)) ≃* Matrix.SpecialLinearGroup (Fin 4) K
Lean

Formalized in Tau Ceti as TauCeti.hyperbolicSixSpinEquivSpecialLinear.

Sources
LeanTauCeti.hyperbolicSixSpinEquivSpecialLinear
Uses 2
Proof usesThe even structure theorem · The structure theorem in operator form

TheoremSplit Spin₅ is Sp₄#

For a nondegenerate quadratic form on a five-dimensional space whose even Clifford algebra splits, C₀ ≃ M₄(K), the group Spin(Q) is isomorphic to the symplectic group Sp₄(K).

CliffordAlgebra.exists_spinGroupEquivSymplecticGroup_of_finrank_eq_five.{u_1, u_2} {K : Type u_1}
  {V : Type u_2} [Field K] [AddCommGroup V] [_root_.Module K V] [Invertible 2]
  (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 5)
  (hsplit : Nonempty (↥(CliffordAlgebra.even Q) ≃ₐ[K] Matrix (Fin 4) (Fin 4) K)) :
  Nonempty (↥(spinGroup Q) ≃* ↥(Matrix.symplecticGroup (Fin 2) K))
Lean

Formalized in Tau Ceti as CliffordAlgebra.exists_spinGroupEquivSymplecticGroup_of_finrank_eq_five.

Sources
LeanCliffordAlgebra.exists_spinGroupEquivSymplecticGroup_of_finrank_eq_five
Uses 2
Proof usesSkolem–Noether for matrix algebras over a local semiring · Spin is the even unitary group in dimensions one to five

TheoremSpin₅ is a twisted form of Sp₄#

For a nondegenerate quadratic form on a five-dimensional space and any separably closed extension L / K, there are a splitting e : C₀ ⊗ L ≃ M₄(L) carrying reversal to the symplectic adjoint and an injective homomorphism f : Spin(Q) → Sp₄(L) with e⁻¹ (f s) the scalar extension of s. Its image consists of exactly those symplectic matrices g for which e⁻¹ g comes from C₀, so Spin(Q) is the group Sp(C₀, σ) of K-rational points of Sp₄(L) for the K-structure C₀ ⊆ C₀ ⊗ L.

CliffordAlgebra.exists_injective_spinGroup_symplecticGroup_of_finrank_eq_five.{u_1, u_2, u_4}
  {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [_root_.Module K V] [Invertible 2]
  (L : Type u_4) [Field L] [Algebra K L] [IsSepClosed L] (Q : QuadraticForm K V)
  (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 5) :
  ∃ e f,
    Function.Injective ⇑f ∧
      (∀ (s : ↥(spinGroup Q)), ↑(e.symm ↑(f s)) = (CliffordAlgebra.ofBaseChangeAux L Q) ↑s) ∧
        ∀ (g : ↥(Matrix.symplecticGroup (Fin 2) L)),
          g ∈ f.range ↔
            ∃ y ∈ CliffordAlgebra.even Q, (CliffordAlgebra.ofBaseChangeAux L Q) y = ↑(e.symm ↑g)
Lean

Formalized in Tau Ceti as CliffordAlgebra.exists_injective_spinGroup_symplecticGroup_of_finrank_eq_five.

Sources
LeanCliffordAlgebra.exists_injective_spinGroup_symplecticGroup_of_finrank_eq_five
Uses 4
Proof usesArtin--Wedderburn over a separably closed field · Skolem–Noether for matrix algebras over a local semiring · Spin is the even unitary group in dimensions one to five · The structure theorem in operator form

TheoremTauCeti.QuadraticMap.isCompact_orthogonalGroup_iff#

The orthogonal group of a quadratic form on a finite-dimensional space over a locally compact nontrivially normed field is compact exactly when the form is anisotropic.

TauCeti.QuadraticMap.isCompact_orthogonalGroup_iff.{u_1, u_2} {K : Type u_1} {V : Type u_2}
  [NontriviallyNormedField K] [WeaklyLocallyCompactSpace K] [AddCommGroup V] [_root_.Module K V]
  [FiniteDimensional K V] (Q : QuadraticForm K V) :
  IsCompact ↑(TauCeti.QuadraticMap.orthogonalGroup Q) ↔ QuadraticMap.Anisotropic Q
Lean

Formalized in Tau Ceti as TauCeti.QuadraticMap.isCompact_orthogonalGroup_iff.

Sources
LeanTauCeti.QuadraticMap.isCompact_orthogonalGroup_iff

TheoremTauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpinDiagonal#

Rational Spin points of a nondegenerate rational quadratic space form a discrete subgroup of the full adelic Spin group for every compatible compact-open reference family.

TauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpinDiagonal.{u_1}
  {V : Type u_1} [AddCommGroup V] [_root_.Module ℚ V] [FiniteDimensional ℚ V]
  {Q : QuadraticForm ℚ V} (U : TauCeti.QuadraticMap.OrthogonalCompactOpens Q)
  (hQ : QuadraticMap.Nondegenerate) : DiscreteTopology ↥U.fullAdelicSpinDiagonal.range
Lean

Formalized in Tau Ceti as TauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpinDiagonal.

Sources
LeanTauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpinDiagonal
Uses 2
Statement usesTauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpin
Proof usesTauCeti.restrictedProductMap

TheoremTauCeti.QuadraticMap.OrthogonalCompactOpens.not_discreteTopology_range_finiteAdelicSpecialOrthogonalDiagonal#

For a nondegenerate isotropic rational quadratic space of dimension at least three, the rational diagonal is not discrete in finite adelic SO. In dimension two the transvection parameter quotient is zero, so the dimension hypothesis is essential to this argument.

TauCeti.QuadraticMap.OrthogonalCompactOpens.not_discreteTopology_range_finiteAdelicSpecialOrthogonalDiagonal.{u_1}
  {V : Type u_1} [AddCommGroup V] [_root_.Module ℚ V] [FiniteDimensional ℚ V]
  {Q : QuadraticForm ℚ V} (U : TauCeti.QuadraticMap.OrthogonalCompactOpens Q)
  (hQ : QuadraticMap.Nondegenerate) (hdim : 3 ≤ Module.finrank ℚ V) (hiso : ∃ u, u ≠ 0 ∧ Q u = 0) :
  ¬DiscreteTopology ↥U.finiteAdelicSpecialOrthogonalDiagonal.range
Lean

Formalized in Tau Ceti as TauCeti.QuadraticMap.OrthogonalCompactOpens.not_discreteTopology_range_finiteAdelicSpecialOrthogonalDiagonal.

Sources
LeanTauCeti.QuadraticMap.OrthogonalCompactOpens.not_discreteTopology_range_finiteAdelicSpecialOrthogonalDiagonal

AbbreviationTauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpin#

The full adelic Spin group Spin(V)(𝔸), with its unrestricted real factor.

TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpin.{u_1} {V : Type u_1} [AddCommGroup V]
  [_root_.Module ℚ V] {Q : QuadraticForm ℚ V} (U : TauCeti.QuadraticMap.OrthogonalCompactOpens Q) :
  Type u_1
Lean

Formalized in Tau Ceti as TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpin.

Sources
LeanTauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpin
Used by 1
Used byTauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpinDiagonal

AbbreviationTauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpin#

The Spin group Spin(V)(𝔸^S) of the adeles away from S: the restricted product over the primes outside S of the local Spin groups relative to the reference subgroups U.spin p.

TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpin.{u_1} {V : Type u_1} [AddCommGroup V]
  [_root_.Module ℚ V] {Q : QuadraticForm ℚ V} (U : TauCeti.QuadraticMap.OrthogonalCompactOpens Q)
  (S : Set Nat.Primes) : Type u_1
Lean

Formalized in Tau Ceti as TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpin.

Sources
LeanTauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpin

AbbreviationTauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCoset#

The finite adelic Spin double-coset set Spin(V)(ℚ) \ Spin(V)(𝔸_f) / ∏_p U_p^{Spin}.

TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCoset.{u_1} {V : Type u_1}
  [AddCommGroup V] [_root_.Module ℚ V] {Q : QuadraticForm ℚ V}
  (U : TauCeti.QuadraticMap.OrthogonalCompactOpens Q) : Type u_1
Lean

Formalized in Tau Ceti as TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCoset.

Sources
LeanTauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCoset

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.