ChartJets.lean`

59 declarations, 0 contain sorry, 0 declared as axioms

Affine chart maps, genuine jets, and universal incidence equations

abbrev OAI.Nagata.W27.PlaneMonomial line 26
Source documentation
The affine monomials of total degree at most d, indexing the usual degree-d homogeneous forms after setting the third coordinate to one.
```
abbrev PlaneMonomial (d : ℕ) :=
…
```
abbrev OAI.Nagata.W27.PlaneJet line 31
Source documentation
Point and Taylor-order indices, allowing a different required order at each point, including order zero.
```
abbrev PlaneJet (r : ℕ) (m : Fin r → ℕ) :=
…
```
def OAI.Nagata.W27.affineJetEntry line 42
Source documentation
The coefficient of ξ^u η^v in (x+ξ)^a (y+η)^b, written as a polynomial in the coordinates of point i. This explicit expression is used without a claimed Taylor/multiplicity bridge.
```
def affineJetEntry (i : ι) (a b u v : ℕ) : MvPolynomial (ι × Fin 2) R :=
…
```
theorem OAI.Nagata.W27.eval_affineJetEntry line 46
theorem OAI.Nagata.W27.affineJetEntry_eq_zero_of_left line 52
theorem OAI.Nagata.W27.affineJetEntry_eq_zero_of_right line 56
def OAI.Nagata.W27.planeJetMatrix line 82
Source documentation
The actual finite matrix of affine jet expressions.
```
def planeJetMatrix (r d : ℕ) (m : Fin r → ℕ) :
    Matrix (PlaneJet r m) (PlaneMonomial d) (MvPolynomial (Fin r × Fin 2) R) :=
…
```
Mentions: OAI.Nagata.W27.PlaneJet, OAI.Nagata.W27.PlaneMonomial
def OAI.Nagata.W27.coefficientEquation line 96
Source documentation
A coefficient-linear equation whose entries are polynomial in the point coordinates.
```
def coefficientEquation (A : Matrix ρ κ (MvPolynomial σ R))
    (p : σ → R) (c : κ → R) (row : ρ) : R :=
…
```
theorem OAI.Nagata.W27.coefficientEquation_add line 100
theorem OAI.Nagata.W27.coefficientEquation_smul line 106
def OAI.Nagata.W27.coefficientLinearMap line 116
Source documentation
The coefficient linear map defining the jet conditions at fixed points.
```
def coefficientLinearMap (A : Matrix ρ κ (MvPolynomial σ R)) (p : σ → R) :
    (κ → R) →ₗ[R] (ρ → R) where
…
```
def OAI.Nagata.W27.incidenceEquation line 124
Source documentation
The affine incidence equation, now polynomial jointly in point coordinates and form coefficients.
```
def incidenceEquation (A : Matrix ρ κ (MvPolynomial σ R)) (row : ρ) :
    MvPolynomial (σ ⊕ κ) R :=
…
```
theorem OAI.Nagata.W27.eval_incidenceEquation line 128
def OAI.Nagata.W27.polynomialZeroSet line 140
Source documentation
Common zero set of a family of actual polynomials. No topological or geometric consequence is built into this definition.
```
def polynomialZeroSet {τ : Type*} (f : τ → MvPolynomial σ R) : Set (σ → R) :=
…
```
theorem OAI.Nagata.W27.incidence_zeroSet_iff line 143
abbrev OAI.Nagata.W27.HomogeneousMonomial line 172
Source documentation
All global ternary monomials of degree exactly d; these columns are independent of the affine charts chosen at the marked points.
```
abbrev HomogeneousMonomial (d : ℕ) := Nagata.W02.DegreeExponent d
…
```
Mentions: OAI.Nagata.W02.DegreeExponent
def OAI.Nagata.W27.homogeneousCoordinates line 178
Source documentation
A genuine coefficient linear equivalence for the full space of degree-d homogeneous ternary forms.
```
def homogeneousCoordinates (d : ℕ) :
    homogeneousSubmodule (Fin 3) R d ≃ₗ[R] (HomogeneousMonomial d → R) :=
