Integral orthogonal subgroups in a basis

For a basis of a quadratic space over ℚ_[p], the integral orthogonal subgroup consists of isometries whose matrices and inverse matrices have entries in ℤ_[p]. Both conditions are included, so the construction is a subgroup even for a degenerate quadratic form. This is the reference family used to form restricted products of local orthogonal groups.

The subgroup is compact and open in the canonical forward-and-inverse topology on linear isometries. For a rational quadratic space and a rational basis, every rational isometry belongs to these subgroups at all but finitely many primes. No integrality of the quadratic form itself is required: the exceptional primes come from the denominators of the isometry and its inverse. The subgroup depends only on the ℤ_[p]-span of the basis, so two rational bases give the same local subgroups at all but finitely many primes.

noncomputable def TauCeti.QuadraticMap.integralOrthogonalSubgroup {p : ℕ} [Fact (Nat.Prime p)] {V : Type u_1} {ι : Type u_2} [AddCommGroup V] [Module ℚ_[p] V] [Fintype ι] [DecidableEq ι] (Q : QuadraticForm ℚ_[p] V) (b : Module.Basis ι ℚ_[p] V) : Subgroup ↥(orthogonalGroup Q)

The subgroup of isometries integral in b in both directions. Equivalently, these isometries preserve the ℤ_[p]-span of the basis as a set.

@[simp]

theorem TauCeti.QuadraticMap.mem_integralOrthogonalSubgroup_iff {p : ℕ} [Fact (Nat.Prime p)] {V : Type u_1} {ι : Type u_2} [AddCommGroup V] [Module ℚ_[p] V] [Fintype ι] [DecidableEq ι] (Q : QuadraticForm ℚ_[p] V) (b : Module.Basis ι ℚ_[p] V) (g : ↥(orthogonalGroup Q)) : g ∈ integralOrthogonalSubgroup Q b ↔ (∀ (i j : ι), (LinearMap.toMatrix b b) (↑↑g) i j ∈ PadicInt.subring p) ∧ ∀ (i j : ι), (LinearMap.toMatrix b b) (↑(↑g)⁻¹) i j ∈ PadicInt.subring p

Membership is integrality of the matrix entries of both the isometry and its inverse.

theorem TauCeti.QuadraticMap.mem_integralOrthogonalSubgroup_iff_norm {p : ℕ} [Fact (Nat.Prime p)] {V : Type u_1} {ι : Type u_2} [AddCommGroup V] [Module ℚ_[p] V] [Fintype ι] [DecidableEq ι] (Q : QuadraticForm ℚ_[p] V) (b : Module.Basis ι ℚ_[p] V) (g : ↥(orthogonalGroup Q)) : g ∈ integralOrthogonalSubgroup Q b ↔ (∀ (i j : ι), ‖(LinearMap.toMatrix b b) (↑↑g) i j‖ ≤ 1) ∧ ∀ (i j : ι), ‖(LinearMap.toMatrix b b) (↑(↑g)⁻¹) i j‖ ≤ 1

The same membership test written as bounds on the p-adic norms of the entries.

theorem TauCeti.QuadraticMap.mem_integralOrthogonalSubgroup_iff_mem_span {p : ℕ} [Fact (Nat.Prime p)] {V : Type u_1} {ι : Type u_2} [AddCommGroup V] [Module ℚ_[p] V] [Fintype ι] [DecidableEq ι] (Q : QuadraticForm ℚ_[p] V) (b : Module.Basis ι ℚ_[p] V) (g : ↥(orthogonalGroup Q)) : g ∈ integralOrthogonalSubgroup Q b ↔ (∀ x ∈ Submodule.span (↥(PadicInt.subring p)) (Set.range ⇑b), ↑g x ∈ Submodule.span (↥(PadicInt.subring p)) (Set.range ⇑b)) ∧ ∀ x ∈ Submodule.span (↥(PadicInt.subring p)) (Set.range ⇑b), ↑g⁻¹ x ∈ Submodule.span (↥(PadicInt.subring p)) (Set.range ⇑b)

Membership means that the isometry and its inverse preserve the ℤ_[p]-span of the basis.

theorem TauCeti.QuadraticMap.integralOrthogonalSubgroup_eq_of_span_eq {p : ℕ} [Fact (Nat.Prime p)] {V : Type u_1} {ι : Type u_2} [AddCommGroup V] [Module ℚ_[p] V] [Fintype ι] [DecidableEq ι] (Q : QuadraticForm ℚ_[p] V) (b : Module.Basis ι ℚ_[p] V) {ι' : Type u_3} [Fintype ι'] [DecidableEq ι'] {b' : Module.Basis ι' ℚ_[p] V} (h : Submodule.span (↥(PadicInt.subring p)) (Set.range ⇑b) = Submodule.span (↥(PadicInt.subring p)) (Set.range ⇑b')) : integralOrthogonalSubgroup Q b = integralOrthogonalSubgroup Q b'

