TorusCharts.lean`

59 declarations, 0 contain sorry, 0 declared as axioms

Common charts and compactness of the multiplicative torus; Local charts and chart coverage of the multiplicative torus; Holomorphic fibre charts of multiplier line bundles; Connectedness of the multiplicative torus

theorem OAI.Nagata.Workers.W05.integer_gap_lower line 32

Source documentation

The distance to every integer is at least the smaller endpoint distance.

theorem integer_gap_lower {a δ : ℝ} (ha : 0 < a) (ha1 : a < 1)
    (hδa : δ ≤ a) (hδ1 : δ ≤ 1 - a) (k : ℤ) : δ ≤ |(k : ℝ) - a| := by
…

theorem OAI.Nagata.Workers.W05.integer_mul_small line 43
Source documentation
A positive real period larger than the disk diameter forces the deck index to vanish.
```
theorem integer_mul_small {R L : ℝ} (hR : 0 < R) (hL : 2 * R < |L|)
    (k : ℤ) (hk : |(k : ℝ) * L| < 2 * R) : k = 0 := by
…
```

theorem OAI.Nagata.Workers.W05.disk_difference_bounds line 55

Source documentation

Real and imaginary parts of a difference between two points in the disk.

theorem disk_difference_bounds {R : ℝ} {x y : ℂ} (hx : ‖x‖ < R) (hy : ‖y‖ < R) :
    |(y - x).re| < 2 * R ∧ |(y - x).im| < 2 * R := by
…

theorem OAI.Nagata.Workers.W05.common_disk_lattice_unique line 62

Source documentation

No nonzero logarithmic period can join two points in the fixed disk.

theorem common_disk_lattice_unique {R L : ℝ} (hR : 0 < R)
    (hRpi : R < Real.pi / 2) (hL : 2 * R < |L|) {x y : ℂ}
    (hx : ‖x‖ < R) (hy : ‖y‖ < R) (a b : ℤ)
    (hxy : y - x = (a : ℂ) * (L : ℂ) + (b : ℂ) * (2 * Real.pi * Complex.I)) :
    a = 0 ∧ b = 0 ∧ y = x := by
…

theorem OAI.Nagata.Workers.W05.exp_injective_on_disk line 82
Source documentation
The fibre exponential is injective on the same fixed disk.
```
theorem exp_injective_on_disk {R : ℝ} (hRpi : R < Real.pi / 2) :
    Set.InjOn Complex.exp {x : ℂ | ‖x‖ < R} := by
…
```

theorem OAI.Nagata.Workers.W05.eventually_common_chart_bounds line 91

Source documentation

Explicit small-parameter requirements eventually hold as tau tends to zero positively.

theorem eventually_common_chart_bounds {R δ : ℝ} (hδ : 0 < δ) :
    ∀ᶠ τ : ℝ in 𝓝[>] 0, 0 < τ ∧ τ < 1 ∧
      2 * R < |Real.log τ| ∧ R < δ * |Real.log τ| := by
…

def OAI.Nagata.Workers.W05.positivePeriod line 108
Source documentation
A positive real period as an actual nonzero complex number.
```
noncomputable def positivePeriod (τ : ℝ) (hτ : 0 < τ) : ℂˣ :=
…
```
def OAI.Nagata.Workers.W05.rayPoint line 112
Source documentation
The covering-space point tau^s, expressed through the genuine real logarithm.
```
noncomputable def rayPoint (τ s : ℝ) : ℂˣ :=
…
```
def OAI.Nagata.Workers.W05.chartPoint line 116
Source documentation
The actual covering-space chart x ↦ tau^x0 exp x.
```
noncomputable def chartPoint (τ x0 : ℝ) (x : ℂ) : ℂˣ :=
…
```
def OAI.Nagata.Workers.W05.torusChart line 121
Source documentation
The common chart into the genuine set quotient of nonzero complex points.
```
noncomputable def torusChart (τ : ℝ) (hτ : 0 < τ) (x0 : ℝ) (x : ℂ) :
    Nagata.W21.TorusPoint (positivePeriod τ hτ) :=
