Full adelic orthogonal, special orthogonal, and Spin groups

For a rational quadratic space and compatible compact-open reference subgroups, the full adelic point group is the product of its real point group with its finite adelic point group. The real factor has no integrality condition. The product topology uses the canonical local group topologies and the restricted-product topology at the finite places.

The real factor is retained for the study of rational diagonal points in the full adeles.

This file constructs all three full adelic groups and the continuous maps Spin → SO → O. Their projections to finite adeles commute with these maps. Membership in the image of SO → O is characterized by properness at every place; for a nondegenerate form on a finite-dimensional space, the kernel of Spin → SO is characterized by scalar ±1 at every place. On a nonzero space the signs are independent; on the zero space the Spin group is trivial.

Local isometries Q ⊗ ℝ ≃ Q' ⊗ ℝ and Q ⊗ ℚ_p ≃ Q' ⊗ ℚ_p which carry the reference subgroups onto one another at almost every prime give isomorphisms of topological groups between the full adelic groups of Q and Q', compatible with the maps Spin → SO → O. The finite component of each is TauCeti.restrictedProductCongrRight, so forgetting the real place recovers the finite adelic transport.

The real coordinate of a full adelic point x is x.1, and its finite coordinates are x.2 p. The product and restricted-product extensionality lemmas therefore apply directly. All carriers and maps are defined without nondegeneracy or a positive-dimension hypothesis.

Main definitions

• OrthogonalCompactOpens.fullAdelicOrthogonalCongr, OrthogonalCompactOpens.fullAdelicSpecialOrthogonalCongr, OrthogonalCompactOpens.fullAdelicSpinCongr: transport of full adelic points along local isometries.

Main results

• fullAdelicSpecialOrthogonalCongr_comp_fullAdelicSpinToSpecialOrthogonal and fullAdelicSpecialOrthogonalToOrthogonal_comp_fullAdelicSpecialOrthogonalCongr, in the namespace TauCeti.QuadraticMap.OrthogonalCompactOpens: the transports intertwine the maps Spin → SO → O.
• fullAdelicOrthogonalToFinite_comp_fullAdelicOrthogonalCongr and its special orthogonal and Spin analogues: forgetting the real place turns each full adelic transport into the corresponding finite adelic transport.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1963), §101.
• A. Weil, Adeles and Algebraic Groups (1982), Chapter I.

@[reducible, inline]

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

The full adelic orthogonal group O(V)(𝔸), with its unrestricted real factor.

@[reducible, inline]

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

The full adelic special orthogonal group SO(V)(𝔸), with its unrestricted real factor.

@[reducible, inline]

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

The full adelic Spin group Spin(V)(𝔸), with its unrestricted real factor.

instance TauCeti.QuadraticMap.OrthogonalCompactOpens.instIsTopologicalGroupFullAdelicOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] : IsTopologicalGroup U.fullAdelicOrthogonal

Full adelic orthogonal points form a topological group in the product topology.

instance TauCeti.QuadraticMap.OrthogonalCompactOpens.instIsTopologicalGroupFullAdelicSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] : IsTopologicalGroup U.fullAdelicSpecialOrthogonal

