Documentation

TauCeti.NumberTheory.QuadraticForm.OrthogonalGroup.Diagonal.Finite

Rational points on the diagonal of the finite adelic orthogonal groups #

Let Q be a quadratic form on a finite-dimensional rational vector space V, and let U be compatible compact-open reference data (TauCeti.QuadraticMap.OrthogonalCompactOpens). Extending scalars to โ„š_p sends a rational point of O(V), SO(V) or Spin(V) to a local point at every prime, and the integrality conditions recorded in U put it in the reference subgroup at almost every prime. These local images therefore assemble into diagonal homomorphisms

O(V)(โ„š) โ†’ O(V)(๐”ธ_f), SO(V)(โ„š) โ†’ SO(V)(๐”ธ_f), Spin(V)(โ„š) โ†’ Spin(V)(๐”ธ_f),

built with TauCeti.rationalDiagonal. For SO the integrality comes from that of O, through OrthogonalCompactOpens.eventually_specialOrthogonal, rather than from a further hypothesis.

Each diagonal is injective, since already the extension of scalars to a single โ„š_p is. The diagonals commute with the componentwise natural maps Spin(V)(๐”ธ_f) โ†’ SO(V)(๐”ธ_f) โ†’ O(V)(๐”ธ_f) (the Spin-to-SO map and the SO-to-O inclusion). In particular the two routes from Spin(V)(โ„š) to SO(V)(๐”ธ_f), through Spin(V)(๐”ธ_f) or through SO(V)(โ„š), agree, so the image of the rational Spin points in adelic SO is unambiguous. Finally the finite adelic spinor norm of a rational proper isometry is, at every prime, the image of its rational spinor norm in the local square classes; so rational proper isometries with trivial spinor norm lie in the adelic spinor kernel.

Main definitions #

Main results #

References #

The three diagonals #

source
noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDiagonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
โ†ฅ(orthogonalGroup Q) โ†’* U.finiteAdelicOrthogonal

The diagonal embedding O(V)(โ„š) โ†’ O(V)(๐”ธ_f), extending the scalars of a rational isometry to โ„š_p at every prime.

