QuotientSections.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

Sections on the torus quotient and holomorphic chart equivalences; Holomorphic division producing quotient sections; Finite lists of quotient sections and their fibre values

theorem OAI.Nagata.W08.automorphicSection_analyticAt line 19
Source documentation
Every concrete multiplier section is complex analytic at every genuine point.
```
theorem automorphicSection_analyticAt {τ γ : ℂ} {n : ℤ}
    (f : automorphicSections τ n γ) {z : ℂ} (hz : z ≠ 0) :
    AnalyticAt ℂ f.val z := by
…
```
Mentions: OAI.Nagata.W08.automorphicSections
theorem OAI.Nagata.W08.automorphicSection_analyticOnNhd line 27
Source documentation
Analyticity on a neighborhood of each point of the punctured plane.
```
theorem automorphicSection_analyticOnNhd {τ γ : ℂ} {n : ℤ}
    (f : automorphicSections τ n γ) :
    AnalyticOnNhd ℂ f.val {z : ℂ | z ≠ 0} :=
…
```
Mentions: OAI.Nagata.W08.automorphicSections
def OAI.Nagata.W08.EquivariantFunctions line 46
Source documentation
Scalar functions with the literal one-step multiplier law on the genuine cover.
```
def EquivariantFunctions (τ γ : Rˣ) (n : ℤ) :=
…
```
def OAI.Nagata.W08.QuotientSections line 50
Source documentation
Actual right-inverse sections of the projection of the actual orbit quotient.
```
def QuotientSections (τ γ : Rˣ) (n : ℤ) :=
…
```

theorem OAI.Nagata.W08.multiplierIterate_graph line 55

Source documentation

Equivariance under one generator propagates to every integer deck transformation.

theorem multiplierIterate_graph (τ γ : Rˣ) (n : ℤ)
    (f : EquivariantFunctions τ γ n) (k : ℤ) (z : Rˣ) :
    multiplierIterate τ γ n k (z, f.val z) = (τ ^ k * z, f.val (τ ^ k * z)) := by
…

Mentions: OAI.Nagata.W08.EquivariantFunctions

def OAI.Nagata.W08.quotientSectionOfEquivariant line 77
Source documentation
An equivariant scalar function descends to an actual quotient section.
```
def quotientSectionOfEquivariant (τ γ : Rˣ) (n : ℤ)
    (f : EquivariantFunctions τ γ n) : QuotientSections τ γ n :=
…
```
Mentions: OAI.Nagata.W08.EquivariantFunctions, OAI.Nagata.W08.QuotientSections
theorem OAI.Nagata.W08.quotientSectionOfEquivariant_apply line 91

theorem OAI.Nagata.W08.quotient_fibre_representative line 97

Source documentation

Every quotient fibre point has a scalar representative over each chosen lift of its base.

theorem quotient_fibre_representative (τ γ : Rˣ) (n : ℤ)
    (q : MultiplierQuotient τ γ n) (z : Rˣ)
    (hq : multiplierQuotientProjection τ γ n q = torusPointMk τ z) :
    ∃ t : R, (Quotient.mk _ (z, t) : MultiplierQuotient τ γ n) = q := by
…

theorem OAI.Nagata.W08.quotient_fibre_coordinate_injective line 113

Source documentation

Freeness ensures that the scalar coordinate over a fixed lift is unique.

theorem quotient_fibre_coordinate_injective (τ γ : Rˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0) (z : Rˣ) :
    Function.Injective (fun t : R ↦ (Quotient.mk _ (z, t) : MultiplierQuotient τ γ n)) := by
…

def OAI.Nagata.W08.quotientSectionScalar line 126
Source documentation
Extract the unique scalar over a chosen lift from an actual quotient section.
```
def quotientSectionScalar (τ γ : Rˣ) (n : ℤ)
    (s : QuotientSections τ γ n) (z : Rˣ) : R :=
…
```
Mentions: OAI.Nagata.W08.QuotientSections
theorem OAI.Nagata.W08.quotientSectionScalar_represents line 131

theorem OAI.Nagata.W08.quotient_mk_multiplierStep line 139

Source documentation

One generator identifies exactly the source multiplier-related representatives.