…
```
Mentions: OAI.Nagata.W21.TorusPoint, OAI.Nagata.Workers.W05.positivePeriod

theorem OAI.Nagata.Workers.W05.exp_orbit_lattice line 126

Source documentation

Exponential orbit equality gives precisely the manuscript's logarithmic lattice.

theorem exp_orbit_lattice {τ : ℝ} (hτ : 0 < τ) (x y : ℂ) (a : ℤ)
    (h : Complex.exp y = (τ : ℂ) ^ a * Complex.exp x) :
    ∃ b : ℤ, y - x = (a : ℂ) * (Real.log τ : ℂ) +
      (b : ℂ) * (2 * Real.pi * Complex.I) := by
…

theorem OAI.Nagata.Workers.W05.torusChart_injective_on_disk line 139

Source documentation

The same fixed disk maps injectively to the multiplicative torus quotient.

theorem torusChart_injective_on_disk {τ R : ℝ} (hτ : 0 < τ) (hR : 0 < R)
    (hRpi : R < Real.pi / 2) (hlog : 2 * R < |Real.log τ|) (x0 : ℝ) :
    Set.InjOn (torusChart τ hτ x0) {x : ℂ | ‖x‖ < R} := by
…

Mentions: OAI.Nagata.Workers.W05.torusChart

theorem OAI.Nagata.Workers.W05.torusChart_avoids_mark line 153

Source documentation

A disk point cannot represent a marked point when the endpoint gap dominates its radius.

theorem torusChart_avoids_mark {τ R δ x0 xi : ℝ} (hτ : 0 < τ)
    (ha0 : 0 < x0 - xi) (ha1 : x0 - xi < 1)
    (hδa : δ ≤ x0 - xi) (hδ1 : δ ≤ 1 - (x0 - xi))
    (hmargin : R < δ * |Real.log τ|) {x : ℂ} (hx : ‖x‖ < R) :
    torusChart τ hτ x0 x ≠
      Nagata.W21.torusPointMk (positivePeriod τ hτ) (rayPoint τ xi) := by
…

Mentions: OAI.Nagata.Workers.W05.torusChart, OAI.Nagata.W21.torusPointMk, OAI.Nagata.Workers.W05.positivePeriod, OAI.Nagata.Workers.W05.rayPoint

def OAI.Nagata.Workers.W05.markedGapValues line 180
theorem OAI.Nagata.Workers.W05.markedGapValues_nonempty line 184
def OAI.Nagata.Workers.W05.markedGap line 190
Source documentation
The actual finite minimum δ_P used in the manuscript.
```
noncomputable def markedGap (x0 : ℝ) (xi : Fin 9 → ℝ) : ℝ :=
…
```
theorem OAI.Nagata.Workers.W05.markedGap_pos line 193
theorem OAI.Nagata.Workers.W05.markedGap_le line 202
theorem OAI.Nagata.Workers.W05.exists_eventual_common_chart line 211
theorem OAI.Nagata.Workers.W05.rayPoint_eq_real_rpow line 245
Source documentation
The logarithmic ray is literally the positive real power used in the source.
```
theorem rayPoint_eq_real_rpow {τ : ℝ} (hτ : 0 < τ) (s : ℝ) :
    (rayPoint τ s : ℂ) = ((τ ^ s : ℝ) : ℂ) := by
…
```
Mentions: OAI.Nagata.Workers.W05.rayPoint
theorem OAI.Nagata.Workers.W05.chartPoint_eq_real_rpow line 252
Source documentation
The covering chart has exactly the source scalar tau^x0 exp x.
```
theorem chartPoint_eq_real_rpow {τ : ℝ} (hτ : 0 < τ) (x0 : ℝ) (x : ℂ) :
    (chartPoint τ x0 x : ℂ) = ((τ ^ x0 : ℝ) : ℂ) * Complex.exp x := by
