@[reducible, inline]

abbrev ComplexLattice.torusQuot (L : ComplexLattice) : Type

The complex torus ℂ / L associated to a lattice L ⊆ ℂ.

noncomputable def ComplexLattice.proj (L : ComplexLattice) : ℂ →+ L.torusQuot

The canonical quotient map ℂ → ℂ / L, as an additive group homomorphism.

theorem ComplexLattice.proj_eq_iff (L : ComplexLattice) (z w : ℂ) : L.proj z = L.proj w ↔ ∃ v ∈ (PeriodPair.lattice L).toAddSubgroup, z + v = w

Two complex numbers project to the same point in ℂ / L iff they differ by a lattice element.

theorem ComplexLattice.proj_eq_zero_iff (L : ComplexLattice) (z : ℂ) : L.proj z = 0 ↔ z ∈ (PeriodPair.lattice L).toAddSubgroup

A complex number projects to 0 in ℂ / L iff it lies in the lattice L.

def ComplexLattice.latticeMulSet (L₁ L₂ : ComplexLattice) : Set ℂ

The set { α ∈ ℂ : α L₁ ⊆ L₂ } of scalars whose multiplication sends L₁ into L₂.

theorem ComplexLattice.zero_mem_latticeMulSet (L₁ L₂ : ComplexLattice) : 0 ∈ L₁.latticeMulSet L₂

The scalar 0 always sends L₁ into L₂, so it lies in latticeMulSet.

@[simp]

theorem ComplexLattice.mem_latticeMulSet_iff {L₁ L₂ : ComplexLattice} {α : ℂ} : α ∈ L₁.latticeMulSet L₂ ↔ ∀ z ∈ ↑(PeriodPair.lattice L₁), α * z ∈ ↑(PeriodPair.lattice L₂)

Membership in latticeMulSet L₁ L₂ unfolds to the condition α z ∈ L₂ for every z ∈ L₁.

def ComplexLattice.mulByAlphaHom (α : ℂ) : ℂ →+ ℂ

Multiplication by a fixed α : ℂ packaged as an additive group homomorphism ℂ →+ ℂ.

noncomputable def ComplexLattice.inducedMap (L₁ L₂ : ComplexLattice) (α : ℂ) (hα : α ∈ L₁.latticeMulSet L₂) : L₁.torusQuot →+ L₂.torusQuot

For α ∈ latticeMulSet L₁ L₂, the induced morphism ℂ / L₁ → ℂ / L₂ between complex tori obtained by passing multiplication-by-α to the quotient.

@[simp]

theorem ComplexLattice.inducedMap_proj (L₁ L₂ : ComplexLattice) (α : ℂ) (hα : α ∈ L₁.latticeMulSet L₂) (z : ℂ) : (L₁.inducedMap L₂ α hα) (L₁.proj z) = L₂.proj (α * z)

The induced map applied to proj L₁ z equals proj L₂ (α * z).

structure ComplexLattice.ComplexTorusHolMap (L₁ L₂ : ComplexLattice) : Type

A holomorphic morphism between complex tori ℂ / L₁ → ℂ / L₂, packaged together with a holomorphic lift ℂ → ℂ making the projection diagram commute.

• toFun : L₁.torusQuot → L₂.torusQuot
• lift : ℂ → ℂ
• lift_differentiable : Differentiable ℂ self.lift
• diagram_commutes (z : ℂ) : self.toFun (L₁.proj z) = L₂.proj (self.lift z)

theorem ComplexLattice.const_of_continuous_latticeValued (L : ComplexLattice) (g : ℂ → ℂ) (hg : Continuous g) (himg : ∀ (z : ℂ), g z ∈ ↑(PeriodPair.lattice L)) (x y : ℂ) : g x = g y

A continuous function from ℂ (connected) to a lattice (discrete) must be constant.

theorem ComplexLattice.deriv_periodic_of_shift_const (f : ℂ → ℂ) (ω c : ℂ) (hc : ∀ (z : ℂ), f (z + ω) = f z + c) (z : ℂ) : deriv f (z + ω) = deriv f z

If f(z + ω) = f(z) + c for a constant c, then the derivative of f is ω-periodic.

theorem ComplexLattice.affine_of_const_deriv (f : ℂ → ℂ) (hf : Differentiable ℂ f) (α : ℂ) (hderiv_eq : ∀ (w : ℂ), deriv f w = α) (z : ℂ) : f z = α * z + f 0

A differentiable function on ℂ with constant derivative α is affine: f(z) = α z + f(0).

theorem ComplexLattice.periodic_of_generators (f : ℂ → ℂ) (L : ComplexLattice) (hp1 : Function.Periodic f L.ω₁) (hp2 : Function.Periodic f L.ω₂) (z w : ℂ) : w ∈ PeriodPair.lattice L → f (z + w) = f z

A function periodic with respect to the two generators ω₁, ω₂ of a lattice L is periodic with respect to every element of L.

theorem ComplexLattice.entire_periodic_isBounded_range (f : ℂ → ℂ) (hf : Differentiable ℂ f) (L : ComplexLattice) (hp1 : Function.Periodic f L.ω₁) (hp2 : Function.Periodic f L.ω₂) : Bornology.IsBounded (Set.range f)

