Complex multiplication of period lattices

DefinitionEndomorphism ring of a period lattice#✓fully proved

Let \(\omega_1, \omega_2\) be \(\mathbb{R}\)-linearly independent complex numbers with period lattice \(\Lambda = \mathbb{Z}\omega_1 + \mathbb{Z}\omega_2\). The endomorphism ring of \(\Lambda\) is the subring of \(\mathbb{C}\) consisting of all \(a \in \mathbb{C}\) such that \(a z \in \Lambda\) for every \(z \in \Lambda\).

def endomorphismRing (L : PeriodPair) : Subring ℂ where
  carrier := {a | ∀ z ∈ L.lattice, a * z ∈ L.lattice}
  mul_mem' ha hb z hz := by
    rw [mul_assoc]
    exact ha _ (hb z hz)
  one_mem' z hz := by simpa using hz
  add_mem' ha hb z hz := by
    rw [add_mul]
    exact add_mem (ha z hz) (hb z hz)
  zero_mem' _ _ := by simp
  neg_mem' ha z hz := by
    rw [neg_mul]
    exact neg_mem (ha z hz)

Used by 1

Used byLattices that are proper ideals

DefinitionLattices that are proper ideals#✓fully proved

Let \(\Lambda\) be the period lattice of a pair of \(\mathbb{R}\)-linearly independent complex numbers, and let \(\mathcal{O}\) be a subring of \(\mathbb{C}\). Then \(\Lambda\) is a proper ideal of \(\mathcal{O}\) when the endomorphism ring of \(\Lambda\), the subring of all \(a \in \mathbb{C}\) with \(a z \in \Lambda\) for every \(z \in \Lambda\), equals \(\mathcal{O}\).

The ambient assumptions that \(\mathcal{O}\) is an imaginary quadratic order and that \(\Lambda\) is an \(\mathcal{O}\)-ideal are deliberately kept separate from this predicate.

def IsProperIdeal (L : PeriodPair) (𝒪 : Subring ℂ) : Prop :=
  L.endomorphismRing = 𝒪

Uses 1

Statement usesEndomorphism ring of a period lattice

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.