Complex characters of the discriminant form

For an integral full lattice L, this file transports IntegralLattice.discriminantPairing through ZLattice.ratModelDiscriminantGroupEquiv and composes it with TauCeti.expCircle. The resulting ZLattice.IsIntegral.discriminantPairingChar is the complex additive character δ ↦ e(b_L(γ, δ)) of the discriminant group A_L = L^∨ ⧸ L. On representatives x, y ∈ L^∨, its value is exp (2πi ⟪x, y⟫). It is symmetric and additive in the two classes and has norm one.

When L is moreover even, transporting IntegralLattice.discriminantQuadraticMap through the same equivalence and composing with TauCeti.expCircle gives ZLattice.IsEven.discriminantQuadraticChar, the complex quadratic phase γ ↦ e(q_L(γ)) on A_L. On a representative x ∈ L^∨, its value is exp (πi ‖x‖²). It satisfies the quadratic refinement law e(q_L(γ + δ)) = e(q_L(γ)) e(q_L(δ)) e(b_L(γ, δ)), is even (e(q_L(-γ)) = e(q_L(γ))), scales by n² in the exponent on scalar multiples n • γ, has level L as the least positive exponent killing all of its values, and gives the eigenvalue by which the modular translation T : τ ↦ τ + 1 acts on the coset theta series θ_γ.

Main definitions

• ZLattice.IsIntegral.discriminantPairingChar: the additive character δ ↦ e(b_L(γ, δ)) of DiscriminantGroup L for an integral full lattice L.
• ZLattice.IsEven.discriminantQuadraticChar: the quadratic phase γ ↦ e(q_L(γ)) on DiscriminantGroup L for an even full lattice L.

Main statements

• ZLattice.IsIntegral.discriminantPairingChar_mk_mk: on x, y ∈ L^∨, e(b_L(x, y)) = exp (2πi ⟪x, y⟫).
• ZLattice.IsEven.discriminantQuadraticChar_mk: on x ∈ L^∨, e(q_L(x)) = exp (πi ‖x‖²).
• ZLattice.IsEven.discriminantQuadraticChar_add: e(q_L(γ + δ)) = e(q_L(γ)) e(q_L(δ)) e(b_L(γ, δ)).
• ZLattice.IsEven.discriminantQuadraticChar_nsmul, ZLattice.IsEven.discriminantQuadraticChar_zsmul: e(q_L(n • γ)) = e(q_L(γ))^(n²).
• ZLattice.IsEven.discriminantQuadraticChar_pow_eq_one_iff: e(q_L(γ))^n = 1 if and only if n • q_L(γ) = 0.
• ZLattice.IsEven.level_dvd_iff_discriminantQuadraticChar_pow_eq_one, ZLattice.IsEven.discriminantQuadraticChar_pow_level: level L ∣ N if and only if e(q_L(γ))^N = 1 for every γ : DiscriminantGroup L.
• ZLattice.IsEven.cexp_two_pi_mul_I_div_eq_discriminantQuadraticChar_iff: exp (2πi m / N) = e(q_L(γ)) if and only if m mod N maps to q_L(γ) under ZMod.toRatAddCircle N.

References

• W. Ebeling, Lattices and Codes, 3rd ed., Chapter 2.

noncomputable def ZLattice.IsIntegral.discriminantPairingChar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (γ : DiscriminantGroup L) : AddChar (DiscriminantGroup L) ℂ

The complex additive character δ ↦ e(b_L(γ, δ)) of the discriminant group, obtained from its rational-model discriminant pairing.

theorem ZLattice.IsIntegral.discriminantPairingChar_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (γ δ : DiscriminantGroup L) : (hL.discriminantPairingChar γ) δ = TauCeti.expCircle (((ratModel hL).discriminantPairing ((ratModelDiscriminantGroupEquiv hL) γ)) ((ratModelDiscriminantGroupEquiv hL) δ))

The discriminant character is the exponential of the existing rational discriminant pairing, transported through the bridge.

@[simp]

theorem ZLattice.IsIntegral.discriminantPairingChar_mk_mk {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (x y : ↥(dual L)) : (hL.discriminantPairingChar (Submodule.Quotient.mk x)) (Submodule.Quotient.mk y) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ ↑x ↑y))

On representatives in the dual lattice the character is exp (2πi ⟪x, y⟫).

theorem ZLattice.IsIntegral.discriminantPairingChar_comm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (γ δ : DiscriminantGroup L) : (hL.discriminantPairingChar γ) δ = (hL.discriminantPairingChar δ) γ

The discriminant pairing character is symmetric in its two class arguments.

@[simp]

theorem ZLattice.IsIntegral.discriminantPairingChar_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : hL.discriminantPairingChar 0 = 0

The zero class gives the trivial character.

@[simp]

theorem ZLattice.IsIntegral.discriminantPairingChar_add_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (γ δ : DiscriminantGroup L) : hL.discriminantPairingChar (γ + δ) = hL.discriminantPairingChar γ + hL.discriminantPairingChar δ

Addition in the first class argument multiplies the corresponding characters.

@[simp]

theorem ZLattice.IsIntegral.discriminantPairingChar_neg_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (γ : DiscriminantGroup L) : hL.discriminantPairingChar (-γ) = -hL.discriminantPairingChar γ

Negation in the first class argument negates the corresponding character.

@[simp]

theorem ZLattice.IsIntegral.norm_discriminantPairingChar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (γ δ : DiscriminantGroup L) : ‖(hL.discriminantPairingChar γ) δ‖ = 1

Every value of the discriminant pairing character has norm one.

noncomputable def ZLattice.IsEven.discriminantQuadraticChar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) : ℂ

