Continuous families of full lattices

Let Λ be a finite free ℤ-module, E a finite-dimensional real normed space and Y a topological space. A period family is a map P : Y → (Λ →ₗ[ℤ] E) such that each period y ↦ P y l is continuous and each P y is injective with discrete, full range: that is, LinearMap.range (P y) is a full lattice of E in the sense of IsZLattice ℝ. A holomorphic family of complex tori E ⧸ LinearMap.range (P y) is described by such data.

Pointwise discreteness says that each lattice LinearMap.range (P y) has nonzero vectors of norm bounded below. This file proves the bound is locally uniform in y: on every compact K ⊆ Y there is one c > 0 with c ≤ ‖P y l‖ for all y ∈ K and all l ≠ 0 (TauCeti.exists_pos_le_norm_period_of_isCompact). After choosing a ℤ-basis b of Λ the statement is a uniform bound for the inverses of the real linear isomorphisms x ↦ ∑ i, x i • P y (b i) (TauCeti.exists_pos_mul_norm_le_norm_sum_smul_period_of_isCompact). The proof is compactness of K times the unit sphere of ι → ℝ, on which the norm of this combination is continuous and positive, a ℤ-basis of a full lattice being an ℝ-basis of E (Module.Basis.ofZLatticeBasis).

Consequently only finitely many l have ‖P y l‖ ≤ R for some y ∈ K (TauCeti.finite_setOf_exists_norm_period_le). This is exactly what makes the period translation action l +ᵥ (y, v) = (y, v + P y l) of Λ on Y × E (TauCeti.periodAddAction) properly discontinuous, whose orbit space is the total space of the family of tori. The action is free and acts by homeomorphisms. The first projection descends to the projection of the family of tori to its parameter space (TauCeti.torusFamilyProjection), a continuous open surjection. The orbit map Y × E → (Y × E)/Λ is a covering map, so by uniqueness of lifts a continuous family of periods over a preconnected space is a single period (TauCeti.exists_eq_period_of_mem_range).

The ℤ-basis of the full lattice LinearMap.range (P y) given by the periods of a ℤ-basis b of Λ is packaged as the real basis TauCeti.periodBasis P b hinj y of E. The global trivialization of the family built from it is in TauCeti.Algebra.Module.ZLattice.Family.HomeomorphProd.

Main definitions

• TauCeti.periodBasis: the periods at y of a ℤ-basis of Λ, as a real basis of E.
• TauCeti.periodAddAction: the period translation action of Λ on Y × E.
• TauCeti.torusFamilyProjection: the projection (Y × E)/Λ → Y descended from Prod.fst.

Main results

• TauCeti.exists_pos_mul_norm_le_norm_sum_smul_period_of_isCompact: on a compact set of parameters, the real linear maps x ↦ ∑ i, x i • P y (b i) are uniformly bounded below.
• TauCeti.exists_pos_le_norm_period_of_isCompact: uniform separation of nonzero periods on a compact set of parameters.
• TauCeti.finite_setOf_exists_norm_period_le: on a compact set of parameters, only finitely many periods have norm at most R.
• TauCeti.properlyDiscontinuousVAdd_periodAddAction, TauCeti.isCancelVAdd_periodAddAction, TauCeti.continuousConstVAdd_periodAddAction: the period translation action on Y × E is properly discontinuous, free, and continuous.
• TauCeti.isAddQuotientCoveringMap_torusFamily_mk: the orbit map Y × E → (Y × E)/Λ is a covering map, the quotient map of the period translation action.
• TauCeti.mem_orbit_periodAddAction_iff: two points lie in one orbit exactly when they have the same parameter y and differ by a period at y.
• TauCeti.exists_eq_period_of_mem_range: a continuous family of periods over a preconnected space is a single period, by uniqueness of lifts through the orbit map.
• TauCeti.continuous_torusFamilyProjection, TauCeti.isOpenMap_torusFamilyProjection: the projection of the family of tori is continuous and open.
• TauCeti.secondCountableTopology_torusFamily: the total space is second countable over a second-countable base.

References

• Christina Birkenhake and Herbert Lange, Complex Abelian Varieties, second edition, Grundlehren der mathematischen Wissenschaften 302, Springer, 2004, Chapter 8 (families of complex tori given by period matrices).
• Tau Ceti PR #20968 (closed, unmerged) proved that the orbit map is a covering map along the lines of TauCeti.isAddQuotientCoveringMap_torusFamily_mk.

noncomputable def TauCeti.periodBasis {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [FiniteDimensional ℝ E] [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] {ι : Type u_4} (b : Module.Basis ι ℤ Λ) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) (y : Y) : Module.Basis ι ℝ E

