A function satisfying the parallelogram law is a quadratic form #

Let M and N be additive commutative groups, suppose doubling is injective on N, and let f : M → N satisfy the parallelogram law

f (x + y) + f (x - y) = 2 • f x + 2 • f y.

Then f is a quadratic form: its polarisation QuadraticMap.polar f x y = f (x + y) - f x - f y is biadditive, and f (n • x) = n ^ 2 • f x. This file proves that, and packages it as a QuadraticMap ℤ M N. Both f 0 = 0 and evenness of f come free from the law rather than being assumed.

Mathlib has the converse direction — QuadraticMap.polar_add_left and friends read biadditivity off a QuadraticMap, and LinearMap.BilinMap.toQuadraticMap builds one from a bilinear map — but nothing in the other direction from the parallelogram law alone. Its parallelogram_law and parallelogram_law_with_norm are statements about inner product spaces, and the Jordan–von Neumann construction in Analysis/InnerProductSpace/OfNorm.lean recovers an inner product from a norm on a real or complex space, using continuity. Neither applies to a function on a bare abelian group.

The elementary helpers need less: evenness holds without any condition on doubling, and zero and evenness need only a left-cancellative additive monoid as target. Natural quadratic scaling needs only a right-cancellative additive monoid as target, while integer scaling needs an additive group. Both scaling results allow arbitrary additive groups as sources and assume f 0 = 0. Thus scaling also applies to targets with 2-torsion.

The quadratic-map construction requires absence of `2`-torsion #

htwo : IsSMulRegular N 2 says that doubling is injective on N. It is sharp in both directions.

It is not IsAddTorsionFree N, which is strictly stronger and excludes codomains where the conclusion holds: IsSMulRegular (ZMod 3) 2 is true even though ZMod 3 has 3-torsion.

Nor can it be weakened away. With M = N = ZMod 2 every function satisfies the parallelogram law, because x - y = x + y and 2 • z = 0 there; the constant function 1 is then one that satisfies it while failing even f 0 = 0, which every quadratic form obeys — and correspondingly ¬ IsSMulRegular (ZMod 2) 2. Even assuming f 0 = 0 is insufficient for biadditivity: on (ZMod 2)³, the function f(x) = x₁x₂x₃ satisfies the law and preserves zero, but violates the three-variable identity at the three standard basis vectors.

For a torsion-free codomain it is one term: smul_right_injective N two_ne_zero supplies it for N = ℝ, the canonical height's target, and for N = ℤ, the degree form's.

Main results #

TauCeti.QuadraticMap.map_zero_of_parallelogram: f 0 = 0 when doubling is injective.
TauCeti.QuadraticMap.map_neg_of_parallelogram: f (-x) = f x.
TauCeti.QuadraticMap.map_add_add_add_map_of_parallelogram: the three-variable identity f (x + y + z) + (f x + f y + f z) = f (x + y) + f (y + z) + f (z + x), stated exactly as QuadraticMap.map_add_add_add_map.
TauCeti.QuadraticMap.polar_add_left_of_parallelogram and polar_zsmul_left_of_parallelogram: the polarisation is additive and ℤ-linear on the left.
TauCeti.QuadraticMap.map_nsmul_of_parallelogram: f (n • x) = n ^ 2 • f x for n : ℕ, assuming f 0 = 0, for an additive group M and right-cancellative additive monoid N.
TauCeti.QuadraticMap.map_zsmul_of_parallelogram: f (n • x) = n ^ 2 • f x for n : ℤ, assuming f 0 = 0, without commutativity of either group or injectivity of doubling on N.
TauCeti.QuadraticMap.ofParallelogram: f as a QuadraticMap ℤ M N, with the polarisation as its companion bilinear map.

Where this is used #

Two constructions in arithmetic geometry arrive at a function known to satisfy the parallelogram law and want it as a quadratic form.

The canonical height of an elliptic curve is one. It satisfies the parallelogram law exactly, and its polarisation is the Néron–Tate height pairing up to a factor of two: by QuadraticMap.polar_self the polarisation here has polar f x x = 2 • f x, whereas the pairing whose Gram determinant on a basis of the free part of the Mordell–Weil group is the regulator is normalised so that ⟨P, P⟩ is the height itself. A consumer wanting the regulator convention halves this one; the choice is not made here, since halving is not available in a general abelian group.

