Homothetic complex period lattices

DefinitionHomothetic period pairs#✓fully proved

A period pair is a pair \((\omega_1, \omega_2)\) of complex numbers that are linearly independent over \(\mathbb{R}\), and its lattice is \(\Lambda = \mathbb{Z}\omega_1 + \mathbb{Z}\omega_2 \subseteq \mathbb{C}\). Two period pairs \(L\) and \(L'\) with lattices \(\Lambda\) and \(\Lambda'\) are homothetic when there is a nonzero complex number \(c\) such that \(\Lambda' = c\Lambda = \{c\lambda : \lambda \in \Lambda\}\).

def IsHomothetic (L L' : PeriodPair) : Prop :=
  ∃ c : ℂ, c ≠ 0 ∧ (L'.lattice : Set ℂ) = c • (L.lattice : Set ℂ)

Used by 4

Used byHomothety of period pairs is an equivalence relation · Homothety of period pairs is reflexive · Homothety of period pairs is symmetric · Homothety of period pairs is transitive

TheoremHomothety of period pairs is reflexive#✓fully proved

Every period pair \(L\) is homothetic to itself.

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

Uses 1 · Used by 1

Statement usesHomothetic period pairs

Used byHomothety of period pairs is an equivalence relation

TheoremHomothety of period pairs is symmetric#✓fully proved

If a period pair \(L\) is homothetic to a period pair \(L'\), then \(L'\) is homothetic to \(L\).

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

Uses 1 · Used by 1

Statement usesHomothetic period pairs

Used byHomothety of period pairs is an equivalence relation

TheoremHomothety of period pairs is transitive#✓fully proved

For period pairs \(L_1\), \(L_2\), \(L_3\), if \(L_1\) is homothetic to \(L_2\) and \(L_2\) is homothetic to \(L_3\), then \(L_1\) is homothetic to \(L_3\).

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

Uses 1 · Used by 1

Statement usesHomothetic period pairs

Used byHomothety of period pairs is an equivalence relation

TheoremHomothety of period pairs is an equivalence relation#✓fully proved

On period pairs, homothety is reflexive, symmetric and transitive.

theorem isHomothetic_equivalence : Equivalence IsHomothetic

Uses 4

Statement usesHomothetic period pairs

Proof usesHomothety of period pairs is reflexive · Homothety of period pairs is symmetric · Homothety of period pairs is transitive

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.