Documentation

TauCeti.NumberTheory.QuadraticForm.OrthogonalGroup.FiniteAdelic

Finite adelic orthogonal, special orthogonal, and Spin groups #

Let Q be a quadratic form on a finite-dimensional rational vector space V, and let U be a compatible family of compact-open reference subgroups of the local orthogonal and Spin groups (TauCeti.QuadraticMap.OrthogonalCompactOpens). This file forms the three finite adelic point groups O(V)(๐”ธ_f), SO(V)(๐”ธ_f) and Spin(V)(๐”ธ_f): the restricted products over the primes of the local groups of Q โŠ— โ„š_p relative to U, the special orthogonal reference subgroups being the ones derived from the orthogonal family.

Every reference subgroup is open, so each of the three restricted products is a Hausdorff topological group for its restricted-product topology, and the orthogonal and Spin ones are locally compact because their reference subgroups are compact. The local topologies are the canonical ones on linear automorphisms and on the Clifford algebra, so the compactness and openness recorded in U are statements about these adelic groups.

The local projections Spin(V_p) โ†’ SO(V_p) โ†’ O(V_p) carry the reference subgroups into one another at every prime, so they assemble into continuous componentwise homomorphisms of finite adelic groups. The map SO(V)(๐”ธ_f) โ†’ O(V)(๐”ธ_f) is injective, and its image is exactly the finite adelic isometries whose every component has determinant one: a proper isometry lying in U_p^O lies in the derived subgroup U_p^{SO} by definition, so no integrality is lost. For a nondegenerate form on a nonzero space, the kernel of Spin(V)(๐”ธ_f) โ†’ SO(V)(๐”ธ_f) consists of the finite adeles whose every component is 1 or -1.

Local isometries Q โŠ— โ„š_p โ‰ƒ Q' โŠ— โ„š_p which carry the reference subgroups onto one another at almost every prime identify the finite adelic groups of Q and Q' through TauCeti.restrictedProductCongrRight, and these identifications intertwine the componentwise projections Spin โ†’ SO โ†’ O.

Main definitions #

Main results #

References #

The three finite adelic groups #

source
@[reducible, inline]
abbrev TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
Type u_1

