The global trivialization of a continuous family of tori

Let P : Y → (Λ →ₗ[ℤ] E) be a continuous family of full lattices in a finite-dimensional real normed space E, as in TauCeti.Algebra.Module.ZLattice.Family.Basic, and let b be a ℤ-basis of Λ indexed by ι. At each y the periods P y (b i) form a real basis of E (TauCeti.periodBasis), whose coordinate map F_y⁻¹ : E ≃ ℝ^ι carries the lattice LinearMap.range (P y) onto the standard lattice ℤ^ι = span ℤ (range (Pi.basisFun ℝ ι)). Both F_y and F_y⁻¹ depend continuously on y in the operator norm, as does any family of bases whose vectors depend continuously on the parameter (Module.Basis.continuous_equivFunL_of_continuous).

Consequently [y, v] ↦ (y, [F_y⁻¹ v]) descends to a homeomorphism (Y × E)/Λ ≃ₜ Y × ℝ^ι/ℤ^ι over Y (TauCeti.torusFamilyHomeomorphProd), from the orbit space of the period translation action to the product of the parameter space with one fixed torus, the quotient (ι → ℝ) ⧸ span ℤ (range (Pi.basisFun ℝ ι)). This is the global trivialization of the family. The trivialization is real-linear on fibres, not complex-linear: when E is a complex vector space the complex structure of the fibre E ⧸ LinearMap.range (P y) varies with y, and a family whose period ratio varies is not holomorphically a product.

Main results

• TauCeti.periodBasis_equivFun_mem_span_iff: the coordinates of v in the period basis at y are integers exactly when v is a period at y.
• TauCeti.continuous_periodBasis_equivFunL_symm, TauCeti.continuous_periodBasis_equivFunL: the frame F_y and its inverse depend continuously on y.
• TauCeti.torusFamilyHomeomorphProd: the homeomorphism (Y × E)/Λ ≃ₜ Y × ℝ^ι/ℤ^ι over Y.

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).

theorem TauCeti.periodBasis_equivFun_mem_span_iff {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (P : Y → Λ →ₗ[ℤ] 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) (v : E) : (periodBasis P b hinj y).equivFun v ∈ Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)) ↔ v ∈ (P y).range

Integral coordinates detect periods. The coordinates of v in the period basis at y lie in the standard lattice ℤ^ι exactly when v is a period at y.

theorem TauCeti.map_range_periodBasis_equivFun {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (P : Y → Λ →ₗ[ℤ] 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) : Submodule.map (↑(LinearEquiv.restrictScalars ℤ (periodBasis P b hinj y).equivFun)) (P y).range = Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))

The period coordinate map carries the period lattice onto the standard integral lattice.

theorem TauCeti.continuous_periodBasis_equivFunL_symm {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (P : Y → Λ →ₗ[ℤ] 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)) [TopologicalSpace Y] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) : Continuous fun (y : Y) => ↑(periodBasis P b hinj y).equivFunL.symm

Continuity of the period frame. The real linear isomorphism F_y : ℝ^ι → E, x ↦ ∑ i, x i • P y (b i), depends continuously on y in the operator norm.

theorem TauCeti.continuous_periodBasis_equivFunL {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (P : Y → Λ →ₗ[ℤ] 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)) [TopologicalSpace Y] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) : Continuous fun (y : Y) => ↑(periodBasis P b hinj y).equivFunL

Continuity of the inverse period frame. The coordinate map F_y⁻¹ : E → ℝ^ι of the period basis depends continuously on y in the operator norm.

noncomputable def TauCeti.torusFamilyHomeomorphProd {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (P : Y → Λ →ₗ[ℤ] 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)) [TopologicalSpace Y] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) : AddAction.orbitRel.Quotient Λ (Y × E) ≃ₜ Y × (ι → ℝ) ⧸ Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))

The global trivialization of a continuous family of full lattices. For a ℤ-basis b of Λ indexed by ι, the map [y, v] ↦ (y, [F_y⁻¹ v]), with F_y⁻¹ the coordinate map of the period basis at y, is a homeomorphism from the orbit space of the period translation action to the product of Y with the fixed torus ℝ^ι/ℤ^ι. It lies over Y (TauCeti.fst_torusFamilyHomeomorphProd), and on each fibre it is induced by the real linear isomorphism F_y⁻¹.

@[simp]

theorem TauCeti.torusFamilyHomeomorphProd_mk {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (P : Y → Λ →ₗ[ℤ] 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)) [TopologicalSpace Y] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (p : Y × E) : (torusFamilyHomeomorphProd P b hinj hcont) ⟦p⟧ = (p.1, Submodule.Quotient.mk ((periodBasis P b hinj p.1).equivFun p.2))

The homeomorphism sends the class of (y, v) to y and the class of the period coordinates of v at y.

@[simp]

theorem TauCeti.torusFamilyHomeomorphProd_symm_mk {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (P : Y → Λ →ₗ[ℤ] 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)) [TopologicalSpace Y] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (y : Y) (x : ι → ℝ) : (torusFamilyHomeomorphProd P b hinj hcont).symm (y, Submodule.Quotient.mk x) = ⟦(y, (periodBasis P b hinj y).equivFun.symm x)⟧

The inverse homeomorphism sends y and the class of x to the class of (y, ∑ i, x i • P y (b i)).

@[simp]

theorem TauCeti.fst_torusFamilyHomeomorphProd {Y : Type u_1} {Λ : Type u_2} [AddCommGroup Λ] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (P : Y → Λ →ₗ[ℤ] 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)) [TopologicalSpace Y] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (z : AddAction.orbitRel.Quotient Λ (Y × E)) : ((torusFamilyHomeomorphProd P b hinj hcont) z).1 = torusFamilyProjection P z

The homeomorphism lies over the parameter space.