Fundamental parallelograms of complex lattices

DefinitionFundamental parallelogram#✓fully proved

Let \(\omega_1, \omega_2\) be \(\mathbb{R}\)-linearly independent complex numbers and let \(\alpha \in \mathbb{C}\). The fundamental parallelogram with vertex \(\alpha\) is the half-open parallelogram \(\alpha + P\), where \(P\) is the set of \(z \in \mathbb{C}\) whose two coordinates in the \(\mathbb{R}\)-basis \(\omega_1, \omega_2\) of \(\mathbb{C}\) both lie in \([0, 1)\); that is, \(P = \{t_1 \omega_1 + t_2 \omega_2 : t_1, t_2 \in [0, 1)\}\).

noncomputable def fundamentalParallelogram (L : PeriodPair) (α : ℂ) : Set ℂ :=
  (α + ·) '' ZSpan.fundamentalDomain L.basis

Used by 6

Used byFundamental parallelogram at the origin · Membership in a fundamental parallelogram · Fundamental parallelograms are bounded · Membership in the pole set of a fundamental parallelogram · Poles in a fundamental parallelogram · Finitely many poles in a fundamental parallelogram

TheoremFundamental parallelogram at the origin#✓fully proved

Let \(\omega_1, \omega_2\) be \(\mathbb{R}\)-linearly independent complex numbers. The fundamental parallelogram with vertex \(0\) equals the set of \(z \in \mathbb{C}\) whose two coordinates in the \(\mathbb{R}\)-basis \(\omega_1, \omega_2\) of \(\mathbb{C}\) both lie in \([0, 1)\).

@[simp]
theorem fundamentalParallelogram_zero (L : PeriodPair) :
    L.fundamentalParallelogram 0 = ZSpan.fundamentalDomain L.basis

Uses 1

Statement usesFundamental parallelogram

LemmaCoordinates in the period basis#✓fully proved

Let \(\omega_1, \omega_2\) be \(\mathbb{R}\)-linearly independent complex numbers, so that they form a basis of \(\mathbb{C}\) over \(\mathbb{R}\). For all real numbers \(t_1, t_2\), the first coordinate of \(t_1 \omega_1 + t_2 \omega_2\) in this basis is \(t_1\) and the second is \(t_2\).

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

Used by 1

Used byMembership in a fundamental parallelogram

TheoremMembership in a fundamental parallelogram#✓fully proved

Let \(\omega_1, \omega_2\) be \(\mathbb{R}\)-linearly independent complex numbers and let \(\alpha, z \in \mathbb{C}\). Then \(z\) lies in the fundamental parallelogram with vertex \(\alpha\) if and only if there are real numbers \(t_1, t_2\) with \(0 \le t_1 < 1\) and \(0 \le t_2 < 1\) such that \(z = \alpha + t_1 \omega_1 + t_2 \omega_2\).

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

Uses 2 · Used by 1

Statement usesFundamental parallelogram

Proof usesCoordinates in the period basis

Used byFundamental parallelograms are bounded

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.