Scale and norm ideals of a bilinear form

The scale ideal is generated by all values of a bilinear form, and the norm ideal by its self-pairings. For a symmetric form, polarization gives twice the scale ideal inside the norm ideal. Spanning sets and bases provide generators for both ideals, and isometric forms have the same ideals. Extending scalars extends both ideals; when 2 is a unit, the ideals coincide.

The ideals are LinearMap.BilinForm.scaleIdeal and LinearMap.BilinForm.normIdeal, so B.scaleIdeal and B.normIdeal elaborate for B : LinearMap.BilinForm R M. The predicate LinearMap.BilinForm.IsScaleEven expresses parity relative to the scale ideal.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §82E.
• Sungmun Cho, Group schemes and local densities of quadratic lattices in residue characteristic 2, Definition 2.1(b), for parity relative to a modular lattice's own scale.

def LinearMap.BilinForm.scaleIdeal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : Ideal R

The ideal generated by the values of a bilinear form.

def LinearMap.BilinForm.normIdeal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : Ideal R

The ideal generated by the self-pairings of a bilinear form.

def LinearMap.BilinForm.IsScaleEven {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (π : R) : Prop

A form is scale-even relative to π if its norm ideal lies in π times its own scale ideal. This is defined for arbitrary π. For symmetric dyadic modular forms at π = 2, it is the usual type II condition. The zero form satisfies the condition, giving the even convention for an empty Jordan constituent.

theorem LinearMap.BilinForm.isScaleEven_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (π : R) : B.IsScaleEven π ↔ B.normIdeal ≤ Ideal.span {π} * B.scaleIdeal

The ideal-containment characterization of scale-relative parity.

theorem LinearMap.BilinForm.scaleIdeal_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : B.scaleIdeal = Ideal.span (Set.range fun (p : M × M) => (B p.1) p.2)

The scale ideal as a span of pairing values.

theorem LinearMap.BilinForm.normIdeal_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : B.normIdeal = Ideal.span (Set.range fun (x : M) => (B x) x)

The norm ideal as a span of self-pairings.

@[simp]

theorem LinearMap.BilinForm.apply_mem_scaleIdeal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (x y : M) : (B x) y ∈ B.scaleIdeal

Every pairing belongs to the scale ideal.

theorem LinearMap.BilinForm.scaleIdeal_le_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (I : Ideal R) : B.scaleIdeal ≤ I ↔ ∀ (x y : M), (B x) y ∈ I

The universal property of the scale ideal.

theorem LinearMap.BilinForm.scaleIdeal_eq_span_of_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) {s : Set M} (hs : Submodule.span R s = ⊤) : B.scaleIdeal = Ideal.span (Set.image2 (fun (x y : M) => (B x) y) s s)

A spanning set generates the scale ideal through its pairings.

theorem LinearMap.BilinForm.scaleIdeal_le_of_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) {s : Set M} (hs : Submodule.span R s = ⊤) (I : Ideal R) (h : ∀ a ∈ s, ∀ b ∈ s, (B a) b ∈ I) : B.scaleIdeal ≤ I

Pairings of a spanning set suffice to bound the scale ideal.

theorem LinearMap.BilinForm.scaleIdeal_eq_span_basis {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} (B : LinearMap.BilinForm R M) (b : Module.Basis ι R M) : B.scaleIdeal = Ideal.span (Set.range fun (ij : ι × ι) => (B (b ij.1)) (b ij.2))

A basis generates the scale ideal through its Gram entries.

@[simp]

theorem LinearMap.BilinForm.self_mem_normIdeal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (x : M) : (B x) x ∈ B.normIdeal

Every self-pairing belongs to the norm ideal.

theorem LinearMap.BilinForm.normIdeal_le_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (I : Ideal R) : B.normIdeal ≤ I ↔ ∀ (x : M), (B x) x ∈ I

The universal property of the norm ideal.

theorem LinearMap.BilinForm.normIdeal_le_scaleIdeal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : B.normIdeal ≤ B.scaleIdeal

The norm ideal is contained in the scale ideal.

