Finite quadratic modules on the Klein four-group

A ℚ/ℤ-valued quadratic map on (ℤ/2)² is determined by its three values on the nonzero elements, and conversely any three values admissible for the two-torsion of the group occur. This file makes that presentation available as a construction: given α β γ : ℚ/ℤ with 4α = 4β = 2γ = 0, TauCeti.FiniteQuadraticModule.kleinFour is the finite quadratic module on ZMod 2 × ZMod 2 with

q(1, 0) = α,   q(0, 1) = β,   q(1, 1) = α + β + γ,   b((1, 0), (0, 1)) = γ.

The construction is a quotient, not a formula in ZMod.val: the parameters define an honest ℤ-bilinear map on ℤ × ℤ, its associated quadratic map (m, k) ↦ m²α + k²β + mkγ has the kernel of the reduction ℤ × ℤ → (ℤ/2)² inside its radical exactly under the three torsion hypotheses, and QuadraticMap.liftOfSurjective descends it. The torsion hypotheses are therefore not technical: 4α = 0 is the statement that q is well defined on a two-torsion generator, and 2γ = 0 the corresponding statement for the pairing.

The companion TauCeti.FiniteQuadraticModule.kleinFourIsometryOfGenerators turns an additive equivalence (ℤ/2)² ≃+ A matching the three displayed values into an isometry onto A, which is how a discriminant form of order four and exponent two is identified.

The quotient construction is the rank-two adaptation of the cyclic one in TauCeti.LinearAlgebra.FiniteBilinearModule.Cyclic, which presents a form on ℤ/m by the single value of its generator.

Main declarations

• TauCeti.FiniteQuadraticModule.kleinFourMap: the quadratic map on ZMod 2 × ZMod 2 with the displayed generator values.
• TauCeti.FiniteQuadraticModule.kleinFour: the resulting finite quadratic module.
• TauCeti.FiniteQuadraticModule.kleinFourIsometryOfGenerators: an additive equivalence matching the three generator values is an isometry.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1 for discriminant forms and §1.8, Proposition 1.8.1 for the forms written u₁ and v₁ in the full-norm convention.
• W. Ebeling, Lattices and Codes, Chapter 1.

This is part of Layer 3 of TauCetiRoadmap/IntegralLattices/README.md.

The presenting quadratic map on ℤ × ℤ

Reduction modulo two

The quadratic module

noncomputable def TauCeti.FiniteQuadraticModule.kleinFourMap (α β γ : AddCircle 1) (h₄α : 4 • α = 0) (h₄β : 4 • β = 0) (h₂γ : 2 • γ = 0) : QuadraticMap ℤ (ZMod 2 × ZMod 2) (AddCircle 1)

The quadratic map on (ℤ/2)² sending (1, 0) to α, (0, 1) to β, and (1, 1) to α + β + γ.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.FiniteQuadraticModule.kleinFourMap_intCast (α β γ : AddCircle 1) (h₄α : 4 • α = 0) (h₄β : 4 • β = 0) (h₂γ : 2 • γ = 0) (m k : ℤ) : (kleinFourMap α β γ h₄α h₄β h₂γ) (↑m, ↑k) = (m * m) • α + (k * k) • β + (m * k) • γ

The value of kleinFourMap on the reduction of a pair of integers.

@[simp]

theorem TauCeti.FiniteQuadraticModule.kleinFourMap_apply_one_zero (α β γ : AddCircle 1) (h₄α : 4 • α = 0) (h₄β : 4 • β = 0) (h₂γ : 2 • γ = 0) : (kleinFourMap α β γ h₄α h₄β h₂γ) (1, 0) = α

@[simp]

theorem TauCeti.FiniteQuadraticModule.kleinFourMap_apply_zero_one (α β γ : AddCircle 1) (h₄α : 4 • α = 0) (h₄β : 4 • β = 0) (h₂γ : 2 • γ = 0) : (kleinFourMap α β γ h₄α h₄β h₂γ) (0, 1) = β

@[simp]

