Coset theta series on the discriminant group

Let L be a lattice in a real inner product space E, with dual lattice L^∨ = ZLattice.dual L and discriminant group A_L = L^∨ ⧸ (L ∩ L^∨) (ZLattice.DiscriminantGroup L). The theta series θ_{γ+L} of a translate depends only on the class of γ modulo L (ZLattice.thetaCoset_eq_of_sub_mem), so the coset theta series descend to a family (θ_γ)_{γ ∈ A_L} indexed by the discriminant group, ZLattice.thetaCosetClass L. This descent needs no hypothesis on L. This is the family that the vector-valued inversion law of coset theta series is stated for. It satisfies θ_0 = Θ_L and θ_{-γ} = θ_γ; in particular, whenever A_L has an element γ ≠ -γ, the family is not linearly independent.

For an even lattice L (in arbitrary dimension, without discreteness or fullness), every coset theta series θ_γ (γ ∈ A_L) has period level L and is invariant under T ^ level L in every weight (ZLattice.IsEven.thetaCosetClass_slash_T_pow_level), descending from the representative-level invariance ZLattice.IsEven.thetaCoset_slash_T_pow_level. When L is an even full lattice, the modular translation T : τ ↦ τ + 1 acts on θ_γ with eigenvalue e(q_L(γ)) (ZLattice.IsEven.thetaCosetClass_slash_T), where e(q_L(γ)) is ZLattice.IsEven.discriminantQuadraticChar, and level L is the least positive exponent killing all of these eigenvalues (ZLattice.IsEven.level_dvd_iff_discriminantQuadraticChar_pow_eq_one).

For an integral full lattice, A_L = L^∨ ⧸ L is finite and the theta series of the dual lattice is the sum of the coset theta series, Θ_{L^∨} = ∑_{γ ∈ A_L} θ_γ (ZLattice.IsIntegral.thetaSeries_dual_eq_sum), by splitting L^∨ into the cosets of L. Integrality is needed: for L = ½ ℤ ⊆ ℝ the dual L^∨ = 2 ℤ lies in L, the discriminant group is trivial, and the identity would read Θ_{2ℤ} = Θ_{½ℤ}, which is false.

Main definitions

• ZLattice.thetaCosetClass L: the coset theta series θ_γ of a class γ of the discriminant group of L.

Main statements

• ZLattice.thetaCosetClass_mk: θ_γ is the theta series of the translate γ + L.
• ZLattice.thetaCosetClass_zero, ZLattice.thetaCosetClass_neg: θ_0 = Θ_L, θ_{-γ} = θ_γ.
• ZLattice.IsEven.thetaCosetClass_slash_T_pow_level: θ_γ is invariant under T ^ level L in every weight.
• ZLattice.IsEven.thetaCosetClass_slash_T, ZLattice.IsEven.thetaCosetClass_slash_T_zpow: θ_γ ∣[k] T ^ n = e(q_L(γ))^n • θ_γ for an even full lattice L.
• ZLattice.IsIntegral.thetaSeries_dual_eq_sum: Θ_{L^∨} = ∑_{γ ∈ A_L} θ_γ for integral L.

References

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

noncomputable def ZLattice.thetaCosetClass {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) (γ : DiscriminantGroup L) : UpperHalfPlane → ℂ

The coset theta series θ_γ = θ_{γ+L} of a class γ of the discriminant group L^∨ ⧸ (L ∩ L^∨) of L: the theta series thetaCoset L x of the translate by any representative x ∈ L^∨ of γ (thetaCosetClass_mk).

@[simp]

theorem ZLattice.thetaCosetClass_mk {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) (x : ↥(dual L)) : thetaCosetClass L (Submodule.Quotient.mk x) = thetaCoset L ↑x

The coset theta series of the class of x ∈ L^∨ is the theta series of the translate x + L.

@[simp]

theorem ZLattice.thetaCosetClass_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) : thetaCosetClass L 0 = thetaSeries L

The coset theta series of the zero class is the theta series of L.

@[simp]

theorem ZLattice.thetaCosetClass_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (L : Submodule ℤ E) (γ : DiscriminantGroup L) : thetaCosetClass L (-γ) = thetaCosetClass L γ

The coset theta series of the classes -γ and γ agree.

Translation invariance at the level

