The signed discriminant of a lattice and its Kronecker character

Let L be a ℤ-submodule of a real inner product space E, with discriminant group A_L = L^∨ ⧸ (L ∩ L^∨) (ZLattice.DiscriminantGroup L). The signed discriminant of L is

D_L = (-1) ^ (finrank ℝ E / 2) * |A_L|

(ZLattice.signedDiscr L). The definition is unguarded: when A_L is infinite, Nat.card A_L = 0 gives D_L = 0, and when L is an integral full lattice of rank n = finrank ℝ E, |A_L| is the positive integer det L = covolume L ^ 2, so D_L = (-1) ^ ⌊n / 2⌋ det L is nonzero with sign (-1) ^ ⌊n / 2⌋.

In even rank 2k, this is the signed determinant D_L = (-1)^k det L of Hecke and Schoeneberg. Because ⌊n / 2⌋ and C(n, 2) have the same parity in every rank n (Nat.even_choose_two_iff), (-1) ^ ⌊n / 2⌋ also equals the quadratic-form sign (-1) ^ (n (n - 1) / 2) in all dimensions: for every integral full lattice L, the rational square class of D_L is the signed discriminant RegularFormClass.signedDiscr of the ambient rational quadratic form of ratModel hL (ZLattice.IsIntegral.signedDiscr_rationalFormClass_ratModel).

For an even full lattice L of even rank 2k, D_L is a nonzero discriminant congruent to 0 or 1 modulo 4 (ZLattice.IsEven.signedDiscr_modEq_zero_or_one), so it defines the quadratic Dirichlet character TauCeti.kroneckerChar R (signedDiscr L) _ _ of modulus |D_L| = det L, whose value at -1 is (-1)^k (ZLattice.IsEven.kroneckerChar_signedDiscr_neg_one). Every integer coprime to level L is coprime to D_L (ZLattice.isCoprime_signedDiscr_of_isCoprime_level). In even rank, scaling L by √m multiplies D_L by the square (m^k)², and the product of D_L with the signed discriminant of its Fricke partner √(level L) • L^∨ is the square (level L ^ k)²; consequently both operations preserve the conductor and primitive character of (D_L / ·).

At the non-integral boundary, for any c : ℝ with c² irrational — in particular for c = 2 ^ (1 / 4 : ℝ) — the rank-one lattice c ℤ ⊆ ℝ has dual c⁻¹ ℤ meeting c ℤ only at 0, so its discriminant group and every quotient L^∨ ⧸ (L^∨ ∩ a L^∨ ∩ L) are infinite and D_L = 0.

Main definitions

• ZLattice.signedDiscr L: the signed discriminant (-1) ^ (finrank ℝ E / 2) * |A_L|.

Main statements

• ZLattice.signedDiscr_comap, ZLattice.signedDiscr_orthSum_of_even_left: isometry invariance of D_L, and multiplicativity D_{L ⊕ M} = D_L * D_M when at least one summand has even ambient dimension.
• ZLattice.IsIntegral.signedDiscr_cast, ZLattice.IsIntegral.signedDiscr_ne_zero, ZLattice.IsEven.signedDiscr_eq_one_of_isUnimodular: for integral full lattices D_L = (-1) ^ ⌊n / 2⌋ det L ≠ 0, and D_L = 1 for even unimodular full lattices.
• ZLattice.IsIntegral.signedDiscr_sqrt_smul, ZLattice.IsIntegral.mul_signedDiscr_sqrt_level_smul_dual: D_{√m • L} = mⁿ D_L and D_L * D_{√N • L^∨} = Nⁿ.
• ZLattice.IsIntegral.signedDiscr_rationalFormClass_ratModel, TauCeti.IntegralLattice.signedDiscr_realModel: comparisons with the rational and real models.
• ZLattice.isCoprime_signedDiscr_of_isCoprime_level, ZLattice.IsEven.signedDiscr_modEq_zero_or_one, ZLattice.IsEven.kroneckerChar_signedDiscr_neg_one, ZLattice.IsEven.conductor_kroneckerChar_signedDiscr_sqrt_level_smul_dual: arithmetic properties of D_L and its Kronecker character (D_L / ·).
• ZLattice.inf_dual_span_two_rpow_one_quarter, ZLattice.infinite_discriminantGroup_span_two_rpow_one_quarter, ZLattice.signedDiscr_span_two_rpow_one_quarter: the non-integral rank-one boundary example 2 ^ (1 / 4 : ℝ) • ℤ ⊆ ℝ.

