Documentation

TauCeti.NumberTheory.QuadraticForm.OrthogonalGroup.AwayAdelic

Orthogonal, special orthogonal, and Spin points of the adeles away from a set of primes #

Let Q be a quadratic form on a finite-dimensional rational vector space V, let U be a compatible family of compact-open reference subgroups of the local orthogonal and Spin groups (TauCeti.QuadraticMap.OrthogonalCompactOpens), and let S be a set of primes. For a finite set of places containing the archimedean one, S is the set of its finite places, and the adelic points away from it are the restricted products over the primes outside S of the local groups of Q โŠ— โ„š_p, relative to U. This file forms them for each of O, SO and Spin, as RestrictedProductGroupAway S of the reference families already used for the finite adelic groups, so that the away groups are the factors split off by awayDecomposition. No finiteness of S is needed for any of the constructions.

Every reference subgroup is open, so each away group is a Hausdorff topological group, locally compact for O and Spin. The local projections Spin(V_p) โ†’ SO(V_p) โ†’ O(V_p) assemble into continuous componentwise homomorphisms of away groups, and these commute with the restrictions restrictAway S from the finite adelic groups, which forget the components at S. As for the finite adelic groups, SO(V)(๐”ธ^S) โ†’ O(V)(๐”ธ^S) is injective with image cut out by the determinant at every prime outside S, and for a nondegenerate form on a nonzero space the kernel of Spin(V)(๐”ธ^S) โ†’ SO(V)(๐”ธ^S) consists of the elements whose every component is 1 or -1.

Local isometries Q โŠ— โ„š_p โ‰ƒ Q' โŠ— โ„š_p at the primes outside S, carrying the reference subgroups onto one another at almost every such prime, give isomorphisms of topological groups between the groups away from S of Q and of Q', compatible with the maps Spin โ†’ SO โ†’ O. When the local isometries are given at every prime, restricting away from S turns the finite adelic transport TauCeti.restrictedProductCongrRight into the transport away from S.

When no finite prime is removed, the named empty-away equivalences identify all three point groups with their finite adelic groups. They specialize the canonical topological reindexing TauCeti.awayEmptyContinuousMulEquiv, preserve every prime coordinate, and have inverses given by restrictAway โˆ….

Main definitions #

Main results #

References #

The three point groups away from S #

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

