OAI/AlgebraicGeometry/PlaneCurves/KernelBridges.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nagata.Workers.W12.actual_basisJetMatrix_eq_of_local_expressions line 22

   Source documentation

   Local scalar formulas of actual basis elements prove every matrix entry. It suffices to identify germs on a genuine neighborhood of the chart origin.

   theorem actual_basisJetMatrix_eq_of_local_expressions
       {τ gammaL gammaP : ℂ} {d : ℤ} {q m : ℕ} {a delta : ℝ} {P : ℂ → ℂ}
       (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z) {z0 : ℂ} (hz0 : z0 ≠ 0)
       (e : Basis (Column d (m : ℤ) a delta) ℂ (ActualSection τ gammaL gammaP d m P))
       (coeff : Column d (m : ℤ) a delta → ℂ → ℂ)
       (hlocal : ∀ col, ∀ᶠ z : ℂ × ℂ in 𝓝 (0, 0),
         localScalar (e col) z0 z.1 z.2 =
           coeff col z.1 * Complex.exp ((col.val.1 : ℂ) * z.2)) :
       basisJetMatrix (K := ℂ) (V := ActualSection τ gammaL gammaP d m P) e (actualJetMap (τ := τ) (γL := gammaL) (γP := gammaP) (d := d) (m := m) hP hz0 q) =
   …

2. theorem OAI.Nagata.Workers.W12.actual_kernel_to_coefficients line 51

   Source documentation

   A nonzero genuine section in the actual jet kernel gives a nonzero vector in the specified matrix kernel, through its genuine basis coordinates.

   theorem actual_kernel_to_coefficients
       {τ gammaL gammaP : ℂ} {d : ℤ} {q m : ℕ} {a delta : ℝ} {P : ℂ → ℂ}
       (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z) {z0 : ℂ} (hz0 : z0 ≠ 0)
       (e : Basis (Column d (m : ℤ) a delta) ℂ (ActualSection τ gammaL gammaP d m P))
       (M : Matrix (JetIndex q m) (Column d (m : ℤ) a delta) ℂ)
       (hmatrix : basisJetMatrix (K := ℂ) (V := ActualSection τ gammaL gammaP d m P) e (actualJetMap hP hz0 q) = M)
   …

3. theorem OAI.Nagata.Workers.W12.actual_collision_to_coefficients line 67

   Source documentation

   Moving actual sections with the genuine local Taylor multiplicities give matrix kernel coefficients. This uses the collision proof, rather than assuming vanishing of the target mixed jets or an already-existing kernel section.

   theorem actual_collision_to_coefficients
       {τ gammaL gammaP : ℂ} {d : ℤ} {q m : ℕ} {a delta : ℝ} {P : ℂ → ℂ}
       (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z) {z0 : ℂ} (hz0 : z0 ≠ 0)
       (e : Basis (Column d (m : ℤ) a delta) ℂ (ActualSection τ gammaL gammaP d m P))
       (M : Matrix (JetIndex q m) (Column d (m : ℤ) a delta) ℂ)
       (hmatrix : basisJetMatrix (K := ℂ) (V := ActualSection τ gammaL gammaP d m P) e (actualJetMap hP hz0 q) = M)
   …

4. theorem OAI.Nagata.Workers.W12.actual_section_kernel_contradiction line 90

   Source documentation

   The same sufficiently small τ supplies both injectivity and the genuine section kernel. The section/basis/coordinate data may vary arbitrarily with τ.

   theorem actual_section_kernel_contradiction
       (d : ℤ) (q m : ℕ) (a delta : ℝ)
       (gammaL gammaP z0 : ℝ → ℂ) (P : ℝ → ℂ → ℂ)
       (M : ℝ → Matrix (JetIndex q m) (Column d (m : ℤ) a delta) ℂ)
       (hinjective : ∀ᶠ τ in 𝓝[>] (0 : ℝ), Function.Injective (M τ).mulVec)
       (hactual : ∀ᶠ τ in 𝓝[>] (0 : ℝ),
         ∃ (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ (P τ) z)
           (hz0 : z0 τ ≠ 0)
           (e : Basis (Column d (m : ℤ) a delta) ℂ
             (ActualSection (τ : ℂ) (gammaL τ) (gammaP τ) d m (P τ)))
           (F : ActualSection (τ : ℂ) (gammaL τ) (gammaP τ) d m (P τ)),
           basisJetMatrix (K := ℂ)
   …

5. theorem OAI.Nagata.Workers.W12.actual_polynomial_collision_to_coefficients line 125

   Source documentation

   The source-facing fixed-τ bridge from ordinary polynomial multiplicities through actual section collision to nonzero coefficient vectors.

   theorem actual_polynomial_collision_to_coefficients
       {τ gammaL gammaP : ℂ} {d : ℤ} {q m : ℕ} {a delta : ℝ} {P : ℂ → ℂ}
       (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z) {z0 : ℂ} (hz0 : z0 ≠ 0)
       (e : Basis (Column d (m : ℤ) a delta) ℂ (ActualSection τ gammaL gammaP d m P))
       (coeff : Column d (m : ℤ) a delta → ℂ → ℂ)
       (hlocal : ∀ col, ∀ᶠ z : ℂ × ℂ in 𝓝 (0, 0),
         localScalar (e col) z0 z.1 z.2 =
           coeff col z.1 * Complex.exp ((col.val.1 : ℂ) * z.2))
       (F : ℕ → ActualSection τ gammaL gammaP d m P) (hF : ∀ n, F n ≠ 0)
       {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
       (xi : ℕ → Fin q → ℂ)
       (hxilim : ∀ i, Tendsto (fun n => xi n i) atTop (𝓝 0))
   …

6. theorem OAI.Nagata.Workers.W12.actual_polynomial_frame_collision_to_coefficients line 158

   Source documentation

   The source-facing fixed-τ bridge from ordinary polynomial multiplicities through actual section collision to nonzero coefficient vectors.

   theorem actual_polynomial_frame_collision_to_coefficients
       {τ gammaL gammaP : ℂ} {d : ℤ} {q m : ℕ} {a delta : ℝ} {P : ℂ → ℂ}
       (hP : ∀ z, z ≠ 0 → DifferentiableAt ℂ P z) {z0 : ℂ} (hz0 : z0 ≠ 0)
       (e : Basis (Column d (m : ℤ) a delta) ℂ (ActualSection τ gammaL gammaP d m P))
       (coeff : Column d (m : ℤ) a delta → ℂ → ℂ)
       (hlocal : ∀ col, ∀ᶠ z : ℂ × ℂ in 𝓝 (0, 0),
         localScalar (e col) z0 z.1 z.2 =
           coeff col z.1 * Complex.exp ((col.val.1 : ℂ) * z.2))
       (F : ℕ → ActualSection τ gammaL gammaP d m P) (hF : ∀ n, F n ≠ 0)
       {U : Set ℂ} (hU : IsOpen U) (h0 : (0 : ℂ) ∈ U)
       (xi : ℕ → Fin q → ℂ)
       (hxilim : ∀ i, Tendsto (fun n => xi n i) atTop (𝓝 0))
   …