Algebraic trivialization of a torus family

Linear identifications carrying each period lattice onto a fixed submodule induce an equivalence from the orbit quotient of the family to a product with the fixed translation quotient. No topology, fullness, or choice of lattice basis is required.

References

• Christina Birkenhake and Herbert Lange, Complex Abelian Varieties, second edition, Chapter 8 (families of complex tori and period data).

noncomputable def TauCeti.torusFamilyLinearEquivProd {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} {F : Type u_4} [AddCommGroup Λ] [AddCommGroup E] [AddCommGroup F] (P : Y → Λ →ₗ[ℤ] E) (L : Submodule ℤ F) (A : Y → E ≃ₗ[ℤ] F) (hL : ∀ (y : Y), Submodule.map (↑(A y)) (P y).range = L) : AddAction.orbitRel.Quotient Λ (Y × E) ≃ Y × AddAction.orbitRel.Quotient (↥L) F

A linear identification of each period lattice with L trivializes the underlying family of tori: [y,v] ↦ (y,[A y v]). No regularity or fullness is required for this equivalence.

@[simp]

theorem TauCeti.torusFamilyLinearEquivProd_mk {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} {F : Type u_4} [AddCommGroup Λ] [AddCommGroup E] [AddCommGroup F] (P : Y → Λ →ₗ[ℤ] E) (L : Submodule ℤ F) (A : Y → E ≃ₗ[ℤ] F) (hL : ∀ (y : Y), Submodule.map (↑(A y)) (P y).range = L) (y : Y) (v : E) : (torusFamilyLinearEquivProd P L A hL) ⟦(y, v)⟧ = (y, ⟦(A y) v⟧)

On representatives the trivialization applies the chosen linear identification.

@[simp]

theorem TauCeti.torusFamilyLinearEquivProd_symm_mk {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} {F : Type u_4} [AddCommGroup Λ] [AddCommGroup E] [AddCommGroup F] (P : Y → Λ →ₗ[ℤ] E) (L : Submodule ℤ F) (A : Y → E ≃ₗ[ℤ] F) (hL : ∀ (y : Y), Submodule.map (↑(A y)) (P y).range = L) (y : Y) (v : F) : (torusFamilyLinearEquivProd P L A hL).symm (y, ⟦v⟧) = ⟦(y, (A y).symm v)⟧

On representatives the inverse trivialization applies the inverse linear identification.

@[simp]

theorem TauCeti.fst_torusFamilyLinearEquivProd {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} {F : Type u_4} [AddCommGroup Λ] [AddCommGroup E] [AddCommGroup F] (P : Y → Λ →ₗ[ℤ] E) (L : Submodule ℤ F) (A : Y → E ≃ₗ[ℤ] F) (hL : ∀ (y : Y), Submodule.map (↑(A y)) (P y).range = L) (x : AddAction.orbitRel.Quotient Λ (Y × E)) : ((torusFamilyLinearEquivProd P L A hL) x).1 = torusFamilyProjection P x

The linear trivialization lies over the parameter space.