References

• W. Ebeling, Lattices and Codes, 3rd ed., Springer, 2013, Chapter 3.
• H. Iwaniec, Topics in Classical Automorphic Forms, AMS, 1997, Chapter 10.
• B. Schoeneberg, Das Verhalten von mehrfachen Thetareihen bei Modulsubstitutionen, Math. Ann. 116 (1939), 511–523.

Definition and general properties of the signed discriminant

noncomputable def ZLattice.signedDiscr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : ℤ

The signed discriminant D_L = (-1) ^ ⌊finrank ℝ E / 2⌋ * |L^∨ ⧸ (L ∩ L^∨)| of a lattice L in a real inner product space E. For an integral full lattice of rank 2k, this is (-1)^k det L; when L^∨ ⧸ (L ∩ L^∨) is infinite, Nat.card vanishes and signedDiscr L = 0.

theorem ZLattice.signedDiscr_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : signedDiscr L = (-1) ^ (Module.finrank ℝ E / 2) * ↑(Nat.card (DiscriminantGroup L))

theorem ZLattice.signedDiscr_of_finrank_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) {k : ℕ} (hk : Module.finrank ℝ E = 2 * k) : signedDiscr L = (-1) ^ k * ↑(Nat.card (DiscriminantGroup L))

In an ambient space of even dimension 2k, signedDiscr L = (-1)^k * |A_L|.

@[simp]

theorem ZLattice.natAbs_signedDiscr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : (signedDiscr L).natAbs = Nat.card (DiscriminantGroup L)

The natural absolute value of the signed discriminant is the order of the discriminant group.

@[simp]

theorem ZLattice.abs_signedDiscr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : |signedDiscr L| = ↑(Nat.card (DiscriminantGroup L))

The absolute value of the signed discriminant is the order of the discriminant group.

@[simp]

theorem ZLattice.signedDiscr_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} : signedDiscr L = 0 ↔ Infinite (DiscriminantGroup L)

The signed discriminant vanishes if and only if the discriminant group is infinite.

theorem ZLattice.IsUnimodular.signedDiscr_eq_neg_one_pow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (h : IsUnimodular L) : signedDiscr L = (-1) ^ (Module.finrank ℝ E / 2)

For a unimodular lattice, signedDiscr L = (-1) ^ ⌊finrank ℝ E / 2⌋.

@[simp]

theorem ZLattice.signedDiscr_of_subsingleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Subsingleton E] (L : Submodule ℤ E) : signedDiscr L = 1

Every submodule of a zero-dimensional space has signed discriminant 1.

@[simp]

theorem ZLattice.signedDiscr_comap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (L : Submodule ℤ E) (e : F ≃ₗᵢ[ℝ] E) : signedDiscr (ZLattice.comap ℝ L ↑e.toLinearEquiv) = signedDiscr L

The signed discriminant is invariant under linear isometry equivalences.

theorem ZLattice.signedDiscr_orthSum_of_even_left {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (L : Submodule ℤ E) (M : Submodule ℤ F) (hE : Even (Module.finrank ℝ E)) : signedDiscr (orthSum L M) = signedDiscr L * signedDiscr M

Multiplicativity of the signed discriminant under orthogonal direct sums when the first ambient space has even dimension. Some parity hypothesis is required: for ℤ ⊕ ℤ ⊆ ℝ², D_{ℤ ⊕ ℤ} = -1 while D_ℤ * D_ℤ = 1 * 1 = 1.

theorem ZLattice.signedDiscr_orthSum_of_even_right {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (L : Submodule ℤ E) (M : Submodule ℤ F) (hF : Even (Module.finrank ℝ F)) : signedDiscr (orthSum L M) = signedDiscr L * signedDiscr M

Multiplicativity of the signed discriminant under orthogonal direct sums when the second ambient space has even dimension.

Full integral, unimodular, scaled, and Fricke-partner lattices

theorem ZLattice.IsIntegral.signedDiscr_ne_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) : signedDiscr L ≠ 0

The signed discriminant of an integral full lattice is nonzero.

theorem ZLattice.IsIntegral.sign_signedDiscr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) : (signedDiscr L).sign = (-1) ^ (Module.finrank ℝ E / 2)

