OAI/AlgebraicGeometry/PlaneCurves/PolynomialBases.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Nagata.Workers.W10.firstCoefficientEquiv line 22

   Source documentation

   The first branch is literally the common automorphic-section space.

   def firstCoefficientEquiv (τ γL γP : ℂ) (d m j : ℤ) (P : ℂ → ℂ) (hj : j ≤ m) :
       automorphicSections τ (3 * (d - 3 * m))
         (γL ^ (d - 3 * m) * normalMinusMarkedMultiplier γL γP ^ (m - j)) ≃ₗ[ℂ]
         coefficientSpace τ γL γP d m j P :=
   …

2. def OAI.Nagata.Workers.W10.highCoefficientMap line 29

   Source documentation

   The high-branch map is actual multiplication by the marked product power.

   def highCoefficientMap (τ γL γP : ℂ) (d m j : ℤ) (P : ℂ → ℂ) (hj : m < j) :
       automorphicSections τ (3 * (d - 3 * j)) (γL ^ (d - 3 * j)) →ₗ[ℂ]
         coefficientSpace τ γL γP d m j P where
   …

3. theorem OAI.Nagata.Workers.W10.highCoefficientMap_apply line 37
4. theorem OAI.Nagata.Workers.W10.highCoefficientMap_surjective line 42
5. theorem OAI.Nagata.Workers.W10.highCoefficientMap_injective line 51
6. def OAI.Nagata.Workers.W10.highCoefficientEquiv line 63

   Source documentation

   The high-branch image is linearly equivalent to its genuine source sections. This applies equally when d-3j=0; no positive-degree assumption hides the tip.

   def highCoefficientEquiv (τ γL γP : ℂ) (d m j : ℤ)
       (P : ℂ → ℂ) (hj : m < j)
       (hP : AnalyticOnNhd ℂ P {z | z ≠ 0})
       (hPfin : ∀ z ≠ 0, analyticOrderAt P z ≠ ⊤) :
       automorphicSections τ (3 * (d - 3 * j)) (γL ^ (d - 3 * j)) ≃ₗ[ℂ]
         coefficientSpace τ γL γP d m j P :=
   …

7. def OAI.Nagata.Workers.W10.highCoefficientBasisFromCoefficients line 75

   Source documentation

   A source basis constructed from checked coefficient data transports to the literal Pi-power image; no independent basis hypothesis is needed.

   def highCoefficientBasisFromCoefficients (τ γL γP : ℂ) (d m j : ℤ)
       (P : ℂ → ℂ) (hj : m < j)
       (hP : AnalyticOnNhd ℂ P {z | z ≠ 0})
       (hPfin : ∀ z ≠ 0, analyticOrderAt P z ≠ ⊤)
       (I : Type*) [Fintype I] [DecidableEq I]
       (c : automorphicSections τ (3 * (d - 3 * j)) (γL ^ (d - 3 * j)) →ₗ[ℂ] (I → ℂ))
       (hc : Function.Injective c)
       (v : I → automorphicSections τ (3 * (d - 3 * j)) (γL ^ (d - 3 * j)))
       (hv : ∀ i, c (v i) = Pi.single i 1) :
       Basis I ℂ (coefficientSpace τ γL γP d m j P) :=
   …

8. theorem OAI.Nagata.Workers.W10.polynomialSectionBasis_localScalar line 100
9. def OAI.Nagata.Workers.W10.sourceBlock line 131

   Source documentation

   The genuine source section space before high-branch multiplication by Pi.

   def sourceBlock (τ γL γP : ℂ) (d m j : ℤ) : Submodule ℂ (ℂ → ℂ) :=
   …

10. def OAI.Nagata.Workers.W10.sourceCoefficientEquiv line 139

    Source documentation

    Both positive-degree branches and the degree-zero tip use the literal source space and the actual injective marked-product multiplication.

    def sourceCoefficientEquiv (τ γL γP : ℂ) (d m j : ℤ) (P : ℂ → ℂ)
        (hP : AnalyticOnNhd ℂ P {z | z ≠ 0})
        (hPfin : ∀ z ≠ 0, analyticOrderAt P z ≠ ⊤) :
        sourceBlock τ γL γP d m j ≃ₗ[ℂ] coefficientSpace τ γL γP d m j P := by
    …

    Mentions: OAI.Nagata.Workers.W10.sourceBlock

