Matrices preserving a Gram matrix

For a square matrix A over a commutative semiring, Matrix.isometryMatrices A is the submonoid of matrices X with Xᵀ * A * X = A, the endomorphisms of the coordinate module that preserve the bilinear form with Gram matrix A. Counting these matrices over the finite rings ZMod (p ^ r) is how the local density of a quadratic lattice is defined, and the results here are what that count needs.

• A change of basis A ↦ Pᵀ * A * P by an invertible P conjugates the submonoid by P, so its cardinality does not depend on the basis. Neither does it change under reindexing or under a ring isomorphism of the coefficients.
• When every solution has unit determinant, the solutions form a group, so for any ring homomorphism f their number is the number of their images under f times the number of solutions sent to 1.
• Let f : R →+* S be surjective with square-zero kernel, let 2 be a unit of R, and let A be symmetric with unit determinant. Then every solution over S lifts to a solution over R, and the solutions over R lying above a fixed one correspond to the skew-symmetric matrices with entries in the kernel. Hence, as an identity of Nat.cards, the count over R is Nat.card (ker f) ^ (k.choose 2) times the count over S, for k the size of the index type; when R is finite these are the actual numbers of solutions. This is the infinitesimal lifting property behind the smoothness of the orthogonal group of a nondegenerate form away from 2, with its relative dimension k (k - 1) / 2.

The lift corrects an arbitrary preimage M of the solution: with error E = A - Mᵀ * A * M, the matrix M * (1 + ½ A⁻¹ E) is a solution, since all quadratic terms in the error vanish.

Main results

• Matrix.natCard_isometryMatrices_transpose_mul_mul: the count is invariant under A ↦ Pᵀ * A * P for invertible P.
• Matrix.natCard_isometryMatrices_reindex, Matrix.natCard_isometryMatrices_map_ringEquiv: the count is invariant under reindexing and under ring isomorphisms.
• Matrix.natCard_isometryMatrices_eq_mul: the count is the number of images under a ring homomorphism times the size of the fibre above 1, when all solutions are invertible.
• Matrix.transposeMulMulEquiv: the solutions of Yᵀ * A * Y = B only depend on A and B up to congruence by invertible matrices.
• Matrix.transpose_mul_mul_add_eq_zero_iff: if Yᵀ * A * Y is invertible, the linear equation Yᵀ * A * Z + D = 0 has a unique solution Z.
• Matrix.exists_map_eq_of_mem_isometryMatrices_map: solutions lift across a surjection with square-zero kernel.
• Matrix.isometryMatricesFiberEquiv: the solutions congruent to a given one modulo a square-zero ideal correspond to the skew-symmetric matrices with entries in the ideal.
• Matrix.natCard_isometryMatrices_eq_pow_mul: the count across such a surjection.

References

• C. L. Siegel, Über die analytische Theorie der quadratischen Formen, Ann. of Math. 36 (1935), where the local densities are defined by these counts.

def Matrix.isometryMatrices {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) : Submonoid (Matrix n n R)

The submonoid of matrices X with Xᵀ * A * X = A, the endomorphisms of the coordinate module that preserve the bilinear form with Gram matrix A.

@[simp]

theorem Matrix.mem_isometryMatrices {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommSemiring R] {A X : Matrix n n R} : X ∈ A.isometryMatrices ↔ X.transpose * A * X = A

Membership in isometryMatrices A is the equation Xᵀ * A * X = A.

theorem Matrix.map_mem_isometryMatrices_map {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] [CommSemiring S] (f : R →+* S) {A X : Matrix n n R} (hX : X ∈ A.isometryMatrices) : X.map ⇑f ∈ (A.map ⇑f).isometryMatrices

A ring homomorphism carries solutions of Xᵀ * A * X = A to solutions for the image of A.

theorem Matrix.mulVec_dotProduct_mulVec_mulVec_of_mem_isometryMatrices {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommSemiring R] {A X : Matrix n n R} (hX : X ∈ A.isometryMatrices) (x y : n → R) : X.mulVec x ⬝ᵥ A.mulVec (X.mulVec y) = x ⬝ᵥ A.mulVec y

A matrix preserving A preserves the values xᵀ A y.

theorem Matrix.natCard_isometryMatrices_reindex {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommSemiring R] {m : Type u_4} [Fintype m] [DecidableEq m] (e : n ≃ m) (A : Matrix n n R) : Nat.card ↥((reindex e e) A).isometryMatrices = Nat.card ↥A.isometryMatrices

The count of matrices preserving a Gram matrix does not depend on the indexing: reindexing A along an equivalence e reindexes the solutions along e.

theorem Matrix.natCard_isometryMatrices_map_ringEquiv {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] [CommSemiring S] (e : R ≃+* S) (A : Matrix n n R) : Nat.card ↥(A.map ⇑e).isometryMatrices = Nat.card ↥A.isometryMatrices

