Documentation

TauCeti.LinearAlgebra.FiniteBilinearModule.Orthogonal.Splitting

Orthogonal splitting along a nondegenerate subgroup #

Let H be a subgroup of a finite bilinear module A on which the restricted pairing is nondegenerate. Then H meets its orthogonal complement trivially, since H ∩ H⊥ is the radical of the restriction, and every x : A is the sum of an element of H and an element of H⊥: the character b(x, ·) on H is b(h, ·) for some h ∈ H, and then x - h ∈ H⊥. So

A = H ⊕ H⊥,

an orthogonal direct sum. No nondegeneracy of A is needed for this. If A is nondegenerate as well, then so is the pairing restricted to H⊥. Mathlib's LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate is the analogue for a bilinear form on a finite-dimensional vector space, where nondegeneracy is injectivity and a dimension count replaces the character argument; it does not apply to ℚ/ℤ-valued pairings on finite groups.

A cyclic subgroup ⟨z⟩ is nondegenerate exactly when b(z, z) has the same order as z. This is the criterion for splitting off a cyclic orthogonal summand.

Summands are found at the top exponent of a primary part. If a prime p divides #A and A is nondegenerate, take x of the largest p-power order p^{k+1}. The character b(x, ·) then has order p^{k+1} too, so p^k b(x, y) ≠ 0 for some y, which can be replaced by its p-primary part. Whether x, y and their combinations generate a cyclic or a rank-two summand depends on p and on the self-pairings.

For a finite quadratic module the quadratic map is additive across the splitting, because the polar pairing of H with H⊥ vanishes, so the splitting is an isometry from the orthogonal product H ⊥ H⊥ onto A. This is the analogue, for ℚ/ℤ-valued quadratic maps, of QuadraticMap.IsometryEquiv.prodRestrictOrthogonal, which is stated for quadratic forms valued in the scalar ring. Splitting off nondegenerate summands one at a time is how a nondegenerate finite quadratic module is decomposed into cyclic and rank-two pieces.

Main declarations #

References #

source
theorem TauCeti.FiniteBilinearModule.isCompl_orthogonalComplement (A : FiniteBilinearModule) {H : AddSubgroup A.carrier} (hH : (A.restrict H).IsNondegenerate) :
IsCompl H (A.orthogonalComplement H)

Orthogonal splitting. If the pairing restricted to H is nondegenerate, then H and its orthogonal complement are complementary subgroups.

source
theorem TauCeti.FiniteBilinearModule.IsNondegenerate.isNondegenerate_restrict_orthogonalComplement {A : FiniteBilinearModule} (hA : A.IsNondegenerate) {H : AddSubgroup A.carrier} (hH : (A.restrict H).IsNondegenerate) :
(A.restrict (A.orthogonalComplement H)).IsNondegenerate

In a nondegenerate finite bilinear module, the orthogonal complement of a subgroup with nondegenerate restricted pairing also has nondegenerate restricted pairing.

source
theorem TauCeti.FiniteBilinearModule.isNondegenerate_restrict_zmultiples_iff (A : FiniteBilinearModule) (z : A.carrier) :
(A.restrict (AddSubgroup.zmultiples z)).IsNondegenerate ↔ addOrderOf ((A.pairing z) z) = addOrderOf z

The cyclic subgroup generated by z is nondegenerate exactly when b(z, z) has the same order as z. The order of b(z, z) always divides that of z; equality says that j • b(z, z) vanishes only when j • z does, and b(j • z, i • z) = ij • b(z, z).

source
theorem TauCeti.FiniteBilinearModule.addOrderOf_eq_and_isNondegenerate_of_pairing (A : FiniteBilinearModule) {p k : ℕ} [Fact (Nat.Prime p)] {z : A.carrier} (hz : p ^ (k + 1) • z = 0) (hzz : p ^ k • (A.pairing z) z ≠ 0) :
addOrderOf z = p ^ (k + 1) ∧ (A.restrict (AddSubgroup.zmultiples z)).IsNondegenerate

If p^{k+1} kills z but not p^k b(z, z), then z has order p^{k+1} and generates a nondegenerate cyclic subgroup.

source
theorem TauCeti.FiniteBilinearModule.exists_nsmul_pairing_ne_zero_of_dvd_card (A : FiniteBilinearModule) {p : ℕ} [hp : Fact (Nat.Prime p)] (hA : A.IsNondegenerate) (hpA : p ∣ Nat.card A.carrier) :
∃ (x : A.carrier) (y : A.carrier) (k : ℕ), p ^ (k + 1) • x = 0 ∧ p ^ (k + 1) • y = 0 ∧ p ^ k • (A.pairing x) y ≠ 0

A pair detecting a nonzero primary pairing. In a nondegenerate finite bilinear module whose order is divisible by a prime p, there are x and y, both killed by p^{k+1}, with p^k b(x, y) ≠ 0. In particular x and y both have order exactly p^{k+1}.

source
noncomputable def TauCeti.FiniteQuadraticModule.restrictProdOrthogonalComplementIsometry (A : FiniteQuadraticModule) {H : AddSubgroup A.carrier} (hH : (A.restrict H).IsNondegenerate) :
((A.restrict H).prod (A.restrict (A.orthogonalComplement H))).Isometry A

The orthogonal splitting of a finite quadratic module along a subgroup H with nondegenerate restricted pairing: addition (h, k) ↦ h + k is an isometry from the orthogonal product of the restrictions to H and to H⊥ onto A.

Instances For
    source
    @[simp]
    theorem TauCeti.FiniteQuadraticModule.restrictProdOrthogonalComplementIsometry_apply (A : FiniteQuadraticModule) {H : AddSubgroup A.carrier} (hH : (A.restrict H).IsNondegenerate) (h : ↥H) (k : ↥(A.orthogonalComplement H)) :
    (A.restrictProdOrthogonalComplementIsometry hH) (h, k) = ↑h + ↑k

    The orthogonal splitting isometry adds the two components.