Gluing.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Holomorphic local division and gluing on multiplier quotient bundles

theorem OAI.Nagata.LocalDivision.exists_analytic_quotient_at_simple_zero line 27

Source documentation

Dividing by a power of a function with a simple zero produces an analytic germ precisely when the numerator has sufficient vanishing. This constructs the germ, rather than assuming a global quotient exists.

theorem exists_analytic_quotient_at_simple_zero {f P : ℂ → ℂ} {z₀ : ℂ}
    (hf : AnalyticAt ℂ f z₀) (hP : AnalyticAt ℂ P z₀)
    (hP0 : P z₀ = 0) (hP' : deriv P z₀ ≠ 0) (k : ℕ)
    (horder : (k : ℕ∞) ≤ analyticOrderAt f z₀) :
    ∃ g : ℂ → ℂ, AnalyticAt ℂ g z₀ ∧
      ∀ᶠ z in 𝓝 z₀, f z = P z ^ k * g z := by
…

theorem OAI.Nagata.LocalDivision.analytic_quotient_at_nonzero line 45

Source documentation

Away from the zero divisor, the usual pointwise quotient is analytic.

theorem analytic_quotient_at_nonzero {f P : ℂ → ℂ} {z₀ : ℂ}
    (hf : AnalyticAt ℂ f z₀) (hP : AnalyticAt ℂ P z₀)
    (hP0 : P z₀ ≠ 0) (k : ℕ) :
    AnalyticAt ℂ (fun z => f z / P z ^ k) z₀ :=
…

theorem OAI.Nagata.LocalDivision.exists_analytic_quotient line 53

Source documentation

One uniform local-division statement handles both marked points and their complement. The derivative condition is needed only at a zero of P.

theorem exists_analytic_quotient {f P : ℂ → ℂ} {z₀ : ℂ}
    (hf : AnalyticAt ℂ f z₀) (hP : AnalyticAt ℂ P z₀) (k : ℕ)
    (hzero : P z₀ = 0 → deriv P z₀ ≠ 0 ∧
      (k : ℕ∞) ≤ analyticOrderAt f z₀) :
    ∃ g : ℂ → ℂ, AnalyticAt ℂ g z₀ ∧
      ∀ᶠ z in 𝓝 z₀, f z = P z ^ k * g z := by
…

theorem OAI.Nagata.LocalDivision.analytic_quotient_germ_unique line 79

Source documentation

Local quotient germs are unique wherever the denominator is not the zero germ.

theorem analytic_quotient_germ_unique {f P g h : ℂ → ℂ} {z₀ : ℂ} (k : ℕ)
    (hP : AnalyticAt ℂ P z₀) (hPfin : analyticOrderAt P z₀ ≠ ⊤)
    (hg : AnalyticAt ℂ g z₀) (hh : AnalyticAt ℂ h z₀)
    (hfg : ∀ᶠ z in 𝓝 z₀, f z = P z ^ k * g z)
    (hfh : ∀ᶠ z in 𝓝 z₀, f z = P z ^ k * h z) :
    g =ᶠ[𝓝 z₀] h := by
…

theorem OAI.Nagata.LocalDivision.continuous_eq_at_of_eq_off_divisor line 96

Source documentation

A continuous identity known off a nonzero analytic divisor extends across its zero set. This is used to recover multiplier transition identities after gluing.

theorem continuous_eq_at_of_eq_off_divisor {P g h : ℂ → ℂ} {U : Set ℂ} {z₀ : ℂ}
    (hU : IsOpen U) (hz₀ : z₀ ∈ U) (hP : AnalyticAt ℂ P z₀)
    (hPfin : analyticOrderAt P z₀ ≠ ⊤) (hg : ContinuousAt g z₀)
    (hh : ContinuousAt h z₀)
    (heq : ∀ z ∈ U, P z ≠ 0 → g z = h z) : g z₀ = h z₀ := by
…

theorem OAI.Nagata.LocalDivision.multiply_power_injective_on line 114

Source documentation

Multiplication by P^k is injective on continuous functions on U when P has no zero germ. This is the noncancellation needed for the positive-index blocks.

theorem multiply_power_injective_on {P f g : ℂ → ℂ} {U : Set ℂ}
    (hU : IsOpen U) (k : ℕ) (hP : AnalyticOnNhd ℂ P U)
    (hPfin : ∀ z ∈ U, analyticOrderAt P z ≠ ⊤)
    (hf : ∀ z ∈ U, ContinuousAt f z) (hg : ∀ z ∈ U, ContinuousAt g z)
    (hmul : ∀ z ∈ U, P z ^ k * f z = P z ^ k * g z) :
    Set.EqOn f g U := by
…

theorem OAI.Nagata.LocalDivision.multiply_power_nonzero line 128

Source documentation

Consequently an actual nonzero coefficient does not vanish identically when multiplied by a marked-product power.

theorem multiply_power_nonzero {P f : ℂ → ℂ} {U : Set ℂ}
    (hU : IsOpen U) (k : ℕ) (hP : AnalyticOnNhd ℂ P U)
    (hPfin : ∀ z ∈ U, analyticOrderAt P z ≠ ⊤)
    (hf : ∀ z ∈ U, ContinuousAt f z) (hne : ∃ z ∈ U, f z ≠ 0) :
    ∃ z ∈ U, P z ^ k * f z ≠ 0 := by
…

theorem OAI.Nagata.LocalDivision.glue_analytic_quotients line 147

Source documentation

Compatible local quotient germs glue to a genuine global analytic function on any open domain. Uniqueness was proved above by ordinary analytic cancellation.

theorem glue_analytic_quotients {f P : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U)
    (k : ℕ) (hP : AnalyticOnNhd ℂ P U)
    (hPfin : ∀ z ∈ U, analyticOrderAt P z ≠ ⊤)
    (hlocal : ∀ z ∈ U, ∃ g : ℂ → ℂ, AnalyticAt ℂ g z ∧
      ∀ᶠ w in 𝓝 z, f w = P w ^ k * g w) :
    ∃ G : ℂ → ℂ, AnalyticOnNhd ℂ G U ∧
      (∀ z ∈ U, f z = P z ^ k * G z) ∧ (∀ z ∉ U, G z = 0) := by
…

theorem OAI.Nagata.LocalDivision.exists_global_analytic_quotient line 174

Source documentation

Global extension across the simple-zero divisor of P. The only vanishing hypothesis is the actual numerator order at the zeros, not a pre-existing quotient.

theorem exists_global_analytic_quotient {f P : ℂ → ℂ} {U : Set ℂ}
    (hU : IsOpen U) (hf : AnalyticOnNhd ℂ f U) (hP : AnalyticOnNhd ℂ P U)
    (k : ℕ) (hzero : ∀ z ∈ U, P z = 0 → deriv P z ≠ 0 ∧
      (k : ℕ∞) ≤ analyticOrderAt f z) :
    ∃ G : ℂ → ℂ, AnalyticOnNhd ℂ G U ∧
      (∀ z ∈ U, f z = P z ^ k * G z) ∧ (∀ z ∉ U, G z = 0) := by
…

theorem OAI.Nagata.LocalDivision.quotient_nonzero_of_nonzero line 191

Source documentation

A nonzero original coefficient stays nonzero after the constructed division.

theorem quotient_nonzero_of_nonzero {f P G : ℂ → ℂ} {U : Set ℂ} (k : ℕ)
    (hfactor : ∀ z ∈ U, f z = P z ^ k * G z)
    (hf : ∃ z ∈ U, f z ≠ 0) : ∃ z ∈ U, G z ≠ 0 := by
…

def OAI.Nagata.CoefficientSpaces.sectionCoverMap line 210
Source documentation
Literal multiplication by a section on the genuine line-bundle cover.
```
def sectionCoverMap {τ δ : ℂˣ} {s : ℤ}
    (P : Nagata.W08.automorphicSections (τ : ℂ) s (δ : ℂ))
    (p : MultiplicativeLineCover ℂ) : MultiplicativeLineCover ℂ :=
…
```
Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.CoefficientSpaces.sectionCoverMap_step line 216

Source documentation

Tensor multiplication commutes with the actual period generator.

theorem sectionCoverMap_step (τ γ δ : ℂˣ) (n s : ℤ)
    (P : Nagata.W08.automorphicSections (τ : ℂ) s (δ : ℂ))
    (p : MultiplicativeLineCover ℂ) :
    sectionCoverMap P (multiplierStep τ γ n p) =
      multiplierStep τ (γ * δ) (n + s) (sectionCoverMap P p) := by
…

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

theorem OAI.Nagata.CoefficientSpaces.sectionCoverMap_iterate line 231

Source documentation

Equivariance holds for every integer period, including inverse transitions.

theorem sectionCoverMap_iterate (τ γ δ : ℂˣ) (n s k : ℤ)
    (P : Nagata.W08.automorphicSections (τ : ℂ) s (δ : ℂ))
    (p : MultiplicativeLineCover ℂ) :
    sectionCoverMap P (multiplierIterate τ γ n k p) =
      multiplierIterate τ (γ * δ) (n + s) k (sectionCoverMap P p) := by
…

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

def OAI.Nagata.CoefficientSpaces.sectionQuotientMap line 257

Source documentation

The actual globally defined map between the two multiplier quotients.

def sectionQuotientMap (τ γ δ : ℂˣ) (n s : ℤ)
    (P : Nagata.W08.automorphicSections (τ : ℂ) s (δ : ℂ)) :
    MultiplierQuotient τ γ n → MultiplierQuotient τ (γ * δ) (n + s) :=
…

Mentions: OAI.Nagata.W08.automorphicSections

theorem OAI.Nagata.CoefficientSpaces.sectionQuotientMap_mk line 267

Source documentation

Evaluation on any genuine lifted fibre is multiplication by the section value.

theorem sectionQuotientMap_mk (τ γ δ : ℂˣ) (n s : ℤ)
    (P : Nagata.W08.automorphicSections (τ : ℂ) s (δ : ℂ))
    (z : ℂˣ) (t : ℂ) :
    sectionQuotientMap τ γ δ n s P (Quotient.mk _ (z, t)) =
      Quotient.mk _ (z, P.val z * t) := rfl
…

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

def OAI.Nagata.FiberCoordinateChange.fibreChart line 283

Source documentation

Actual fibre substitution w=P(z)*v over an open base where P is nonzero.

noncomputable def fibreChart (P : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U)
    (hP : AnalyticOnNhd ℂ P U) (hne : ∀ z ∈ U, P z ≠ 0) :
    OpenPartialHomeomorph (ℂ × ℂ) (ℂ × ℂ) where
…

theorem OAI.Nagata.FiberCoordinateChange.fibreChart_analyticAt line 315

Source documentation

Analyticity of the actual forward fibre coordinate map.

theorem fibreChart_analyticAt (P : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U)
    (hP : AnalyticOnNhd ℂ P U) (hne : ∀ z ∈ U, P z ≠ 0)
    (x : ℂ × ℂ) (hx : x.1 ∈ U) :
    AnalyticAt ℂ (fibreChart P U hU hP hne) x := by
…

Mentions: OAI.Nagata.FiberCoordinateChange.fibreChart

theorem OAI.Nagata.FiberCoordinateChange.fibreChart_symm_analyticAt line 324

Source documentation

Analyticity of the actual inverse fibre coordinate map.

theorem fibreChart_symm_analyticAt (P : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U)
    (hP : AnalyticOnNhd ℂ P U) (hne : ∀ z ∈ U, P z ≠ 0)
    (x : ℂ × ℂ) (hx : x.1 ∈ U) :
    AnalyticAt ℂ (fibreChart P U hU hP hne).symm x := by
…

Mentions: OAI.Nagata.FiberCoordinateChange.fibreChart

theorem OAI.Nagata.FiberCoordinateChange.order_preserved_by_fibre_substitution line 334

Source documentation

Exactly the multiplicity-preserving transformation in necessary-W: substitute w=P*v and divide the value frame by P^m.

theorem order_preserved_by_fibre_substitution
    (P : ℂ → ℂ) (U : Set ℂ) (hU : IsOpen U)
    (hP : AnalyticOnNhd ℂ P U) (hne : ∀ z ∈ U, P z ≠ 0)
    (F : (ℂ × ℂ) → ℂ) (x : ℂ × ℂ) (hx : x.1 ∈ U) (m : ℕ) :
    HasAnalyticOrderAtLeast (𝕜 := ℂ)
…

theorem OAI.Nagata.LocalDivision.quotient_transition_off_zero line 363

Source documentation

Cancellation derives the quotient transition wherever the denominator is nonzero.

theorem quotient_transition_off_zero {T : ℂ → ℂ} {f P G A B : ℂ → ℂ}
    (k : ℕ) (z : ℂ) (hP : P z ≠ 0) (hB : B z ≠ 0)
    (hfz : f z = P z ^ k * G z) (hfT : f (T z) = P (T z) ^ k * G (T z))
    (htf : f (T z) = A z * f z) (htP : P (T z) = B z * P z) :
    G (T z) = (A z / B z ^ k) * G z := by
…

theorem OAI.Nagata.LocalDivision.quotient_transition_global line 384

Source documentation

The actual quotient transition extends over all zeros by continuity and isolated zeros. This closes the local-to-global transition step.

theorem quotient_transition_global {T : ℂ → ℂ} {f P G A B : ℂ → ℂ}
    {U : Set ℂ} (hU : IsOpen U) (k : ℕ)
    (hP : AnalyticOnNhd ℂ P U) (hPfin : ∀ z ∈ U, analyticOrderAt P z ≠ ⊤)
    (hTU : Set.MapsTo T U U) (hB : ∀ z ∈ U, B z ≠ 0)
    (hfactor : ∀ z ∈ U, f z = P z ^ k * G z)
    (htf : ∀ z ∈ U, f (T z) = A z * f z)
    (htP : ∀ z ∈ U, P (T z) = B z * P z)
    (hleft : ∀ z ∈ U, ContinuousAt (fun w => G (T w)) z)
    (hright : ∀ z ∈ U, ContinuousAt (fun w => (A w / B w ^ k) * G w) z) :
    ∀ z ∈ U, G (T z) = (A z / B z ^ k) * G z := by
…

def OAI.Nagata.CoefficientSpaces.multiplySection line 410
Source documentation
The literal multiplication map restricted to actual automorphic sections.
```
noncomputable def multiplySection (τ γ : ℂ) (n : ℤ) (P : ℂ → ℂ) (k : ℕ) :
    Nagata.W08.automorphicSections τ n γ →ₗ[ℂ] (ℂ → ℂ) :=
…
```
Mentions: OAI.Nagata.W08.automorphicSections
theorem OAI.Nagata.CoefficientSpaces.multiplySection_injective line 417
Source documentation
No nonzero source section is lost in the positive-index coefficient image. The omitted point contributes no fake section because both representatives are normalized to zero there.
```
theorem multiplySection_injective (τ γ : ℂ) (n : ℤ) (P : ℂ → ℂ) (k : ℕ)
    (hP : AnalyticOnNhd ℂ P {z | z ≠ 0})
    (hPfin : ∀ z ≠ 0, analyticOrderAt P z ≠ ⊤) :
    Function.Injective (multiplySection τ γ n P k) := by
…
```
Mentions: OAI.Nagata.CoefficientSpaces.multiplySection

theorem OAI.Nagata.CoefficientSpaces.quotient_multiplier_identity line 441

Source documentation

The exact degree and multiplier of a quotient coefficient.

theorem quotient_multiplier_identity {γ δ z : ℂ} (hδ : δ ≠ 0) (hz : z ≠ 0)
    (n s : ℤ) (k : ℕ) :
    (γ * z ^ (-n)) / (δ * z ^ (-s)) ^ k =
      (γ / δ ^ k) * z ^ (-(n - (k : ℤ) * s)) := by
…

theorem OAI.Nagata.CoefficientSpaces.exists_automorphic_quotient line 449