Compatible compact-open subgroups for orthogonal and Spin groups

A restricted product of the local orthogonal, special orthogonal, and Spin groups needs compatible reference subgroups at every prime. The independent data are a compact-open subgroup of the local orthogonal group and one of the local Spin group. The special orthogonal subgroup is derived by intersecting the orthogonal subgroup with SO, and compatibility asks that the local Spin projection land in this intersection.

This file packages the independent families, their compactness and openness, the almost-everywhere integrality of rational points, and the compatibility condition. It derives the special orthogonal family, its membership criterion, its openness and compactness, the restricted Spin projection, and almost-everywhere integrality for rational special orthogonal points. In particular, no separately chosen special orthogonal family can drift away from the orthogonal family.

New tuples are obtained from old ones by shrinking: intersecting the orthogonal reference subgroups with open subgroups W p that contain them at almost every prime, and the Spin ones with the preimages of the W p, gives a compatible tuple agreeing with the original at almost every prime. This is how tuples differing at finitely many primes, such as level structures at a single prime, arise.

Tuples are also functorial in the quadratic space: a rational isometry e : Q ≃ Q' carries a tuple for Q to one for Q' by applying the local isometries e ⊗ ℚ_p at every prime. The local isometries are homeomorphisms of the local point groups, so compactness and openness are preserved, and they carry the derived special orthogonal family of one tuple to that of the other. At every prime they restrict to bijections of all three reference subgroups, which is the hypothesis under which a rational isometry identifies the finite adelic groups and class sets of the two tuples.

The topology on every group is the canonical one inherited from the ambient finite-dimensional algebra; the package stores no topology of its own.

Main definitions

• TauCeti.QuadraticMap.OrthogonalCompactOpens: compatible orthogonal and Spin compact-open reference families for a rational quadratic space.
• TauCeti.QuadraticMap.OrthogonalCompactOpens.specialOrthogonal: the derived local special orthogonal family.
• TauCeti.QuadraticMap.OrthogonalCompactOpens.spinToSpecialOrthogonal: the local Spin projection restricted to the reference subgroups.
• TauCeti.QuadraticMap.OrthogonalCompactOpens.infOpenSubgroup: the shrinking of a tuple by a family of open subgroups of the local orthogonal groups.
• TauCeti.QuadraticMap.OrthogonalCompactOpens.map: the transport of a tuple along a rational isometry.

Main results

• TauCeti.QuadraticMap.OrthogonalCompactOpens.map_specialOrthogonal: transport carries the derived special orthogonal family along.
• TauCeti.QuadraticMap.OrthogonalCompactOpens.bijOn_map_orthogonal, and its Spin and special orthogonal versions: the local isometries match the reference subgroups of a tuple with those of its transport at every prime.
• TauCeti.QuadraticMap.OrthogonalCompactOpens.map_refl and TauCeti.QuadraticMap.OrthogonalCompactOpens.map_trans: transport is functorial.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1963), §101.

structure TauCeti.QuadraticMap.OrthogonalCompactOpens {V : Type u_1} [AddCommGroup V] [Module ℚ V] (Q : QuadraticForm ℚ V) : Type u_1

Compatible compact-open reference subgroups for the local orthogonal and Spin groups of a rational quadratic space.

The special orthogonal reference subgroup is deliberately not a field: it is recovered as the preimage of orthogonal p under SO(Q_p) → O(Q_p). The compatibility field is phrased using the Spin-to-special-orthogonal projection, so it supplies the restricted map needed by adelic special orthogonal points rather than merely a map into the full orthogonal group.

• orthogonal (p : Nat.Primes) : Subgroup ↥(orthogonalGroup (QuadraticForm.baseChange ℚ_[↑p] Q))

  The compact-open reference subgroup of the local orthogonal group.

• spin (p : Nat.Primes) : Subgroup ↥(spinGroup (QuadraticForm.baseChange ℚ_[↑p] Q))

  The compact-open reference subgroup of the local Spin group.

• isOpen_orthogonal (p : Nat.Primes) : IsOpen ↑(self.orthogonal p)

  The local orthogonal reference subgroup is open.

• isCompact_orthogonal (p : Nat.Primes) : IsCompact ↑(self.orthogonal p)

  The local orthogonal reference subgroup is compact.

• isOpen_spin (p : Nat.Primes) : IsOpen ↑(self.spin p)

  The local Spin reference subgroup is open.