theorem quotient_mk_multiplierStep (τ γ : Rˣ) (n : ℤ) (z : Rˣ) (t : R) :
    (Quotient.mk _ (τ * z, (↑(γ * z ^ (-n)) : R) * t) : MultiplierQuotient τ γ n) =
      Quotient.mk _ (z, t) := by
…

theorem OAI.Nagata.W08.quotientSectionScalar_equivariant line 149

Source documentation

The scalar extracted from an actual quotient section is genuinely equivariant.

theorem quotientSectionScalar_equivariant (τ γ : Rˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0)
    (s : QuotientSections τ γ n) (z : Rˣ) :
    quotientSectionScalar τ γ n s (τ * z) =
      (↑(γ * z ^ (-n)) : R) * quotientSectionScalar τ γ n s z := by
…

Mentions: OAI.Nagata.W08.QuotientSections, OAI.Nagata.W08.quotientSectionScalar

def OAI.Nagata.W08.equivariantOfQuotientSection line 161
Source documentation
Extract an equivariant function from an actual quotient section.
```
def equivariantOfQuotientSection (τ γ : Rˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0)
    (s : QuotientSections τ γ n) : EquivariantFunctions τ γ n :=
…
```
Mentions: OAI.Nagata.W08.QuotientSections, OAI.Nagata.W08.EquivariantFunctions
theorem OAI.Nagata.W08.equivariantOfQuotientSection_left_inverse line 167
Source documentation
Extracting after descending returns every original scalar value.
```
theorem equivariantOfQuotientSection_left_inverse (τ γ : Rˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0)
    (f : EquivariantFunctions τ γ n) :
    equivariantOfQuotientSection τ γ n hfree (quotientSectionOfEquivariant τ γ n f) = f := by
…
```
Mentions: OAI.Nagata.W08.EquivariantFunctions, OAI.Nagata.W08.equivariantOfQuotientSection, OAI.Nagata.W08.quotientSectionOfEquivariant
theorem OAI.Nagata.W08.quotientSectionOfEquivariant_right_inverse line 177
Source documentation
Descending after extracting returns the actual original quotient section.
```
theorem quotientSectionOfEquivariant_right_inverse (τ γ : Rˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0)
    (s : QuotientSections τ γ n) :
    quotientSectionOfEquivariant τ γ n (equivariantOfQuotientSection τ γ n hfree s) = s := by
…
```
Mentions: OAI.Nagata.W08.QuotientSections, OAI.Nagata.W08.quotientSectionOfEquivariant, OAI.Nagata.W08.equivariantOfQuotientSection
def OAI.Nagata.W08.equivariantQuotientSectionEquiv line 189
Source documentation
The actual algebraic section/function equivalence of the actual quotient projection. Holomorphic compatibility is not asserted by this set-level equivalence.
```
def equivariantQuotientSectionEquiv (τ γ : Rˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0) :
    EquivariantFunctions τ γ n ≃ QuotientSections τ γ n where
…
```
Mentions: OAI.Nagata.W08.EquivariantFunctions, OAI.Nagata.W08.QuotientSections
abbrev OAI.Nagata.W06.TorusConfiguration.QuotientFibre line 211
Source documentation
An actual fibre of the multiplier-orbit quotient projection.
```
abbrev QuotientFibre (τ γ : ℂˣ) (n : ℤ) (p : TorusPoint τ) :=
…
```
def OAI.Nagata.W06.TorusConfiguration.fibreRepresentative line 215
Source documentation
The vector with scalar c over the chosen nonzero lift z.
```
def fibreRepresentative (τ γ : ℂˣ) (n : ℤ) (z : ℂˣ) (c : ℂ) :
    QuotientFibre τ γ n (torusPointMk τ z) :=
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.QuotientFibre
theorem OAI.Nagata.W06.TorusConfiguration.fibreRepresentative_injective line 219
theorem OAI.Nagata.W06.TorusConfiguration.fibreRepresentative_surjective line 225
def OAI.Nagata.W06.TorusConfiguration.fibreCoordinateEquiv line 232
Source documentation
A proved coordinate bijection for the actual quotient fibre over a fixed lift.
```
def fibreCoordinateEquiv (τ γ : ℂˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0) (z : ℂˣ) :
    ℂ ≃ QuotientFibre τ γ n (torusPointMk τ z) :=
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.QuotientFibre
theorem OAI.Nagata.W06.TorusConfiguration.fibreCoordinateEquiv_apply line 238
def OAI.Nagata.W06.TorusConfiguration.fibreScaleAtLift line 244
Source documentation
Scalar multiplication between the actual two fibres in the specified covering frames. This finite-fibre map does not assert that these maps glue into a global bundle morphism.
```
def fibreScaleAtLift (τ γA γM : ℂˣ) (nA nM : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0) (z : ℂˣ) (P : ℂ) :
    QuotientFibre τ γA nA (torusPointMk τ z) → QuotientFibre τ γM nM (torusPointMk τ z) :=
…
```
Mentions: OAI.Nagata.W06.TorusConfiguration.QuotientFibre
theorem OAI.Nagata.W06.TorusConfiguration.fibreScaleAtLift_representative line 250