The count of matrices preserving a Gram matrix is invariant under ring isomorphisms: a ring isomorphism e carries the solutions for A to the solutions for A.map e.

theorem Matrix.add_transpose_mul_mul_add_of_sq_eq_bot {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {I : Ideal R} (hI : I ^ 2 = ⊥) {A X D : Matrix n n R} (hA : A.transpose = A) (hX : X ∈ A.isometryMatrices) (hD : ∀ (i j : n), D i j ∈ I) : (X + D).transpose * A * (X + D) = A + X.transpose * A * D + (X.transpose * A * D).transpose

The square-zero expansion of the isometry equation. If X preserves a symmetric Gram matrix A and the entries of D lie in a square-zero ideal, then the quadratic term of (X + D)ᵀ * A * (X + D) vanishes, leaving A + K + Kᵀ for K = Xᵀ * A * D.

theorem Matrix.isUnit_det_of_mem_isometryMatrices {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {A X : Matrix n n R} (hA : IsUnit A.det) (hX : X ∈ A.isometryMatrices) : IsUnit X.det

A matrix preserving a Gram matrix with unit determinant has unit determinant, its square being 1.

theorem Matrix.nonsing_inv_mem_isometryMatrices {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {A X : Matrix n n R} (hX : X ∈ A.isometryMatrices) (hdet : IsUnit X.det) : X⁻¹ ∈ A.isometryMatrices

The inverse of a matrix with unit determinant preserving A also preserves A.

theorem Matrix.natCard_isometryMatrices_eq_mul {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [CommRing S] (f : R →+* S) {A : Matrix n n R} (hunit : ∀ X ∈ A.isometryMatrices, IsUnit X.det) : Nat.card ↥A.isometryMatrices = Nat.card ↥(Submonoid.map f.mapMatrix A.isometryMatrices) * Nat.card ↑{X : Matrix n n R | X ∈ A.isometryMatrices ∧ X.map ⇑f = 1}

Counting matrices preserving a Gram matrix fibrewise. If every matrix preserving A has unit determinant, these matrices form a group, so the fibres of a ring homomorphism f on them are the cosets of the fibre above 1: their number is the number of their images under f times the number of them that f sends to 1.

noncomputable def Matrix.transposeMulMulEquiv {R : Type u_2} [CommRing R] {m : Type u_4} {k : Type u_5} [Fintype m] [DecidableEq m] [Fintype k] [DecidableEq k] {A A' P : Matrix m m R} {B B' Q : Matrix k k R} (hP : IsUnit P.det) (hQ : IsUnit Q.det) (hA : P.transpose * A * P = A') (hB : Q.transpose * B * Q = B') : { Y : Matrix m k R // Y.transpose * A' * Y = B' } ≃ { Y : Matrix m k R // Y.transpose * A * Y = B }

Solutions of Yᵀ * A * Y = B under congruence of A and B. If Pᵀ * A * P = A' and Qᵀ * B * Q = B' for invertible P and Q, then Y ↦ P * Y * Q⁻¹ matches the solutions of Yᵀ * A' * Y = B' with those of Yᵀ * A * Y = B.

@[simp]

theorem Matrix.transposeMulMulEquiv_apply_coe {R : Type u_2} [CommRing R] {m : Type u_4} {k : Type u_5} [Fintype m] [DecidableEq m] [Fintype k] [DecidableEq k] {A A' P : Matrix m m R} {B B' Q : Matrix k k R} (hP : IsUnit P.det) (hQ : IsUnit Q.det) (hA : P.transpose * A * P = A') (hB : Q.transpose * B * Q = B') (Y : { Y : Matrix m k R // Y.transpose * A' * Y = B' }) : ↑((transposeMulMulEquiv hP hQ hA hB) Y) = P * ↑Y * Q⁻¹

Matrix.transposeMulMulEquiv sends a solution Y to P * Y * Q⁻¹.

@[simp]

theorem Matrix.transposeMulMulEquiv_symm_apply_coe {R : Type u_2} [CommRing R] {m : Type u_4} {k : Type u_5} [Fintype m] [DecidableEq m] [Fintype k] [DecidableEq k] {A A' P : Matrix m m R} {B B' Q : Matrix k k R} (hP : IsUnit P.det) (hQ : IsUnit Q.det) (hA : P.transpose * A * P = A') (hB : Q.transpose * B * Q = B') (Y : { Y : Matrix m k R // Y.transpose * A * Y = B }) : ↑((transposeMulMulEquiv hP hQ hA hB).symm Y) = P⁻¹ * ↑Y * Q

The inverse of Matrix.transposeMulMulEquiv sends a solution Y to P⁻¹ * Y * Q.

theorem Matrix.transpose_mul_mul_add_eq_zero_iff {R : Type u_2} [CommRing R] {m : Type u_4} {k : Type u_5} [Fintype m] [DecidableEq m] {A C Y : Matrix m m R} (hC : IsUnit C.det) (hY : Y.transpose * A * Y = C) {Z D : Matrix m k R} : Y.transpose * A * Z + D = 0 ↔ Z = -(Y * C⁻¹ * D)

Solving a linear equation through a congruence. If Yᵀ * A * Y = C with C invertible, then the equation Yᵀ * A * Z + D = 0 has the unique solution Z = -(Y * C⁻¹ * D).

theorem Matrix.natCard_isometryMatrices_transpose_mul_mul {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {A P : Matrix n n R} (hP : IsUnit P.det) : Nat.card ↥(P.transpose * A * P).isometryMatrices = Nat.card ↥A.isometryMatrices

The count of matrices preserving a Gram matrix does not depend on the basis: for an invertible P, conjugation by P matches the solutions for Pᵀ * A * P with those for A.

theorem Matrix.exists_map_eq_of_mem_isometryMatrices_map {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) (hker : RingHom.ker f ^ 2 = ⊥) (h2 : IsUnit 2) {A : Matrix n n R} (hA : A.transpose = A) (hdet : IsUnit A.det) {Y : Matrix n n S} (hY : Y ∈ (A.map ⇑f).isometryMatrices) : ∃ X ∈ A.isometryMatrices, X.map ⇑f = Y

Matrices preserving a Gram matrix lift across a square-zero extension. Let f be a surjective ring homomorphism whose kernel squares to zero, let 2 be a unit, and let A be symmetric with unit determinant. Then every solution of Yᵀ * A * Y = A over the target is the image of a solution over the source.

noncomputable def Matrix.isometryMatricesFiberEquiv {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {I : Ideal R} (hI : I ^ 2 = ⊥) {A X₀ : Matrix n n R} (hA : A.transpose = A) (hdet : IsUnit A.det) (hX₀ : X₀ ∈ A.isometryMatrices) : { X : ↥A.isometryMatrices // ∀ (i j : n), ↑X i j - X₀ i j ∈ I } ≃ { K : Matrix n n R // (∀ (i j : n), K i j ∈ I) ∧ K.transpose = -K }

The solutions congruent to a given one modulo a square-zero ideal form a torsor under the skew-symmetric matrices with entries in the ideal. Let A be symmetric with unit determinant and let X₀ preserve A. The solutions X with X - X₀ having entries in a square-zero ideal I correspond to the skew-symmetric K with entries in I, via K = X₀ᵀ * A * (X - X₀) and X = X₀ + (X₀ᵀ * A)⁻¹ * K.

@[simp]

theorem Matrix.isometryMatricesFiberEquiv_apply_coe {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {I : Ideal R} (hI : I ^ 2 = ⊥) {A X₀ : Matrix n n R} (hA : A.transpose = A) (hdet : IsUnit A.det) (hX₀ : X₀ ∈ A.isometryMatrices) (X : { X : ↥A.isometryMatrices // ∀ (i j : n), ↑X i j - X₀ i j ∈ I }) : ↑((isometryMatricesFiberEquiv hI hA hdet hX₀) X) = X₀.transpose * A * (↑↑X - X₀)

Matrix.isometryMatricesFiberEquiv sends a solution X to X₀ᵀ * A * (X - X₀).

@[simp]

theorem Matrix.isometryMatricesFiberEquiv_symm_apply_coe_coe {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {I : Ideal R} (hI : I ^ 2 = ⊥) {A X₀ : Matrix n n R} (hA : A.transpose = A) (hdet : IsUnit A.det) (hX₀ : X₀ ∈ A.isometryMatrices) (K : { K : Matrix n n R // (∀ (i j : n), K i j ∈ I) ∧ K.transpose = -K }) : ↑↑((isometryMatricesFiberEquiv hI hA hdet hX₀).symm K) = X₀ + (X₀.transpose * A)⁻¹ * ↑K

The inverse of Matrix.isometryMatricesFiberEquiv sends a skew-symmetric K to X₀ + (X₀ᵀ * A)⁻¹ * K.

theorem Matrix.natCard_isometryMatrices_eq_pow_mul {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) (hker : RingHom.ker f ^ 2 = ⊥) (h2 : IsUnit 2) {A : Matrix n n R} (hA : A.transpose = A) (hdet : IsUnit A.det) : Nat.card ↥A.isometryMatrices = Nat.card ↥(RingHom.ker f) ^ (Fintype.card n).choose 2 * Nat.card ↥(A.map ⇑f).isometryMatrices

Counting matrices preserving a Gram matrix across a square-zero extension. Let f be a surjective ring homomorphism whose kernel squares to zero, let 2 be a unit, and let A be symmetric with unit determinant. The solutions over the source lying above a solution over the target are a torsor under the skew-symmetric matrices with entries in ker f (Matrix.isometryMatricesFiberEquiv), so the Nat.card of the solutions over the source is Nat.card (ker f) ^ (k.choose 2) times that over the target, for k the size of the index type.