Bases with the same ℤ_[p]-span have the same integral orthogonal subgroup.

theorem TauCeti.QuadraticMap.mem_integralOrthogonalSubgroup_orthogonalGroupCongr {p : ℕ} [Fact (Nat.Prime p)] {V : Type u_1} {ι : Type u_2} [AddCommGroup V] [Module ℚ_[p] V] [Fintype ι] [DecidableEq ι] (Q : QuadraticForm ℚ_[p] V) (b : Module.Basis ι ℚ_[p] V) {W : Type u_3} [AddCommGroup W] [Module ℚ_[p] W] {Q' : QuadraticForm ℚ_[p] W} (e : QuadraticMap.IsometryEquiv Q Q') (g : ↥(orthogonalGroup Q)) : e.orthogonalGroupCongr g ∈ integralOrthogonalSubgroup Q' (b.map e.toLinearEquiv) ↔ g ∈ integralOrthogonalSubgroup Q b

Transporting the basis along an isometry transports the integral orthogonal subgroup.

theorem TauCeti.QuadraticMap.isOpen_integralOrthogonalSubgroup {p : ℕ} [Fact (Nat.Prime p)] {V : Type u_1} {ι : Type u_2} [AddCommGroup V] [Module ℚ_[p] V] [Fintype ι] [DecidableEq ι] (Q : QuadraticForm ℚ_[p] V) (b : Module.Basis ι ℚ_[p] V) : IsOpen ↑(integralOrthogonalSubgroup Q b)

The integral orthogonal subgroup is open in the canonical topology on isometries.

theorem TauCeti.QuadraticMap.isCompact_integralOrthogonalSubgroup {p : ℕ} [Fact (Nat.Prime p)] {V : Type u_1} {ι : Type u_2} [AddCommGroup V] [Module ℚ_[p] V] [Fintype ι] [DecidableEq ι] (Q : QuadraticForm ℚ_[p] V) (b : Module.Basis ι ℚ_[p] V) : IsCompact ↑(integralOrthogonalSubgroup Q b)

The integral orthogonal subgroup is compact, including for degenerate forms.

theorem TauCeti.QuadraticMap.mem_integralOrthogonalSubgroup_baseChange_of_not_dvd_den {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {W : Type u_3} [AddCommGroup W] [Module ℚ W] (Q₀ : QuadraticForm ℚ W) (b₀ : Module.Basis ι ℚ W) (g : ↥(orthogonalGroup Q₀)) (hg : ∀ (i j : ι), ¬p ∣ ((LinearMap.toMatrix b₀ b₀) (↑↑g) i j).den) (hginv : ∀ (i j : ι), ¬p ∣ ((LinearMap.toMatrix b₀ b₀) (↑(↑g)⁻¹) i j).den) : (orthogonalGroupBaseChange Q₀) g ∈ integralOrthogonalSubgroup (QuadraticForm.baseChange ℚ_[p] Q₀) (Module.Basis.baseChange ℚ_[p] b₀)

Avoiding the denominators of the entries of an isometry and its inverse ensures local integrality. This gives an explicit finite exceptional set.

theorem TauCeti.QuadraticMap.eventually_mem_integralOrthogonalSubgroup {ι : Type u_2} [Fintype ι] [DecidableEq ι] {W : Type u_3} [AddCommGroup W] [Module ℚ W] (Q₀ : QuadraticForm ℚ W) (b₀ : Module.Basis ι ℚ W) (g : ↥(orthogonalGroup Q₀)) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, have x := ⋯; (orthogonalGroupBaseChange Q₀) g ∈ integralOrthogonalSubgroup (QuadraticForm.baseChange ℚ_[↑p] Q₀) (Module.Basis.baseChange ℚ_[↑p] b₀)

Every rational isometry is integral in a fixed rational basis at almost every prime, in both directions. Thus its local scalar extensions define a point of the restricted product relative to the integral orthogonal subgroups.

theorem TauCeti.QuadraticMap.eventually_integralOrthogonalSubgroup_baseChange_eq {ι : Type u_2} [Fintype ι] [DecidableEq ι] {W : Type u_3} [AddCommGroup W] [Module ℚ W] (Q₀ : QuadraticForm ℚ W) (b₀ : Module.Basis ι ℚ W) {ι' : Type u_4} [Fintype ι'] [DecidableEq ι'] (b₀' : Module.Basis ι' ℚ W) : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, have x := ⋯; integralOrthogonalSubgroup (QuadraticForm.baseChange ℚ_[↑p] Q₀) (Module.Basis.baseChange ℚ_[↑p] b₀) = integralOrthogonalSubgroup (QuadraticForm.baseChange ℚ_[↑p] Q₀) (Module.Basis.baseChange ℚ_[↑p] b₀')

For two rational bases, the integral orthogonal subgroups of their scalar extensions agree at almost every prime: away from finitely many primes the two bases span the same ℤ_[p]-lattice, since the entries of both change-of-basis matrices are p-adic integers.