Instances For
    source
    @[simp]
    theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDiagonal_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (g : โ†ฅ(orthogonalGroup Q)) (p : Nat.Primes) :
    (U.finiteAdelicOrthogonalDiagonal g) p = (orthogonalGroupBaseChange Q) g

    The p-component of the diagonal image of a rational isometry is its extension of scalars to โ„š_p.

    source
    theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDiagonal_injective {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
    Function.Injective โ‡‘U.finiteAdelicOrthogonalDiagonal

    The diagonal embedding of rational isometries is injective.

    source
    noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDiagonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
    โ†ฅ(spinGroup Q) โ†’* U.finiteAdelicSpin

    The diagonal embedding Spin(V)(โ„š) โ†’ Spin(V)(๐”ธ_f), extending the scalars of a rational Spin element to โ„š_p at every prime.

    Instances For
      source
      @[simp]
      theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDiagonal_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : โ†ฅ(spinGroup Q)) (p : Nat.Primes) :
      (U.finiteAdelicSpinDiagonal x) p = (CliffordAlgebra.spinGroupBaseChange Q) x

      The p-component of the diagonal image of a rational Spin element is its extension of scalars to โ„š_p.

      source
      theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDiagonal_injective {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
      Function.Injective โ‡‘U.finiteAdelicSpinDiagonal

      The diagonal embedding of rational Spin elements is injective.

      source
      noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDiagonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] :
      โ†ฅ(specialOrthogonalGroup Q) โ†’* U.finiteAdelicSpecialOrthogonal

      The diagonal embedding SO(V)(โ„š) โ†’ SO(V)(๐”ธ_f). Its integrality at almost every prime is derived from that of the orthogonal reference subgroups.

      Instances For
        source
        @[simp]
        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDiagonal_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (g : โ†ฅ(specialOrthogonalGroup Q)) (p : Nat.Primes) :
        (U.finiteAdelicSpecialOrthogonalDiagonal g) p = (specialOrthogonalGroupBaseChange Q) g

        The p-component of the diagonal image of a rational proper isometry is its extension of scalars to โ„š_p.

        source
        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDiagonal_injective {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] :
        Function.Injective โ‡‘U.finiteAdelicSpecialOrthogonalDiagonal

        The diagonal embedding of rational proper isometries is injective.

        Compatibility with the componentwise natural maps #

        source
        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinToSpecialOrthogonal_comp_finiteAdelicSpinDiagonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] :
        U.finiteAdelicSpinToSpecialOrthogonal.comp U.finiteAdelicSpinDiagonal = U.finiteAdelicSpecialOrthogonalDiagonal.comp (CliffordAlgebra.spinToSpecialOrthogonal Q)

        The diagonal commutes with the projections Spin โ†’ SO: mapping Spin(V)(โ„š) to SO(V)(๐”ธ_f) through Spin(V)(๐”ธ_f) or through SO(V)(โ„š) gives the same homomorphism.

        source
        @[simp]
        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinToSpecialOrthogonal_finiteAdelicSpinDiagonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (x : โ†ฅ(spinGroup Q)) :
        U.finiteAdelicSpinToSpecialOrthogonal (U.finiteAdelicSpinDiagonal x) = U.finiteAdelicSpecialOrthogonalDiagonal ((CliffordAlgebra.spinToSpecialOrthogonal Q) x)

        Pointwise form of finiteAdelicSpinToSpecialOrthogonal_comp_finiteAdelicSpinDiagonal.

        source
        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalToOrthogonal_comp_finiteAdelicSpecialOrthogonalDiagonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] :
        U.finiteAdelicSpecialOrthogonalToOrthogonal.comp U.finiteAdelicSpecialOrthogonalDiagonal = U.finiteAdelicOrthogonalDiagonal.comp (QuadraticMap.specialOrthogonalToOrthogonal Q)

        The diagonal commutes with the inclusions SO โ†’ O.

        source
        @[simp]
        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalToOrthogonal_finiteAdelicSpecialOrthogonalDiagonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (g : โ†ฅ(specialOrthogonalGroup Q)) :
        U.finiteAdelicSpecialOrthogonalToOrthogonal (U.finiteAdelicSpecialOrthogonalDiagonal g) = U.finiteAdelicOrthogonalDiagonal ((QuadraticMap.specialOrthogonalToOrthogonal Q) g)

        Pointwise form of finiteAdelicSpecialOrthogonalToOrthogonal_comp_finiteAdelicSpecialOrthogonalDiagonal.

        The adelic spinor norm of a rational point #

        source
        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.adelicSpinorNorm_finiteAdelicSpecialOrthogonalDiagonal_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (hQ : QuadraticMap.Nondegenerate) (g : โ†ฅ(specialOrthogonalGroup Q)) (p : Nat.Primes) :
        ((U.adelicSpinorNorm hQ) (U.finiteAdelicSpecialOrthogonalDiagonal g)) p = (algebraMap โ„š โ„š_[โ†‘p]).multiplicativeSquareClassMap ((CliffordAlgebra.spinorNorm Q hQ) g)

        The p-component of the finite adelic spinor norm of a rational proper isometry is the image of its rational spinor norm in the local square classes.

        source
        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDiagonal_mem_adelicSpinorKernel {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (hQ : QuadraticMap.Nondegenerate) {g : โ†ฅ(specialOrthogonalGroup Q)} (hg : (CliffordAlgebra.spinorNorm Q hQ) g = 1) :
        U.finiteAdelicSpecialOrthogonalDiagonal g โˆˆ U.adelicSpinorKernel hQ

        A rational proper isometry of trivial spinor norm lies, diagonally, in the adelic spinor kernel.