The period basis at y: the periods P y (b i) of a ℤ-basis b of Λ, viewed as a real basis of E. They form a ℤ-basis of the full lattice LinearMap.range (P y), hence a real basis of E. Its inverse coordinate map x ↦ ∑ i, x i • P y (b i) is the real linear isomorphism ℝ^ι ≃ E carrying the standard lattice ℤ^ι onto the periods at y.

@[simp]

theorem TauCeti.periodBasis_apply {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [FiniteDimensional ℝ E] [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] {ι : Type u_4} (b : Module.Basis ι ℤ Λ) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) (y : Y) (i : ι) : (periodBasis P b hinj y) i = (P y) (b i)

The i-th vector of the period basis at y is the period P y (b i).

theorem TauCeti.span_range_periodBasis {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [FiniteDimensional ℝ E] [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] {ι : Type u_4} (b : Module.Basis ι ℤ Λ) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) (y : Y) : Submodule.span ℤ (Set.range ⇑(periodBasis P b hinj y)) = (P y).range

The period basis at y spans the lattice of periods at y over ℤ.

@[simp]

theorem TauCeti.periodBasis_repr_period {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [FiniteDimensional ℝ E] [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] {ι : Type u_4} (b : Module.Basis ι ℤ Λ) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) (y : Y) (l : Λ) (i : ι) : ((periodBasis P b hinj y).repr ((P y) l)) i = ↑((b.repr l) i)

The coordinates of a period P y l in the period basis at y are the integer coordinates of l in b.

theorem TauCeti.periodBasis_equivFun_period {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [FiniteDimensional ℝ E] [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] {ι : Type u_4} [Finite ι] (b : Module.Basis ι ℤ Λ) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) (y : Y) (l : Λ) : (periodBasis P b hinj y).equivFun ((P y) l) = fun (i : ι) => ↑((b.repr l) i)

The coordinate vector of a period P y l in the period basis at y is the integer coordinate vector of l in b.

theorem TauCeti.exists_pos_mul_norm_le_norm_sum_smul_period_of_isCompact {Y : Type u_1} [TopologicalSpace Y] {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] {K : Set Y} {ι : Type u_4} [Fintype ι] (b : Module.Basis ι ℤ Λ) (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) (hK : IsCompact K) : ∃ c > 0, ∀ y ∈ K, ∀ (x : ι → ℝ), c * ‖x‖ ≤ ‖∑ i : ι, x i • (P y) (b i)‖

Uniform bound for inverse period maps. For a basis b of Λ, the real linear maps x ↦ ∑ i, x i • P y (b i) are bounded below by one constant c > 0 as y ranges over a compact set: c * ‖x‖ ≤ ‖∑ i, x i • P y (b i)‖.

theorem TauCeti.exists_pos_mul_norm_equivFun_le_norm_period_of_isCompact {Y : Type u_1} [TopologicalSpace Y] {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] {K : Set Y} {ι : Type u_4} [Fintype ι] (b : Module.Basis ι ℤ Λ) (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) (hK : IsCompact K) : ∃ c > 0, ∀ y ∈ K, ∀ (l : Λ), c * ‖b.equivFun l‖ ≤ ‖(P y) l‖

Uniform bound for lattice coordinates. For a basis b of Λ, on a compact set of parameters the coordinates of l are bounded by a fixed multiple of the norm of its period: c * ‖b.equivFun l‖ ≤ ‖P y l‖.