theorem OAI.Nagata.W06.TorusConfiguration.fibreScaleAtLift_one line 261

Source documentation

The source scalar-one vector is sent to the target scalar-P vector.

theorem fibreScaleAtLift_one (τ γA γM : ℂˣ) (nA nM : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0) (z : ℂˣ) (P : ℂ) :
    fibreScaleAtLift τ γA γM nA nM hfree z P (fibreRepresentative τ γA nA z 1) =
      fibreRepresentative τ γM nM z P := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.fibreScaleAtLift, OAI.Nagata.W06.TorusConfiguration.fibreRepresentative

theorem OAI.Nagata.W06.TorusConfiguration.fibreRepresentative_ne_zero line 267
def OAI.Nagata.W08.automorphicToEquivariant line 291
Source documentation
Restriction of the actual holomorphic section to its genuine unit-valued cover.
```
def automorphicToEquivariant (τ γ : ℂˣ) (n : ℤ)
    (f : automorphicSections (τ : ℂ) n (γ : ℂ)) : EquivariantFunctions τ γ n :=
…
```
Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.W08.EquivariantFunctions
theorem OAI.Nagata.W08.automorphicToEquivariant_injective line 298
Source documentation
Restriction loses no actual holomorphic sections.
```
theorem automorphicToEquivariant_injective (τ γ : ℂˣ) (n : ℤ) :
    Function.Injective (automorphicToEquivariant τ γ n) := by
…
```
Mentions: OAI.Nagata.W08.automorphicToEquivariant
def OAI.Nagata.W08.quotientSectionOfAutomorphic line 306
Source documentation
An actual holomorphic multiplier function yields an actual right-inverse section.
```
def quotientSectionOfAutomorphic (τ γ : ℂˣ) (n : ℤ)
    (f : automorphicSections (τ : ℂ) n (γ : ℂ)) : QuotientSections τ γ n :=
…
```
Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.W08.QuotientSections

theorem OAI.Nagata.W08.quotientSectionOfAutomorphic_apply line 311

Source documentation

The quotient representative uses exactly the function's covering-frame scalar.

@[simp] theorem quotientSectionOfAutomorphic_apply (τ γ : ℂˣ) (n : ℤ)
    (f : automorphicSections (τ : ℂ) n (γ : ℂ)) (z : ℂˣ) :
    (quotientSectionOfAutomorphic τ γ n f).val (torusPointMk τ z) =
      (Quotient.mk _ (z, f.val (z : ℂ)) : MultiplierQuotient τ γ n) := rfl

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.W08.quotientSectionOfAutomorphic

theorem OAI.Nagata.W08.quotientSectionOfAutomorphic_scalar line 317
Source documentation
Scalar extraction from the descended actual quotient section recovers the original value.
```
theorem quotientSectionOfAutomorphic_scalar (τ γ : ℂˣ) (n : ℤ)
    (hτ : ‖(τ : ℂ)‖ < 1) (f : automorphicSections (τ : ℂ) n (γ : ℂ)) (z : ℂˣ) :
    quotientSectionScalar τ γ n (quotientSectionOfAutomorphic τ γ n f) z = f.val (z : ℂ) := by
…
```
Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.W08.quotientSectionScalar, OAI.Nagata.W08.quotientSectionOfAutomorphic
theorem OAI.Nagata.W08.quotientSectionOfAutomorphic_injective line 324
Source documentation
Distinct holomorphic covering functions give distinct actual quotient sections.
```
theorem quotientSectionOfAutomorphic_injective (τ γ : ℂˣ) (n : ℤ)
    (hτ : ‖(τ : ℂ)‖ < 1) : Function.Injective (quotientSectionOfAutomorphic τ γ n) := by
…
```
Mentions: OAI.Nagata.W08.quotientSectionOfAutomorphic

