OAI/AlgebraicGeometry/PlaneCurves/SectionKernels.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Nagata.W20.ActualSection line 21
2. def OAI.Nagata.W20.localScalar line 25

   Source documentation

   The actual fixed local covering-space expression in logarithmic coordinates.

   def localScalar {τ γL γP : ℂ} {d : ℤ} {m : ℕ} {P : ℂ → ℂ}
       (F : ActualSection τ γL γP d m P) (z₀ x y : ℂ) : ℂ :=
   …

   Mentions: OAI.Nagata.W20.ActualSection

3. def OAI.Nagata.W20.actualTransverse line 30

   Source documentation

   The finite coefficient formula for the b-th transverse derivative at y=0.

   def actualTransverse {τ γL γP : ℂ} {d : ℤ} {m : ℕ} {P : ℂ → ℂ}
       (F : ActualSection τ γL γP d m P) (z₀ : ℂ) (b : ℕ) (x : ℂ) : ℂ :=
   …

   Mentions: OAI.Nagata.W20.ActualSection

4. theorem OAI.Nagata.W20.scalarExpression_eq_sum_range line 37

   Source documentation

   A bounded polynomial section has exactly the expected finite sum in the covering frame, including all zero coefficients and the degree-zero block.

   theorem scalarExpression_eq_sum_range {τ γL γP : ℂ} {d : ℤ} {m : ℕ}
       {P : ℂ → ℂ} (F : ActualSection τ γL γP d m P) (z v : ℂ) :
       scalarExpression F.val z v =
         ∑ j ∈ Finset.range ((d / 3).toNat + 1), F.val.coeff j z * v ^ j := by
   …

   Mentions: OAI.Nagata.W20.ActualSection

5. theorem OAI.Nagata.W20.localScalar_eq_sum_exp line 52

   Source documentation

   The logarithmic fiber coordinate yields exponential monomials exactly.

   theorem localScalar_eq_sum_exp {τ γL γP : ℂ} {d : ℤ} {m : ℕ}
       {P : ℂ → ℂ} (F : ActualSection τ γL γP d m P) (z₀ x y : ℂ) :
       localScalar F z₀ x y =
         ∑ j ∈ Finset.range ((d / 3).toNat + 1),
           F.val.coeff j (z₀ * Complex.exp x) * Complex.exp ((j : ℂ) * y) := by
   …

   Mentions: OAI.Nagata.W20.ActualSection, OAI.Nagata.W20.localScalar

6. theorem OAI.Nagata.W20.actualTransverse_eq_derivative line 62

   Source documentation

   This proves that the finite coefficient formula is the actual repeated y derivative of the genuine local scalar expression.

   theorem actualTransverse_eq_derivative {τ γL γP : ℂ} {d : ℤ} {m : ℕ}
       {P : ℂ → ℂ} (F : ActualSection τ γL γP d m P) (z₀ x : ℂ) (b : ℕ) :
       actualTransverse F z₀ b x = iteratedDeriv b (fun y => localScalar F z₀ x y) 0 := by
   …

   Mentions: OAI.Nagata.W20.ActualSection, OAI.Nagata.W20.actualTransverse, OAI.Nagata.W20.localScalar

7. theorem OAI.Nagata.W20.logarithmicCoefficient_differentiable line 81

   Source documentation

   Each coefficient is holomorphic after the actual common logarithmic coordinate change; z₀≠0 guarantees the chart remains in the punctured plane.

   theorem logarithmicCoefficient_differentiable {τ γL γP : ℂ} {d : ℤ} {m : ℕ}
       {P : ℂ → ℂ} (F : ActualSection τ γL γP d m P)
       (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z) {z₀ : ℂ} (hz₀ : z₀ ≠ 0) (j : ℕ) :
       Differentiable ℂ (fun x => F.val.coeff j (z₀ * Complex.exp x)) := by
   …

   Mentions: OAI.Nagata.W20.ActualSection

8. theorem OAI.Nagata.W20.actualTransverse_differentiable line 92

   Source documentation

   The transverse expressions needed in collision are genuine entire holomorphic functions, proved from the actual coefficient-space definition.

   theorem actualTransverse_differentiable {τ γL γP : ℂ} {d : ℤ} {m : ℕ}
       {P : ℂ → ℂ} (F : ActualSection τ γL γP d m P)
       (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z) {z₀ : ℂ} (hz₀ : z₀ ≠ 0) (b : ℕ) :
       Differentiable ℂ (actualTransverse F z₀ b) := by
   …

   Mentions: OAI.Nagata.W20.ActualSection, OAI.Nagata.W20.actualTransverse