…
```
Mentions: OAI.Nagata.W27.HomogeneousMonomial
theorem OAI.Nagata.W27.homogeneousCoordinates_apply line 183
theorem OAI.Nagata.W27.homogeneousCoordinates_symm_coeff line 187
theorem OAI.Nagata.W27.homogeneousCoordinates_symm_single line 192
theorem OAI.Nagata.W27.homogeneousCoordinates_ne_zero_iff line 197
theorem OAI.Nagata.W27.homogeneousCoordinates_symm_ne_zero_iff line 211
def OAI.Nagata.W27.universalTranslate line 234
Source documentation
Translation with indeterminate point coordinates. The coefficients are actual polynomials in the point variables.
```
def universalTranslate (i : ι) :
    MvPolynomial (Fin 2) R →+*
      MvPolynomial (Fin 2) (MvPolynomial (ι × Fin 2) R) :=
…
```
def OAI.Nagata.W27.universalJetCoefficient line 241
Source documentation
An actual Taylor coefficient polynomial, without a binomial-formula assumption.
```
def universalJetCoefficient (i : ι) (s : Fin 2 →₀ ℕ)
    (f : MvPolynomial (Fin 2) R) : MvPolynomial (ι × Fin 2) R :=
…
```
theorem OAI.Nagata.W27.map_universalTranslate line 245

theorem OAI.Nagata.W27.eval_universalJetCoefficient line 260

Source documentation

Specializing the polynomial point parameters gives the genuine finite Taylor coefficient of the translated polynomial.

theorem eval_universalJetCoefficient (p : ι × Fin 2 → R) (i : ι)
    (s : Fin 2 →₀ ℕ) (f : MvPolynomial (Fin 2) R) :
    eval p (universalJetCoefficient i s f) =
      (eval₂Hom C (fun j => X j + C (p (i, j))) f).coeff s := by
…

Mentions: OAI.Nagata.W27.universalJetCoefficient

theorem OAI.Nagata.W27.universalJetCoefficient_add line 266
theorem OAI.Nagata.W27.universalJetCoefficient_C_mul line 272
def OAI.Nagata.W27.minorPolynomial line 304
Source documentation
Full-column-size minor polynomial, with rows selected by s. Repeated row selections cause no problem and require no artificial ordering of the finite column set.
```
def minorPolynomial (A : Matrix ρ κ (MvPolynomial σ R)) (s : κ → ρ) :
    MvPolynomial σ R :=
…
```
theorem OAI.Nagata.W27.eval_minorPolynomial line 308
theorem OAI.Nagata.W27.minor_zeroSet_iff line 313
theorem OAI.Nagata.W27.minor_eq_zero_of_nonzero_kernel line 318
theorem OAI.Nagata.W27.mem_minor_zeroSet_of_nonzero_kernel line 333
def OAI.Nagata.W27.affineZariski line 357
Source documentation
Affine Zariski topology: the topology generated by principal open sets on which a multivariate polynomial does not vanish.
```
@[reducible] def affineZariski (σ R : Type*) [CommRing R] : TopologicalSpace (σ → R) :=
…
```
theorem OAI.Nagata.W27.isClosed_polynomialEquation line 361
theorem OAI.Nagata.W27.isClosed_polynomialZeroSet line 368
theorem OAI.Nagata.W27.isClosed_affineIncidence line 381
Source documentation
The coefficient-linear incidence equations form a Zariski-closed subset of the joint affine point/coefficient space. This includes the zero coefficient vector; projectivization of coefficients remains separate.
```
theorem isClosed_affineIncidence {σ R κ ρ : Type*} [CommRing R] [Fintype κ]
    (A : Matrix ρ κ (MvPolynomial σ R)) :
    @IsClosed ((σ ⊕ κ) → R) (affineZariski (σ ⊕ κ) R)
      (polynomialZeroSet (incidenceEquation A)) :=