Full adelic special orthogonal points form a topological group in the product topology.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicOrthogonalToFinite {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : U.fullAdelicOrthogonal →* U.finiteAdelicOrthogonal

Forget the real component of a full adelic orthogonal point.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalToFinite {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : U.fullAdelicSpecialOrthogonal →* U.finiteAdelicSpecialOrthogonal

Forget the real component of a full adelic special orthogonal point.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpinToFinite {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : U.fullAdelicSpin →* U.finiteAdelicSpin

Forget the real component of a full adelic Spin point.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicOrthogonalToFinite_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (x : U.fullAdelicOrthogonal) : U.fullAdelicOrthogonalToFinite x = x.2

The finite projection retains the finite component of an orthogonal point.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalToFinite_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (x : U.fullAdelicSpecialOrthogonal) : U.fullAdelicSpecialOrthogonalToFinite x = x.2

The finite projection retains the finite component of a special orthogonal point.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpinToFinite_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (x : U.fullAdelicSpin) : U.fullAdelicSpinToFinite x = x.2

The finite projection retains the finite component of a Spin point.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_fullAdelicOrthogonalToFinite {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : Continuous ⇑U.fullAdelicOrthogonalToFinite

The projection from full to finite adelic orthogonal points is continuous.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_fullAdelicSpecialOrthogonalToFinite {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : Continuous ⇑U.fullAdelicSpecialOrthogonalToFinite

The projection from full to finite adelic special orthogonal points is continuous.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_fullAdelicSpinToFinite {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : Continuous ⇑U.fullAdelicSpinToFinite

The projection from full to finite adelic Spin points is continuous.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpinToSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : U.fullAdelicSpin →* U.fullAdelicSpecialOrthogonal

The full adelic Spin projection, applying the local projection at the real place and the everywhere-preserving finite adelic projection at the finite places.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalToOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : U.fullAdelicSpecialOrthogonal →* U.fullAdelicOrthogonal

The full adelic inclusion of special orthogonal points into orthogonal points.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpinToSpecialOrthogonal_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (x : U.fullAdelicSpin) : U.fullAdelicSpinToSpecialOrthogonal x = ((CliffordAlgebra.spinToSpecialOrthogonal (QuadraticForm.baseChange ℝ Q)) x.1, U.finiteAdelicSpinToSpecialOrthogonal x.2)

The full adelic Spin projection acts on the real and finite components separately.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalToOrthogonal_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (x : U.fullAdelicSpecialOrthogonal) : U.fullAdelicSpecialOrthogonalToOrthogonal x = ((QuadraticMap.specialOrthogonalToOrthogonal (QuadraticForm.baseChange ℝ Q)) x.1, U.finiteAdelicSpecialOrthogonalToOrthogonal x.2)

The full adelic special orthogonal inclusion acts on the real and finite components separately.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_fullAdelicSpinToSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] : Continuous ⇑U.fullAdelicSpinToSpecialOrthogonal

The full adelic Spin projection is continuous in the product topology.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_fullAdelicSpecialOrthogonalToOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : Continuous ⇑U.fullAdelicSpecialOrthogonalToOrthogonal

The full adelic inclusion of special orthogonal points is continuous.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalToFinite_comp_fullAdelicSpinToSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : U.fullAdelicSpecialOrthogonalToFinite.comp U.fullAdelicSpinToSpecialOrthogonal = U.finiteAdelicSpinToSpecialOrthogonal.comp U.fullAdelicSpinToFinite

Forgetting the real component commutes with the adelic Spin projection.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicOrthogonalToFinite_comp_fullAdelicSpecialOrthogonalToOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : U.fullAdelicOrthogonalToFinite.comp U.fullAdelicSpecialOrthogonalToOrthogonal = U.finiteAdelicSpecialOrthogonalToOrthogonal.comp U.fullAdelicSpecialOrthogonalToFinite

Forgetting the real component commutes with the adelic special orthogonal inclusion.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalToOrthogonal_injective {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : Function.Injective ⇑U.fullAdelicSpecialOrthogonalToOrthogonal

The full adelic inclusion SO → O is injective.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_range_fullAdelicSpecialOrthogonalToOrthogonal_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (x : U.fullAdelicOrthogonal) : x ∈ U.fullAdelicSpecialOrthogonalToOrthogonal.range ↔ x.1 ∈ QuadraticMap.specialOrthogonalWithin (QuadraticForm.baseChange ℝ Q) ∧ ∀ (p : Nat.Primes), x.2 p ∈ QuadraticMap.specialOrthogonalWithin (QuadraticForm.baseChange ℚ_[↑p] Q)

A full adelic isometry comes from adelic SO exactly when it is proper at the real place and at every finite place.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_ker_fullAdelicSpinToSpecialOrthogonal_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] (hQ : QuadraticMap.Nondegenerate) (x : U.fullAdelicSpin) : x ∈ U.fullAdelicSpinToSpecialOrthogonal.ker ↔ (↑x.1 = 1 ∨ ↑x.1 = -1) ∧ ∀ (p : Nat.Primes), ↑(x.2 p) = 1 ∨ ↑(x.2 p) = -1

For a nondegenerate form, a full adelic Spin element lies in the kernel exactly when each component is 1 or -1 in its local Clifford algebra.

Transport along local isometries

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicOrthogonalCongr {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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.fullAdelicOrthogonal ≃ₜ* U'.fullAdelicOrthogonal

The isomorphism of full adelic orthogonal groups induced by a real isometry and by local isometries at the primes which carry the orthogonal reference subgroups onto one another at almost every prime.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicOrthogonalCongr_apply {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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)) (x : U.fullAdelicOrthogonal) : (U.fullAdelicOrthogonalCongr U' eR e he) x = (eR.orthogonalGroupCongr x.1, (restrictedProductCongrRight U.orthogonal U'.orthogonal (fun (p : Nat.Primes) => (e p).orthogonalGroupCongr) he) x.2)

Full adelic orthogonal transport applies the real isometry to the real component and the local isometries to the finite components.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicOrthogonalCongr_symm_apply {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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)) (y : U'.fullAdelicOrthogonal) : (U.fullAdelicOrthogonalCongr U' eR e he).symm y = (eR.orthogonalGroupCongr.symm y.1, (restrictedProductCongrRight U.orthogonal U'.orthogonal (fun (p : Nat.Primes) => (e p).orthogonalGroupCongr) he).symm y.2)

Inverse full adelic orthogonal transport applies the inverse isometries componentwise.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalCongr {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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.fullAdelicSpecialOrthogonal ≃ₜ* U'.fullAdelicSpecialOrthogonal

The isomorphism of full adelic special orthogonal groups induced by a real isometry and by local isometries at the primes which carry the special orthogonal reference subgroups onto one another at almost every prime.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalCongr_apply {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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)) (x : U.fullAdelicSpecialOrthogonal) : (U.fullAdelicSpecialOrthogonalCongr U' eR e hso) x = (eR.specialOrthogonalGroupCongr x.1, (restrictedProductCongrRight U.specialOrthogonal U'.specialOrthogonal (fun (p : Nat.Primes) => (e p).specialOrthogonalGroupCongr) hso) x.2)

Full adelic special orthogonal transport applies the real isometry to the real component and the local isometries to the finite components.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalCongr_symm_apply {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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)) (y : U'.fullAdelicSpecialOrthogonal) : (U.fullAdelicSpecialOrthogonalCongr U' eR e hso).symm y = (eR.specialOrthogonalGroupCongr.symm y.1, (restrictedProductCongrRight U.specialOrthogonal U'.specialOrthogonal (fun (p : Nat.Primes) => (e p).specialOrthogonalGroupCongr) hso).symm y.2)

Inverse full adelic special orthogonal transport applies the inverse isometries componentwise.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpinCongr {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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.fullAdelicSpin ≃ₜ* U'.fullAdelicSpin

The isomorphism of full adelic Spin groups induced by a real isometry and by local isometries at the primes which carry the Spin reference subgroups onto one another at almost every prime.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpinCongr_apply {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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)) (x : U.fullAdelicSpin) : (U.fullAdelicSpinCongr U' eR e hs) x = (eR.spinGroupEquiv x.1, (restrictedProductCongrRight U.spin U'.spin (fun (p : Nat.Primes) => (e p).spinGroupEquiv) hs) x.2)

Full adelic Spin transport applies the real isometry to the real component and the local isometries to the finite components.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpinCongr_symm_apply {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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)) (y : U'.fullAdelicSpin) : (U.fullAdelicSpinCongr U' eR e hs).symm y = (eR.spinGroupEquiv.symm y.1, (restrictedProductCongrRight U.spin U'.spin (fun (p : Nat.Primes) => (e p).spinGroupEquiv) hs).symm y.2)

Inverse full adelic Spin transport applies the inverse isometries componentwise.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalCongr_comp_fullAdelicSpinToSpecialOrthogonal {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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)) : (↑(U.fullAdelicSpecialOrthogonalCongr U' eR e hso)).comp U.fullAdelicSpinToSpecialOrthogonal = U'.fullAdelicSpinToSpecialOrthogonal.comp ↑(U.fullAdelicSpinCongr U' eR e hs)

Full adelic transport intertwines the full adelic Spin projections.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalToOrthogonal_comp_fullAdelicSpecialOrthogonalCongr {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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)) : U'.fullAdelicSpecialOrthogonalToOrthogonal.comp ↑(U.fullAdelicSpecialOrthogonalCongr U' eR e hso) = (↑(U.fullAdelicOrthogonalCongr U' eR e he)).comp U.fullAdelicSpecialOrthogonalToOrthogonal

Full adelic transport intertwines the full adelic inclusions of SO into O.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicOrthogonalToFinite_comp_fullAdelicOrthogonalCongr {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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'.fullAdelicOrthogonalToFinite.comp ↑(U.fullAdelicOrthogonalCongr U' eR e he) = (↑(restrictedProductCongrRight U.orthogonal U'.orthogonal (fun (p : Nat.Primes) => (e p).orthogonalGroupCongr) he)).comp U.fullAdelicOrthogonalToFinite

Forgetting the real component turns full adelic orthogonal transport into finite adelic orthogonal transport.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalToFinite_comp_fullAdelicSpecialOrthogonalCongr {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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'.fullAdelicSpecialOrthogonalToFinite.comp ↑(U.fullAdelicSpecialOrthogonalCongr U' eR e hso) = (↑(restrictedProductCongrRight U.specialOrthogonal U'.specialOrthogonal (fun (p : Nat.Primes) => (e p).specialOrthogonalGroupCongr) hso)).comp U.fullAdelicSpecialOrthogonalToFinite

Forgetting the real component turns full adelic special orthogonal transport into finite adelic special orthogonal transport.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpinToFinite_comp_fullAdelicSpinCongr {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') (eR : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℝ Q) (QuadraticForm.baseChange ℝ 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'.fullAdelicSpinToFinite.comp ↑(U.fullAdelicSpinCongr U' eR e hs) = (↑(restrictedProductCongrRight U.spin U'.spin (fun (p : Nat.Primes) => (e p).spinGroupEquiv) hs)).comp U.fullAdelicSpinToFinite

Forgetting the real component turns full adelic Spin transport into finite adelic Spin transport.