theorem OAI.Nagata.W08.quotientSection_fibreChart line 349

Source documentation

The actual fibre chart recovers the unique scalar of an arbitrary quotient section.

theorem quotientSection_fibreChart (τ γ : ℂˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0)
    (U : Set ℂˣ) (hU : IsOpen U) (hinj : Set.InjOn (torusPointMk τ) U)
    (s : QuotientSections τ γ n) {z : ℂˣ} (hz : z ∈ U) :
    (multiplierFibreChart τ γ n hfree U hU hinj).symm (s.val (torusPointMk τ z)) =
      (z, quotientSectionScalar τ γ n s z) := by
…

Mentions: OAI.Nagata.W08.QuotientSections, OAI.Nagata.W08.quotientSectionScalar

def OAI.Nagata.W08.quotientChartScalar line 360
Source documentation
The scalar local coordinate of a quotient section, expressed in the genuine complex base coordinate. Outside the chart domain its values have no geometric meaning.
```
def quotientChartScalar (τ γ : ℂˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0)
    (U : Set ℂˣ) (hU : IsOpen U) (hinj : Set.InjOn (torusPointMk τ) U)
    (s : QuotientSections τ γ n) (w : ℂ) : ℂ :=
…
```
Mentions: OAI.Nagata.W08.QuotientSections

theorem OAI.Nagata.W08.quotientChartScalar_eq line 369

Source documentation

Exact local-coordinate formula for every actual section.

theorem quotientChartScalar_eq (τ γ : ℂˣ) (n : ℤ)
    (hfree : ∀ k : ℤ, τ ^ k = 1 → k = 0)
    (U : Set ℂˣ) (hU : IsOpen U) (hinj : Set.InjOn (torusPointMk τ) U)
    (s : QuotientSections τ γ n) {z : ℂˣ} (hz : z ∈ U) :
    quotientChartScalar τ γ n hfree U hU hinj s (z : ℂ) =
      quotientSectionScalar τ γ n s z := by
…

Mentions: OAI.Nagata.W08.QuotientSections, OAI.Nagata.W08.quotientChartScalar, OAI.Nagata.W08.quotientSectionScalar

theorem OAI.Nagata.W08.quotientChartScalar_automorphic_eq line 380

Source documentation

The actual quotient fibre-coordinate function equals the original holomorphic scalar.

theorem quotientChartScalar_automorphic_eq (τ γ : ℂˣ) (n : ℤ)
    (hτ : ‖(τ : ℂ)‖ < 1)
    (U : Set ℂˣ) (hU : IsOpen U) (hinj : Set.InjOn (torusPointMk τ) U)
    (f : automorphicSections (τ : ℂ) n (γ : ℂ)) {z : ℂˣ} (hz : z ∈ U) :
    quotientChartScalar τ γ n (unitPeriod_free τ hτ) U hU hinj
      (quotientSectionOfAutomorphic τ γ n f) (z : ℂ) = f.val (z : ℂ) := by
…

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.W08.quotientChartScalar, OAI.Nagata.W08.unitPeriod_free, OAI.Nagata.W08.quotientSectionOfAutomorphic

theorem OAI.Nagata.W08.quotientChartScalar_automorphic_differentiableAt line 390

Source documentation

The descended actual section is holomorphic in every actual fibre chart.

theorem quotientChartScalar_automorphic_differentiableAt (τ γ : ℂˣ) (n : ℤ)
    (hτ : ‖(τ : ℂ)‖ < 1)
    (U : Set ℂˣ) (hU : IsOpen U) (hinj : Set.InjOn (torusPointMk τ) U)
    (f : automorphicSections (τ : ℂ) n (γ : ℂ)) {z : ℂˣ} (hz : z ∈ U) :
    DifferentiableAt ℂ (quotientChartScalar τ γ n (unitPeriod_free τ hτ) U hU hinj
      (quotientSectionOfAutomorphic τ γ n f)) (z : ℂ) := by
