9.5. JacobianConstruction.ZLatticeQuotient🔗

Jacobians.JacobianConstruction.ZLatticeQuotient — source

isCoveringMap_mk

The quotient map E → E ⧸ Λ is a covering map.

theorem isCoveringMap_mk : IsCoveringMap (QuotientAddGroup.mk : E → E ⧸ Λ)

isLocalHomeomorph_mk

The quotient map E → E ⧸ Λ is a local homeomorphism.

theorem isLocalHomeomorph_mk :
    IsLocalHomeomorph (QuotientAddGroup.mk : E → E ⧸ Λ)

chartedSpaceQuotient

Charted space structure on E ⧸ Λ modelled on E, coming from the fact that the quotient map is a surjective local homeomorphism.

noncomputable instance chartedSpaceQuotient : ChartedSpace E (E ⧸ Λ)

instCompactSpaceQuotient

The quotient E ⧸ Λ is compact. The quotient map is continuous, periodic with respect to Λ, and surjective, so its range (the whole quotient) is compact by IsZLattice.isCompact_range_of_periodic.

instance instCompactSpaceQuotient : CompactSpace (E ⧸ Λ.toAddSubgroup)

transition_sub_mem_lattice

Step 1: transition displacement lies in the lattice.

theorem transition_sub_mem_lattice
    (P P' : OpenPartialHomeomorph E (E ⧸ Λ.toAddSubgroup))
    (hP : (P : E → E ⧸ Λ.toAddSubgroup) = QuotientAddGroup.mk)
    (hP' : (P' : E → E ⧸ Λ.toAddSubgroup) = QuotientAddGroup.mk)
    {y : E} (hy : y ∈ (P ≫ₕ P'.symm).source) :
    (P ≫ₕ P'.symm) y - y ∈ Λ.toAddSubgroup

transition_displacement_continuousOn

Step 2 + 3: the displacement y ↦ transition y - y is continuous.

theorem transition_displacement_continuousOn
    (P P' : OpenPartialHomeomorph E (E ⧸ Λ.toAddSubgroup)) :
    ContinuousOn (fun y : E => (P ≫ₕ P'.symm) y - y) (P ≫ₕ P'.symm).source

transition_displacement_eventuallyEq

Step 4: near any point of the source, the displacement is constant.

Proof: displacement d is continuous on T.source (open) into E, with values in Λ. Λ is discrete in E, so near y₀ the value d y must equal d y₀.

theorem transition_displacement_eventuallyEq [DiscreteTopology Λ]
    (P P' : OpenPartialHomeomorph E (E ⧸ Λ.toAddSubgroup))
    (hP : (P : E → E ⧸ Λ.toAddSubgroup) = QuotientAddGroup.mk)
    (hP' : (P' : E → E ⧸ Λ.toAddSubgroup) = QuotientAddGroup.mk)
    {y₀ : E} (hy₀ : y₀ ∈ (P ≫ₕ P'.symm).source) :
    ∀ᶠ y in 𝓝 y₀, (P ≫ₕ P'.symm) y - y = (P ≫ₕ P'.symm) y₀ - y₀

transition_contDiffOn_of_agrees_with_mk

Step 5: the transition between mk-matching partial homs is ContDiffOn 𝕜 n on its source. Near any point of the source, the transition equals a translation by a fixed lattice element (step 4), and translations are ContDiff.

theorem transition_contDiffOn_of_agrees_with_mk [DiscreteTopology Λ]
    (P P' : OpenPartialHomeomorph E (E ⧸ Λ.toAddSubgroup))
    (hP : (P : E → E ⧸ Λ.toAddSubgroup) = QuotientAddGroup.mk)
    (hP' : (P' : E → E ⧸ Λ.toAddSubgroup) = QuotientAddGroup.mk) :
    ContDiffOn 𝕜 n (P ≫ₕ P'.symm : E → E) (P ≫ₕ P'.symm).source

instIsManifoldQuotient

The analytic manifold structure on E ⧸ Λ.

noncomputable instance instIsManifoldQuotient [DiscreteTopology Λ] :
    IsManifold 𝓘(𝕜, E) n (E ⧸ Λ.toAddSubgroup)

contDiffOn_symm_mk

theorem contDiffOn_symm_mk [DiscreteTopology Λ]
    (P : OpenPartialHomeomorph E (E ⧸ Λ.toAddSubgroup))
    (hP : (P : E → E ⧸ Λ.toAddSubgroup) = QuotientAddGroup.mk) :
    ContDiffOn 𝕜 n
      (fun y : E => P.symm (QuotientAddGroup.mk y : E ⧸ Λ.toAddSubgroup))
      ((QuotientAddGroup.mk : E → E ⧸ Λ.toAddSubgroup) ⁻¹' P.target)

contMDiff_mk

The quotient projection mk : E → E ⧸ Λ.toAddSubgroup is ContMDiff.

The chart on E ⧸ Λ at mk x is essentially mk⁻¹ on a neighborhood (via IsLocalHomeomorph.chartedSpacePreimage), so the chart-pullback of mk along the trivial chart on E and this inverse chart is locally the identity, hence ContDiff. The proof mirrors the structure of contMDiff_neg but with id in place of the neg ambient map.

theorem contMDiff_mk [DiscreteTopology Λ] : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E) n
    (QuotientAddGroup.mk : E → E ⧸ Λ.toAddSubgroup)

contMDiff_neg

The negation map q ↦ -q on E ⧸ Λ is ContMDiff.

theorem contMDiff_neg [DiscreteTopology Λ] :
    ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E) n
      (fun q : E ⧸ Λ.toAddSubgroup => -q)

contMDiff_add

Addition on E ⧸ Λ is ContMDiff.

theorem contMDiff_add [DiscreteTopology Λ] :
    ContMDiff (𝓘(𝕜, E).prod 𝓘(𝕜, E)) 𝓘(𝕜, E) n
      (fun p : (E ⧸ Λ.toAddSubgroup) × (E ⧸ Λ.toAddSubgroup) => p.1 + p.2)

instLieAddGroupQuotient

The analytic Lie-group structure on E ⧸ Λ.

noncomputable instance instLieAddGroupQuotient [DiscreteTopology Λ] :
    LieAddGroup 𝓘(𝕜, E) n (E ⧸ Λ.toAddSubgroup) where

pushforward

The descended pushforward map on quotient tori, from a lattice-respecting ambient ℂ-linear map. (The body uses only Φ.toAddMonoidHom and Φ.continuous, so →L[ℂ] vs →L[ℝ] doesn't matter for the construction; we take →L[ℂ] here because the downstream pushforward_contMDiff_of_ambient needs the ℂ-linearity for ContDiff ℂ ω Φ.)

def pushforward {gX gY : ℕ}
    (ΛX : Submodule ℤ (Fin gX → ℂ)) (ΛY : Submodule ℤ (Fin gY → ℂ))
    (Φ : (Fin gX → ℂ) →L[ℂ] (Fin gY → ℂ))
    (hΦ : ΛX.toAddSubgroup ≤ ΛY.toAddSubgroup.comap Φ.toAddMonoidHom) :
    ((Fin gX → ℂ) ⧸ ΛX.toAddSubgroup) →ₜ+ ((Fin gY → ℂ) ⧸ ΛY.toAddSubgroup) where

pullback

The descended pullback map (dual direction). Defined via pushforward.

def pullback {gX gY : ℕ}
    (ΛX : Submodule ℤ (Fin gX → ℂ)) (ΛY : Submodule ℤ (Fin gY → ℂ))
    (Ψ : (Fin gY → ℂ) →L[ℂ] (Fin gX → ℂ))
    (hΨ : ΛY.toAddSubgroup ≤ ΛX.toAddSubgroup.comap Ψ.toAddMonoidHom) :
    ((Fin gY → ℂ) ⧸ ΛY.toAddSubgroup) →ₜ+ ((Fin gX → ℂ) ⧸ ΛX.toAddSubgroup)

pushforward_pullback_of_ambient

Headline: the degree identity Φ ∘ Ψ = d • id on the ambient descends to pushforward ∘ pullback = d • id on the quotient.

theorem pushforward_pullback_of_ambient
    {gX gY : ℕ}
    (ΛX : Submodule ℤ (Fin gX → ℂ)) (ΛY : Submodule ℤ (Fin gY → ℂ))
    (Φ : (Fin gX → ℂ) →L[ℂ] (Fin gY → ℂ))
    (Ψ : (Fin gY → ℂ) →L[ℂ] (Fin gX → ℂ))
    (hΦ : ΛX.toAddSubgroup ≤ ΛY.toAddSubgroup.comap Φ.toAddMonoidHom)
    (hΨ : ΛY.toAddSubgroup ≤ ΛX.toAddSubgroup.comap Ψ.toAddMonoidHom)
    (d : ℕ)
    (hΦΨ : ∀ y : (Fin gY → ℂ), Φ (Ψ y) = (d : ℕ) • y)
    (P : (Fin gY → ℂ) ⧸ ΛY.toAddSubgroup) :
    pushforward ΛX ΛY Φ hΦ (pullback ΛX ΛY Ψ hΨ P) = d • P

pushforward_id_of_ambient

Functoriality: ambient identity descends to quotient identity.

theorem pushforward_id_of_ambient
    {g : ℕ} (Λ : Submodule ℤ (Fin g → ℂ))
    (Φ : (Fin g → ℂ) →L[ℂ] (Fin g → ℂ))
    (hΦΛ : Λ.toAddSubgroup ≤ Λ.toAddSubgroup.comap Φ.toAddMonoidHom)
    (hΦid : ∀ x : (Fin g → ℂ), Φ x = x)
    (P : (Fin g → ℂ) ⧸ Λ.toAddSubgroup) :
    pushforward Λ Λ Φ hΦΛ P = P

pushforward_contMDiff_of_ambient

Smoothness: a ℂ-linear continuous ambient map descends to a ContMDiff map on the quotient tori. Uses chart-pullback + contDiffOn_symm_mk + ContDiff ℂ of the ambient linear map.

theorem pushforward_contMDiff_of_ambient {gX gY : ℕ}
    (ΛX : Submodule ℤ (Fin gX → ℂ))
    [DiscreteTopology ΛX] [IsZLattice ℝ ΛX]
    (ΛY : Submodule ℤ (Fin gY → ℂ))
    [DiscreteTopology ΛY] [IsZLattice ℝ ΛY]
    (Φ : (Fin gX → ℂ) →L[ℂ] (Fin gY → ℂ))
    (hΦ : ΛX.toAddSubgroup ≤ ΛY.toAddSubgroup.comap Φ.toAddMonoidHom) :
    ContMDiff 𝓘(ℂ, Fin gX → ℂ) 𝓘(ℂ, Fin gY → ℂ) ω
      (pushforward ΛX ΛY Φ hΦ : _ → _)

pullback_contMDiff_of_ambient

Pullback smoothness, via pushforward.

theorem pullback_contMDiff_of_ambient {gX gY : ℕ}
    (ΛX : Submodule ℤ (Fin gX → ℂ))
    [DiscreteTopology ΛX] [IsZLattice ℝ ΛX]
    (ΛY : Submodule ℤ (Fin gY → ℂ))
    [DiscreteTopology ΛY] [IsZLattice ℝ ΛY]
    (Ψ : (Fin gY → ℂ) →L[ℂ] (Fin gX → ℂ))
    (hΨ : ΛY.toAddSubgroup ≤ ΛX.toAddSubgroup.comap Ψ.toAddMonoidHom) :
    ContMDiff 𝓘(ℂ, Fin gY → ℂ) 𝓘(ℂ, Fin gX → ℂ) ω
      (pullback ΛX ΛY Ψ hΨ : _ → _)