theorem TauCeti.exists_pos_le_norm_period_of_isCompact {Y : Type u_1} [TopologicalSpace Y] {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [FiniteDimensional ℝ E] [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] {K : Set Y} (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) (hK : IsCompact K) : ∃ c > 0, ∀ y ∈ K, ∀ (l : Λ), l ≠ 0 → c ≤ ‖(P y) l‖

Uniform period separation on compact sets. On a compact set K of parameters there is a single c > 0 bounding below the norm of every nonzero period at every point of K.

theorem TauCeti.finite_setOf_exists_norm_period_le {Y : Type u_1} [TopologicalSpace Y] {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [FiniteDimensional ℝ E] [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] {K : Set Y} (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) (hK : IsCompact K) (R : ℝ) : {l : Λ | ∃ y ∈ K, ‖(P y) l‖ ≤ R}.Finite

On a compact set K of parameters, only finitely many l have a period P y l of norm at most R at some point y ∈ K.

The period translation action

@[instance_reducible]

def TauCeti.periodAddAction {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ] {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) : AddAction Λ (Y × E)

The translation action of Λ on Y × E by periods, l +ᵥ (y, v) = (y, v + P y l). Its orbit space is the total space of the family of tori E ⧸ LinearMap.range (P y) over Y.

@[simp]

theorem TauCeti.periodAddAction_vadd {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ] {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (l : Λ) (p : Y × E) : l +ᵥ p = (p.1, p.2 + (P p.1) l)

The period translation action fixes the parameter and translates by the period.

theorem TauCeti.mem_orbit_periodAddAction_iff {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ] {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) {p q : Y × E} : q ∈ AddAction.orbit Λ p ↔ q.1 = p.1 ∧ q.2 - p.2 ∈ (P p.1).range

Two points of Y × E lie in one period orbit exactly when they have the same parameter y and their difference is a period at y.

theorem TauCeti.isCancelVAdd_periodAddAction {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ] {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) : IsCancelVAdd Λ (Y × E)

The period translation action is free when each period map is injective.

theorem TauCeti.continuousConstVAdd_periodAddAction {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ] {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) [TopologicalSpace Y] [TopologicalSpace E] [ContinuousAdd E] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) : ContinuousConstVAdd Λ (Y × E)

Each period translation is continuous when the periods depend continuously on the parameter.

def TauCeti.torusFamilyProjection {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ] {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) : AddAction.orbitRel.Quotient Λ (Y × E) → Y

The projection (Y × E)/Λ → Y of the family of tori to its parameter space, descended from Prod.fst along the period translation action.

@[simp]

theorem TauCeti.torusFamilyProjection_mk {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ] {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (p : Y × E) : torusFamilyProjection P ⟦p⟧ = p.1

The projection of the family of tori sends the class of (y, v) to y.

theorem TauCeti.torusFamilyProjection_surjective {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ] {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) : Function.Surjective (torusFamilyProjection P)

The projection of the family of tori is surjective: the class of (y, 0) lies over y.

theorem TauCeti.continuous_torusFamilyProjection {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ] {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) [TopologicalSpace Y] [TopologicalSpace E] : Continuous (torusFamilyProjection P)

The projection of the family of tori is continuous.

theorem TauCeti.isOpenMap_torusFamilyProjection {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ] {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) [TopologicalSpace Y] [TopologicalSpace E] : IsOpenMap (torusFamilyProjection P)

The projection of the family of tori is open, since it is descended from the open map Prod.fst along the quotient map.

theorem TauCeti.secondCountableTopology_torusFamily {Y : Type u_4} {Λ : Type u_5} [AddCommGroup Λ] {E : Type u_6} [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) [TopologicalSpace Y] [SecondCountableTopology Y] [TopologicalSpace E] [ContinuousAdd E] [SecondCountableTopology E] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) : SecondCountableTopology (AddAction.orbitRel.Quotient Λ (Y × E))

A family of tori over a second-countable base is second countable. If the periods depend continuously on the parameter, the orbit space (Y × E)/Λ of the period translation action is second countable whenever Y and E are, since its orbit map is open. No lattice hypothesis on the periods is needed.

theorem TauCeti.properlyDiscontinuousVAdd_periodAddAction {Y : Type u_1} [TopologicalSpace Y] {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [FiniteDimensional ℝ E] [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) : ProperlyDiscontinuousVAdd Λ (Y × E)

Orbit-local finiteness. The period translation action of a continuous family of full lattices is properly discontinuous.

theorem TauCeti.isAddQuotientCoveringMap_torusFamily_mk {Y : Type u_1} [TopologicalSpace Y] {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [FiniteDimensional ℝ E] [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] [T2Space Y] [LocallyCompactSpace Y] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) : IsAddQuotientCoveringMap (Quotient.mk (AddAction.orbitRel Λ (Y × E))) Λ

The orbit map is a covering map. For a continuous family of full lattices, the orbit map Y × E → (Y × E)/Λ of the period translation action is a covering map, and (Y × E)/Λ is its quotient by the free action of Λ.

theorem TauCeti.exists_eq_period_of_mem_range {Y : Type u_1} [TopologicalSpace Y] {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Y → Λ →ₗ[ℤ] E) [FiniteDimensional ℝ E] [∀ (y : Y), DiscreteTopology ↥(P y).range] [∀ (y : Y), IsZLattice ℝ (P y).range] [T2Space Y] [LocallyCompactSpace Y] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (hinj : ∀ (y : Y), Function.Injective ⇑(P y)) {Z : Type u_4} [TopologicalSpace Z] [PreconnectedSpace Z] {f : Z → Y} (hf : Continuous f) {S : Z → E} (hS : Continuous S) (hmem : ∀ (z : Z), S z ∈ (P (f z)).range) : ∃ (l : Λ), ∀ (z : Z), S z = (P (f z)) l

A continuous family of periods is a single period. Over a preconnected space Z, let f : Z → Y and S : Z → E be continuous with S z a period at f z for every z. Then there is one l : Λ with S z = P (f z) l for every z.