…
```
Mentions: OAI.Nagata.Workers.W05.chartPoint

theorem OAI.Nagata.Workers.W05.chartPoint_deck_unique line 266

Source documentation

The disk bounds identify the actual integer deck translate, not just the quotient point.

theorem chartPoint_deck_unique {τ R : ℝ} (hτ : 0 < τ) (hR : 0 < R)
    (hRpi : R < Real.pi / 2) (hlog : 2 * R < |Real.log τ|) (x0 : ℝ)
    {x y : ℂ} (hx : ‖x‖ < R) (hy : ‖y‖ < R) (k : ℤ)
    (hk : positivePeriod τ hτ ^ k * chartPoint τ x0 x = chartPoint τ x0 y) :
    k = 0 ∧ x = y := by
…

Mentions: OAI.Nagata.Workers.W05.positivePeriod, OAI.Nagata.Workers.W05.chartPoint

def OAI.Nagata.Workers.W05.multiplierChart line 281
Source documentation
The source formulas into the genuine multiplier-bundle set quotient.
```
noncomputable def multiplierChart (τ : ℝ) (hτ : 0 < τ) (γ : ℂˣ) (n : ℤ)
    (x0 : ℝ) (p : ℂ × ℂ) : Nagata.W21.MultiplierQuotient (positivePeriod τ hτ) γ n :=
…
```
Mentions: OAI.Nagata.W21.MultiplierQuotient, OAI.Nagata.Workers.W05.positivePeriod

theorem OAI.Nagata.Workers.W05.multiplierChart_injective_on_polydisk line 287

Source documentation

For every multiplier and degree, the common polydisk injects into the actual cyclic total-space quotient; degree zero specializes to the source bundle A.

theorem multiplierChart_injective_on_polydisk {τ R : ℝ} (hτ : 0 < τ) (hR : 0 < R)
    (hRpi : R < Real.pi / 2) (hlog : 2 * R < |Real.log τ|)
    (γ : ℂˣ) (n : ℤ) (x0 : ℝ) :
    Set.InjOn (multiplierChart τ hτ γ n x0)
      {p : ℂ × ℂ | ‖p.1‖ < R ∧ ‖p.2‖ < R} := by
…

Mentions: OAI.Nagata.Workers.W05.multiplierChart

theorem OAI.Nagata.Workers.W05.exists_eventual_common_polydisk line 309

Source documentation

One fixed polydisk injects into every multiplier total-space quotient for all sufficiently small positive periods, and its base avoids the nine marks.

theorem exists_eventual_common_polydisk (x0 : ℝ) (xi : Fin 9 → ℝ)
    (hxi : ∀ i, 0 < x0 - xi i ∧ x0 - xi i < 1) :
    ∃ R : ℝ, 0 < R ∧ R < Real.pi / 2 ∧
      ∀ᶠ τ : ℝ in 𝓝[>] 0, 0 < τ ∧ τ < 1 ∧
        ∀ (hτ : 0 < τ) (γ : ℂˣ) (n : ℤ),
          Set.InjOn (multiplierChart τ hτ γ n x0)
            {p : ℂ × ℂ | ‖p.1‖ < R ∧ ‖p.2‖ < R} ∧
          ∀ i : Fin 9, ∀ p : ℂ × ℂ, (‖p.1‖ < R ∧ ‖p.2‖ < R) →
            torusChart τ hτ x0 p.1 ≠
              Nagata.W21.torusPointMk (positivePeriod τ hτ) (rayPoint τ (xi i)) := by
…

Mentions: OAI.Nagata.Workers.W05.multiplierChart, OAI.Nagata.Workers.W05.torusChart, OAI.Nagata.W21.torusPointMk, OAI.Nagata.Workers.W05.positivePeriod, OAI.Nagata.Workers.W05.rayPoint

theorem OAI.Nagata.W21.torusPointMk_preimage_image line 339

Source documentation

Saturation under the period action, expressed with actual inverse images.

theorem torusPointMk_preimage_image {G : Type*} [CommGroup G] (τ : G) (U : Set G) :
    torusPointMk τ ⁻¹' (torusPointMk τ '' U) =
      ⋃ k : ℤ, (fun z : G ↦ τ ^ k * z) ⁻¹' U := by
…

Mentions: OAI.Nagata.W21.torusPointMk

theorem OAI.Nagata.W21.isOpenMap_torusPointMk line 352
Source documentation
The period quotient map is open, proved from continuous translations.
```
theorem isOpenMap_torusPointMk {G : Type*} [CommGroup G] [TopologicalSpace G]
    [ContinuousMul G] (τ : G) : IsOpenMap (torusPointMk τ) := by