9. theorem OAI.Nagata.W20.actualTransverse_add line 100
10. theorem OAI.Nagata.W20.actualTransverse_smul line 107
11. def OAI.Nagata.W20.actualTransverseLinear line 115

    Source documentation

    A transverse expression is a linear function of the actual polynomial section, before any choice of basis.

    def actualTransverseLinear {τ γL γP : ℂ} {d : ℤ} {m : ℕ} {P : ℂ → ℂ}
        (z₀ : ℂ) (b : ℕ) : ActualSection τ γL γP d m P →ₗ[ℂ] (ℂ → ℂ) where
    …

    Mentions: OAI.Nagata.W20.ActualSection

12. def OAI.Nagata.W20.actualJetMap line 135

    Source documentation

    The actual manuscript jet map on the concrete polynomial section space. Its linearity follows from proved holomorphicity and differentiation rules.

    def actualJetMap {τ γL γP : ℂ} {d : ℤ} {m : ℕ} {P : ℂ → ℂ}
        (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z) {z₀ : ℂ} (hz₀ : z₀ ≠ 0) (q : ℕ) :
        ActualSection τ γL γP d m P →ₗ[ℂ] (Nagata.Workers.W30.JetIndex q m → ℂ) where
    …

    Mentions: OAI.Nagata.W20.ActualSection, OAI.Nagata.Workers.W30.JetIndex

13. theorem OAI.Nagata.W20.actualJetMap_apply_eq_mixed_derivative line 158

    Source documentation

    The constructed linear map is exactly the mixed partial derivative operator in the fixed local frame, not merely a matrix given a matching name.

    theorem actualJetMap_apply_eq_mixed_derivative {τ γL γP : ℂ} {d : ℤ} {m : ℕ}
        {P : ℂ → ℂ} (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z)
        {z₀ : ℂ} (hz₀ : z₀ ≠ 0) {q : ℕ}
        (F : ActualSection τ γL γP d m P) (row : Nagata.Workers.W30.JetIndex q m) :
        actualJetMap hP hz₀ q F row =
          iteratedDeriv row.2.val (fun x =>
            iteratedDeriv row.1.val (fun y => localScalar F z₀ x y) 0) 0 := by
    …

    Mentions: OAI.Nagata.W20.ActualSection, OAI.Nagata.Workers.W30.JetIndex, OAI.Nagata.W20.actualJetMap, OAI.Nagata.W20.localScalar

14. def OAI.Nagata.W20.transverseExpression line 190

    Source documentation

    The local scalar expression of the b-th transverse derivative, written in a fixed finite family of actual holomorphic functions.

    def transverseExpression {ι : Type*} [Fintype ι] {m : ℕ}
        (basis : ι → Fin m → ℂ → ℂ) (c : ι → ℂ) (b : Fin m) (z : ℂ) : ℂ :=
    …

15. theorem OAI.Nagata.W20.transverseExpression_smul line 194
16. theorem OAI.Nagata.W20.transverseExpression_differentiableOn line 200

    Source documentation

    Finite linear combinations retain holomorphicity of the local basis.

    theorem transverseExpression_differentiableOn {ι : Type*} [Fintype ι]
        {m : ℕ} {U : Set ℂ} (basis : ι → Fin m → ℂ → ℂ)
        (hbasis : ∀ i b, DifferentiableOn ℂ (basis i b) U)
        (c : ι → ℂ) (b : Fin m) :
        DifferentiableOn ℂ (transverseExpression basis c b) U := by
    …

    Mentions: OAI.Nagata.W20.transverseExpression

17. def OAI.Nagata.W20.coefficientJetMap line 211

    Source documentation

    The manuscript's actual finite row shape, with entries obtained by complex differentiation of the local basis functions.

    def coefficientJetMap {ι : Type*} [Fintype ι] (q m : ℕ)
        (basis : ι → Fin m → ℂ → ℂ) :
        (ι → ℂ) →ₗ[ℂ] (Nagata.Workers.W30.JetIndex q m → ℂ) where
    …

    Mentions: OAI.Nagata.Workers.W30.JetIndex