• isCompact_spin (p : Nat.Primes) : IsCompact ↑(self.spin p)

  The local Spin reference subgroup is compact.

• spin_maps (p : Nat.Primes) : Set.MapsTo ⇑(CliffordAlgebra.spinToSpecialOrthogonal (QuadraticForm.baseChange ℚ_[↑p] Q)) ↑(self.spin p) ↑(Subgroup.comap (QuadraticMap.specialOrthogonalToOrthogonal (QuadraticForm.baseChange ℚ_[↑p] Q)) (self.orthogonal p))

  Local Spin reference points map into the special orthogonal subgroup cut out by the orthogonal reference subgroup.

• eventually_orthogonal (g : ↥(orthogonalGroup Q)) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, (orthogonalGroupBaseChange Q) g ∈ self.orthogonal p

  Every rational orthogonal point belongs to the reference subgroup at almost every prime.

• eventually_spin (x : ↥(spinGroup Q)) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, (CliffordAlgebra.spinGroupBaseChange Q) x ∈ self.spin p

  Every rational Spin point belongs to the reference subgroup at almost every prime.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.ext_iff {V : Type u_1} {inst✝ : AddCommGroup V} {inst✝¹ : Module ℚ V} {Q : QuadraticForm ℚ V} {x y : OrthogonalCompactOpens Q} : x = y ↔ x.orthogonal = y.orthogonal ∧ x.spin = y.spin

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.ext {V : Type u_1} {inst✝ : AddCommGroup V} {inst✝¹ : Module ℚ V} {Q : QuadraticForm ℚ V} {x y : OrthogonalCompactOpens Q} (orthogonal : x.orthogonal = y.orthogonal) (spin : x.spin = y.spin) : x = y

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.specialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (p : Nat.Primes) : Subgroup ↥(specialOrthogonalGroup (QuadraticForm.baseChange ℚ_[↑p] Q))

The special orthogonal reference subgroup derived from the orthogonal one.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_specialOrthogonal_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (p : Nat.Primes) (g : ↥(specialOrthogonalGroup (QuadraticForm.baseChange ℚ_[↑p] Q))) : g ∈ U.specialOrthogonal p ↔ (QuadraticMap.specialOrthogonalToOrthogonal (QuadraticForm.baseChange ℚ_[↑p] Q)) g ∈ U.orthogonal p

A local special orthogonal point belongs to the derived reference subgroup exactly when its image in the orthogonal group belongs to the orthogonal reference subgroup.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.isOpen_specialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (p : Nat.Primes) : IsOpen ↑(U.specialOrthogonal p)

The derived special orthogonal reference subgroup is open, being the preimage of an open subgroup under the continuous inclusion SO(Q_p) → O(Q_p).

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.isCompact_specialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (p : Nat.Primes) : IsCompact ↑(U.specialOrthogonal p)

The derived special orthogonal reference subgroup is compact, being the preimage of a compact subgroup under the closed embedding SO(Q_p) → O(Q_p).

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.mapsTo_specialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (p : Nat.Primes) : Set.MapsTo ⇑(CliffordAlgebra.spinToSpecialOrthogonal (QuadraticForm.baseChange ℚ_[↑p] Q)) ↑(U.spin p) ↑(U.specialOrthogonal p)

The local Spin projection carries the Spin reference subgroup into the derived special orthogonal reference subgroup.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.spinToSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (p : Nat.Primes) : ↥(U.spin p) →* ↥(U.specialOrthogonal p)

The Spin-to-special-orthogonal projection restricted to the compatible local reference subgroups.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.coe_spinToSpecialOrthogonal_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (p : Nat.Primes) (x : ↥(U.spin p)) : ↑((U.spinToSpecialOrthogonal p) x) = (CliffordAlgebra.spinToSpecialOrthogonal (QuadraticForm.baseChange ℚ_[↑p] Q)) ↑x

The restricted local Spin projection has the same value as the ambient projection.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.eventually_specialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] (g : ↥(specialOrthogonalGroup Q)) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, (specialOrthogonalGroupBaseChange Q) g ∈ U.specialOrthogonal p

Every rational special orthogonal point belongs to the derived reference subgroup at almost every prime. This is a consequence of orthogonal integrality, not additional data.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.spinToOrthogonal_mem_orthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (p : Nat.Primes) {x : ↥(spinGroup (QuadraticForm.baseChange ℚ_[↑p] Q))} (hx : x ∈ U.spin p) : (CliffordAlgebra.spinToOrthogonal (QuadraticForm.baseChange ℚ_[↑p] Q)) x ∈ U.orthogonal p