…
```
Mentions: OAI.Nagata.W21.torusPointMk
def OAI.Nagata.W21.torusLocalChart line 361
Source documentation
Every genuinely injective open piece supplies an actual local homeomorphism onto its image in the torus quotient. The chart injectivity must be proved by the caller.
```
noncomputable def torusLocalChart {G : Type*} [CommGroup G] [TopologicalSpace G]
    [ContinuousMul G] (τ : G) (U : Set G) (hU : IsOpen U)
    (hinj : Set.InjOn (torusPointMk τ) U) : OpenPartialHomeomorph G (TorusPoint τ) :=
…
```
Mentions: OAI.Nagata.W21.torusPointMk, OAI.Nagata.W21.TorusPoint
theorem OAI.Nagata.W21.torusLocalChart_source line 370
theorem OAI.Nagata.W21.torusLocalChart_target line 374
theorem OAI.Nagata.Workers.W05.isOpen_chartDisk line 390
Source documentation
The fixed coordinate disk is open in the complex plane.
```
theorem isOpen_chartDisk (R : ℝ) : IsOpen {x : ℂ | ‖x‖ < R} :=
…
```
theorem OAI.Nagata.Workers.W05.chartDisk_subset_exp_source line 394
Source documentation
Every disk under consideration lies inside the canonical exponential branch.
```
theorem chartDisk_subset_exp_source {R : ℝ} (hRpi : R < Real.pi / 2) :
    {x : ℂ | ‖x‖ < R} ⊆ Complex.expOpenPartialHomeomorph.source := by
…
```
theorem OAI.Nagata.Workers.W05.continuous_chartPoint line 403
Source documentation
The explicit covering-space chart is continuous for the canonical units topology.
```
theorem continuous_chartPoint (τ x0 : ℝ) : Continuous (chartPoint τ x0) := by
…
```
Mentions: OAI.Nagata.Workers.W05.chartPoint
theorem OAI.Nagata.Workers.W05.isOpen_chartPoint_image line 412
Source documentation
The image of every open subset of the disk is open among actual nonzero complex points.
```
theorem isOpen_chartPoint_image {R : ℝ} (hRpi : R < Real.pi / 2)
    (τ x0 : ℝ) {U : Set ℂ} (hU : IsOpen U) (hUD : U ⊆ {x : ℂ | ‖x‖ < R}) :
    IsOpen (chartPoint τ x0 '' U) := by
…
```
Mentions: OAI.Nagata.Workers.W05.chartPoint
theorem OAI.Nagata.Workers.W05.continuous_torusChart line 435
Source documentation
The explicit torus chart is continuous for the canonical quotient topology.
```
theorem continuous_torusChart (τ : ℝ) (hτ : 0 < τ) (x0 : ℝ) :
    Continuous (torusChart τ hτ x0) :=
…
```
Mentions: OAI.Nagata.Workers.W05.torusChart

theorem OAI.Nagata.Workers.W05.isOpen_torusChart_image line 440

Source documentation

The actual local torus image is open; this is stronger than set injectivity.

theorem isOpen_torusChart_image {R : ℝ} (hRpi : R < Real.pi / 2)
    (τ : ℝ) (hτ : 0 < τ) (x0 : ℝ) {U : Set ℂ}
    (hU : IsOpen U) (hUD : U ⊆ {x : ℂ | ‖x‖ < R}) :
    IsOpen (torusChart τ hτ x0 '' U) := by
…

Mentions: OAI.Nagata.Workers.W05.torusChart

theorem OAI.Nagata.Workers.W05.isOpenMap_torusChart_restrict line 451

Source documentation

The disk-restricted quotient chart is an open map.

theorem isOpenMap_torusChart_restrict {R : ℝ} (hRpi : R < Real.pi / 2)
    (τ : ℝ) (hτ : 0 < τ) (x0 : ℝ) :
    IsOpenMap (({x : ℂ | ‖x‖ < R} : Set ℂ).domRestrict (torusChart τ hτ x0)) := by
…

Mentions: OAI.Nagata.Workers.W05.torusChart

def OAI.Nagata.Workers.W05.commonTorusOpenPartialHomeomorph line 465
Source documentation
The fixed exponential disk is a genuine local homeomorphism into the torus. Its inverse is continuous on the actual open quotient image.
```
noncomputable def commonTorusOpenPartialHomeomorph {τ R : ℝ}
    (hτ : 0 < τ) (hR : 0 < R) (hRpi : R < Real.pi / 2)
    (hlog : 2 * R < |Real.log τ|) (x0 : ℝ) :
    OpenPartialHomeomorph ℂ (Nagata.W21.TorusPoint (positivePeriod τ hτ)) :=