11. def OAI.Nagata.Workers.W10.blockCoordinateMap line 150

    Source documentation

    Extract the source coordinates after the proved coefficient-image equivalence.

    def blockCoordinateMap (τ γL γP : ℂ) (d m j : ℤ) (a Δ : ℝ) (P : ℂ → ℂ)
        (hP : AnalyticOnNhd ℂ P {z | z ≠ 0})
        (hPfin : ∀ z ≠ 0, analyticOrderAt P z ≠ ⊤)
        (c : sourceBlock τ γL γP d m j →ₗ[ℂ] (ColumnFiber d m a Δ j → ℂ)) :
        coefficientSpace τ γL γP d m j P →ₗ[ℂ] (ColumnFiber d m a Δ j → ℂ) :=
    …

    Mentions: OAI.Nagata.Workers.W10.sourceBlock, OAI.Nagata.Workers.W10.ColumnFiber

12. theorem OAI.Nagata.Workers.W10.blockCoordinateMap_injective line 157
13. def OAI.Nagata.Workers.W10.literalPolynomialBasis line 168

    Source documentation

    A genuine basis on the literal polynomial-section space, conditional exactly on the source Laurent-coordinate injectivity and theta coefficient identities. Every index is an actual column in the manuscript's three-branch exponent set.

    def literalPolynomialBasis (τ γL γP : ℂ) (d m : ℤ) (a Δ : ℝ) (P : ℂ → ℂ)
        (hm : 0 ≤ m) (hd : 3 * m < d)
        (hP : AnalyticOnNhd ℂ P {z | z ≠ 0})
        (hPfin : ∀ z ≠ 0, analyticOrderAt P z ≠ ⊤)
        (c : ∀ j : Fin ((d / 3).toNat + 1), sourceBlock τ γL γP d m (j.val : ℤ) →ₗ[ℂ]
          (ColumnFiber d m a Δ (j.val : ℤ) → ℂ))
        (hc : ∀ j, Function.Injective (c j))
        (theta : ∀ j : Fin ((d / 3).toNat + 1), ColumnFiber d m a Δ (j.val : ℤ) →
          sourceBlock τ γL γP d m (j.val : ℤ))
        (htheta : ∀ j K, c j (theta j K) = Pi.single K 1) :
        Basis (Column d m a Δ) ℂ (polynomialSections τ γL γP d m P) := by
    …

    Mentions: OAI.Nagata.Workers.W10.sourceBlock, OAI.Nagata.Workers.W10.ColumnFiber

14. theorem OAI.Nagata.Workers.W10.literalPolynomialBasis_as_monomial line 220

    Source documentation

    Every literal column basis element is exactly its fiber monomial.

    theorem literalPolynomialBasis_as_monomial
        (j : Fin ((d / 3).toNat + 1)) (K : ColumnFiber d (m : ℤ) a Δ (j.val : ℤ)) :
        (literalPolynomialBasis τ γL γP d (m : ℤ) a Δ P (Int.natCast_nonneg m) hd hP hPfin
          c hc theta htheta (columnFiberEquiv d (m : ℤ) a Δ (Int.natCast_nonneg m) hd ⟨j, K⟩)).val =
        Polynomial.monomial j.val
          (sourceCoefficientEquiv τ γL γP d (m : ℤ) (j.val : ℤ) P hP hPfin (theta j K)).val := by
    …

    Mentions: OAI.Nagata.Workers.W10.ColumnFiber, OAI.Nagata.Workers.W10.literalPolynomialBasis, OAI.Nagata.Workers.W10.columnFiberEquiv, OAI.Nagata.Workers.W10.sourceCoefficientEquiv

15. theorem OAI.Nagata.Workers.W10.literalPolynomialBasis_localScalar line 233

    Source documentation

    The actual scalar expression equals a coefficient function times the fiber exponential. The equality is global, hence supplies every required local germ.

    theorem literalPolynomialBasis_localScalar
        (j : Fin ((d / 3).toNat + 1)) (K : ColumnFiber d (m : ℤ) a Δ (j.val : ℤ))
        (z₀ x y : ℂ) :
        Nagata.W20.localScalar
          (literalPolynomialBasis τ γL γP d (m : ℤ) a Δ P (Int.natCast_nonneg m) hd hP hPfin
            c hc theta htheta (columnFiberEquiv d (m : ℤ) a Δ (Int.natCast_nonneg m) hd ⟨j, K⟩))
          z₀ x y =
        (sourceCoefficientEquiv τ γL γP d (m : ℤ) (j.val : ℤ) P hP hPfin (theta j K)).val
          (z₀ * Complex.exp x) * Complex.exp ((j.val : ℂ) * y) := by
    …

    Mentions: OAI.Nagata.Workers.W10.ColumnFiber, OAI.Nagata.W20.localScalar, OAI.Nagata.Workers.W10.literalPolynomialBasis, OAI.Nagata.Workers.W10.columnFiberEquiv, OAI.Nagata.Workers.W10.sourceCoefficientEquiv