OAI/AlgebraicGeometry/PlaneCurves/FixedCurveSections.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nagata.CoefficientSpaces.source_necessary_W_of_smooth_cubic_geometry line 20

   Source documentation

   Genuine universal-support specialization, transported to the exact Wτ used by the source basis and collision map, with all scalar identifications discharged.

   theorem source_necessary_W_of_smooth_cubic_geometry {q d m : ℕ} {τ : ℝ}
       (hτ : 0 < τ) (hτone : τ < 1)
       (hUniversal : Nagata.W13.UniversalSupport (9 + q) d (fun _ => m))
       (marks : Fin 9 → ℝ) (a x0 : ℝ)
       (hdisjoint : Pairwise (fun i j => ∀ k : ℤ,
         ((τ ^ marks i : ℝ) : ℂ) ≠ ((τ ^ marks j : ℝ) : ℂ) * (τ : ℂ) ^ k))
       (ξ : Fin q → ℂ)
       (hpP : ∀ i, (Nagata.W22.rayMarkedSection hτ hτone marks).val
         (tauPower τ x0 * Complex.exp (ξ i)) ≠ 0)
       (C : MvPolynomial (Fin 3) ℂ) (hC : C.IsHomogeneous 3)
       (X : Fin 3 → Nagata.W08.automorphicSections (τ : ℂ) 3
         (tauPower τ (((∑ i, marks i) + a) / 3)))
   …

   Mentions: OAI.Nagata.W13.UniversalSupport, OAI.Nagata.W22.rayMarkedSection, OAI.Nagata.W08.automorphicSections

2. theorem OAI.Nagata.CoefficientSpaces.source_fixed_necessary_W line 93

   Source documentation

   For every fixed period, all distinct nearby moving configurations have an actual nonzero section with the required multiplicities, with the source's fixed marks and eta=(sum marks+a)/3 retained literally.

   theorem source_fixed_necessary_W {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
       (marks : Fin 9 → ℝ) (hmarks : Function.Injective marks)
       (hmbounds : ∀ i, 0 < marks i ∧ marks i < 1 / 2)
       (a : ℝ) (d m q : ℕ)
       (hUniversal : Nagata.W13.UniversalSupport (9 + q) d (fun _ => m)) :
       ∃ U : Set ℂ, IsOpen U ∧ (0 : ℂ) ∈ U ∧
         ∀ ξ : Fin q → ℂ, Function.Injective ξ → (∀ i, ξ i ∈ U) →
           ∃ F : genuineSourceSections hτ hτone marks a (d : ℤ) m, F ≠ 0 ∧
             ∀ i, HasAnalyticOrderAtLeast (𝕜 := ℂ)
   …

   Mentions: OAI.Nagata.W13.UniversalSupport

3. theorem OAI.Nagata.CoefficientSpaces.source_fixed_scaled_construction line 138

   Source documentation

   Scaling the actual universal plane equations gives the source construction for the same fixed marks at every period, hence on the required punctured limit.

   theorem source_fixed_scaled_construction {r d m : ℕ} (hr : 9 ≤ r)
       (hUniversal : Nagata.W13.UniversalSupport r d (fun _ => m))
       (n : ℕ) (marks : Fin 9 → ℝ) (hmarks : Function.Injective marks)
       (hmbounds : ∀ i, 0 < marks i ∧ marks i < 1 / 2) (a : ℝ) :
       ∀ᶠ τ : ℝ in 𝓝[>] (0 : ℝ),
         ∃ (hτ : 0 < τ) (hτone : τ < 1) (U : Set ℂ),
           IsOpen U ∧ (0 : ℂ) ∈ U ∧
           ∀ ξ : Fin (r - 9) → ℂ, Function.Injective ξ → (∀ i, ξ i ∈ U) →
             ∃ F : genuineSourceSections hτ hτone marks a ((n * d : ℕ) : ℤ) (n * m),
               F ≠ 0 ∧ ∀ i, HasAnalyticOrderAtLeast (𝕜 := ℂ)
   …

   Mentions: OAI.Nagata.W13.UniversalSupport