theorem TauCeti.FiniteQuadraticModule.kleinFourMap_apply_one_one (α β γ : AddCircle 1) (h₄α : 4 • α = 0) (h₄β : 4 • β = 0) (h₂γ : 2 • γ = 0) : (kleinFourMap α β γ h₄α h₄β h₂γ) (1, 1) = α + β + γ

@[simp]

theorem TauCeti.FiniteQuadraticModule.polar_kleinFourMap_one_zero_zero_one (α β γ : AddCircle 1) (h₄α : 4 • α = 0) (h₄β : 4 • β = 0) (h₂γ : 2 • γ = 0) : QuadraticMap.polar ⇑(kleinFourMap α β γ h₄α h₄β h₂γ) (1, 0) (0, 1) = γ

The two standard generators of (ℤ/2)² pair to γ.

noncomputable def TauCeti.FiniteQuadraticModule.kleinFour (α β γ : AddCircle 1) (h₄α : 4 • α = 0) (h₄β : 4 • β = 0) (h₂γ : 2 • γ = 0) : FiniteQuadraticModule

The finite quadratic module on (ℤ/2)² with generator values α, β and α + β + γ.

Equations

• TauCeti.FiniteQuadraticModule.kleinFour α β γ h₄α h₄β h₂γ = TauCeti.FiniteQuadraticModule.ofQuadraticMap (TauCeti.FiniteQuadraticModule.kleinFourMap α β γ h₄α h₄β h₂γ)

@[simp]

theorem TauCeti.FiniteQuadraticModule.kleinFour_quadratic (α β γ : AddCircle 1) (h₄α : 4 • α = 0) (h₄β : 4 • β = 0) (h₂γ : 2 • γ = 0) (x : ZMod 2 × ZMod 2) : (kleinFour α β γ h₄α h₄β h₂γ).quadratic x = (kleinFourMap α β γ h₄α h₄β h₂γ) x

@[simp]

theorem TauCeti.FiniteQuadraticModule.kleinFour_pairing (α β γ : AddCircle 1) (h₄α : 4 • α = 0) (h₄β : 4 • β = 0) (h₂γ : 2 • γ = 0) (x y : ZMod 2 × ZMod 2) : ((kleinFour α β γ h₄α h₄β h₂γ).pairing x) y = QuadraticMap.polar (⇑(kleinFourMap α β γ h₄α h₄β h₂γ)) x y

noncomputable def TauCeti.FiniteQuadraticModule.kleinFourIsometryOfGenerators {A : Type u_1} [AddCommGroup A] (q : QuadraticMap ℤ (ZMod 2 × ZMod 2) (AddCircle 1)) (r : QuadraticMap ℤ A (AddCircle 1)) (e : ZMod 2 × ZMod 2 ≃+ A) (h₁ : r (e (1, 0)) = q (1, 0)) (h₂ : r (e (0, 1)) = q (0, 1)) (h₃ : r (e (1, 1)) = q (1, 1)) : q.IsometryEquiv r

An additive equivalence from (ℤ/2)² matching all three nonzero values is an isometry.

No hypothesis beyond the three displayed values is needed. Both forms are stated as bare quadratic maps so that the construction applies before either is packaged as a finite quadratic module.

Equations

• TauCeti.FiniteQuadraticModule.kleinFourIsometryOfGenerators q r e h₁ h₂ h₃ = { toLinearEquiv := e.toIntLinearEquiv, map_app' := ⋯ }

@[simp]

theorem TauCeti.FiniteQuadraticModule.kleinFourIsometryOfGenerators_apply {A : Type u_1} [AddCommGroup A] (q : QuadraticMap ℤ (ZMod 2 × ZMod 2) (AddCircle 1)) (r : QuadraticMap ℤ A (AddCircle 1)) (e : ZMod 2 × ZMod 2 ≃+ A) (h₁ : r (e (1, 0)) = q (1, 0)) (h₂ : r (e (0, 1)) = q (0, 1)) (h₃ : r (e (1, 1)) = q (1, 1)) (x : ZMod 2 × ZMod 2) : (kleinFourIsometryOfGenerators q r e h₁ h₂ h₃) x = e x