Orthogonal groups of finite quadratic modules

The orthogonal group O(A) of a finite quadratic module consists of its additive automorphisms preserving the quadratic map. This file specializes the general quadratic-map orthogonal group to finite quadratic modules and records its action on the underlying module and its isotropic and Lagrangian subgroups. The imported generic orthogonal-group API transports this group across isometries of finite quadratic modules, and QuadraticMap.orthogonalGroupEquivIsometryEquiv identifies its underlying type with the type Isometry A A of self-isometries of A.

These actions are the group-theoretic interface used when discriminant-form automorphisms act on gluing data and primitive embeddings.

Main definitions

• TauCeti.FiniteQuadraticModule.orthogonalGroup: the group O(A).

Main results

• TauCeti.FiniteQuadraticModule.finite_orthogonalGroup: O(A) is finite.
• TauCeti.FiniteQuadraticModule.isIsotropic_smul_iff and TauCeti.FiniteQuadraticModule.isLagrangian_smul_iff: O(A) preserves the two classes of subgroups used in gluing theory.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1.

@[reducible, inline]

abbrev TauCeti.FiniteQuadraticModule.orthogonalGroup (A : FiniteQuadraticModule) : Subgroup (A.carrier ≃ₗ[ℤ] A.carrier)

The orthogonal group O(A) of a finite quadratic module A.

instance TauCeti.FiniteQuadraticModule.finite_orthogonalGroup (A : FiniteQuadraticModule) : Finite ↥A.orthogonalGroup

The orthogonal group of a finite quadratic module is finite.

@[simp]

theorem TauCeti.FiniteQuadraticModule.quadratic_smul {A : FiniteQuadraticModule} (g : ↥A.orthogonalGroup) (x : A.carrier) : A.quadratic (g • x) = A.quadratic x

The action of O(A) on A preserves the quadratic map.

theorem TauCeti.FiniteQuadraticModule.smul_eq_map_toAddEquiv {A : FiniteQuadraticModule} (g : ↥A.orthogonalGroup) (H : AddSubgroup A.carrier) : g • H = AddSubgroup.map (↑((QuadraticMap.orthogonalGroupEquivIsometryEquiv A.quadratic) g).toAddEquiv) H

Pointwise transport of an additive subgroup by an element of O(A) is its image under the corresponding self-isometry.

@[simp]

theorem TauCeti.FiniteQuadraticModule.isIsotropic_smul_iff {A : FiniteQuadraticModule} (g : ↥A.orthogonalGroup) (H : AddSubgroup A.carrier) : A.IsIsotropic (g • H) ↔ A.IsIsotropic H

The orthogonal group preserves quadratic-isotropic subgroups.

@[simp]

theorem TauCeti.FiniteQuadraticModule.isLagrangian_smul_iff {A : FiniteQuadraticModule} (g : ↥A.orthogonalGroup) (H : AddSubgroup A.carrier) : A.IsLagrangian (g • H) ↔ A.IsLagrangian H

The orthogonal group preserves quadratic Lagrangian subgroups.

@[simp]

theorem TauCeti.FiniteQuadraticModule.smul_orthogonalComplement {A : FiniteQuadraticModule} (g : ↥A.orthogonalGroup) (H : AddSubgroup A.carrier) : g • A.orthogonalComplement H = A.orthogonalComplement (g • H)

The action of the orthogonal group commutes with taking the orthogonal complement for the polar pairing.