Rational diagonal points in the full adelic orthogonal groups

The rational diagonal in the full adelic point group retains both the real scalar extension and the finite adelic diagonal. This file constructs those embeddings for O, SO, and Spin, with their coordinate formulas, injectivity, and compatibility with Spin → SO → O.

The finite projection recovers the existing finite diagonal. In particular, adding the real place does not change the finite-place integrality conditions. No nondegeneracy or nonzero rank assumption is needed. These are the embeddings whose images are studied when discussing discreteness of rational points in the full adeles; no discreteness in the finite adeles is asserted here.

The construction uses MonoidHom.prod and the finite diagonals assembled by TauCeti.rationalDiagonal.

References

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

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

The rational diagonal in full adelic O, extending scalars at the real place and at all finite places.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicOrthogonalDiagonal_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (g : ↥(orthogonalGroup Q)) : U.fullAdelicOrthogonalDiagonal g = ((orthogonalGroupBaseChange Q) g, U.finiteAdelicOrthogonalDiagonal g)

The real and finite components of the full orthogonal diagonal.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicOrthogonalToFinite_comp_fullAdelicOrthogonalDiagonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : U.fullAdelicOrthogonalToFinite.comp U.fullAdelicOrthogonalDiagonal = U.finiteAdelicOrthogonalDiagonal

Forgetting the real place recovers the finite orthogonal diagonal.

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

The full adelic orthogonal diagonal is injective.

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

The rational diagonal in full adelic Spin, with no integrality condition at the real place.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpinDiagonal_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (x : ↥(spinGroup Q)) : U.fullAdelicSpinDiagonal x = ((CliffordAlgebra.spinGroupBaseChange Q) x, U.finiteAdelicSpinDiagonal x)

The real and finite components of the full Spin diagonal.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpinToFinite_comp_fullAdelicSpinDiagonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) : U.fullAdelicSpinToFinite.comp U.fullAdelicSpinDiagonal = U.finiteAdelicSpinDiagonal

Forgetting the real place recovers the finite Spin diagonal.

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

The full adelic Spin diagonal is injective.

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

The rational diagonal in full adelic SO. The finite-place integrality condition is derived from that for O.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalDiagonal_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] (g : ↥(specialOrthogonalGroup Q)) : U.fullAdelicSpecialOrthogonalDiagonal g = ((specialOrthogonalGroupBaseChange Q) g, U.finiteAdelicSpecialOrthogonalDiagonal g)

The real and finite components of the full special orthogonal diagonal.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalToFinite_comp_fullAdelicSpecialOrthogonalDiagonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] : U.fullAdelicSpecialOrthogonalToFinite.comp U.fullAdelicSpecialOrthogonalDiagonal = U.finiteAdelicSpecialOrthogonalDiagonal

Forgetting the real place recovers the finite special orthogonal diagonal.

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

The full adelic special orthogonal diagonal is injective.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpinToSpecialOrthogonal_comp_fullAdelicSpinDiagonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] : U.fullAdelicSpinToSpecialOrthogonal.comp U.fullAdelicSpinDiagonal = U.fullAdelicSpecialOrthogonalDiagonal.comp (CliffordAlgebra.spinToSpecialOrthogonal Q)

The two routes from rational Spin to full adelic SO, through the rational projection or through the full adelic projection, agree.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalToOrthogonal_comp_fullAdelicSpecialOrthogonalDiagonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) [FiniteDimensional ℚ V] : U.fullAdelicSpecialOrthogonalToOrthogonal.comp U.fullAdelicSpecialOrthogonalDiagonal = U.fullAdelicOrthogonalDiagonal.comp (QuadraticMap.specialOrthogonalToOrthogonal Q)

The full adelic inclusion SO → O commutes with the rational diagonals.