A Spin reference point acts through an orthogonal reference point.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.specialOrthogonal_mono {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} {U U' : OrthogonalCompactOpens Q} (h : ∀ (p : Nat.Primes), U.orthogonal p ≤ U'.orthogonal p) (p : Nat.Primes) : U.specialOrthogonal p ≤ U'.specialOrthogonal p

Shrinking the orthogonal reference subgroups shrinks the derived special orthogonal ones.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.eventually_specialOrthogonal_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} {U U' : OrthogonalCompactOpens Q} (h : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.orthogonal p = U'.orthogonal p) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.specialOrthogonal p = U'.specialOrthogonal p

Orthogonal reference families agreeing at almost every prime have derived special orthogonal families agreeing at almost every prime.

Shrinking a compatible tuple at finitely many primes

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.infOpenSubgroup {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] (W : (p : Nat.Primes) → OpenSubgroup ↥(orthogonalGroup (QuadraticForm.baseChange ℚ_[↑p] Q))) (hW : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.orthogonal p ≤ ↑(W p)) : OrthogonalCompactOpens Q

Intersect the orthogonal reference subgroups of U with open subgroups W p of the local orthogonal groups, and the Spin reference subgroups with the preimages of the W p. When U.orthogonal p ≤ W p at almost every prime, as for a family W that is ⊤ away from finitely many primes, the result is again a compatible compact-open tuple. It agrees with U at almost every prime and is contained in U at every prime.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.infOpenSubgroup_orthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] (W : (p : Nat.Primes) → OpenSubgroup ↥(orthogonalGroup (QuadraticForm.baseChange ℚ_[↑p] Q))) (hW : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.orthogonal p ≤ ↑(W p)) (p : Nat.Primes) : (U.infOpenSubgroup W hW).orthogonal p = U.orthogonal p ⊓ ↑(W p)

The orthogonal reference subgroups of the shrunken tuple are the intersections with W.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.infOpenSubgroup_spin {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] (W : (p : Nat.Primes) → OpenSubgroup ↥(orthogonalGroup (QuadraticForm.baseChange ℚ_[↑p] Q))) (hW : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.orthogonal p ≤ ↑(W p)) (p : Nat.Primes) : (U.infOpenSubgroup W hW).spin p = U.spin p ⊓ Subgroup.comap (CliffordAlgebra.spinToOrthogonal (QuadraticForm.baseChange ℚ_[↑p] Q)) ↑(W p)

The Spin reference subgroups of the shrunken tuple are cut out by the preimages of W.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.infOpenSubgroup_orthogonal_le {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] (W : (p : Nat.Primes) → OpenSubgroup ↥(orthogonalGroup (QuadraticForm.baseChange ℚ_[↑p] Q))) (hW : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.orthogonal p ≤ ↑(W p)) (p : Nat.Primes) : (U.infOpenSubgroup W hW).orthogonal p ≤ U.orthogonal p

The shrunken orthogonal reference subgroups are contained in those of U.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.infOpenSubgroup_spin_le {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] (W : (p : Nat.Primes) → OpenSubgroup ↥(orthogonalGroup (QuadraticForm.baseChange ℚ_[↑p] Q))) (hW : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.orthogonal p ≤ ↑(W p)) (p : Nat.Primes) : (U.infOpenSubgroup W hW).spin p ≤ U.spin p

The shrunken Spin reference subgroups are contained in those of U.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.eventually_infOpenSubgroup_orthogonal_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] (W : (p : Nat.Primes) → OpenSubgroup ↥(orthogonalGroup (QuadraticForm.baseChange ℚ_[↑p] Q))) (hW : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.orthogonal p ≤ ↑(W p)) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, (U.infOpenSubgroup W hW).orthogonal p = U.orthogonal p

The shrunken tuple has the orthogonal reference subgroups of U at almost every prime.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.eventually_infOpenSubgroup_spin_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] (W : (p : Nat.Primes) → OpenSubgroup ↥(orthogonalGroup (QuadraticForm.baseChange ℚ_[↑p] Q))) (hW : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.orthogonal p ≤ ↑(W p)) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, (U.infOpenSubgroup W hW).spin p = U.spin p

The shrunken tuple has the Spin reference subgroups of U at almost every prime.