…
```
Mentions: OAI.Nagata.W21.TorusPoint, OAI.Nagata.Workers.W05.positivePeriod
theorem OAI.Nagata.Workers.W05.commonTorusOpenPartialHomeomorph_source line 476
theorem OAI.Nagata.Workers.W05.commonTorusOpenPartialHomeomorph_target line 482

theorem OAI.Nagata.W21.multiplierQuotientMk_injOn_fibre line 501

Source documentation

A base slice for a free period action is a slice for the whole fibre, including the zero vector.

theorem multiplierQuotientMk_injOn_fibre (τ γ : Rˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0) (U : Set Rˣ)
    (hinj : Set.InjOn (torusPointMk τ) U) :
    Set.InjOn (multiplierQuotientMk τ γ n) (U ×ˢ (Set.univ : Set R)) := by
…

Mentions: OAI.Nagata.W21.torusPointMk, OAI.Nagata.W21.multiplierQuotientMk

theorem OAI.Nagata.W21.multiplierQuotientMk_image_fibre line 518
Source documentation
Every point above a base slice has a representative in the full fibre over that slice; this proves that the local chart covers complete fibres.
```
theorem multiplierQuotientMk_image_fibre (τ γ : Rˣ) (n : ℤ) (U : Set Rˣ) :
    multiplierQuotientMk τ γ n '' (U ×ˢ (Set.univ : Set R)) =
      multiplierQuotientProjection τ γ n ⁻¹' (torusPointMk τ '' U) := by
…
```
Mentions: OAI.Nagata.W21.multiplierQuotientMk, OAI.Nagata.W21.multiplierQuotientProjection, OAI.Nagata.W21.torusPointMk
def OAI.Nagata.W21.multiplierFibreChart line 539
Source documentation
An actual quotient local homeomorphism whose image covers every fibre above the base slice, rather than a bounded portion of each fibre.
```
noncomputable def multiplierFibreChart (τ γ : Rˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0) (U : Set Rˣ) (hU : IsOpen U)
    (hinj : Set.InjOn (torusPointMk τ) U) :
    OpenPartialHomeomorph (MultiplicativeLineCover R) (MultiplierQuotient τ γ n) :=