The complex quadratic phase γ ↦ e(q_L(γ)) on the discriminant group of an even full lattice, obtained by composing TauCeti.expCircle with the discriminant quadratic map of its rational model.

theorem ZLattice.IsEven.discriminantQuadraticChar_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) : hL.discriminantQuadraticChar γ = TauCeti.expCircle (((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ))

discriminantQuadraticChar is the exponential of the rational-model discriminant quadratic map, transported across ratModelDiscriminantGroupEquiv.

@[simp]

theorem ZLattice.IsEven.discriminantQuadraticChar_mk {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (x : ↥(dual L)) : hL.discriminantQuadraticChar (Submodule.Quotient.mk x) = Complex.exp (↑Real.pi * Complex.I * ↑(‖↑x‖ ^ 2))

On a representative x ∈ L^∨, the quadratic phase e(q_L(x + L)) is exp (πi ‖x‖²).

@[simp]

theorem ZLattice.IsEven.discriminantQuadraticChar_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) : hL.discriminantQuadraticChar 0 = 1

At the zero class of L^∨ ⧸ L, the quadratic phase is 1.

@[simp]

theorem ZLattice.IsEven.discriminantQuadraticChar_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) : hL.discriminantQuadraticChar (-γ) = hL.discriminantQuadraticChar γ

The quadratic phase is even on the discriminant group: e(q_L(-γ)) = e(q_L(γ)).

theorem ZLattice.IsEven.discriminantQuadraticChar_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ δ : DiscriminantGroup L) : hL.discriminantQuadraticChar (γ + δ) = hL.discriminantQuadraticChar γ * hL.discriminantQuadraticChar δ * (⋯.discriminantPairingChar γ) δ

Quadratic refinement. On the discriminant group of an even full lattice, e(q_L(γ + δ)) = e(q_L(γ)) e(q_L(δ)) e(b_L(γ, δ)).

theorem ZLattice.IsEven.discriminantQuadraticChar_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ δ : DiscriminantGroup L) : hL.discriminantQuadraticChar (γ - δ) = hL.discriminantQuadraticChar γ * hL.discriminantQuadraticChar δ * (⋯.discriminantPairingChar γ) (-δ)

On differences in the discriminant group, e(q_L(γ - δ)) = e(q_L(γ)) e(q_L(δ)) e(b_L(γ, -δ)).

theorem ZLattice.IsEven.discriminantQuadraticChar_nsmul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (n : ℕ) (γ : DiscriminantGroup L) : hL.discriminantQuadraticChar (n • γ) = hL.discriminantQuadraticChar γ ^ n ^ 2

Scaling a discriminant class by n : ℕ raises its quadratic phase to the n²-th power.

theorem ZLattice.IsEven.discriminantQuadraticChar_zsmul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (n : ℤ) (γ : DiscriminantGroup L) : hL.discriminantQuadraticChar (n • γ) = hL.discriminantQuadraticChar γ ^ n ^ 2

Scaling a discriminant class by n : ℤ raises its quadratic phase to the n²-th power.

@[simp]

theorem ZLattice.IsEven.norm_discriminantQuadraticChar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) : ‖hL.discriminantQuadraticChar γ‖ = 1

Every value of the discriminant quadratic phase has norm one.

theorem ZLattice.IsEven.discriminantQuadraticChar_ne_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) : hL.discriminantQuadraticChar γ ≠ 0

Every value of the discriminant quadratic phase is nonzero.

@[simp]

theorem ZLattice.IsEven.conj_discriminantQuadraticChar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) : (starRingEnd ℂ) (hL.discriminantQuadraticChar γ) = (hL.discriminantQuadraticChar γ)⁻¹

Complex conjugation inverts the discriminant quadratic phase.

theorem ZLattice.IsEven.discriminantQuadraticChar_eq_one_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) : hL.discriminantQuadraticChar γ = 1 ↔ ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ) = 0

e(q_L(γ)) = 1 if and only if q_L(γ) = 0 in ℚ/ℤ.

theorem ZLattice.IsEven.discriminantQuadraticChar_pow_eq_one_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) (n : ℕ) : hL.discriminantQuadraticChar γ ^ n = 1 ↔ n • ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ) = 0

e(q_L(γ))^n = 1 if and only if n annihilates q_L(γ) in ℚ/ℤ.

theorem ZLattice.IsEven.level_dvd_iff_discriminantQuadraticChar_pow_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) {N : ℕ} : level L ∣ N ↔ ∀ (γ : DiscriminantGroup L), hL.discriminantQuadraticChar γ ^ N = 1

For an even full lattice L, level L ∣ N if and only if e(q_L(γ)) ^ N = 1 for every γ : DiscriminantGroup L.

@[simp]

theorem ZLattice.IsEven.discriminantQuadraticChar_pow_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) : hL.discriminantQuadraticChar γ ^ level L = 1

The level L-th power of every discriminant quadratic phase e(q_L(γ)) is 1.

theorem ZLattice.IsEven.cexp_two_pi_mul_I_div_eq_discriminantQuadraticChar_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) (N : ℕ) (m : ℤ) : Complex.exp (2 * ↑Real.pi * Complex.I * (↑↑m / ↑N)) = hL.discriminantQuadraticChar γ ↔ (ZMod.toRatAddCircle N) ↑m = ((ratModel ⋯).discriminantQuadraticMap ⋯) ((ratModelDiscriminantGroupEquiv ⋯) γ)

The complex phase exp (2πi m / N) agrees with e(q_L(γ)) exactly when the residue of m modulo N maps to q_L(γ) under ZMod.toRatAddCircle N.