@[reducible, inline]

abbrev ComplexLattice : Type

A complex lattice is identified with a PeriodPair: a pair (ω₁, ω₂) of complex numbers that are linearly independent over ℝ, generating a rank-2 ℤ-lattice in ℂ.

def ComplexLattice.mk' (ω₁ ω₂ : ℂ) (h : LinearIndependent ℝ ![ω₁, ω₂]) : ComplexLattice

Construct a complex lattice from two periods ω₁, ω₂ : ℂ together with a proof that they are linearly independent over ℝ.

theorem ComplexLattice.linearIndependent (L : ComplexLattice) : LinearIndependent ℝ ![L.ω₁, L.ω₂]

The two periods ω₁, ω₂ of a complex lattice are linearly independent over ℝ.

theorem ComplexLattice.mem_lattice_iff (L : ComplexLattice) {x : ℂ} : x ∈ PeriodPair.lattice L ↔ ∃ (n₁ : ℤ) (n₂ : ℤ), ↑n₁ * L.ω₁ + ↑n₂ * L.ω₂ = x

A complex number x lies in the lattice L iff it has an integer expression n₁ ω₁ + n₂ ω₂ in terms of the lattice's periods.

theorem ComplexLattice.ω₁_mem (L : ComplexLattice) : L.ω₁ ∈ PeriodPair.lattice L

The first period ω₁ belongs to the lattice L.

theorem ComplexLattice.ω₂_mem (L : ComplexLattice) : L.ω₂ ∈ PeriodPair.lattice L

The second period ω₂ belongs to the lattice L.

instance ComplexLattice.discreteTopology_lattice (L : ComplexLattice) : DiscreteTopology ↥(PeriodPair.lattice L)

The subgroup underlying a complex lattice carries the discrete topology induced from ℂ.

instance ComplexLattice.isZLattice_lattice (L : ComplexLattice) : IsZLattice ℝ (PeriodPair.lattice L)

A complex lattice is a ℤ-lattice in ℂ (viewed as an ℝ-vector space).

theorem ComplexLattice.finrank_eq_two (L : ComplexLattice) : Module.finrank ℤ ↥(PeriodPair.lattice L) = 2

The complex lattice has ℤ-rank equal to 2.

noncomputable def ComplexLattice.intBasis (L : ComplexLattice) : Module.Basis (Fin 2) ℤ ↥(PeriodPair.lattice L)

A ℤ-basis of the lattice of size 2, given by the two periods of L.

noncomputable def ComplexLattice.equivIntProd (L : ComplexLattice) : ↥(PeriodPair.lattice L) ≃ₗ[ℤ] ℤ × ℤ

The ℤ-linear equivalence between the lattice L and ℤ × ℤ provided by the basis of periods.

theorem ComplexLattice.isClosed (L : ComplexLattice) : IsClosed ↑(PeriodPair.lattice L)

A complex lattice is a closed subset of ℂ.

noncomputable def ComplexLattice.toAddSubgroup (L : ComplexLattice) : AddSubgroup ℂ

The complex lattice viewed as an additive subgroup of ℂ.

theorem ComplexLattice.linearIndependent_int (L : ComplexLattice) (a b : ℤ) : a • L.ω₁ + b • L.ω₂ = 0 → a = 0 ∧ b = 0

The periods ω₁, ω₂ of a complex lattice are linearly independent over ℤ: the only integer combination summing to 0 is the trivial one.

def ComplexLattice.toSet (L : ComplexLattice) : Set ℂ

The lattice as a set: all complex numbers of the form a • ω₁ + b • ω₂ with a, b ∈ ℤ.

def ComplexLattice.IsNormalized (L : ComplexLattice) : Prop

A complex lattice L is normalized if ω₂ / ω₁ lies in the upper half plane, i.e. its imaginary part is positive.