…
```
Mentions: OAI.Nagata.W21.torusPointMk, OAI.Nagata.W21.MultiplicativeLineCover, OAI.Nagata.W21.MultiplierQuotient
theorem OAI.Nagata.W21.multiplierFibreChart_source line 546
theorem OAI.Nagata.W21.multiplierFibreChart_target line 551

theorem OAI.Nagata.W21.torusPointMk_injOn_translate line 571

Source documentation

Every translate of an injective base slice remains injective.

theorem torusPointMk_injOn_translate (τ c : G) (U : Set G)
    (hinj : Set.InjOn (torusPointMk τ) U) :
    Set.InjOn (torusPointMk τ) ((fun z : G ↦ c⁻¹ * z) ⁻¹' U) := by
…

Mentions: OAI.Nagata.W21.torusPointMk

theorem OAI.Nagata.W21.exists_open_torus_slice line 582

Source documentation

An open identity slice supplies an injective open slice containing any point.

theorem exists_open_torus_slice [TopologicalSpace G] [ContinuousMul G]
    (τ : G) (U : Set G) (hU : IsOpen U) (h1 : 1 ∈ U)
    (hinj : Set.InjOn (torusPointMk τ) U) (z : G) :
    ∃ V : Set G, IsOpen V ∧ z ∈ V ∧ Set.InjOn (torusPointMk τ) V := by
…

Mentions: OAI.Nagata.W21.torusPointMk

theorem OAI.Nagata.W21.torus_slice_covers line 592

Source documentation

The actual quotient is covered by the images of these open slices.

theorem torus_slice_covers [TopologicalSpace G] [ContinuousMul G]
    (τ : G) (U : Set G) (hU : IsOpen U) (h1 : 1 ∈ U)
    (hinj : Set.InjOn (torusPointMk τ) U) (q : TorusPoint τ) :
    ∃ V : Set G, IsOpen V ∧ Set.InjOn (torusPointMk τ) V ∧ q ∈ torusPointMk τ '' V := by
…

Mentions: OAI.Nagata.W21.torusPointMk, OAI.Nagata.W21.TorusPoint

theorem OAI.Nagata.Workers.W05.exists_int_scale_interval line 612

Source documentation

An integer power of a contraction moves every positive real into [tau,1].

theorem exists_int_scale_interval {τ a : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1) (ha : 0 < a) :
    ∃ k : ℤ, τ ≤ τ ^ k * a ∧ τ ^ k * a ≤ 1 := by
…

theorem OAI.Nagata.Workers.W05.exists_zpow_in_annulus line 636

Source documentation

Every actual complex period orbit has a representative in the closed annulus.

theorem exists_zpow_in_annulus {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    (z : ℂ) (hz : z ≠ 0) :
    ∃ k : ℤ, τ ≤ ‖(τ : ℂ) ^ k * z‖ ∧ ‖(τ : ℂ) ^ k * z‖ ≤ 1 := by
…

def OAI.Nagata.Workers.W05.closedAnnulus line 645
Source documentation
The genuine closed annulus in the complex plane.
```
def closedAnnulus (τ : ℝ) : Set ℂ := {z | τ ≤ ‖z‖ ∧ ‖z‖ ≤ 1}
```
theorem OAI.Nagata.Workers.W05.isCompact_closedAnnulus line 647
theorem OAI.Nagata.Workers.W05.closedAnnulus_ne_zero line 655
def OAI.Nagata.Workers.W05.annulusUnits line 659
Source documentation
The annulus maps to actual nonzero complex points without a chosen surrogate.
```
noncomputable def annulusUnits {τ : ℝ} (hτ : 0 < τ) (z : closedAnnulus τ) : ℂˣ :=
…
```
Mentions: OAI.Nagata.Workers.W05.closedAnnulus
theorem OAI.Nagata.Workers.W05.continuous_annulusUnits line 662
theorem OAI.Nagata.Workers.W05.annulus_torus_surjective line 669
Source documentation
Every point of the genuine quotient is represented by an annulus point.
```
theorem annulus_torus_surjective {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1) :
    Function.Surjective (fun z : closedAnnulus τ =>
      Nagata.W21.torusPointMk (positivePeriod τ hτ) (annulusUnits hτ z)) := by
…
```
Mentions: OAI.Nagata.Workers.W05.closedAnnulus, OAI.Nagata.W21.torusPointMk, OAI.Nagata.Workers.W05.positivePeriod, OAI.Nagata.Workers.W05.annulusUnits
theorem OAI.Nagata.Workers.W05.compactSpace_torusPoint line 687
Source documentation
The actual torus quotient with its canonical quotient topology is compact.
```
theorem compactSpace_torusPoint {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1) :
    CompactSpace (Nagata.W21.TorusPoint (positivePeriod τ hτ)) := by
…
```
Mentions: OAI.Nagata.W21.TorusPoint, OAI.Nagata.Workers.W05.positivePeriod
theorem OAI.Nagata.W21.chartPoint_zero_surjective line 707
Source documentation
The exponential map surjects onto the actual complex units.
```
theorem chartPoint_zero_surjective :
    Function.Surjective (Nagata.Workers.W05.chartPoint 1 0) := by
…
```
Mentions: OAI.Nagata.Workers.W05.chartPoint
theorem OAI.Nagata.W21.torusPoint_connectedSpace line 716
Source documentation
The canonical topology on the period quotient is connected, proved from the continuous surjective exponential parametrization.
```
theorem torusPoint_connectedSpace (τ : ℂˣ) : ConnectedSpace (TorusPoint τ) := by
…
```
Mentions: OAI.Nagata.W21.TorusPoint