Documentation

TauCeti.NumberTheory.QuadraticForm.OrthogonalGroup.DoubleCoset.Basic

Finite adelic double cosets of orthogonal and Spin groups #

Let Q be a quadratic form over โ„š and let U be compatible compact-open reference data. The finite adelic class sets attached to U are

G(โ„š) \ G(๐”ธ_f) / โˆ_p U_p

for G = O, SO, and Spin. The left subgroup is the range of the corresponding rational diagonal, rather than an unrelated copy of G(โ„š), and the right subgroup is the everywhere-integral subgroup of the restricted product.

The comparisons for these types are deliberately the general double-coset constructions:

Keeping these maps separate matters. An eventual change of reference family canonically identifies the ambient restricted products, but need not carry one everywhere-integral subgroup to the other.

References #

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

The finite adelic orthogonal double-coset set O(V)(โ„š) \ O(V)(๐”ธ_f) / โˆ_p U_p^O.

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

    The finite adelic Spin double-coset set Spin(V)(โ„š) \ Spin(V)(๐”ธ_f) / โˆ_p U_p^{Spin}.

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

      The finite adelic special-orthogonal double-coset set SO(V)(โ„š) \ SO(V)(๐”ธ_f) / โˆ_p U_p^{SO}.

      Instances For

        Enlargement and conjugation of the right subgroup #

        source
        noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetMapOfLE {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (K : Subgroup U.finiteAdelicOrthogonal) (hK : integralSubgroup U.orthogonal โ‰ค K) :
        U.finiteAdelicOrthogonalDoubleCoset โ†’ DoubleCoset.Quotient โ†‘U.finiteAdelicOrthogonalDiagonal.range โ†‘K

        Enlarging the right subgroup of the finite adelic orthogonal class set gives a surjection.

        Instances For
          source
          @[simp]
          theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetMapOfLE_apply_mk {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (K : Subgroup U.finiteAdelicOrthogonal) (hK : integralSubgroup U.orthogonal โ‰ค K) (x : U.finiteAdelicOrthogonal) :
          U.finiteAdelicOrthogonalDoubleCosetMapOfLE K hK (DoubleCoset.mk U.finiteAdelicOrthogonalDiagonal.range (integralSubgroup U.orthogonal) x) = DoubleCoset.mk U.finiteAdelicOrthogonalDiagonal.range K x

          Enlarging the orthogonal right subgroup preserves representatives.

          source
          theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetMapOfLE_surjective {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (K : Subgroup U.finiteAdelicOrthogonal) (hK : integralSubgroup U.orthogonal โ‰ค K) :
          Function.Surjective (U.finiteAdelicOrthogonalDoubleCosetMapOfLE K hK)

          The finite adelic orthogonal double-coset map obtained by enlarging the right subgroup is surjective.

          source
          noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetConj {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (g : U.finiteAdelicOrthogonal) :
          U.finiteAdelicOrthogonalDoubleCoset โ‰ƒ DoubleCoset.Quotient โ†‘U.finiteAdelicOrthogonalDiagonal.range โ†‘(Subgroup.map (โ†‘(MulEquiv.symm (MulAut.conj g))) (integralSubgroup U.orthogonal))

          Right translation identifies the finite adelic orthogonal class set with the quotient by the conjugate of its right compact-open subgroup.

          Instances For
            source
            theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetConj_apply_mk {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (g x : U.finiteAdelicOrthogonal) :
            (U.finiteAdelicOrthogonalDoubleCosetConj g) (DoubleCoset.mk U.finiteAdelicOrthogonalDiagonal.range (integralSubgroup U.orthogonal) x) = DoubleCoset.mk U.finiteAdelicOrthogonalDiagonal.range (Subgroup.map (โ†‘(MulEquiv.symm (MulAut.conj g))) (integralSubgroup U.orthogonal)) (x * g)

            Orthogonal right translation sends the class of x to the class of x * g.

            Not a simp lemma: the codomain contains a coerced mapped subgroup, which simp rewrites to a set image in the dependent type.

            source
            theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetConj_symm_apply_mk {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (g y : U.finiteAdelicOrthogonal) :
            (U.finiteAdelicOrthogonalDoubleCosetConj g).symm (DoubleCoset.mk U.finiteAdelicOrthogonalDiagonal.range (Subgroup.map (โ†‘(MulEquiv.symm (MulAut.conj g))) (integralSubgroup U.orthogonal)) y) = DoubleCoset.mk U.finiteAdelicOrthogonalDiagonal.range (integralSubgroup U.orthogonal) (y * gโปยน)

            The inverse orthogonal right translation sends the class of y to the class of y * gโปยน.

            Not a simp lemma, for the same dependent-type reason as finiteAdelicOrthogonalDoubleCosetConj_apply_mk.

            source
            noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetMapOfLE {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (K : Subgroup U.finiteAdelicSpin) (hK : integralSubgroup U.spin โ‰ค K) :
            U.finiteAdelicSpinDoubleCoset โ†’ DoubleCoset.Quotient โ†‘U.finiteAdelicSpinDiagonal.range โ†‘K

            Enlarging the right subgroup of the finite adelic Spin class set gives a surjection.

            Instances For
              source
              @[simp]
              theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetMapOfLE_apply_mk {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (K : Subgroup U.finiteAdelicSpin) (hK : integralSubgroup U.spin โ‰ค K) (x : U.finiteAdelicSpin) :
              U.finiteAdelicSpinDoubleCosetMapOfLE K hK (DoubleCoset.mk U.finiteAdelicSpinDiagonal.range (integralSubgroup U.spin) x) = DoubleCoset.mk U.finiteAdelicSpinDiagonal.range K x

              Enlarging the Spin right subgroup preserves representatives.

              source
              theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetMapOfLE_surjective {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (K : Subgroup U.finiteAdelicSpin) (hK : integralSubgroup U.spin โ‰ค K) :
              Function.Surjective (U.finiteAdelicSpinDoubleCosetMapOfLE K hK)

              The finite adelic Spin double-coset map obtained by enlarging the right subgroup is surjective.

              source
              noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetConj {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (g : U.finiteAdelicSpin) :
              U.finiteAdelicSpinDoubleCoset โ‰ƒ DoubleCoset.Quotient โ†‘U.finiteAdelicSpinDiagonal.range โ†‘(Subgroup.map (โ†‘(MulEquiv.symm (MulAut.conj g))) (integralSubgroup U.spin))

              Right translation identifies the finite adelic Spin class set with the quotient by the conjugate of its right compact-open subgroup.

              Instances For
                source
                theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetConj_apply_mk {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (g x : U.finiteAdelicSpin) :
                (U.finiteAdelicSpinDoubleCosetConj g) (DoubleCoset.mk U.finiteAdelicSpinDiagonal.range (integralSubgroup U.spin) x) = DoubleCoset.mk U.finiteAdelicSpinDiagonal.range (Subgroup.map (โ†‘(MulEquiv.symm (MulAut.conj g))) (integralSubgroup U.spin)) (x * g)

                Spin right translation sends the class of x to the class of x * g.

                Not a simp lemma: the codomain contains a coerced mapped subgroup, which simp rewrites to a set image in the dependent type.

                source
                theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetConj_symm_apply_mk {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) (g y : U.finiteAdelicSpin) :
                (U.finiteAdelicSpinDoubleCosetConj g).symm (DoubleCoset.mk U.finiteAdelicSpinDiagonal.range (Subgroup.map (โ†‘(MulEquiv.symm (MulAut.conj g))) (integralSubgroup U.spin)) y) = DoubleCoset.mk U.finiteAdelicSpinDiagonal.range (integralSubgroup U.spin) (y * gโปยน)

                The inverse Spin right translation sends the class of y to the class of y * gโปยน.

                Not a simp lemma, for the same dependent-type reason as finiteAdelicSpinDoubleCosetConj_apply_mk.

                source
                noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetMapOfLE {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (K : Subgroup U.finiteAdelicSpecialOrthogonal) (hK : integralSubgroup U.specialOrthogonal โ‰ค K) :
                U.finiteAdelicSpecialOrthogonalDoubleCoset โ†’ DoubleCoset.Quotient โ†‘U.finiteAdelicSpecialOrthogonalDiagonal.range โ†‘K

                Enlarging the right subgroup of the finite adelic special-orthogonal class set gives a surjection.

                Instances For
                  source
                  @[simp]
                  theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetMapOfLE_apply_mk {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (K : Subgroup U.finiteAdelicSpecialOrthogonal) (hK : integralSubgroup U.specialOrthogonal โ‰ค K) (x : U.finiteAdelicSpecialOrthogonal) :
                  U.finiteAdelicSpecialOrthogonalDoubleCosetMapOfLE K hK (DoubleCoset.mk U.finiteAdelicSpecialOrthogonalDiagonal.range (integralSubgroup U.specialOrthogonal) x) = DoubleCoset.mk U.finiteAdelicSpecialOrthogonalDiagonal.range K x

                  Enlarging the special-orthogonal right subgroup preserves representatives.

                  source
                  theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetMapOfLE_surjective {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (K : Subgroup U.finiteAdelicSpecialOrthogonal) (hK : integralSubgroup U.specialOrthogonal โ‰ค K) :
                  Function.Surjective (U.finiteAdelicSpecialOrthogonalDoubleCosetMapOfLE K hK)

                  The finite adelic special-orthogonal double-coset map obtained by enlarging the right subgroup is surjective.

                  source
                  noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetConj {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (g : U.finiteAdelicSpecialOrthogonal) :
                  U.finiteAdelicSpecialOrthogonalDoubleCoset โ‰ƒ DoubleCoset.Quotient โ†‘U.finiteAdelicSpecialOrthogonalDiagonal.range โ†‘(Subgroup.map (โ†‘(MulEquiv.symm (MulAut.conj g))) (integralSubgroup U.specialOrthogonal))

                  Right translation identifies the finite adelic special-orthogonal class set with the quotient by the conjugate of its right compact-open subgroup.

                  Instances For
                    source
                    theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetConj_apply_mk {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (g x : U.finiteAdelicSpecialOrthogonal) :
                    (U.finiteAdelicSpecialOrthogonalDoubleCosetConj g) (DoubleCoset.mk U.finiteAdelicSpecialOrthogonalDiagonal.range (integralSubgroup U.specialOrthogonal) x) = DoubleCoset.mk U.finiteAdelicSpecialOrthogonalDiagonal.range (Subgroup.map (โ†‘(MulEquiv.symm (MulAut.conj g))) (integralSubgroup U.specialOrthogonal)) (x * g)

                    Special-orthogonal right translation sends the class of x to the class of x * g.

                    Not a simp lemma: the codomain contains a coerced mapped subgroup, which simp rewrites to a set image in the dependent type.

                    source
                    theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetConj_symm_apply_mk {V : Type u_1} [AddCommGroup V] [Module โ„š V] {Q : QuadraticForm โ„š V} (U : OrthogonalCompactOpens Q) [FiniteDimensional โ„š V] (g y : U.finiteAdelicSpecialOrthogonal) :
                    (U.finiteAdelicSpecialOrthogonalDoubleCosetConj g).symm (DoubleCoset.mk U.finiteAdelicSpecialOrthogonalDiagonal.range (Subgroup.map (โ†‘(MulEquiv.symm (MulAut.conj g))) (integralSubgroup U.specialOrthogonal)) y) = DoubleCoset.mk U.finiteAdelicSpecialOrthogonalDiagonal.range (integralSubgroup U.specialOrthogonal) (y * gโปยน)

                    The inverse special-orthogonal right translation sends the class of y to the class of y * gโปยน.

                    Not a simp lemma, for the same dependent-type reason as finiteAdelicSpecialOrthogonalDoubleCosetConj_apply_mk.

                    Change of quadratic space and compatible tuple #

                    source
                    noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetCongr {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') (ฯ† : (p : Nat.Primes) โ†’ โ†ฅ(orthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q)) โ‰ƒ* โ†ฅ(orthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q'))) (hฯ† : โˆ€ (p : Nat.Primes), Set.BijOn โ‡‘(ฯ† p) โ†‘(U.orthogonal p) โ†‘(U'.orthogonal p)) (hdiag : Subgroup.map (โ†‘(restrictedProductCongrRight U.orthogonal U'.orthogonal ฯ† โ‹ฏ)) U.finiteAdelicOrthogonalDiagonal.range = U'.finiteAdelicOrthogonalDiagonal.range) :
                    U.finiteAdelicOrthogonalDoubleCoset โ‰ƒ U'.finiteAdelicOrthogonalDoubleCoset

                    Componentwise equivalences which preserve every orthogonal reference subgroup and carry the rational diagonal subgroup onto the target diagonal subgroup identify the finite adelic class sets.

                    Instances For
                      source
                      @[simp]
                      theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetCongr_apply_mk {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') (ฯ† : (p : Nat.Primes) โ†’ โ†ฅ(orthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q)) โ‰ƒ* โ†ฅ(orthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q'))) (hฯ† : โˆ€ (p : Nat.Primes), Set.BijOn โ‡‘(ฯ† p) โ†‘(U.orthogonal p) โ†‘(U'.orthogonal p)) (hdiag : Subgroup.map (โ†‘(restrictedProductCongrRight U.orthogonal U'.orthogonal ฯ† โ‹ฏ)) U.finiteAdelicOrthogonalDiagonal.range = U'.finiteAdelicOrthogonalDiagonal.range) (x : U.finiteAdelicOrthogonal) :
                      (U.finiteAdelicOrthogonalDoubleCosetCongr U' ฯ† hฯ† hdiag) (DoubleCoset.mk U.finiteAdelicOrthogonalDiagonal.range (integralSubgroup U.orthogonal) x) = DoubleCoset.mk U'.finiteAdelicOrthogonalDiagonal.range (integralSubgroup U'.orthogonal) ((restrictedProductCongrRight U.orthogonal U'.orthogonal ฯ† โ‹ฏ) x)

                      Change of orthogonal tuple applies the componentwise equivalence to representatives.

                      source
                      @[simp]
                      theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetCongr_symm_apply_mk {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') (ฯ† : (p : Nat.Primes) โ†’ โ†ฅ(orthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q)) โ‰ƒ* โ†ฅ(orthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q'))) (hฯ† : โˆ€ (p : Nat.Primes), Set.BijOn โ‡‘(ฯ† p) โ†‘(U.orthogonal p) โ†‘(U'.orthogonal p)) (hdiag : Subgroup.map (โ†‘(restrictedProductCongrRight U.orthogonal U'.orthogonal ฯ† โ‹ฏ)) U.finiteAdelicOrthogonalDiagonal.range = U'.finiteAdelicOrthogonalDiagonal.range) (y : U'.finiteAdelicOrthogonal) :
                      (U.finiteAdelicOrthogonalDoubleCosetCongr U' ฯ† hฯ† hdiag).symm (DoubleCoset.mk U'.finiteAdelicOrthogonalDiagonal.range (integralSubgroup U'.orthogonal) y) = DoubleCoset.mk U.finiteAdelicOrthogonalDiagonal.range (integralSubgroup U.orthogonal) ((restrictedProductCongrRight U.orthogonal U'.orthogonal ฯ† โ‹ฏ).symm y)

                      The inverse change of orthogonal tuple applies the inverse componentwise equivalence to representatives.

                      source
                      noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetCongr {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') (ฯ† : (p : Nat.Primes) โ†’ โ†ฅ(spinGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q)) โ‰ƒ* โ†ฅ(spinGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q'))) (hฯ† : โˆ€ (p : Nat.Primes), Set.BijOn โ‡‘(ฯ† p) โ†‘(U.spin p) โ†‘(U'.spin p)) (hdiag : Subgroup.map (โ†‘(restrictedProductCongrRight U.spin U'.spin ฯ† โ‹ฏ)) U.finiteAdelicSpinDiagonal.range = U'.finiteAdelicSpinDiagonal.range) :
                      U.finiteAdelicSpinDoubleCoset โ‰ƒ U'.finiteAdelicSpinDoubleCoset

                      Componentwise equivalences which preserve every Spin reference subgroup and carry the rational diagonal subgroup onto the target diagonal subgroup identify the finite adelic class sets.

                      Instances For
                        source
                        @[simp]
                        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetCongr_apply_mk {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') (ฯ† : (p : Nat.Primes) โ†’ โ†ฅ(spinGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q)) โ‰ƒ* โ†ฅ(spinGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q'))) (hฯ† : โˆ€ (p : Nat.Primes), Set.BijOn โ‡‘(ฯ† p) โ†‘(U.spin p) โ†‘(U'.spin p)) (hdiag : Subgroup.map (โ†‘(restrictedProductCongrRight U.spin U'.spin ฯ† โ‹ฏ)) U.finiteAdelicSpinDiagonal.range = U'.finiteAdelicSpinDiagonal.range) (x : U.finiteAdelicSpin) :
                        (U.finiteAdelicSpinDoubleCosetCongr U' ฯ† hฯ† hdiag) (DoubleCoset.mk U.finiteAdelicSpinDiagonal.range (integralSubgroup U.spin) x) = DoubleCoset.mk U'.finiteAdelicSpinDiagonal.range (integralSubgroup U'.spin) ((restrictedProductCongrRight U.spin U'.spin ฯ† โ‹ฏ) x)

                        Change of Spin tuple applies the componentwise equivalence to representatives.

                        source
                        @[simp]
                        theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetCongr_symm_apply_mk {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') (ฯ† : (p : Nat.Primes) โ†’ โ†ฅ(spinGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q)) โ‰ƒ* โ†ฅ(spinGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q'))) (hฯ† : โˆ€ (p : Nat.Primes), Set.BijOn โ‡‘(ฯ† p) โ†‘(U.spin p) โ†‘(U'.spin p)) (hdiag : Subgroup.map (โ†‘(restrictedProductCongrRight U.spin U'.spin ฯ† โ‹ฏ)) U.finiteAdelicSpinDiagonal.range = U'.finiteAdelicSpinDiagonal.range) (y : U'.finiteAdelicSpin) :
                        (U.finiteAdelicSpinDoubleCosetCongr U' ฯ† hฯ† hdiag).symm (DoubleCoset.mk U'.finiteAdelicSpinDiagonal.range (integralSubgroup U'.spin) y) = DoubleCoset.mk U.finiteAdelicSpinDiagonal.range (integralSubgroup U.spin) ((restrictedProductCongrRight U.spin U'.spin ฯ† โ‹ฏ).symm y)

                        The inverse change of Spin tuple applies the inverse componentwise equivalence to representatives.

                        source
                        noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetCongr {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} [FiniteDimensional โ„š V] [FiniteDimensional โ„š W] (U' : OrthogonalCompactOpens Q') (ฯ† : (p : Nat.Primes) โ†’ โ†ฅ(specialOrthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q)) โ‰ƒ* โ†ฅ(specialOrthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q'))) (hฯ† : โˆ€ (p : Nat.Primes), Set.BijOn โ‡‘(ฯ† p) โ†‘(U.specialOrthogonal p) โ†‘(U'.specialOrthogonal p)) (hdiag : Subgroup.map (โ†‘(restrictedProductCongrRight U.specialOrthogonal U'.specialOrthogonal ฯ† โ‹ฏ)) U.finiteAdelicSpecialOrthogonalDiagonal.range = U'.finiteAdelicSpecialOrthogonalDiagonal.range) :
                        U.finiteAdelicSpecialOrthogonalDoubleCoset โ‰ƒ U'.finiteAdelicSpecialOrthogonalDoubleCoset

                        Componentwise equivalences which preserve every special-orthogonal reference subgroup and carry the rational diagonal subgroup onto the target diagonal subgroup identify the finite adelic class sets.

                        Instances For
                          source
                          @[simp]
                          theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetCongr_apply_mk {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} [FiniteDimensional โ„š V] [FiniteDimensional โ„š W] (U' : OrthogonalCompactOpens Q') (ฯ† : (p : Nat.Primes) โ†’ โ†ฅ(specialOrthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q)) โ‰ƒ* โ†ฅ(specialOrthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q'))) (hฯ† : โˆ€ (p : Nat.Primes), Set.BijOn โ‡‘(ฯ† p) โ†‘(U.specialOrthogonal p) โ†‘(U'.specialOrthogonal p)) (hdiag : Subgroup.map (โ†‘(restrictedProductCongrRight U.specialOrthogonal U'.specialOrthogonal ฯ† โ‹ฏ)) U.finiteAdelicSpecialOrthogonalDiagonal.range = U'.finiteAdelicSpecialOrthogonalDiagonal.range) (x : U.finiteAdelicSpecialOrthogonal) :
                          (U.finiteAdelicSpecialOrthogonalDoubleCosetCongr U' ฯ† hฯ† hdiag) (DoubleCoset.mk U.finiteAdelicSpecialOrthogonalDiagonal.range (integralSubgroup U.specialOrthogonal) x) = DoubleCoset.mk U'.finiteAdelicSpecialOrthogonalDiagonal.range (integralSubgroup U'.specialOrthogonal) ((restrictedProductCongrRight U.specialOrthogonal U'.specialOrthogonal ฯ† โ‹ฏ) x)

                          Change of special-orthogonal tuple applies the componentwise equivalence to representatives.

                          source
                          @[simp]
                          theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetCongr_symm_apply_mk {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} [FiniteDimensional โ„š V] [FiniteDimensional โ„š W] (U' : OrthogonalCompactOpens Q') (ฯ† : (p : Nat.Primes) โ†’ โ†ฅ(specialOrthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q)) โ‰ƒ* โ†ฅ(specialOrthogonalGroup (QuadraticForm.baseChange โ„š_[โ†‘p] Q'))) (hฯ† : โˆ€ (p : Nat.Primes), Set.BijOn โ‡‘(ฯ† p) โ†‘(U.specialOrthogonal p) โ†‘(U'.specialOrthogonal p)) (hdiag : Subgroup.map (โ†‘(restrictedProductCongrRight U.specialOrthogonal U'.specialOrthogonal ฯ† โ‹ฏ)) U.finiteAdelicSpecialOrthogonalDiagonal.range = U'.finiteAdelicSpecialOrthogonalDiagonal.range) (y : U'.finiteAdelicSpecialOrthogonal) :
                          (U.finiteAdelicSpecialOrthogonalDoubleCosetCongr U' ฯ† hฯ† hdiag).symm (DoubleCoset.mk U'.finiteAdelicSpecialOrthogonalDiagonal.range (integralSubgroup U'.specialOrthogonal) y) = DoubleCoset.mk U.finiteAdelicSpecialOrthogonalDiagonal.range (integralSubgroup U.specialOrthogonal) ((restrictedProductCongrRight U.specialOrthogonal U'.specialOrthogonal ฯ† โ‹ฏ).symm y)

                          The inverse change of special-orthogonal tuple applies the inverse componentwise equivalence to representatives.