The degree form on End E is the other: its polarisation is the trace form, and non-negativity of the degree gives the Hasse bound by Cauchy–Schwarz (Silverman, The Arithmetic of Elliptic Curves, V.1.2).

Both take values in a torsion-free group — ℝ and ℤ respectively — so both satisfy the hypothesis below with room to spare. Stated for a general abelian group so that neither carries its own copy.

source

theorem TauCeti.QuadraticMap.map_zero_of_parallelogram {M : Type u_1} {N : Type u_2} [SubNegZeroMonoid M] [AddLeftCancelMonoid N] {f : M → N} (htwo : IsSMulRegular N 2) (hf : ∀ (x y : M), f (x + y) + f (x - y) = 2 • f x + 2 • f y) :

f 0 = 0

A parallelogram-law function preserves zero.

source

theorem TauCeti.QuadraticMap.map_neg_of_parallelogram {M : Type u_1} {N : Type u_2} [SubNegZeroMonoid M] [AddLeftCancelMonoid N] {f : M → N} (hf : ∀ (x y : M), f (x + y) + f (x - y) = 2 • f x + 2 • f y) (x : M) :

f (-x) = f x

A parallelogram-law function is even.

source

theorem TauCeti.QuadraticMap.map_nsmul_of_parallelogram {M : Type u_1} {N : Type u_2} [AddGroup M] [AddRightCancelMonoid N] {f : M → N} (hzero : f 0 = 0) (hf : ∀ (x y : M), f (x + y) + f (x - y) = 2 • f x + 2 • f y) (n : ℕ) (x : M) :

f (n • x) = (n * n) • f x

Quadraticity: a parallelogram-law function that preserves zero satisfies f (n • x) = n ^ 2 • f x for a natural number n, with an additive group source and a right-cancellative additive monoid target.

source

theorem TauCeti.QuadraticMap.map_zsmul_of_parallelogram {M : Type u_1} {N : Type u_2} [AddGroup M] [AddGroup N] {f : M → N} (hzero : f 0 = 0) (hf : ∀ (x y : M), f (x + y) + f (x - y) = 2 • f x + 2 • f y) (n : ℤ) (x : M) :

f (n • x) = (n * n) • f x

Quadraticity: a parallelogram-law function that preserves zero satisfies f (n • x) = n ^ 2 • f x for an integer n, even for noncommutative additive groups.

source

theorem TauCeti.QuadraticMap.map_add_add_add_map_of_parallelogram {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {f : M → N} (htwo : IsSMulRegular N 2) (hf : ∀ (x y : M), f (x + y) + f (x - y) = 2 • f x + 2 • f y) (x y z : M) :

f (x + y + z) + (f x + f y + f z) = f (x + y) + f (y + z) + f (z + x)

The three-variable identity satisfied by every quadratic form, in subtraction-free form.

source

theorem TauCeti.QuadraticMap.polar_add_left_of_parallelogram {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {f : M → N} (htwo : IsSMulRegular N 2) (hf : ∀ (x y : M), f (x + y) + f (x - y) = 2 • f x + 2 • f y) (x x' y : M) :

QuadraticMap.polar f (x + x') y = QuadraticMap.polar f x y + QuadraticMap.polar f x' y

The polarisation is additive in its left argument.

source

theorem TauCeti.QuadraticMap.polar_zsmul_left_of_parallelogram {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {f : M → N} (htwo : IsSMulRegular N 2) (hf : ∀ (x y : M), f (x + y) + f (x - y) = 2 • f x + 2 • f y) (a : ℤ) (x y : M) :

QuadraticMap.polar f (a • x) y = a • QuadraticMap.polar f x y

The polarisation is ℤ-linear in its left argument.

source

def TauCeti.QuadraticMap.ofParallelogram {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {f : M → N} (htwo : IsSMulRegular N 2) (hf : ∀ (x y : M), f (x + y) + f (x - y) = 2 • f x + 2 • f y) :

QuadraticMap ℤ M N

A function satisfying the parallelogram law is a quadratic form. Its companion bilinear map is QuadraticMap.polarBilin of it, which is the polarisation.

Equations