…
```
Mentions: OAI.Nagata.W27.affineZariski, OAI.Nagata.W27.polynomialZeroSet, OAI.Nagata.W27.incidenceEquation
theorem OAI.Nagata.W27.shifted_power_expansion line 403

theorem OAI.Nagata.W27.coeff_shifted_monomial line 415

Source documentation

The two-variable translated monomial has exactly the displayed binomial Taylor coefficient, including Taylor exponents outside its support.

theorem coeff_shifted_monomial (x y : R) (a b u v : ℕ) :
    ((X (0 : Fin 2) + C x) ^ a * (X (1 : Fin 2) + C y) ^ b).coeff
        (Nagata.Workers.W30.exponentPair u v) =
      (Nat.choose a u : R) * (Nat.choose b v : R) *
        x ^ (a - u) * y ^ (b - v) := by
…

Mentions: OAI.Nagata.Workers.W30.exponentPair

theorem OAI.Nagata.W27.universalJetCoefficient_monomial line 444
Source documentation
The initially displayed binomial matrix entries are exactly the genuine universal Taylor-coefficient polynomials, as a polynomial identity over any commutative coefficient ring.
```
theorem universalJetCoefficient_monomial {ι : Type*} (i : ι) (a b u v : ℕ) :
    universalJetCoefficient i (Nagata.Workers.W30.exponentPair u v)
      ((X (0 : Fin 2)) ^ a * (X 1) ^ b : MvPolynomial (Fin 2) R) =
      affineJetEntry i a b u v := by
…
```
Mentions: OAI.Nagata.W27.universalJetCoefficient, OAI.Nagata.Workers.W30.exponentPair, OAI.Nagata.W27.affineJetEntry
def OAI.Nagata.W27.directChartHom line 470
Source documentation
Actual dehomogenization in chart c, with the two surviving coordinates ordered by Fin.succAbove.
```
def directChartHom (c : Fin 3) : MvPolynomial (Fin 3) R →+* MvPolynomial (Fin 2) R :=
…
```
def OAI.Nagata.W27.directChartLinearMap line 473
def OAI.Nagata.W27.universalJetLinearMap line 479
theorem OAI.Nagata.W27.linearMap_eq_sum_basis line 486
theorem OAI.Nagata.W27.isClosed_minorZeroSet line 519
Source documentation
Vanishing of all full-column-size minors is a Zariski-closed condition on the affine point coordinates.
```
theorem isClosed_minorZeroSet {σ R κ ρ : Type*} [CommRing R]
    [Fintype κ] [DecidableEq κ] (A : Matrix ρ κ (MvPolynomial σ R)) :
    @IsClosed (σ → R) (affineZariski σ R) (polynomialZeroSet (minorPolynomial A)) :=
…
```
Mentions: OAI.Nagata.W27.affineZariski, OAI.Nagata.W27.polynomialZeroSet, OAI.Nagata.W27.minorPolynomial
theorem OAI.Nagata.W27.directChartHom_monomial line 542
Source documentation
Dehomogenization of an actual global ternary monomial in any chart. Its two exponents are read from the same global exponent vector.
```
theorem directChartHom_monomial (c : Fin 3) (a : Fin 3 →₀ ℕ) (z : R) :
    directChartHom c (monomial a z) =
      C z * (X (0 : Fin 2)) ^ a (c.succAbove 0) * (X 1) ^ a (c.succAbove 1) := by
…
```
Mentions: OAI.Nagata.W27.directChartHom
theorem OAI.Nagata.W27.universalJetCoefficient_chart_monomial line 551
Source documentation
In every point chart, the genuine Taylor coefficient of a global monomial is the claimed binomial polynomial in that chart's coordinates.
```
theorem universalJetCoefficient_chart_monomial {ι : Type*}
    (i : ι) (c : Fin 3) (a : Fin 3 →₀ ℕ) (u v : ℕ) :
    universalJetCoefficient i (Nagata.Workers.W30.exponentPair u v)
      (directChartHom c (monomial a (1 : R))) =
        affineJetEntry i (a (c.succAbove 0)) (a (c.succAbove 1)) u v := by
…
```
Mentions: OAI.Nagata.W27.universalJetCoefficient, OAI.Nagata.Workers.W30.exponentPair, OAI.Nagata.W27.directChartHom, OAI.Nagata.W27.affineJetEntry
theorem OAI.Nagata.W27.nonzero_kernel_iff_minor_zeroSet line 578
Source documentation
The full rectangular determinantal criterion. No cardinal restriction, positive multiplicity, or nonempty-row hypothesis is imposed.
```
theorem nonzero_kernel_iff_minor_zeroSet
    (A : Matrix ρ κ (MvPolynomial σ K)) (p : σ → K) :
    (∃ c : κ → K, c ≠ 0 ∧ coefficientLinearMap A p c = 0) ↔
      p ∈ polynomialZeroSet (minorPolynomial A) := by