…

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.W08.quotientChartScalar, OAI.Nagata.W08.unitPeriod_free, OAI.Nagata.W08.quotientSectionOfAutomorphic

theorem OAI.Nagata.CoefficientSpaces.exists_holomorphic_quotient line 414

Source documentation

Quotient construction directly from genuine holomorphic multiplier sections: analyticity is derived, with no additional analyticity hypotheses.

theorem exists_holomorphic_quotient {τ γ δ : ℂ} {n s : ℤ}
    (hτ : τ ≠ 0) (hδ : δ ≠ 0)
    (f : Nagata.W08.automorphicSections τ n γ)
    (P : Nagata.W08.automorphicSections τ s δ) (k : ℕ)
    (hzero : ∀ z ≠ 0, P.val z = 0 → deriv P.val z ≠ 0 ∧
      (k : ℕ∞) ≤ analyticOrderAt f.val z) :
    ∃ G : Nagata.W08.automorphicSections τ (n - (k : ℤ) * s) (γ / δ ^ k),
      ∀ z ≠ 0, f.val z = P.val z ^ k * G.val z :=
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.CoefficientSpaces.exists_low_holomorphic_coefficient line 427

Source documentation

The actual low coefficient extension without redundant analytic assumptions.

theorem exists_low_holomorphic_coefficient {τ L Q : ℂ}
    (hτ : τ ≠ 0) (hL : L ≠ 0) (hQ : Q ≠ 0)
    (d m j : ℤ) (hj : j ≤ m)
    (P : Nagata.W08.automorphicSections τ 9 Q)
    (f : Nagata.W08.automorphicSections τ (3 * (d - 3 * j)) (L ^ (d - 3 * j)))
    (hzero : ∀ z ≠ 0, P.val z = 0 → deriv P.val z ≠ 0 ∧
      ((m - j).toNat : ℕ∞) ≤ analyticOrderAt f.val z) :
    ∃ g ∈ coefficientSpace τ L Q d m j P.val,
      ∀ z ≠ 0, f.val z = P.val z ^ (m - j).toNat * g z :=
…

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.CoefficientSpaces.coefficientSpace

def OAI.Nagata.W08.IsChartHolomorphic line 459
Source documentation
Standard local-coordinate holomorphy for an actual section of the quotient projection.
```
def IsChartHolomorphic (τ γ : ℂˣ) (n : ℤ) (hτ : ‖(τ : ℂ)‖ < 1)
    (s : QuotientSections τ γ n) : Prop :=
…
```
Mentions: OAI.Nagata.W08.QuotientSections
def OAI.Nagata.W08.quotientSectionZeroScalar line 466
Source documentation
The unique scalar extracted from an actual section, represented by a zero extension.
```
def quotientSectionZeroScalar (τ γ : ℂˣ) (n : ℤ) (s : QuotientSections τ γ n) (w : ℂ) : ℂ :=
…
```
Mentions: OAI.Nagata.W08.QuotientSections
theorem OAI.Nagata.W08.quotientSectionZeroScalar_zero line 469
theorem OAI.Nagata.W08.quotientSectionZeroScalar_unit line 473
theorem OAI.Nagata.W08.quotientSectionZeroScalar_differentiableAt line 481
Source documentation
Holomorphy in an actual fibre chart implies holomorphy of the extracted covering scalar.
```
theorem quotientSectionZeroScalar_differentiableAt (τ γ : ℂˣ) (n : ℤ)
    (hτ : ‖(τ : ℂ)‖ < 1) (s : QuotientSections τ γ n)
    (hs : IsChartHolomorphic τ γ n hτ s) {w : ℂ} (hw : w ≠ 0) :
    DifferentiableAt ℂ (quotientSectionZeroScalar τ γ n s) w := by
…
```
Mentions: OAI.Nagata.W08.QuotientSections, OAI.Nagata.W08.IsChartHolomorphic, OAI.Nagata.W08.quotientSectionZeroScalar