The sign of the signed discriminant of an integral full lattice is (-1) ^ ⌊finrank ℝ E / 2⌋.

theorem ZLattice.IsIntegral.signedDiscr_cast {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] [MeasurableSpace E] [BorelSpace E] (h : IsIntegral L) : ↑(signedDiscr L) = (-1) ^ (Module.finrank ℝ E / 2) * det L

Cast to ℝ, the signed discriminant of an integral full lattice is (-1) ^ ⌊finrank ℝ E / 2⌋ * det L.

theorem ZLattice.IsIntegral.signedDiscr_eq_neg_one_pow_mul_det_toMatrix {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L) : signedDiscr L = (-1) ^ (Module.finrank ℝ E / 2) * ((LinearMap.BilinForm.toMatrix b) h.integralForm).det

In any ℤ-basis b of an integral full lattice L, the signed discriminant is (-1) ^ ⌊finrank ℝ E / 2⌋ times the determinant of the integral Gram matrix of b.

theorem ZLattice.IsEven.signedDiscr_eq_one_of_isUnimodular {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsEven L) (hU : IsUnimodular L) : signedDiscr L = 1

An even unimodular full lattice has signed discriminant 1, since its rank is divisible by 4 (ZLattice.IsEven.four_dvd_finrank_of_level_dvd_two).

theorem ZLattice.IsIntegral.signedDiscr_sqrt_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) {m : ℕ} (hm : m ≠ 0) : signedDiscr (√↑m • L) = ↑m ^ Module.finrank ℝ E * signedDiscr L

Scaling an integral full lattice L of rank n by √m (m ≠ 0) multiplies its signed discriminant by mⁿ.

theorem ZLattice.signedDiscr_span_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [Fintype ι] (b : OrthonormalBasis ι ℝ E) : signedDiscr (Submodule.span ℤ (Set.range ⇑b)) = (-1) ^ (Fintype.card ι / 2)

The ℤ-span of an orthonormal basis indexed by ι has signed discriminant (-1) ^ ⌊|ι| / 2⌋.

theorem ZLattice.signedDiscr_sqrt_smul_span_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ι : Type u_3} [Fintype ι] (b : OrthonormalBasis ι ℝ E) {m : ℕ} (hm : m ≠ 0) : signedDiscr (√↑m • Submodule.span ℤ (Set.range ⇑b)) = (-1) ^ (Fintype.card ι / 2) * ↑m ^ Fintype.card ι

For an orthonormal basis b indexed by ι and m ≠ 0, the scaled cubic lattice √m • ℤ b has signed discriminant (-1) ^ ⌊|ι| / 2⌋ * m ^ |ι|. In particular √2 • ℤ² has signed discriminant -4.

theorem ZLattice.IsIntegral.mul_signedDiscr_sqrt_level_smul_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) : signedDiscr L * signedDiscr (√↑(level L) • dual L) = ↑(level L) ^ Module.finrank ℝ E

Fricke partner product identity. For an integral full lattice L of rank n and level N, the signed discriminants of L and of its Fricke partner √N • L^∨ multiply to Nⁿ.

theorem ZLattice.IsIntegral.isSquare_mul_signedDiscr_sqrt_level_smul_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) (hE : Even (Module.finrank ℝ E)) : IsSquare (signedDiscr L * signedDiscr (√↑(level L) • dual L))

In even ambient dimension, the product of the signed discriminants of an integral full lattice and of its Fricke partner is an integer square.

Comparison with the rational and real models

theorem ZLattice.IsIntegral.signedDiscr_eq_ratModel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : signedDiscr L = (-1) ^ (Module.finrank ℤ ↥(ratModel hL).carrier / 2) * (ratModel hL).determinant

The signed discriminant of an integral full lattice agrees with the signed determinant of its rational model.