The finite adelic orthogonal group O(V)(๐”ธ_f): the restricted product of the local orthogonal groups O(V_p) relative to the reference subgroups U.orthogonal p.

Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
    Type u_1

    The finite adelic special orthogonal group SO(V)(๐”ธ_f): the restricted product of the local special orthogonal groups relative to the derived reference subgroups U.specialOrthogonal p.

    Instances For
      source
      @[reducible, inline]
      abbrev TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpin {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
      Type u_1

      The finite adelic Spin group Spin(V)(๐”ธ_f): the restricted product of the local Spin groups relative to the reference subgroups U.spin p.

      Instances For

        Topology #

        source
        instance TauCeti.QuadraticMap.OrthogonalCompactOpens.factIsOpenOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
        Fact (โˆ€ (p : Nat.Primes), IsOpen โ†‘(U.orthogonal p))

        The orthogonal reference subgroups are open, which makes the finite adelic orthogonal group a topological group.

        source
        instance TauCeti.QuadraticMap.OrthogonalCompactOpens.factIsOpenSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
        Fact (โˆ€ (p : Nat.Primes), IsOpen โ†‘(U.specialOrthogonal p))

        The special orthogonal reference subgroups are open, which makes the finite adelic special orthogonal group a topological group.

        source
        instance TauCeti.QuadraticMap.OrthogonalCompactOpens.factIsOpenSpin {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
        Fact (โˆ€ (p : Nat.Primes), IsOpen โ†‘(U.spin p))

        The Spin reference subgroups are open, which makes the finite adelic Spin group a topological group.

        source
        instance TauCeti.QuadraticMap.OrthogonalCompactOpens.compactSpace_orthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (p : Nat.Primes) :
        CompactSpace โ†ฅ(U.orthogonal p)

        The orthogonal reference subgroups are compact spaces.

        source
        instance TauCeti.QuadraticMap.OrthogonalCompactOpens.compactSpace_spin {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (p : Nat.Primes) :
        CompactSpace โ†ฅ(U.spin p)

        The Spin reference subgroups are compact spaces.

        The componentwise projections #

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

        The componentwise projection Spin(V)(๐”ธ_f) โ†’ SO(V)(๐”ธ_f), assembled from the local Spin projections, which carry U.spin p into the derived subgroup U.specialOrthogonal p.

        Instances For
          source
          @[simp]
          theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinToSpecialOrthogonal_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : U.finiteAdelicSpin) (p : Nat.Primes) :
          (U.finiteAdelicSpinToSpecialOrthogonal x) p = (CliffordAlgebra.spinToSpecialOrthogonal (QuadraticForm.baseChange โ„š_[โ†‘p] Q)) (x p)

          The adelic Spin projection is the local Spin projection at every prime.

          source
          theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_finiteAdelicSpinToSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] :
          Continuous โ‡‘U.finiteAdelicSpinToSpecialOrthogonal

          The adelic Spin projection is continuous.

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

          The componentwise inclusion SO(V)(๐”ธ_f) โ†’ O(V)(๐”ธ_f). It is well defined because the special orthogonal reference subgroups are the preimages of the orthogonal ones.

          Instances For
            source
            @[simp]
            theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalToOrthogonal_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : U.finiteAdelicSpecialOrthogonal) (p : Nat.Primes) :
            (U.finiteAdelicSpecialOrthogonalToOrthogonal x) p = (QuadraticMap.specialOrthogonalToOrthogonal (QuadraticForm.baseChange โ„š_[โ†‘p] Q)) (x p)

            The adelic inclusion of SO into O is the local inclusion at every prime.

            source
            theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_finiteAdelicSpecialOrthogonalToOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
            Continuous โ‡‘U.finiteAdelicSpecialOrthogonalToOrthogonal

            The adelic inclusion of SO into O is continuous.

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

            The adelic inclusion of SO into O is injective.

            source
            theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_range_finiteAdelicSpecialOrthogonalToOrthogonal_iff {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : U.finiteAdelicOrthogonal) :
            x โˆˆ U.finiteAdelicSpecialOrthogonalToOrthogonal.range โ†” โˆ€ (p : Nat.Primes), x p โˆˆ QuadraticMap.specialOrthogonalWithin (QuadraticForm.baseChange โ„š_[โ†‘p] Q)

            A finite adelic isometry comes from the finite adelic special orthogonal group exactly when each of its components has determinant one. The derived reference subgroups make this exact: a proper local isometry in U.orthogonal p lies in U.specialOrthogonal p.

            source
            theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_ker_finiteAdelicSpinToSpecialOrthogonal_iff {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (hQ : QuadraticMap.Nondegenerate) (x : U.finiteAdelicSpin) :
            x โˆˆ U.finiteAdelicSpinToSpecialOrthogonal.ker โ†” โˆ€ (p : Nat.Primes), โ†‘(x p) = 1 โˆจ โ†‘(x p) = -1

            For a nondegenerate form, a finite adelic Spin element projects to the identity of SO(V)(๐”ธ_f) exactly when each of its components is 1 or -1 in the local Clifford algebra.

            Transport along local isometries #

            source
            @[simp]
            theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.restrictedProductCongrRight_finiteAdelicSpinToSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : Nat.Primes) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘p] Q')) (hs : โˆ€แถ  (p : Nat.Primes) in Filter.cofinite, Set.BijOn โ‡‘(e p).spinGroupEquiv โ†‘(U.spin p) โ†‘(U'.spin p)) (hso : โˆ€แถ  (p : Nat.Primes) in Filter.cofinite, Set.BijOn โ‡‘(e p).specialOrthogonalGroupCongr โ†‘(U.specialOrthogonal p) โ†‘(U'.specialOrthogonal p)) (x : U.finiteAdelicSpin) :
            (restrictedProductCongrRight U.specialOrthogonal U'.specialOrthogonal (fun (p : Nat.Primes) => (e p).specialOrthogonalGroupCongr) hso) (U.finiteAdelicSpinToSpecialOrthogonal x) = U'.finiteAdelicSpinToSpecialOrthogonal ((restrictedProductCongrRight U.spin U'.spin (fun (p : Nat.Primes) => (e p).spinGroupEquiv) hs) x)

            Local isometric transport of finite adelic points intertwines the adelic Spin projections.

            source
            @[simp]
            theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalToOrthogonal_restrictedProductCongrRight {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : Nat.Primes) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘p] Q')) (he : โˆ€แถ  (p : Nat.Primes) in Filter.cofinite, Set.BijOn โ‡‘(e p).orthogonalGroupCongr โ†‘(U.orthogonal p) โ†‘(U'.orthogonal p)) (hso : โˆ€แถ  (p : Nat.Primes) in Filter.cofinite, Set.BijOn โ‡‘(e p).specialOrthogonalGroupCongr โ†‘(U.specialOrthogonal p) โ†‘(U'.specialOrthogonal p)) (g : U.finiteAdelicSpecialOrthogonal) :
            U'.finiteAdelicSpecialOrthogonalToOrthogonal ((restrictedProductCongrRight U.specialOrthogonal U'.specialOrthogonal (fun (p : Nat.Primes) => (e p).specialOrthogonalGroupCongr) hso) g) = (restrictedProductCongrRight U.orthogonal U'.orthogonal (fun (p : Nat.Primes) => (e p).orthogonalGroupCongr) he) (U.finiteAdelicSpecialOrthogonalToOrthogonal g)

            Local isometric transport of finite adelic points intertwines the adelic inclusions of SO into O.