An entire function that is doubly periodic with respect to a lattice has bounded range (the key input for Liouville's theorem).

theorem ComplexLattice.theorem_16_1_existence (L₁ L₂ : ComplexLattice) (φ : L₁.ComplexTorusHolMap L₂) (hφ0 : φ.toFun 0 = 0) : ∃ (α : ℂ) (hα : α ∈ L₁.latticeMulSet L₂), ∀ (z : ℂ), φ.toFun (L₁.proj z) = (L₁.inducedMap L₂ α hα) (L₁.proj z)

Existence half of Theorem 16.1: every holomorphic morphism ℂ / L₁ → ℂ / L₂ sending 0 to 0 arises from multiplication by some α ∈ ℂ with α L₁ ⊆ L₂.

theorem ComplexLattice.inducedMap_unique (L₁ L₂ : ComplexLattice) (α γ : ℂ) (hα : α ∈ L₁.latticeMulSet L₂) (hγ : γ ∈ L₁.latticeMulSet L₂) (heq : ∀ (z : ℂ), (L₁.inducedMap L₂ α hα) (L₁.proj z) = (L₁.inducedMap L₂ γ hγ) (L₁.proj z)) : α = γ

The scalar α such that inducedMap α = inducedMap γ on all of ℂ / L₁ is uniquely determined.

theorem ComplexLattice.theorem_16_1 (L₁ L₂ : ComplexLattice) (φ : L₁.ComplexTorusHolMap L₂) (hφ0 : φ.toFun 0 = 0) : ∃! α : ℂ, ∃ (hα : α ∈ L₁.latticeMulSet L₂), ∀ (z : ℂ), φ.toFun (L₁.proj z) = (L₁.inducedMap L₂ α hα) (L₁.proj z)

Theorem 16.1 (Sutherland): The map {α ∈ ℂ : α L₁ ⊆ L₂} → Hom(ℂ/L₁, ℂ/L₂) sending α ↦ φ_α is an isomorphism — i.e., every holomorphic torus morphism sending 0 to 0 is uniquely induced by some such scalar α.

theorem ComplexLattice.add_mem_latticeMulSet (L₁ L₂ : ComplexLattice) (α β : ℂ) (hα : α ∈ L₁.latticeMulSet L₂) (hβ : β ∈ L₁.latticeMulSet L₂) : α + β ∈ L₁.latticeMulSet L₂

The set latticeMulSet L₁ L₂ is closed under addition (it is an additive subgroup of ℂ).

theorem ComplexLattice.inducedMap_add_proj (L₁ L₂ : ComplexLattice) (α β : ℂ) (hα : α ∈ L₁.latticeMulSet L₂) (hβ : β ∈ L₁.latticeMulSet L₂) (z : ℂ) : (L₁.inducedMap L₂ (α + β) ⋯) (L₁.proj z) = (L₁.inducedMap L₂ α hα) (L₁.proj z) + (L₁.inducedMap L₂ β hβ) (L₁.proj z)

The induced map is additive in the scalar: inducedMap (α + β) = inducedMap α + inducedMap β on every projected point.

theorem ComplexLattice.latticeMulSet_to_torusMorphism_addGroupIso (L₁ L₂ : ComplexLattice) : (∀ (α β : ℂ) (hα : α ∈ L₁.latticeMulSet L₂) (hβ : β ∈ L₁.latticeMulSet L₂) (z : ℂ), (L₁.inducedMap L₂ (α + β) ⋯) (L₁.proj z) = (L₁.inducedMap L₂ α hα) (L₁.proj z) + (L₁.inducedMap L₂ β hβ) (L₁.proj z)) ∧ (∀ (z : ℂ), (L₁.inducedMap L₂ 0 ⋯) (L₁.proj z) = 0) ∧ (∀ (α γ : ℂ) (hα : α ∈ L₁.latticeMulSet L₂) (hγ : γ ∈ L₁.latticeMulSet L₂), (∀ (z : ℂ), (L₁.inducedMap L₂ α hα) (L₁.proj z) = (L₁.inducedMap L₂ γ hγ) (L₁.proj z)) → α = γ) ∧ ∀ (φ : L₁.ComplexTorusHolMap L₂), φ.toFun 0 = 0 → ∃ (α : ℂ) (hα : α ∈ L₁.latticeMulSet L₂), ∀ (z : ℂ), φ.toFun (L₁.proj z) = (L₁.inducedMap L₂ α hα) (L₁.proj z)

Conjunction packaging the four properties witnessing that α ↦ φ_α is an additive group isomorphism latticeMulSet L₁ L₂ ≃+ Hom(ℂ/L₁, ℂ/L₂): additivity, sending 0 ↦ 0, injectivity, and surjectivity (Theorem 16.1).

theorem ComplexLattice.mul_mem_latticeMulSet (L : ComplexLattice) (α β : ℂ) (hα : α ∈ L.latticeMulSet L) (hβ : β ∈ L.latticeMulSet L) : α * β ∈ L.latticeMulSet L

When L₁ = L₂ = L, the set latticeMulSet L L is closed under multiplication (it is a subring of ℂ, the endomorphism ring of ℂ / L).

theorem ComplexLattice.one_mem_latticeMulSet (L : ComplexLattice) : 1 ∈ L.latticeMulSet L

The scalar 1 lies in latticeMulSet L L, corresponding to the identity endomorphism.

theorem ComplexLattice.inducedMap_comp (L : ComplexLattice) (α β : ℂ) (hα : α ∈ L.latticeMulSet L) (hβ : β ∈ L.latticeMulSet L) (z : ℂ) : (L.inducedMap L (α * β) ⋯) (L.proj z) = (L.inducedMap L α hα) ((L.inducedMap L β hβ) (L.proj z))

Composition of induced endomorphisms corresponds to multiplication of scalars: inducedMap (α β) = inducedMap α ∘ inducedMap β. This gives the ring-isomorphism structure when L₁ = L₂.