The orthogonal group O(V)(๐”ธ^S) of the adeles away from S: the restricted product over the primes outside S of the local orthogonal groups relative to the reference subgroups U.orthogonal p.

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

    The special orthogonal group SO(V)(๐”ธ^S) of the adeles away from S: the restricted product over the primes outside S of the local special orthogonal groups relative to the derived reference subgroups U.specialOrthogonal p.

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

      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.

      Instances For

        The comparison when only the archimedean place is removed #

        source
        noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicOrthogonalEmptyEquiv {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
        U.awayAdelicOrthogonal โˆ… โ‰ƒโ‚œ* U.finiteAdelicOrthogonal

        With no finite primes removed, the away adelic orthogonal group is canonically the finite adelic group. The comparison preserves every prime coordinate.

        Instances For
          source
          noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalEmptyEquiv {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
          U.awayAdelicSpecialOrthogonal โˆ… โ‰ƒโ‚œ* U.finiteAdelicSpecialOrthogonal

          With no finite primes removed, the away adelic special orthogonal group is canonically the finite adelic group. The comparison preserves every prime coordinate.

          Instances For
            source
            noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpinEmptyEquiv {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) :
            U.awayAdelicSpin โˆ… โ‰ƒโ‚œ* U.finiteAdelicSpin

            With no finite primes removed, the away adelic spin group is canonically the finite adelic group. The comparison preserves every prime coordinate.

            Instances For
              source
              @[simp]
              theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicOrthogonalEmptyEquiv_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : U.awayAdelicOrthogonal โˆ…) (p : Nat.Primes) :
              (U.awayAdelicOrthogonalEmptyEquiv x) p = x โŸจp, โ‹ฏโŸฉ

              The empty-away orthogonal comparison preserves each local coordinate.

              source
              @[simp]
              theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalEmptyEquiv_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : U.awayAdelicSpecialOrthogonal โˆ…) (p : Nat.Primes) :
              (U.awayAdelicSpecialOrthogonalEmptyEquiv x) p = x โŸจp, โ‹ฏโŸฉ

              The empty-away special orthogonal comparison preserves each local coordinate.

              source
              @[simp]
              theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpinEmptyEquiv_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : U.awayAdelicSpin โˆ…) (p : Nat.Primes) :
              (U.awayAdelicSpinEmptyEquiv x) p = x โŸจp, โ‹ฏโŸฉ

              The empty-away spin comparison preserves each local coordinate.

              source
              @[simp]
              theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicOrthogonalEmptyEquiv_symm_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : U.finiteAdelicOrthogonal) :
              U.awayAdelicOrthogonalEmptyEquiv.symm x = (restrictAway โˆ… U.orthogonal) x

              The inverse empty-away orthogonal comparison is restriction away from the empty set.

              source
              @[simp]
              theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalEmptyEquiv_symm_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : U.finiteAdelicSpecialOrthogonal) :
              U.awayAdelicSpecialOrthogonalEmptyEquiv.symm x = (restrictAway โˆ… U.specialOrthogonal) x

              The inverse empty-away special orthogonal comparison is restriction away from the empty set.

              source
              @[simp]
              theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpinEmptyEquiv_symm_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : U.finiteAdelicSpin) :
              U.awayAdelicSpinEmptyEquiv.symm x = (restrictAway โˆ… U.spin) x

              The inverse empty-away Spin comparison is restriction away from the empty set.

              Topology #

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

              The orthogonal reference subgroups at the primes outside S are open, which makes the orthogonal group away from S a topological group.

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

              The special orthogonal reference subgroups at the primes outside S are open, which makes the special orthogonal group away from S a topological group.

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

              The Spin reference subgroups at the primes outside S are open, which makes the Spin group away from S a topological group.

              The componentwise projections #

              source
              noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpinToSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) :
              U.awayAdelicSpin S โ†’* U.awayAdelicSpecialOrthogonal S

              The componentwise projection Spin(V)(๐”ธ^S) โ†’ SO(V)(๐”ธ^S), assembled from the local Spin projections at the primes outside S.

              Instances For
                source
                @[simp]
                theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpinToSpecialOrthogonal_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) (x : U.awayAdelicSpin S) (p : { p : Nat.Primes // p โˆ‰ S }) :
                ((U.awayAdelicSpinToSpecialOrthogonal S) x) p = (CliffordAlgebra.spinToSpecialOrthogonal (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q)) (x p)

                The Spin projection away from S is the local Spin projection at every prime outside S.

                source
                theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_awayAdelicSpinToSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) [FiniteDimensional โ„š V] :
                Continuous โ‡‘(U.awayAdelicSpinToSpecialOrthogonal S)

                The Spin projection away from S is continuous.

                source
                noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalToOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) :
                U.awayAdelicSpecialOrthogonal S โ†’* U.awayAdelicOrthogonal S

                The componentwise inclusion SO(V)(๐”ธ^S) โ†’ O(V)(๐”ธ^S). 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.awayAdelicSpecialOrthogonalToOrthogonal_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) (x : U.awayAdelicSpecialOrthogonal S) (p : { p : Nat.Primes // p โˆ‰ S }) :
                  ((U.awayAdelicSpecialOrthogonalToOrthogonal S) x) p = (QuadraticMap.specialOrthogonalToOrthogonal (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q)) (x p)

                  The inclusion of SO into O away from S is the local inclusion at every prime outside S.

                  source
                  theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_awayAdelicSpecialOrthogonalToOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) :
                  Continuous โ‡‘(U.awayAdelicSpecialOrthogonalToOrthogonal S)

                  The inclusion of SO into O away from S is continuous.

                  source
                  @[simp]
                  theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalEmptyEquiv_spinToSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : U.awayAdelicSpin โˆ…) :
                  U.awayAdelicSpecialOrthogonalEmptyEquiv ((U.awayAdelicSpinToSpecialOrthogonal โˆ…) x) = U.finiteAdelicSpinToSpecialOrthogonal (U.awayAdelicSpinEmptyEquiv x)

                  The empty-away comparison commutes with the projection from Spin to SO.

                  source
                  @[simp]
                  theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicOrthogonalEmptyEquiv_specialOrthogonalToOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (x : U.awayAdelicSpecialOrthogonal โˆ…) :
                  U.awayAdelicOrthogonalEmptyEquiv ((U.awayAdelicSpecialOrthogonalToOrthogonal โˆ…) x) = U.finiteAdelicSpecialOrthogonalToOrthogonal (U.awayAdelicSpecialOrthogonalEmptyEquiv x)

                  The empty-away comparison commutes with the inclusion from SO to O.

                  Compatibility with the restrictions from the finite adeles #

                  source
                  @[simp]
                  theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpinToSpecialOrthogonal_comp_restrictAway {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) :
                  (U.awayAdelicSpinToSpecialOrthogonal S).comp (restrictAway S U.spin) = (restrictAway S U.specialOrthogonal).comp U.finiteAdelicSpinToSpecialOrthogonal

                  Restricting a finite adelic Spin point away from S commutes with projecting it to SO.

                  source
                  @[simp]
                  theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalToOrthogonal_comp_restrictAway {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) :
                  (U.awayAdelicSpecialOrthogonalToOrthogonal S).comp (restrictAway S U.specialOrthogonal) = (restrictAway S U.orthogonal).comp U.finiteAdelicSpecialOrthogonalToOrthogonal

                  Restricting a finite adelic special orthogonal point away from S commutes with including it in O.

                  The image of SO and the kernel of the Spin projection #

                  source
                  theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalToOrthogonal_injective {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) :
                  Function.Injective โ‡‘(U.awayAdelicSpecialOrthogonalToOrthogonal S)

                  The inclusion of SO into O away from S is injective.

                  source
                  theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_range_awayAdelicSpecialOrthogonalToOrthogonal_iff {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) (x : U.awayAdelicOrthogonal S) :
                  x โˆˆ (U.awayAdelicSpecialOrthogonalToOrthogonal S).range โ†” โˆ€ (p : { p : Nat.Primes // p โˆ‰ S }), x p โˆˆ QuadraticMap.specialOrthogonalWithin (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q)

                  An orthogonal point away from S comes from the special orthogonal group away from S exactly when each of its components has determinant one. As for the finite adelic groups, 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_awayAdelicSpinToSpecialOrthogonal_iff {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) [FiniteDimensional โ„š V] (hQ : QuadraticMap.Nondegenerate) (x : U.awayAdelicSpin S) :
                  x โˆˆ (U.awayAdelicSpinToSpecialOrthogonal S).ker โ†” โˆ€ (p : { p : Nat.Primes // p โˆ‰ S }), โ†‘(x p) = 1 โˆจ โ†‘(x p) = -1

                  For a nondegenerate form, a Spin point away from S projects to the identity of SO(V)(๐”ธ^S) exactly when each of its components is 1 or -1 in the local Clifford algebra.

                  Transport along local isometries #

                  source
                  noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicOrthogonalCongr {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : { p : Nat.Primes // p โˆ‰ S }) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q')) (he : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).orthogonalGroupCongr โ†‘(U.orthogonal โ†‘p) โ†‘(U'.orthogonal โ†‘p)) :
                  U.awayAdelicOrthogonal S โ‰ƒโ‚œ* U'.awayAdelicOrthogonal S

                  The isomorphism of orthogonal groups away from S induced by local isometries at the primes outside S which carry the orthogonal reference subgroups onto one another at almost every such prime.

                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicOrthogonalCongr_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : { p : Nat.Primes // p โˆ‰ S }) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q')) (he : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).orthogonalGroupCongr โ†‘(U.orthogonal โ†‘p) โ†‘(U'.orthogonal โ†‘p)) (x : U.awayAdelicOrthogonal S) (p : { p : Nat.Primes // p โˆ‰ S }) :
                    ((U.awayAdelicOrthogonalCongr S U' e he) x) p = (e p).orthogonalGroupCongr (x p)

                    Orthogonal transport away from S applies the local isometry at every prime outside S.

                    source
                    @[simp]
                    theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicOrthogonalCongr_symm_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : { p : Nat.Primes // p โˆ‰ S }) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q')) (he : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).orthogonalGroupCongr โ†‘(U.orthogonal โ†‘p) โ†‘(U'.orthogonal โ†‘p)) (y : U'.awayAdelicOrthogonal S) (p : { p : Nat.Primes // p โˆ‰ S }) :
                    ((U.awayAdelicOrthogonalCongr S U' e he).symm y) p = (e p).orthogonalGroupCongr.symm (y p)

                    Inverse orthogonal transport away from S applies the inverse local isometries.

                    source
                    noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalCongr {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : { p : Nat.Primes // p โˆ‰ S }) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q')) (hso : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).specialOrthogonalGroupCongr โ†‘(U.specialOrthogonal โ†‘p) โ†‘(U'.specialOrthogonal โ†‘p)) :
                    U.awayAdelicSpecialOrthogonal S โ‰ƒโ‚œ* U'.awayAdelicSpecialOrthogonal S

                    The isomorphism of special orthogonal groups away from S induced by local isometries at the primes outside S which carry the special orthogonal reference subgroups onto one another at almost every such prime.

                    Instances For
                      source
                      @[simp]
                      theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalCongr_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : { p : Nat.Primes // p โˆ‰ S }) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q')) (hso : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).specialOrthogonalGroupCongr โ†‘(U.specialOrthogonal โ†‘p) โ†‘(U'.specialOrthogonal โ†‘p)) (x : U.awayAdelicSpecialOrthogonal S) (p : { p : Nat.Primes // p โˆ‰ S }) :
                      ((U.awayAdelicSpecialOrthogonalCongr S U' e hso) x) p = (e p).specialOrthogonalGroupCongr (x p)

                      Special orthogonal transport away from S applies the local isometry at every prime outside S.

                      source
                      @[simp]
                      theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalCongr_symm_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : { p : Nat.Primes // p โˆ‰ S }) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q')) (hso : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).specialOrthogonalGroupCongr โ†‘(U.specialOrthogonal โ†‘p) โ†‘(U'.specialOrthogonal โ†‘p)) (y : U'.awayAdelicSpecialOrthogonal S) (p : { p : Nat.Primes // p โˆ‰ S }) :
                      ((U.awayAdelicSpecialOrthogonalCongr S U' e hso).symm y) p = (e p).specialOrthogonalGroupCongr.symm (y p)

                      Inverse special orthogonal transport away from S applies the inverse local isometries.

                      source
                      noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpinCongr {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : { p : Nat.Primes // p โˆ‰ S }) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q')) (hs : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).spinGroupEquiv โ†‘(U.spin โ†‘p) โ†‘(U'.spin โ†‘p)) :
                      U.awayAdelicSpin S โ‰ƒโ‚œ* U'.awayAdelicSpin S

                      The isomorphism of Spin groups away from S induced by local isometries at the primes outside S which carry the Spin reference subgroups onto one another at almost every such prime.

                      Instances For
                        source
                        @[simp]
                        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpinCongr_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : { p : Nat.Primes // p โˆ‰ S }) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q')) (hs : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).spinGroupEquiv โ†‘(U.spin โ†‘p) โ†‘(U'.spin โ†‘p)) (x : U.awayAdelicSpin S) (p : { p : Nat.Primes // p โˆ‰ S }) :
                        ((U.awayAdelicSpinCongr S U' e hs) x) p = (e p).spinGroupEquiv (x p)

                        Spin transport away from S applies the local isometry at every prime outside S.

                        source
                        @[simp]
                        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpinCongr_symm_apply {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : { p : Nat.Primes // p โˆ‰ S }) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q')) (hs : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).spinGroupEquiv โ†‘(U.spin โ†‘p) โ†‘(U'.spin โ†‘p)) (y : U'.awayAdelicSpin S) (p : { p : Nat.Primes // p โˆ‰ S }) :
                        ((U.awayAdelicSpinCongr S U' e hs).symm y) p = (e p).spinGroupEquiv.symm (y p)

                        Inverse Spin transport away from S applies the inverse local isometries.

                        source
                        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalCongr_comp_awayAdelicSpinToSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : { p : Nat.Primes // p โˆ‰ S }) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q')) (hs : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).spinGroupEquiv โ†‘(U.spin โ†‘p) โ†‘(U'.spin โ†‘p)) (hso : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).specialOrthogonalGroupCongr โ†‘(U.specialOrthogonal โ†‘p) โ†‘(U'.specialOrthogonal โ†‘p)) :
                        (โ†‘(U.awayAdelicSpecialOrthogonalCongr S U' e hso)).comp (U.awayAdelicSpinToSpecialOrthogonal S) = (U'.awayAdelicSpinToSpecialOrthogonal S).comp โ†‘(U.awayAdelicSpinCongr S U' e hs)

                        Transport away from S intertwines the Spin projections away from S.

                        source
                        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalToOrthogonal_comp_awayAdelicSpecialOrthogonalCongr {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {W : Type u_2} [AddCommGroup W] [Module โ„š W] {Q' : QuadraticForm โ„š W} (U' : OrthogonalCompactOpens Q') (e : (p : { p : Nat.Primes // p โˆ‰ S }) โ†’ QuadraticMap.IsometryEquiv (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q) (QuadraticForm.baseChange โ„š_[โ†‘โ†‘p] Q')) (he : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).orthogonalGroupCongr โ†‘(U.orthogonal โ†‘p) โ†‘(U'.orthogonal โ†‘p)) (hso : โˆ€แถ  (p : { p : Nat.Primes // p โˆ‰ S }) in Filter.cofinite, Set.BijOn โ‡‘(e p).specialOrthogonalGroupCongr โ†‘(U.specialOrthogonal โ†‘p) โ†‘(U'.specialOrthogonal โ†‘p)) :
                        (U'.awayAdelicSpecialOrthogonalToOrthogonal S).comp โ†‘(U.awayAdelicSpecialOrthogonalCongr S U' e hso) = (โ†‘(U.awayAdelicOrthogonalCongr S U' e he)).comp (U.awayAdelicSpecialOrthogonalToOrthogonal S)

                        Transport away from S intertwines the inclusions of SO into O away from S.

                        Compatibility of transport with the restrictions from the finite adeles #

                        source
                        @[simp]
                        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicOrthogonalCongr_comp_restrictAway {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {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)) :
                        (โ†‘(U.awayAdelicOrthogonalCongr S U' (fun (p : { p : Nat.Primes // p โˆ‰ S }) => e โ†‘p) โ‹ฏ)).comp (restrictAway S U.orthogonal) = (restrictAway S U'.orthogonal).comp โ†‘(restrictedProductCongrRight U.orthogonal U'.orthogonal (fun (p : Nat.Primes) => (e p).orthogonalGroupCongr) he)

                        Restricting away from S turns finite adelic orthogonal transport into orthogonal transport away from S.

                        source
                        @[simp]
                        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalCongr_comp_restrictAway {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {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')) (hso : โˆ€แถ  (p : Nat.Primes) in Filter.cofinite, Set.BijOn โ‡‘(e p).specialOrthogonalGroupCongr โ†‘(U.specialOrthogonal p) โ†‘(U'.specialOrthogonal p)) :
                        (โ†‘(U.awayAdelicSpecialOrthogonalCongr S U' (fun (p : { p : Nat.Primes // p โˆ‰ S }) => e โ†‘p) โ‹ฏ)).comp (restrictAway S U.specialOrthogonal) = (restrictAway S U'.specialOrthogonal).comp โ†‘(restrictedProductCongrRight U.specialOrthogonal U'.specialOrthogonal (fun (p : Nat.Primes) => (e p).specialOrthogonalGroupCongr) hso)

                        Restricting away from S turns finite adelic special orthogonal transport into special orthogonal transport away from S.

                        source
                        @[simp]
                        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpinCongr_comp_restrictAway {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (S : Set Nat.Primes) {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)) :
                        (โ†‘(U.awayAdelicSpinCongr S U' (fun (p : { p : Nat.Primes // p โˆ‰ S }) => e โ†‘p) โ‹ฏ)).comp (restrictAway S U.spin) = (restrictAway S U'.spin).comp โ†‘(restrictedProductCongrRight U.spin U'.spin (fun (p : Nat.Primes) => (e p).spinGroupEquiv) hs)

                        Restricting away from S turns finite adelic Spin transport into Spin transport away from S.