theorem LinearMap.BilinForm.IsometryEquiv.scaleIdeal_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} (f : B.IsometryEquiv C) : B.scaleIdeal = C.scaleIdeal

Isometric forms have the same scale ideal.

theorem LinearMap.BilinForm.IsometryEquiv.normIdeal_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} (f : B.IsometryEquiv C) : B.normIdeal = C.normIdeal

Isometric forms have the same norm ideal.

theorem LinearMap.BilinForm.Equivalent.scaleIdeal_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} (h : B.Equivalent C) : B.scaleIdeal = C.scaleIdeal

Equivalent forms have the same scale ideal.

theorem LinearMap.BilinForm.Equivalent.normIdeal_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {B : LinearMap.BilinForm R M} {C : LinearMap.BilinForm R N} (h : B.Equivalent C) : B.normIdeal = C.normIdeal

Equivalent forms have the same norm ideal.

theorem LinearMap.BilinForm.two_mul_apply_mem_normIdeal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (hB : B.IsSymm) (x y : M) : 2 * (B x) y ∈ B.normIdeal

Twice a pairing of a symmetric form belongs to its norm ideal.

theorem LinearMap.BilinForm.normIdeal_eq_span_of_span {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (hB : B.IsSymm) {s : Set M} (hs : Submodule.span R s = ⊤) : B.normIdeal = Ideal.span ((fun (x : M) => (B x) x) '' s ∪ Set.image2 (fun (x y : M) => 2 * (B x) y) s s)

A spanning set generates the norm ideal through self-pairings and twice the pairings.

theorem LinearMap.BilinForm.normIdeal_eq_span_basis {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] {ι : Type u_3} (B : LinearMap.BilinForm R M) (hB : B.IsSymm) (b : Module.Basis ι R M) : B.normIdeal = Ideal.span ((Set.range fun (i : ι) => (B (b i)) (b i)) ∪ Set.range fun (ij : ι × ι) => 2 * (B (b ij.1)) (b ij.2))

A basis generates the norm ideal through diagonal Gram entries and twice all entries.

theorem LinearMap.BilinForm.span_singleton_two_mul_scaleIdeal_le_normIdeal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (hB : B.IsSymm) : Ideal.span {2} * B.scaleIdeal ≤ B.normIdeal

Polarization gives twice the scale ideal inside the norm ideal.

theorem LinearMap.BilinForm.normIdeal_eq_scaleIdeal_of_isUnit_two {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (hB : B.IsSymm) (h2 : IsUnit 2) : B.normIdeal = B.scaleIdeal

When two is invertible, polarization makes the scale and norm ideals equal.

theorem LinearMap.BilinForm.dvd_apply_of_forall_dvd_basis {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {ι : Type u_3} (b : Module.Basis ι R M) {d : R} (hd : ∀ (i j : ι), d ∣ (B (b i)) (b j)) (x y : M) : d ∣ (B x) y

A common divisor of the Gram entries of a bilinear form in a basis divides every value of the form.

theorem LinearMap.BilinForm.IsSymm.two_mul_dvd_apply_self_of_forall_dvd_basis {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsSymm) {ι : Type u_3} (b : Module.Basis ι R M) {d : R} (hd : ∀ (i j : ι), d ∣ (B (b i)) (b j)) (hdd : ∀ (i : ι), 2 * d ∣ (B (b i)) (b i)) (x : M) : 2 * d ∣ (B x) x

If d divides the Gram entries of a symmetric form in a basis and 2 * d divides the diagonal ones, then 2 * d divides every self-pairing: the norm ideal lies in 2 d R.

@[simp]

theorem LinearMap.BilinForm.scaleIdeal_baseChange {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : (BilinForm.baseChange A B).scaleIdeal = Ideal.map (algebraMap R A) B.scaleIdeal

The scale ideal of a base-changed form is the extension of its scale ideal.

@[simp]

theorem LinearMap.BilinForm.normIdeal_baseChange {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : (BilinForm.baseChange A B).normIdeal = Ideal.map (algebraMap R A) B.normIdeal

The norm ideal commutes with extension of scalars.