UniversalFamilies.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Universal polynomial families and moving matrix kernels

def OAI.Nagata.Workers.W14.parameterMatrix line 19

Source documentation

Substitute genuine polynomial coordinate motions into every matrix entry.

def parameterMatrix {K σ ρ κ : Type*} [CommRing K]
    (A : Matrix ρ κ (MvPolynomial σ K)) (p : σ → Polynomial K) :
    Matrix ρ κ (Polynomial K) :=
…

theorem OAI.Nagata.Workers.W14.specialize_parameterMatrix line 26

Source documentation

Evaluating after polynomial-coordinate substitution equals evaluating each coordinate first; the identity is of actual matrices.

theorem specialize_parameterMatrix {K σ ρ κ : Type*} [CommRing K]
    (A : Matrix ρ κ (MvPolynomial σ K)) (p : σ → Polynomial K) (s : K) :
    (parameterMatrix A p).map (Polynomial.evalRingHom s) =
      A.map (MvPolynomial.eval (fun j => (p j).eval s)) := by
…

Mentions: OAI.Nagata.Workers.W14.parameterMatrix

theorem OAI.Nagata.Workers.W14.parameterMatrix_mulVec line 40

theorem OAI.Nagata.Workers.W14.normalized_kernel_of_parameter_equations line 50

Source documentation

Nonzero solutions of the specialized actual jet equations supply a normalized polynomial coefficient family in their parameter-substituted matrix.

theorem normalized_kernel_of_parameter_equations
    {K σ ρ κ : Type*} [Field K] [Infinite K]
    [Fintype κ] [Fintype ρ] [DecidableEq κ] [DecidableEq ρ]
    (A : Matrix ρ κ (MvPolynomial σ K)) (p : σ → Polynomial K) (E : Finset K)
    (hkernel : ∀ s ∉ E, ∃ v : κ → K, v ≠ 0 ∧
      Nagata.W27.coefficientLinearMap A (fun j => (p j).eval s) v = 0) :
    ∃ q : κ → Polynomial K, (∃ i, (q i).coeff 0 ≠ 0) ∧
      (parameterMatrix A p).mulVec q = 0 := by
…

Mentions: OAI.Nagata.W27.coefficientLinearMap, OAI.Nagata.Workers.W14.parameterMatrix

theorem OAI.Nagata.Workers.W14.universalSupport_general_chart_kernels line 79

Source documentation

Actual universal homogeneous equations give actual nonzero specialized kernels along every good polynomial affine-chart motion.

theorem universalSupport_general_chart_kernels {r d : ℕ} {m : Fin r → ℕ}
    (hU : Nagata.W13.UniversalSupport r d m)
    (c : Fin r → Fin 3) (p : Fin r × Fin 2 → Polynomial ℂ)
    (hbase : Function.Injective
      (configurationChartEmbedding c (fun ij => (p ij).eval 0))) :
    ∃ E : Finset ℂ, 0 ∉ E ∧ ∀ s ∉ E,
      ∃ v : Nagata.W27.HomogeneousMonomial d → ℂ, v ≠ 0 ∧
        Nagata.W27.coefficientLinearMap (Nagata.W27.chartPlaneJetMatrix c d m)
          (fun ij => (p ij).eval s) v = 0 := by
…

Mentions: OAI.Nagata.W13.UniversalSupport, OAI.Nagata.W27.HomogeneousMonomial, OAI.Nagata.W27.coefficientLinearMap, OAI.Nagata.W27.chartPlaneJetMatrix

theorem OAI.Nagata.Workers.W14.universalSupport_normalized_parameter_family line 102

Source documentation

Complete algebraic family bridge along genuine moving projective tuples: from an actual universal system to a polynomial coefficient family with a nonzero constant coefficient, in the genuine global homogeneous jet matrix.