…
```
Mentions: OAI.Nagata.W27.coefficientLinearMap, OAI.Nagata.W27.polynomialZeroSet, OAI.Nagata.W27.minorPolynomial
theorem OAI.Nagata.W27.isClosed_nonzero_kernel_locus line 593
Source documentation
Existence of a nonzero coefficient vector solving a polynomial linear system is an affine Zariski-closed condition on its parameters.
```
theorem isClosed_nonzero_kernel_locus
    (A : Matrix ρ κ (MvPolynomial σ K)) :
    @IsClosed (σ → K) (affineZariski σ K)
      {p | ∃ c : κ → K, c ≠ 0 ∧ coefficientLinearMap A p c = 0} := by
…
```
Mentions: OAI.Nagata.W27.affineZariski, OAI.Nagata.W27.coefficientLinearMap
def OAI.Nagata.W27.planeJetExponent line 620
Source documentation
The actual two-variable exponent selected by a finite plane jet row.
```
def planeJetExponent {m : Fin r → ℕ} (row : PlaneJet r m) : Fin 2 →₀ ℕ :=
…
```
Mentions: OAI.Nagata.W27.PlaneJet
theorem OAI.Nagata.W27.all_orders_iff_universal_jets line 626
Source documentation
Finite jet rows exactly express ordinary evaluation-ideal multiplicity at every point. Different affine polynomials at different chart locations are allowed here; the projective application uses charts of one global form.
```
theorem all_orders_iff_universal_jets (p : Fin r × Fin 2 → R)
    (m : Fin r → ℕ) (f : Fin r → MvPolynomial (Fin 2) R) :
    (∀ i, Nagata.AffineMultiplicity.orderAtLeast (fun j => p (i, j)) (m i) (f i)) ↔
      ∀ row : PlaneJet r m,
        eval p (universalJetCoefficient row.1 (planeJetExponent row) (f row.1)) = 0 := by
…
```
Mentions: OAI.Nagata.W27.PlaneJet, OAI.Nagata.W27.universalJetCoefficient, OAI.Nagata.W27.planeJetExponent

def OAI.Nagata.W27.chartJetPolynomialMap line 667

Source documentation

Polynomial jet of one actual global homogeneous form at one point chart.

def chartJetPolynomialMap (c : Fin r → Fin 3) (d : ℕ) (m : Fin r → ℕ)
    (row : PlaneJet r m) :
    homogeneousSubmodule (Fin 3) R d →ₗ[R] MvPolynomial (Fin r × Fin 2) R :=
…

Mentions: OAI.Nagata.W27.PlaneJet

def OAI.Nagata.W27.chartPlaneJetMatrix line 675
Source documentation
The matrix uses a single basis of the global homogeneous form space, regardless of which affine chart is selected at each individual point.
```
def chartPlaneJetMatrix (c : Fin r → Fin 3) (d : ℕ) (m : Fin r → ℕ) :
    Matrix (PlaneJet r m) (HomogeneousMonomial d) (MvPolynomial (Fin r × Fin 2) R) :=
…
```
Mentions: OAI.Nagata.W27.PlaneJet, OAI.Nagata.W27.HomogeneousMonomial
theorem OAI.Nagata.W27.chartPlaneJetMatrix_entry line 682
Source documentation
The matrix's global-basis columns have exactly the expected binomial entries in each individual affine chart.
```
theorem chartPlaneJetMatrix_entry (c : Fin r → Fin 3) (d : ℕ)
    (m : Fin r → ℕ) (row : PlaneJet r m) (col : HomogeneousMonomial d) :
    chartPlaneJetMatrix (R := R) c d m row col =