theorem OAI.Nagata.W08.quotientSectionZeroScalar_automorphy line 496

Source documentation

The extracted scalar satisfies the actual multiplier equation.

theorem quotientSectionZeroScalar_automorphy (τ γ : ℂˣ) (n : ℤ)
    (hτ : ‖(τ : ℂ)‖ < 1) (s : QuotientSections τ γ n) {w : ℂ} (hw : w ≠ 0) :
    quotientSectionZeroScalar τ γ n s ((τ : ℂ) * w) =
      (γ : ℂ) * w ^ (-n) * quotientSectionZeroScalar τ γ n s w := by
…

Mentions: OAI.Nagata.W08.QuotientSections, OAI.Nagata.W08.quotientSectionZeroScalar

def OAI.Nagata.W08.automorphicOfChartHolomorphic line 507
Source documentation
Extract a genuine holomorphic multiplier function from a chart-holomorphic actual section.
```
def automorphicOfChartHolomorphic (τ γ : ℂˣ) (n : ℤ)
    (hτ : ‖(τ : ℂ)‖ < 1) (s : QuotientSections τ γ n)
    (hs : IsChartHolomorphic τ γ n hτ s) : automorphicSections (τ : ℂ) n (γ : ℂ) :=
…
```
Mentions: OAI.Nagata.W08.QuotientSections, OAI.Nagata.W08.IsChartHolomorphic, OAI.Nagata.W08.automorphicSections
theorem OAI.Nagata.W08.automorphicOfChartHolomorphic_right_inverse line 515
Source documentation
Descent of the extracted holomorphic scalar recovers the actual original section.
```
theorem automorphicOfChartHolomorphic_right_inverse (τ γ : ℂˣ) (n : ℤ)
    (hτ : ‖(τ : ℂ)‖ < 1) (s : QuotientSections τ γ n)
    (hs : IsChartHolomorphic τ γ n hτ s) :
    quotientSectionOfAutomorphic τ γ n (automorphicOfChartHolomorphic τ γ n hτ s hs) = s := by
…
```
Mentions: OAI.Nagata.W08.QuotientSections, OAI.Nagata.W08.IsChartHolomorphic, OAI.Nagata.W08.quotientSectionOfAutomorphic, OAI.Nagata.W08.automorphicOfChartHolomorphic

theorem OAI.Nagata.W08.quotientSectionOfAutomorphic_isChartHolomorphic line 528

Source documentation

When the actual chart slices cover the base, descent is holomorphic everywhere.

theorem quotientSectionOfAutomorphic_isChartHolomorphic (τ γ : ℂˣ) (n : ℤ)
    (hτ : ‖(τ : ℂ)‖ < 1)
    (hcover : ∀ z : ℂˣ, ∃ U : Set ℂˣ, ∃ _ : IsOpen U,
      ∃ _ : Set.InjOn (torusPointMk τ) U, z ∈ U)
    (f : automorphicSections (τ : ℂ) n (γ : ℂ)) :
    IsChartHolomorphic τ γ n hτ (quotientSectionOfAutomorphic τ γ n f) := by
…

Mentions: OAI.Nagata.W08.automorphicSections, OAI.Nagata.W08.IsChartHolomorphic, OAI.Nagata.W08.quotientSectionOfAutomorphic

def OAI.Nagata.W08.holomorphicQuotientSectionEquiv line 538
theorem OAI.Nagata.W08.positivePeriod_norm_lt_one line 572
Source documentation
The source's actual unit-valued positive period has norm less than one.
```
theorem positivePeriod_norm_lt_one {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) :
    ‖((positivePeriod τ hτ : ℂˣ) : ℂ)‖ < 1 := by
…
```

theorem OAI.Nagata.W08.sourcePeriod_chartCover line 578

Source documentation

Actual injective open slices cover every source covering-space point.

theorem sourcePeriod_chartCover {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) :
    ∀ z : ℂˣ, ∃ U : Set ℂˣ, ∃ _ : IsOpen U,
      ∃ _ : Set.InjOn (torusPointMk (positivePeriod τ hτ)) U, z ∈ U := by
…

def OAI.Nagata.W08.sourceHolomorphicQuotientSectionEquiv line 586