theorem ZLattice.IsIntegral.signedDiscr_rationalFormClass_ratModel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : (ratModel hL).rationalFormClass.signedDiscr = TauCeti.squareClass (Units.mk0 ↑(signedDiscr L) ⋯)

Rational square-class bridge. For any integral full lattice L (in even or odd dimension), the signed discriminant RegularFormClass.signedDiscr of the ambient rational quadratic form of ratModel hL is the square class of signedDiscr L in ℚˣ.

Level coprimality and the Kronecker character

theorem ZLattice.coprime_natAbs_signedDiscr_of_coprime_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {a : ℕ} (ha : a.Coprime (level L)) : a.Coprime (signedDiscr L).natAbs

Any natural number coprime to level L is coprime to |signedDiscr L|.

theorem ZLattice.isCoprime_signedDiscr_of_isCoprime_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] {d : ℤ} (hd : IsCoprime d ↑(level L)) : IsCoprime d (signedDiscr L)

Every integer coprime to level L is coprime to signedDiscr L.

theorem ZLattice.IsEven.signedDiscr_modEq_zero_or_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (hE : Even (Module.finrank ℝ E)) : signedDiscr L ≡ 0 [ZMOD 4] ∨ signedDiscr L ≡ 1 [ZMOD 4]

The signed discriminant of an even full lattice of even rank is a discriminant, congruent to 0 or 1 modulo 4.

theorem ZLattice.IsEven.kroneckerChar_signedDiscr_neg_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (R : Type u_3) [CommRing R] (hL : IsEven L) {k : ℕ} (hk : Module.finrank ℝ E = 2 * k) : (TauCeti.kroneckerChar R (signedDiscr L) ⋯ ⋯) (-1) = (-1) ^ k

Parity of the Kronecker character of an even lattice. For an even full lattice L of rank 2k, the Kronecker character (D_L / ·) takes the value (-1)^k at -1.

theorem ZLattice.IsIntegral.signedDiscr_sqrt_smul_ne_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) {m : ℕ} (hm : m ≠ 0) : signedDiscr (√↑m • L) ≠ 0

The signed discriminant of √m • L (m ≠ 0) for an integral full lattice L is nonzero.

theorem ZLattice.IsEven.signedDiscr_sqrt_smul_modEq_zero_or_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (hE : Even (Module.finrank ℝ E)) {m : ℕ} (hm : m ≠ 0) : signedDiscr (√↑m • L) ≡ 0 [ZMOD 4] ∨ signedDiscr (√↑m • L) ≡ 1 [ZMOD 4]

For an even full lattice L of even rank and m ≠ 0, signedDiscr (√m • L) is congruent to 0 or 1 modulo 4.

theorem ZLattice.IsEven.conductor_kroneckerChar_signedDiscr_sqrt_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (R : Type u_3) [CommRing R] (hL : IsEven L) (hE : Even (Module.finrank ℝ E)) {m : ℕ} (hm : m ≠ 0) : (TauCeti.kroneckerChar R (signedDiscr (√↑m • L)) ⋯ ⋯).conductor = (TauCeti.kroneckerChar R (signedDiscr L) ⋯ ⋯).conductor

In even ambient dimension, scaling an even full lattice L by √m (m ≠ 0) preserves the conductor of its Kronecker character (D_L / ·).

theorem ZLattice.IsEven.primitiveCharacter_kroneckerChar_signedDiscr_sqrt_smul_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (R : Type u_3) [CommRing R] (hL : IsEven L) (hE : Even (Module.finrank ℝ E)) {m : ℕ} (hm : m ≠ 0) (a : ℤ) : (TauCeti.kroneckerChar R (signedDiscr (√↑m • L)) ⋯ ⋯).primitiveCharacter ↑a = (TauCeti.kroneckerChar R (signedDiscr L) ⋯ ⋯).primitiveCharacter ↑a

In even ambient dimension, scaling an even full lattice L by √m (m ≠ 0) preserves the primitive character values of (D_L / ·) at every integer a.

theorem ZLattice.IsIntegral.signedDiscr_sqrt_level_smul_dual_ne_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) : signedDiscr (√↑(level L) • dual L) ≠ 0

The signed discriminant of the Fricke partner √(level L) • L^∨ of an integral full lattice is nonzero.