…
```
Mentions: OAI.Nagata.W27.PlaneJet, OAI.Nagata.W27.HomogeneousMonomial, OAI.Nagata.W27.chartPlaneJetMatrix
theorem OAI.Nagata.W27.coefficientEquation_chartPlaneJetMatrix line 694
Source documentation
Specialization of the actual global-basis matrix is exactly the ordinary Taylor jet of the actual dehomogenized homogeneous polynomial.
```
theorem coefficientEquation_chartPlaneJetMatrix (c : Fin r → Fin 3)
    (d : ℕ) (m : Fin r → ℕ) (p : Fin r × Fin 2 → R)
    (F : homogeneousSubmodule (Fin 3) R d) (row : PlaneJet r m) :
    coefficientEquation (chartPlaneJetMatrix c d m) p (homogeneousCoordinates d F) row =
      eval p (universalJetCoefficient row.1 (planeJetExponent row)
        (directChartHom (c row.1) F.val)) := by
…
```
Mentions: OAI.Nagata.W27.PlaneJet, OAI.Nagata.W27.coefficientEquation, OAI.Nagata.W27.chartPlaneJetMatrix, OAI.Nagata.W27.homogeneousCoordinates, OAI.Nagata.W27.universalJetCoefficient, OAI.Nagata.W27.planeJetExponent, OAI.Nagata.W27.directChartHom

theorem OAI.Nagata.W27.chart_orders_iff_kernel line 713

Source documentation

Genuine geometric order conditions in any chosen point charts are exactly the kernel equations of the actual polynomial matrix.

theorem chart_orders_iff_kernel (c : Fin r → Fin 3)
    (d : ℕ) (m : Fin r → ℕ) (p : Fin r × Fin 2 → R)
    (F : homogeneousSubmodule (Fin 3) R d) :
    (∀ i, Nagata.AffineMultiplicity.orderAtLeast (fun j => p (i, j)) (m i)
      (directChartHom (c i) F.val)) ↔
      coefficientLinearMap (chartPlaneJetMatrix c d m) p (homogeneousCoordinates d F) = 0 := by
…

Mentions: OAI.Nagata.W27.directChartHom, OAI.Nagata.W27.coefficientLinearMap, OAI.Nagata.W27.chartPlaneJetMatrix, OAI.Nagata.W27.homogeneousCoordinates

theorem OAI.Nagata.W27.exists_nonzero_form_iff_chart_kernel line 726

Source documentation

Both directions retain nonzero actual forms; no curve existence is hidden in the coordinate-space construction.

theorem exists_nonzero_form_iff_chart_kernel (c : Fin r → Fin 3)
    (d : ℕ) (m : Fin r → ℕ) (p : Fin r × Fin 2 → R) :
    (∃ F : homogeneousSubmodule (Fin 3) R d, F.val ≠ 0 ∧
      ∀ i, Nagata.AffineMultiplicity.orderAtLeast (fun j => p (i, j)) (m i)
        (directChartHom (c i) F.val)) ↔
      ∃ v : HomogeneousMonomial d → R, v ≠ 0 ∧
        coefficientLinearMap (chartPlaneJetMatrix c d m) p v = 0 := by
…

Mentions: OAI.Nagata.W27.directChartHom, OAI.Nagata.W27.HomogeneousMonomial, OAI.Nagata.W27.coefficientLinearMap, OAI.Nagata.W27.chartPlaneJetMatrix

theorem OAI.Nagata.W27.exists_nonzero_form_iff_chart_minors line 764
Source documentation
On each product chart, existence of an actual nonzero homogeneous form with arbitrary assigned ordinary multiplicities is precisely a common zero set of actual polynomial minors.
```
theorem exists_nonzero_form_iff_chart_minors (c : Fin r → Fin 3)
    (d : ℕ) (m : Fin r → ℕ) (p : Fin r × Fin 2 → K) :
    (∃ F : homogeneousSubmodule (Fin 3) K d, F.val ≠ 0 ∧
      ∀ i, Nagata.AffineMultiplicity.orderAtLeast (fun j => p (i, j)) (m i)
        (directChartHom (c i) F.val)) ↔
      p ∈ polynomialZeroSet (minorPolynomial (chartPlaneJetMatrix c d m)) := by
…
```
Mentions: OAI.Nagata.W27.directChartHom, OAI.Nagata.W27.polynomialZeroSet, OAI.Nagata.W27.minorPolynomial, OAI.Nagata.W27.chartPlaneJetMatrix
theorem OAI.Nagata.W27.isClosed_chart_form_locus line 774