def ComplexLattice.IsHomothetic (L L' : ComplexLattice) : Prop

Two complex lattices L and L' are homothetic if there is a nonzero complex scalar c such that L' (as a set in ℂ) equals c • L.

theorem ComplexLattice.IsHomothetic.refl (L : ComplexLattice) : L.IsHomothetic L

Homothety is reflexive: any lattice is homothetic to itself via the scalar 1.

theorem ComplexLattice.IsHomothetic.symm {L L' : ComplexLattice} (h : L.IsHomothetic L') : L'.IsHomothetic L

Homothety is symmetric: if L and L' are homothetic via c, they are homothetic via c⁻¹ the other way.

theorem ComplexLattice.IsHomothetic.trans {L₁ L₂ L₃ : ComplexLattice} (h₁₂ : L₁.IsHomothetic L₂) (h₂₃ : L₂.IsHomothetic L₃) : L₁.IsHomothetic L₃

Homothety is transitive: composing two homotheties yields a homothety.

theorem ComplexLattice.isHomothetic_equivalence : Equivalence IsHomothetic

Homothety of complex lattices is an equivalence relation.

noncomputable def ComplexLattice.discriminantLattice (L : ComplexLattice) : ℂ

The discriminant g₂³ - 27·g₃² of the Weierstrass cubic associated to the lattice.

@[simp]

theorem ComplexLattice.discriminantLattice_def (L : ComplexLattice) : L.discriminantLattice = PeriodPair.g₂ L ^ 3 - 27 * PeriodPair.g₃ L ^ 2

Definitional equation for the discriminant of a complex lattice.

noncomputable def ComplexLattice.jInvariantLattice (L : ComplexLattice) : ℂ

The j-invariant of a complex lattice, given by 1728 g₂³ / Δ where Δ is the discriminant.

@[simp]

theorem ComplexLattice.jInvariantLattice_def (L : ComplexLattice) : L.jInvariantLattice = 1728 * PeriodPair.g₂ L ^ 3 / (PeriodPair.g₂ L ^ 3 - 27 * PeriodPair.g₃ L ^ 2)

Definitional equation for the j-invariant of a complex lattice.

def ComplexLattice.fundamentalParallelogram (L : ComplexLattice) (α : ℂ) : Set ℂ

The fundamental parallelogram translated by α: the image of the fundamental domain of L under translation by α.

@[simp]

theorem ComplexLattice.fundamentalParallelogram_zero (L : ComplexLattice) : L.fundamentalParallelogram 0 = ZSpan.fundamentalDomain (PeriodPair.basis L)

When the translation is 0, the fundamental parallelogram coincides with the standard fundamental domain of the lattice.

theorem ComplexLattice.basis_repr_omega (L : ComplexLattice) (t₁ t₂ : ℝ) (i : Fin 2) : ((PeriodPair.basis L).repr (t₁ • L.ω₁ + t₂ • L.ω₂)) i = ![t₁, t₂] i

The coordinates of t₁ ω₁ + t₂ ω₂ with respect to the basis (ω₁, ω₂) are exactly t₁ and t₂.

theorem ComplexLattice.mem_fundamentalParallelogram_iff (L : ComplexLattice) {α z : ℂ} : z ∈ L.fundamentalParallelogram α ↔ ∃ (t₁ : ℝ) (t₂ : ℝ), 0 ≤ t₁ ∧ t₁ < 1 ∧ 0 ≤ t₂ ∧ t₂ < 1 ∧ z = α + t₁ • L.ω₁ + t₂ • L.ω₂

A point z lies in the fundamental parallelogram based at α iff it can be written as α + t₁ ω₁ + t₂ ω₂ with 0 ≤ t₁, t₂ < 1.

noncomputable def ComplexLattice.quotientEquivFundDomain (L : ComplexLattice) : ℂ ⧸ PeriodPair.lattice L ≃ ↑(ZSpan.fundamentalDomain (PeriodPair.basis L))

The quotient ℂ / L is in bijection with the fundamental domain of the lattice: every coset has a unique representative in the fundamental parallelogram.