theorem ZLattice.IsIntegral.signedDiscr_sqrt_level_smul_dual_modEq_zero_or_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) (hE : Even (Module.finrank ℝ E)) : signedDiscr (√↑(level L) • dual L) ≡ 0 [ZMOD 4] ∨ signedDiscr (√↑(level L) • dual L) ≡ 1 [ZMOD 4]

In even ambient dimension, the signed discriminant of the Fricke partner √(level L) • L^∨ of an integral full lattice is congruent to 0 or 1 modulo 4.

theorem ZLattice.IsEven.conductor_kroneckerChar_signedDiscr_sqrt_level_smul_dual {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (R : Type u_3) [CommRing R] (hL : IsEven L) (hE : Even (Module.finrank ℝ E)) : (TauCeti.kroneckerChar R (signedDiscr (√↑(level L) • dual L)) ⋯ ⋯).conductor = (TauCeti.kroneckerChar R (signedDiscr L) ⋯ ⋯).conductor

Fricke invariance of the Kronecker conductor. For an even full lattice L of even rank and level N, the Kronecker characters of L and of its Fricke partner √N • L^∨ have the same conductor.

theorem ZLattice.IsEven.primitiveCharacter_kroneckerChar_signedDiscr_sqrt_level_smul_dual_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (R : Type u_3) [CommRing R] (hL : IsEven L) (hE : Even (Module.finrank ℝ E)) (a : ℤ) : (TauCeti.kroneckerChar R (signedDiscr (√↑(level L) • dual L)) ⋯ ⋯).primitiveCharacter ↑a = (TauCeti.kroneckerChar R (signedDiscr L) ⋯ ⋯).primitiveCharacter ↑a

Fricke invariance of the primitive Kronecker character. For an even full lattice L of even rank and level N, the primitive Kronecker characters of L and of its Fricke partner √N • L^∨ agree at every integer a.

Non-integral rank-one boundary examples

theorem ZLattice.signedDiscr_span_singleton_of_irrational_sq {c : ℝ} (hc : Irrational (c ^ 2)) : signedDiscr (ℤ ∙ c) = 0

When c² is irrational, signedDiscr (c ℤ) = 0.

theorem ZLattice.inf_dual_span_two_rpow_one_quarter : ℤ ∙ 2 ^ (1 / 4) ⊓ dual (ℤ ∙ 2 ^ (1 / 4)) = ⊥

Non-integral boundary check: L = 2 ^ (1 / 4) ℤ ⊆ ℝ meets its dual 2 ^ (-1 / 4) ℤ only at 0.

theorem ZLattice.infinite_discriminantGroup_span_two_rpow_one_quarter : Infinite (DiscriminantGroup (ℤ ∙ 2 ^ (1 / 4)))

Non-integral boundary check: L = 2 ^ (1 / 4) ℤ ⊆ ℝ has infinite discriminant group.

theorem ZLattice.infinite_quotient_smul_dual_inf_span_two_rpow_one_quarter (a : ℝ) : Infinite (↥(dual (ℤ ∙ 2 ^ (1 / 4))) ⧸ (a • dual (ℤ ∙ 2 ^ (1 / 4)) ⊓ ℤ ∙ 2 ^ (1 / 4)).submoduleOf (dual (ℤ ∙ 2 ^ (1 / 4))))

Non-integral boundary check: for L = 2 ^ (1 / 4) ℤ ⊆ ℝ and every a : ℝ, the quotient L^∨ ⧸ (L^∨ ∩ a L^∨ ∩ L) is infinite.

theorem ZLattice.signedDiscr_span_two_rpow_one_quarter : signedDiscr (ℤ ∙ 2 ^ (1 / 4)) = 0

Non-integral boundary check: L = 2 ^ (1 / 4) ℤ ⊆ ℝ has signedDiscr L = 0.

@[simp]

theorem TauCeti.IntegralLattice.signedDiscr_realModel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : ZLattice.signedDiscr (M.realModel hM) = (-1) ^ (Module.finrank ℤ ↥M.carrier / 2) * M.determinant

The signed discriminant of the real model of a positive definite rational lattice M is (-1) ^ ⌊finrank ℤ M / 2⌋ * M.determinant.