theorem universalSupport_normalized_parameter_family {r d : ℕ} {m : Fin r → ℕ}
    (hU : Nagata.W13.UniversalSupport r d m)
    (c : Fin r → Fin 3) (p : Fin r × Fin 2 → Polynomial ℂ)
    (hbase : Function.Injective
      (configurationChartEmbedding c (fun ij => (p ij).eval 0))) :
    ∃ q : Nagata.W27.HomogeneousMonomial d → Polynomial ℂ,
      (∃ i, (q i).coeff 0 ≠ 0) ∧
      (parameterMatrix (Nagata.W27.chartPlaneJetMatrix c d m) p).mulVec q = 0 := by
…

Mentions: OAI.Nagata.W13.UniversalSupport, OAI.Nagata.W27.HomogeneousMonomial, OAI.Nagata.Workers.W14.parameterMatrix, OAI.Nagata.W27.chartPlaneJetMatrix

def OAI.Nagata.Workers.W14.affineChartCoordinateMotion line 135
Source documentation
The manuscript's affine-linear motions in the chosen local charts, expressed as actual coordinate polynomials in the parameter.
```
def affineChartCoordinateMotion {r : ℕ} (c : ConfigurationChart r)
    (base : Fin r → PlanePoint) (velocity : Fin r × Fin 2 → ℂ) :
    Fin r × Fin 2 → Polynomial ℂ :=
…
```
theorem OAI.Nagata.Workers.W14.affineChartCoordinateMotion_eval line 141

theorem OAI.Nagata.Workers.W14.universalSupport_affine_chart_family line 151

Source documentation

Every actual universal system yields a normalized polynomial family along arbitrary affine-linear motions based at a genuine distinct configuration.

theorem universalSupport_affine_chart_family {r d : ℕ} {m : Fin r → ℕ}
    (hU : Nagata.W13.UniversalSupport r d m)
    (base : Fin r → PlanePoint) (hbase : Function.Injective base)
    (c : ConfigurationChart r) (hc : InConfigurationChart c base)
    (velocity : Fin r × Fin 2 → ℂ) :
    ∃ q : Nagata.W27.HomogeneousMonomial d → Polynomial ℂ,
      (∃ i, (q i).coeff 0 ≠ 0) ∧
      (parameterMatrix (Nagata.W27.chartPlaneJetMatrix c d m)
        (affineChartCoordinateMotion c base velocity)).mulVec q = 0 := by
…

Mentions: OAI.Nagata.W13.UniversalSupport, OAI.Nagata.W27.HomogeneousMonomial, OAI.Nagata.Workers.W14.parameterMatrix, OAI.Nagata.W27.chartPlaneJetMatrix, OAI.Nagata.Workers.W14.affineChartCoordinateMotion

theorem OAI.Nagata.Workers.W14.universalSupport_family_with_normal_displacements line 168

Source documentation

Choose arbitrary scalar normal displacements and simultaneously obtain the normalized polynomial family of actual universal equations along those motions. Smoothness-to-differential identification is the explicit hnonzero input.

theorem universalSupport_family_with_normal_displacements {r d : ℕ} {m : Fin r → ℕ}
    (hU : Nagata.W13.UniversalSupport r d m)
    (base : Fin r → PlanePoint) (hbase : Function.Injective base)
    (c : ConfigurationChart r) (hc : InConfigurationChart c base)
    (normalDifferential : Fin r → (Fin 2 → ℂ) →ₗ[ℂ] ℂ)
    (hnonzero : ∀ i, normalDifferential i ≠ 0) (displacement : Fin r → ℂ) :
    ∃ velocity : Fin r × Fin 2 → ℂ,
      (∀ i, normalDifferential i (fun j => velocity (i, j)) = displacement i) ∧
      ∃ q : Nagata.W27.HomogeneousMonomial d → Polynomial ℂ,
        (∃ i, (q i).coeff 0 ≠ 0) ∧
        (parameterMatrix (Nagata.W27.chartPlaneJetMatrix c d m)
          (affineChartCoordinateMotion c base velocity)).mulVec q = 0 := by
…