theorem ZLattice.IsEven.thetaCosetClass_intCast_vadd_of_level_dvd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsEven L) (γ : DiscriminantGroup L) {N : ℤ} (hN : ↑(level L) ∣ N) (τ : UpperHalfPlane) : thetaCosetClass L γ (↑N +ᵥ τ) = thetaCosetClass L γ τ

For an even lattice L and γ : DiscriminantGroup L, every integer multiple of level L is a period of θ_γ.

@[simp]

theorem ZLattice.IsEven.thetaCosetClass_level_vadd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsEven L) (γ : DiscriminantGroup L) (τ : UpperHalfPlane) : thetaCosetClass L γ (↑(level L) +ᵥ τ) = thetaCosetClass L γ τ

For an even lattice L and γ : DiscriminantGroup L, θ_γ has period level L.

theorem ZLattice.IsEven.thetaCosetClass_slash_T_zpow_of_level_dvd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsEven L) (γ : DiscriminantGroup L) (k : ℤ) {N : ℤ} (hN : ↑(level L) ∣ N) : SlashAction.map k (ModularGroup.T ^ N) (thetaCosetClass L γ) = thetaCosetClass L γ

For an even lattice L and γ : DiscriminantGroup L, θ_γ is invariant under T ^ N in every weight whenever (level L : ℤ) ∣ N.

theorem ZLattice.IsEven.thetaCosetClass_slash_T_zpow_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsEven L) (γ : DiscriminantGroup L) (k : ℤ) : SlashAction.map k (ModularGroup.T ^ ↑(level L)) (thetaCosetClass L γ) = thetaCosetClass L γ

For an even lattice L and γ : DiscriminantGroup L, θ_γ is invariant under T ^ (level L : ℤ) in every weight.

@[simp]

theorem ZLattice.IsEven.thetaCosetClass_slash_T_pow_level {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} (hL : IsEven L) (γ : DiscriminantGroup L) (k : ℤ) : SlashAction.map k (ModularGroup.T ^ level L) (thetaCosetClass L γ) = thetaCosetClass L γ

For an even lattice L and γ : DiscriminantGroup L, θ_γ is invariant under T ^ level L in every weight.

Full lattices

theorem ZLattice.IsIntegral.thetaSeries_dual_eq_sum {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (h : IsIntegral L) [Fintype (DiscriminantGroup L)] (τ : UpperHalfPlane) : thetaSeries (dual L) τ = ∑ γ : DiscriminantGroup L, thetaCosetClass L γ τ

For an integral lattice L, the theta series of the dual lattice is the sum of the coset theta series over the finite discriminant group L^∨ ⧸ L: Θ_{L^∨} = ∑_{γ ∈ A_L} θ_γ. The discriminant group of an integral lattice is finite (IsIntegral.finite_discriminantGroup), so a Fintype instance is always available.

theorem ZLattice.IsEven.thetaCosetClass_intCast_vadd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) (n : ℤ) (τ : UpperHalfPlane) : thetaCosetClass L γ (↑n +ᵥ τ) = hL.discriminantQuadraticChar γ ^ n * thetaCosetClass L γ τ

The translation law of a coset theta series on the discriminant group of an even full lattice: for γ : DiscriminantGroup L and n : ℤ, θ_γ(τ + n) = e(q_L(γ))^n θ_γ(τ).

theorem ZLattice.IsEven.thetaCosetClass_one_vadd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) (τ : UpperHalfPlane) : thetaCosetClass L γ (1 +ᵥ τ) = hL.discriminantQuadraticChar γ * thetaCosetClass L γ τ

For an even full lattice L and γ : DiscriminantGroup L, θ_γ(τ + 1) = e(q_L(γ)) θ_γ(τ).

theorem ZLattice.IsEven.thetaCosetClass_slash_T_zpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) (k n : ℤ) : SlashAction.map k (ModularGroup.T ^ n) (thetaCosetClass L γ) = hL.discriminantQuadraticChar γ ^ n • thetaCosetClass L γ

In slash form, θ_γ ∣[k] T ^ n = e(q_L(γ))^n • θ_γ for an even full lattice L and γ : DiscriminantGroup L.

theorem ZLattice.IsEven.thetaCosetClass_slash_T {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsEven L) (γ : DiscriminantGroup L) (k : ℤ) : SlashAction.map k ModularGroup.T (thetaCosetClass L γ) = hL.discriminantQuadraticChar γ • thetaCosetClass L γ

In slash form, θ_γ ∣[k] T = e(q_L(γ)) • θ_γ for an even full lattice L and γ : DiscriminantGroup L.