Transport along a rational isometry

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.map {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {V' : Type u_2} [AddCommGroup V'] [Module ℚ V'] {Q' : QuadraticForm ℚ V'} (e : QuadraticMap.IsometryEquiv Q Q') : OrthogonalCompactOpens Q'

Transport a compatible compact-open tuple along a rational isometry e : Q ≃ Q': at every prime the orthogonal and Spin reference subgroups are carried to those of Q' by the local isometry e ⊗ ℚ_p. The derived special orthogonal family is carried along as well (map_specialOrthogonal), so the local isometries restrict to bijections of all three families of reference subgroups (bijOn_map_orthogonal and its Spin and special orthogonal versions).

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.map_orthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {V' : Type u_2} [AddCommGroup V'] [Module ℚ V'] {Q' : QuadraticForm ℚ V'} (e : QuadraticMap.IsometryEquiv Q Q') (p : Nat.Primes) : (U.map e).orthogonal p = Subgroup.map (↑(e.baseChange ℚ_[↑p]).orthogonalGroupCongr) (U.orthogonal p)

The orthogonal reference subgroups of a transported tuple are the images under the local isometries.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.map_spin {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {V' : Type u_2} [AddCommGroup V'] [Module ℚ V'] {Q' : QuadraticForm ℚ V'} (e : QuadraticMap.IsometryEquiv Q Q') (p : Nat.Primes) : (U.map e).spin p = Subgroup.map (↑(e.baseChange ℚ_[↑p]).spinGroupEquiv) (U.spin p)

The Spin reference subgroups of a transported tuple are the images under the local isometries.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.map_specialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {V' : Type u_2} [AddCommGroup V'] [Module ℚ V'] {Q' : QuadraticForm ℚ V'} (e : QuadraticMap.IsometryEquiv Q Q') (p : Nat.Primes) : (U.map e).specialOrthogonal p = Subgroup.map (↑(e.baseChange ℚ_[↑p]).specialOrthogonalGroupCongr) (U.specialOrthogonal p)

The derived special orthogonal reference subgroups of a transported tuple are the images of those of the original tuple under the local isometries.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.bijOn_map_orthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {V' : Type u_2} [AddCommGroup V'] [Module ℚ V'] {Q' : QuadraticForm ℚ V'} (e : QuadraticMap.IsometryEquiv Q Q') (p : Nat.Primes) : Set.BijOn ⇑(e.baseChange ℚ_[↑p]).orthogonalGroupCongr ↑(U.orthogonal p) ↑((U.map e).orthogonal p)

The local isometry e ⊗ ℚ_p restricts to a bijection between the orthogonal reference subgroups of a tuple and of its transport.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.bijOn_map_spin {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {V' : Type u_2} [AddCommGroup V'] [Module ℚ V'] {Q' : QuadraticForm ℚ V'} (e : QuadraticMap.IsometryEquiv Q Q') (p : Nat.Primes) : Set.BijOn ⇑(e.baseChange ℚ_[↑p]).spinGroupEquiv ↑(U.spin p) ↑((U.map e).spin p)

The local Spin equivalence induced by e ⊗ ℚ_p restricts to a bijection between the Spin reference subgroups of a tuple and of its transport.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.bijOn_map_specialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {V' : Type u_2} [AddCommGroup V'] [Module ℚ V'] {Q' : QuadraticForm ℚ V'} (e : QuadraticMap.IsometryEquiv Q Q') (p : Nat.Primes) : Set.BijOn ⇑(e.baseChange ℚ_[↑p]).specialOrthogonalGroupCongr ↑(U.specialOrthogonal p) ↑((U.map e).specialOrthogonal p)

The local isometry e ⊗ ℚ_p restricts to a bijection between the derived special orthogonal reference subgroups of a tuple and of its transport.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.map_refl {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : U.map (QuadraticMap.IsometryEquiv.refl Q) = U

Transport along the identity isometry is the identity.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.map_trans {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {V' : Type u_2} [AddCommGroup V'] [Module ℚ V'] {Q' : QuadraticForm ℚ V'} (e : QuadraticMap.IsometryEquiv Q Q') {V'' : Type u_3} [AddCommGroup V''] [Module ℚ V''] {Q'' : QuadraticForm ℚ V''} (e' : QuadraticMap.IsometryEquiv Q' Q'') : U.map (e.trans e') = (U.map e).map e'

Transport along a composite of isometries is the composite of the transports.