18. theorem OAI.Nagata.W20.coefficientJetMap_apply_eq_derivative line 225

    Source documentation

    The derivative-entry matrix agrees with differentiating the synthesized local scalar expression. This is an actual bridge, not the definition of geometric multiplicity.

    theorem coefficientJetMap_apply_eq_derivative {ι : Type*} [Fintype ι]
        {q m : ℕ} {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
        (basis : ι → Fin m → ℂ → ℂ)
        (hbasis : ∀ i b, DifferentiableOn ℂ (basis i b) U)
        (c : ι → ℂ) (row : Nagata.Workers.W30.JetIndex q m) :
        coefficientJetMap q m basis c row =
          iteratedDeriv row.2.val (transverseExpression basis c row.1) 0 := by
    …

    Mentions: OAI.Nagata.Workers.W30.JetIndex, OAI.Nagata.W20.coefficientJetMap, OAI.Nagata.W20.transverseExpression

19. theorem OAI.Nagata.W20.nonzero_collision_jet_kernel line 248

    Source documentation

    One normalized subsequence works for every transverse order b and every jet row simultaneously. The conclusion is a genuine nonzero vector in the kernel of the actual derivative matrix, with no factorization assumption.

    theorem nonzero_collision_jet_kernel {ι : Type*} [Fintype ι]
        {q m : ℕ} {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
        (basis : ι → Fin m → ℂ → ℂ)
        (hbasis : ∀ i b, DifferentiableOn ℂ (basis i b) U)
        (c : ℕ → ι → ℂ) (hcnorm : ∀ n, ‖c n‖ = 1)
        (ξ : ℕ → Fin q → ℂ)
        (hξlim : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
        (hξinj : ∀ n, Function.Injective (ξ n))
        (hξmem : ∀ n i, ξ n i ∈ U)
        (horder : ∀ n (b : Fin m) i, (↑(m - b.val) : ℕ∞) ≤
          analyticOrderAt (transverseExpression basis (c n) b) (ξ n i)) :
        ∃ c₀ : ι → ℂ, ‖c₀‖ = 1 ∧ c₀ ≠ 0 ∧ coefficientJetMap q m basis c₀ = 0 := by
    …

    Mentions: OAI.Nagata.W20.transverseExpression, OAI.Nagata.W20.coefficientJetMap

20. theorem OAI.Nagata.W20.nonzero_collision_jet_kernel_of_nonzero line 287

    Source documentation

    Nonzero input coefficient vectors can be normalized without weakening any analytic-order lower bound. Thus the normalization hypothesis in the compactness lemma is discharged for actual nonzero vectors.

    theorem nonzero_collision_jet_kernel_of_nonzero {ι : Type*} [Fintype ι]
        {q m : ℕ} {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
        (basis : ι → Fin m → ℂ → ℂ)
        (hbasis : ∀ i b, DifferentiableOn ℂ (basis i b) U)
        (c : ℕ → ι → ℂ) (hc : ∀ n, c n ≠ 0)
        (ξ : ℕ → Fin q → ℂ)
        (hξlim : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
        (hξinj : ∀ n, Function.Injective (ξ n))
        (hξmem : ∀ n i, ξ n i ∈ U)
        (horder : ∀ n (b : Fin m) i, (↑(m - b.val) : ℕ∞) ≤
          analyticOrderAt (transverseExpression basis (c n) b) (ξ n i)) :
        ∃ c₀ : ι → ℂ, ‖c₀‖ = 1 ∧ c₀ ≠ 0 ∧ coefficientJetMap q m basis c₀ = 0 := by
    …

    Mentions: OAI.Nagata.W20.transverseExpression, OAI.Nagata.W20.coefficientJetMap

21. theorem OAI.Nagata.W20.actualTransverse_basis_repr line 329

    Source documentation

    Basis coordinates reconstruct the actual transverse expression.

    theorem actualTransverse_basis_repr {ι : Type*} [Fintype ι]
        {τ γL γP : ℂ} {d : ℤ} {m : ℕ} {P : ℂ → ℂ}
        (B : Basis ι ℂ (ActualSection τ γL γP d m P))
        (F : ActualSection τ γL γP d m P) (z₀ : ℂ) (b : Fin m) (x : ℂ) :
        transverseExpression (fun i b => actualTransverse (B i) z₀ b.val)
          (fun i => B.repr F i) b x = actualTransverse F z₀ b.val x := by
    …

    Mentions: OAI.Nagata.W20.ActualSection, OAI.Nagata.W20.transverseExpression, OAI.Nagata.W20.actualTransverse

22. theorem OAI.Nagata.W20.actual_nonzero_collision_kernel line 339
23. theorem OAI.Nagata.W20.actual_kernel_from_local_powerSeries line 392

    Source documentation

    Concrete local power-series multiplicity implies a nonzero element of the actual Wτ jet kernel. The input is vanishing of genuine convergent Taylor coefficients, not vanishing of the desired output jets.

    theorem actual_kernel_from_local_powerSeries {ι : Type*} [Fintype ι]
        {τ γL γP : ℂ} {d : ℤ} {m q : ℕ} {P : ℂ → ℂ}
        (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z)
        {z₀ : ℂ} (hz₀ : z₀ ≠ 0)
        (B : Basis ι ℂ (ActualSection τ γL γP d m P))
        (F : ℕ → ActualSection τ γL γP d m P) (hF : ∀ n, F n ≠ 0)
        {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
        (ξ : ℕ → Fin q → ℂ)
        (hξlim : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
        (hξinj : ∀ n, Function.Injective (ξ n))
        (hξmem : ∀ n i, ξ n i ∈ U)
        (S : ℕ → Fin q → FormalMultilinearSeries ℂ (ℂ × ℂ) ℂ)
    …

    Mentions: OAI.Nagata.W20.ActualSection

24. theorem OAI.Nagata.W20.actual_kernel_of_every_configuration line 436

    Source documentation

    Universal necessary-W existence with genuine local Taylor multiplicity forces a nonzero vector in the actual section jet kernel, at one fixed τ.

    theorem actual_kernel_of_every_configuration {ι : Type*} [Fintype ι]
        {τ γL γP : ℂ} {d : ℤ} {m q : ℕ} {P : ℂ → ℂ}
        (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z)
        {z₀ : ℂ} (hz₀ : z₀ ≠ 0)
        (B : Basis ι ℂ (ActualSection τ γL γP d m P))
        {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
        (hEvery : ∀ p : Fin q → ℂ, Function.Injective p → (∀ i, p i ∈ U) →
          ∃ F : ActualSection τ γL γP d m P, F ≠ 0 ∧
            ∀ i, Nagata.Workers.W28.HasAnalyticOrderAtLeast (𝕜 := ℂ)
    …

    Mentions: OAI.Nagata.W20.ActualSection, OAI.Nagata.Workers.W28.HasAnalyticOrderAtLeast

25. theorem OAI.Nagata.W20.not_every_configuration_of_injective_actualJetMap line 461

    Source documentation

    In particular, an injective actual jet map excludes the universal necessary-W property. This formulation needs no choice across degeneration parameters: every parameter is fixed before applying the theorem.

    theorem not_every_configuration_of_injective_actualJetMap {ι : Type*} [Fintype ι]
        {τ γL γP : ℂ} {d : ℤ} {m q : ℕ} {P : ℂ → ℂ}
        (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z)
        {z₀ : ℂ} (hz₀ : z₀ ≠ 0)
        (B : Basis ι ℂ (ActualSection τ γL γP d m P))
        {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
        (hJ : Function.Injective (actualJetMap (τ := τ) (γL := γL) (γP := γP)
    …

    Mentions: OAI.Nagata.W20.ActualSection, OAI.Nagata.W20.actualJetMap

26. theorem OAI.Nagata.W20.actual_kernel_from_local_polynomial_multiplicity line 493

    Source documentation

    Local analytic polynomial representatives turn ordinary maximal-ideal-power multiplicity into the Taylor hypotheses of the actual section kernel theorem.

    theorem actual_kernel_from_local_polynomial_multiplicity {ι : Type*} [Fintype ι]
        {τ γL γP : ℂ} {d : ℤ} {m q : ℕ} {P : ℂ → ℂ}
        (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z)
        {z₀ : ℂ} (hz₀ : z₀ ≠ 0)
        (B : Basis ι ℂ (ActualSection τ γL γP d m P))
        (F : ℕ → ActualSection τ γL γP d m P) (hF : ∀ n, F n ≠ 0)
        {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
        (ξ : ℕ → Fin q → ℂ)
        (hξlim : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
        (hξinj : ∀ n, Function.Injective (ξ n))
        (hξmem : ∀ n i, ξ n i ∈ U)
        (A : ℕ → Fin q → MvPolynomial (Fin 2) ℂ)
    …

    Mentions: OAI.Nagata.W20.ActualSection

27. theorem OAI.Nagata.W20.actual_kernel_from_local_polynomial_with_frame line 528

    Source documentation

    The same genuine polynomial multiplicity bridge allows an analytic local frame factor, including all holomorphic units used by the manuscript.

    theorem actual_kernel_from_local_polynomial_with_frame {ι : Type*} [Fintype ι]
        {τ γL γP : ℂ} {d : ℤ} {m q : ℕ} {P : ℂ → ℂ}
        (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z)
        {z₀ : ℂ} (hz₀ : z₀ ≠ 0)
        (B : Basis ι ℂ (ActualSection τ γL γP d m P))
        (F : ℕ → ActualSection τ γL γP d m P) (hF : ∀ n, F n ≠ 0)
        {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
        (ξ : ℕ → Fin q → ℂ)
        (hξlim : ∀ i, Tendsto (fun n => ξ n i) atTop (𝓝 0))
        (hξinj : ∀ n, Function.Injective (ξ n))
        (hξmem : ∀ n i, ξ n i ∈ U)
        (A : ℕ → Fin q → MvPolynomial (Fin 2) ℂ)
    …

    Mentions: OAI.Nagata.W20.ActualSection