The fibres of a period quotient

For a period family P : Y → (Λ →ₗ[ℤ] E), the fibre over y of the standard orbit quotient (Y × E)/Λ → Y is canonically homeomorphic to the standard translation quotient E / LinearMap.range (P y). The map sends [v] to [y, v] and is independent of any choice of lattice basis. Its composite with the inclusion of the fibre is a topological embedding.

Only continuity of the periods is needed: neither injectivity nor fullness nor discreteness is required for this topological identification. In particular it applies to continuous and holomorphic families of full lattices. Both quotients carry their quotient topologies, and the fibre carries its subspace topology in the total period quotient.

The quotient topology on the slice {y} × E agrees with the subspace topology of the fibre.

References

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

def TauCeti.torusFamilyFiberMap {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} [AddCommGroup Λ] [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (y : Y) : AddAction.orbitRel.Quotient (↥(P y).range) E → AddAction.orbitRel.Quotient Λ (Y × E)

The map from the translation quotient at y into the total period quotient, sending [v] to [y, v].

@[simp]

theorem TauCeti.torusFamilyFiberMap_mk {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} [AddCommGroup Λ] [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (y : Y) (v : E) : torusFamilyFiberMap P y ⟦v⟧ = ⟦(y, v)⟧

The inclusion of a fibre sends the class of v to the class of (y, v).

@[simp]

theorem TauCeti.torusFamilyProjection_fiberMap {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} [AddCommGroup Λ] [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (y : Y) (z : AddAction.orbitRel.Quotient (↥(P y).range) E) : torusFamilyProjection P (torusFamilyFiberMap P y z) = y

The image of the fibre map lies over y.

theorem TauCeti.torusFamilyFiberMap_injective {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} [AddCommGroup Λ] [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (y : Y) : Function.Injective (torusFamilyFiberMap P y)

Passing from one period fibre to the total quotient identifies no further points.

theorem TauCeti.range_torusFamilyFiberMap {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} [AddCommGroup Λ] [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (y : Y) : Set.range (torusFamilyFiberMap P y) = {z : AddAction.orbitRel.Quotient Λ (Y × E) | torusFamilyProjection P z = y}

The image of the fibre quotient is exactly the set-theoretic fibre of the projection.

theorem TauCeti.isEmbedding_torusFamilyFiberMap {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} [AddCommGroup Λ] [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (y : Y) [TopologicalSpace Y] [TopologicalSpace E] [ContinuousAdd E] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) : Topology.IsEmbedding (torusFamilyFiberMap P y)

The quotient topology on a period fibre agrees with its subspace topology in the total period quotient.

noncomputable def TauCeti.torusFamilyFiberHomeomorph {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} [AddCommGroup Λ] [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (y : Y) [TopologicalSpace Y] [TopologicalSpace E] [ContinuousAdd E] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) : AddAction.orbitRel.Quotient (↥(P y).range) E ≃ₜ ↑{z : AddAction.orbitRel.Quotient Λ (Y × E) | torusFamilyProjection P z = y}

The canonical identification of the translation quotient at y with the literal fibre of the total period quotient. It sends [v] to [y, v] and needs no lattice basis.

@[simp]

theorem TauCeti.coe_torusFamilyFiberHomeomorph {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} [AddCommGroup Λ] [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (y : Y) [TopologicalSpace Y] [TopologicalSpace E] [ContinuousAdd E] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (z : AddAction.orbitRel.Quotient (↥(P y).range) E) : ↑((torusFamilyFiberHomeomorph P y hcont) z) = torusFamilyFiberMap P y z

The fibre homeomorphism is the canonical inclusion on underlying points.

@[simp]

theorem TauCeti.torusFamilyFiberHomeomorph_mk {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} [AddCommGroup Λ] [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (y : Y) [TopologicalSpace Y] [TopologicalSpace E] [ContinuousAdd E] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (v : E) : (torusFamilyFiberHomeomorph P y hcont) ⟦v⟧ = ⟨⟦(y, v)⟧, ⋯⟩

On representatives, the canonical fibre homeomorphism sends [v] to [y, v].

@[simp]

theorem TauCeti.torusFamilyFiberHomeomorph_symm_mk {Y : Type u_1} {Λ : Type u_2} {E : Type u_3} [AddCommGroup Λ] [AddCommGroup E] (P : Y → Λ →ₗ[ℤ] E) (y : Y) [TopologicalSpace Y] [TopologicalSpace E] [ContinuousAdd E] (hcont : ∀ (l : Λ), Continuous fun (y : Y) => (P y) l) (v : E) : (torusFamilyFiberHomeomorph P y hcont).symm ⟨⟦(y, v)⟧, ⋯⟩ = ⟦v⟧

The inverse fibre homeomorphism sends the class of (y, v) to the class of v.