Configuration.lean`

68 declarations, 0 contain sorry, 0 declared as axioms

Ordered distinct plane configurations and product Zariski geometry

abbrev OAI.Nagata.ProjectiveGeometry.PlanePoint line 36
Also declared: ComparatorChallenges/Nagata.lean:101 (same declaration text).
abbrev OAI.Nagata.ProjectiveGeometry.OrderedDistinctPoints line 39
Source documentation
The genuine set of ordered tuples of pairwise distinct plane points.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:103 (different declaration text). Qualify references as OAI.Nagata.ProjectiveGeometry.OrderedDistinctPoints@path.
```
abbrev OrderedDistinctPoints (r : ℕ) :=
…
```
def OAI.Nagata.ProjectiveGeometry.affineLineVector line 43
Source documentation
Explicit nonzero homogeneous coordinates [1 : z : 0].
```
def affineLineVector (z : ℂ) : Fin 3 → ℂ :=
…
```
theorem OAI.Nagata.ProjectiveGeometry.affineLineVector_ne_zero line 46
def OAI.Nagata.ProjectiveGeometry.affineLinePoint line 51
theorem OAI.Nagata.ProjectiveGeometry.affineLinePoint_injective line 54
def OAI.Nagata.ProjectiveGeometry.standardConfiguration line 68
Source documentation
The ordered distinct tuple [1 : i : 0], for i = 0, ..., r-1.
```
def standardConfiguration (r : ℕ) : OrderedDistinctPoints r :=
…
```
theorem OAI.Nagata.ProjectiveGeometry.orderedDistinctPoints_nonempty line 75
Source documentation
The configuration domain is nonempty for every finite number of points.
```
theorem orderedDistinctPoints_nonempty (r : ℕ) : Nonempty (OrderedDistinctPoints r) :=
…
```
def OAI.Nagata.ProjectiveGeometry.affinePlaneVector line 79
Source documentation
The standard two-dimensional affine chart [1 : z₀ : z₁].
```
def affinePlaneVector (z : Fin 2 → ℂ) : Fin 3 → ℂ :=
…
```
theorem OAI.Nagata.ProjectiveGeometry.affinePlaneVector_ne_zero line 82
def OAI.Nagata.ProjectiveGeometry.affinePlanePoint line 87
theorem OAI.Nagata.ProjectiveGeometry.affinePlanePoint_injective line 90
structure OAI.Nagata.ProjectiveGeometry.MultihomogeneousEquation line 113
Source documentation
An equation homogeneous separately in each block of three coordinates. The support condition is the ordinary definition of multihomogeneity.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:106 (different declaration text). Qualify references as OAI.Nagata.ProjectiveGeometry.MultihomogeneousEquation@path.
```
structure MultihomogeneousEquation (r : ℕ) where
…
```
def OAI.Nagata.ProjectiveGeometry.equationVanishes line 122
Source documentation
Vanishing of a multihomogeneous equation on a tuple. Quantifying over representatives makes independence of the chosen homogeneous coordinates explicit in the definition. Such representatives exist for every point.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:112 (different declaration text). Qualify references as OAI.Nagata.ProjectiveGeometry.equationVanishes@path.
```
def equationVanishes {r : ℕ} (F : MultihomogeneousEquation r)
    (p : Fin r → PlanePoint) : Prop :=
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint
def OAI.Nagata.ProjectiveGeometry.IsProductZariskiClosed line 130
Source documentation
The common zero loci of multihomogeneous equations: the algebraic Zariski closed subsets of a product of projective planes.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:118 (different declaration text). Qualify references as OAI.Nagata.ProjectiveGeometry.IsProductZariskiClosed@path.
```
def IsProductZariskiClosed {r : ℕ} (S : Set (Fin r → PlanePoint)) : Prop :=
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint
def OAI.Nagata.ProjectiveGeometry.IsConfigurationZariskiClosed line 135
Source documentation
Relative Zariski closedness on the open subset of distinct tuples.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:122 (different declaration text). Qualify references as OAI.Nagata.ProjectiveGeometry.IsConfigurationZariskiClosed@path.
```
def IsConfigurationZariskiClosed {r : ℕ}
    (S : Set (OrderedDistinctPoints r)) : Prop :=
…
```
theorem OAI.Nagata.ProjectiveGeometry.isProductZariskiClosed_univ line 140
theorem OAI.Nagata.ProjectiveGeometry.isProductZariskiClosed_inter line 145
theorem OAI.Nagata.ProjectiveGeometry.representatives_exist line 164
Source documentation
There is an actual simultaneous nonzero representative for every tuple. This rules out a vacuous representative quantifier in equationVanishes.
```
theorem representatives_exist {r : ℕ} (p : Fin r → PlanePoint) :
    ∃ (v : Fin r → Fin 3 → ℂ) (hv : ∀ i, v i ≠ 0),
      ∀ i, Projectivization.mk ℂ (v i) (hv i) = p i := by
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint

theorem OAI.Nagata.ProjectiveGeometry.equationVanishes_rep line 171

Source documentation

Vanishing implies vanishing at the library's chosen representatives.

theorem equationVanishes_rep {r : ℕ} (F : MultihomogeneousEquation r)
    (p : Fin r → PlanePoint) (h : equationVanishes F p) :
    MvPolynomial.eval (fun ij => (p ij.1).rep ij.2) F.polynomial = 0 := by
…

Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint

def OAI.Nagata.ProjectiveGeometry.oneEquation line 178
Source documentation
The constant equation 1 = 0, of multidegree zero.
```
def oneEquation (r : ℕ) : MultihomogeneousEquation r where
…
```
theorem OAI.Nagata.ProjectiveGeometry.not_equationVanishes_one line 187
theorem OAI.Nagata.ProjectiveGeometry.isProductZariskiClosed_empty line 193
theorem OAI.Nagata.ProjectiveGeometry.isConfigurationZariskiClosed_empty line 203
theorem OAI.Nagata.ProjectiveGeometry.configuration_empty_ne_univ line 207
abbrev OAI.Nagata.ProjectiveGeometry.ChartVariables line 217
Source documentation
Each affine projective chart has exactly the two coordinates other than its distinguished nonzero homogeneous coordinate.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:127 (different declaration text). Qualify references as OAI.Nagata.ProjectiveGeometry.ChartVariables@path.
```
abbrev ChartVariables (c : Fin 3) := {j : Fin 3 // j ≠ c}
```
def OAI.Nagata.ProjectiveGeometry.dehomogenize line 220
Source documentation
The equation of a projective form in the affine chart X_c = 1.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:129 (different declaration text). Qualify references as OAI.Nagata.ProjectiveGeometry.dehomogenize@path.
```
def dehomogenize (c : Fin 3) (F : MvPolynomial (Fin 3) ℂ) :
    MvPolynomial (ChartVariables c) ℂ :=
…
```
def OAI.Nagata.ProjectiveGeometry.chartCoordinates line 227
Source documentation
Coordinates of a projective point in chart c. This map is used only when the chart coordinate is nonzero.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:135 (different declaration text). Qualify references as OAI.Nagata.ProjectiveGeometry.chartCoordinates@path.
```
def chartCoordinates (c : Fin 3) (p : PlanePoint) : ChartVariables c → ℂ :=
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint

theorem OAI.Nagata.ProjectiveGeometry.chartCoordinates_mk line 232

Source documentation

Normalized affine coordinates do not depend on the representative chosen by Projectivization.rep.

theorem chartCoordinates_mk (c : Fin 3) (v : Fin 3 → ℂ) (hv : v ≠ 0) :
    chartCoordinates c (Projectivization.mk ℂ v hv) =
      fun j : ChartVariables c => v j.val / v c := by
…

theorem OAI.Nagata.ProjectiveGeometry.mk_rep_coordinate_ne_zero_iff line 240
def OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast line 248
Source documentation
Algebraic vanishing order in every chart containing the point, using powers of the genuine maximal ideal in the affine coordinate ring.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:139 (different declaration text). Qualify references as OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast@path.
```
def multiplicityAtLeast (F : MvPolynomial (Fin 3) ℂ)
    (p : PlanePoint) (m : ℕ) : Prop :=
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint
theorem OAI.Nagata.ProjectiveGeometry.chart_exists line 254
Source documentation
Every point lies in one of the three ordinary affine charts.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:145 (different declaration text). Qualify references as OAI.Nagata.ProjectiveGeometry.chart_exists@path.
```
theorem chart_exists (p : PlanePoint) : ∃ c : Fin 3, p.rep c ≠ 0 := by
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint
theorem OAI.Nagata.ProjectiveGeometry.dehomogenize_mul line 260
theorem OAI.Nagata.ProjectiveGeometry.dehomogenize_C line 264
theorem OAI.Nagata.ProjectiveGeometry.dehomogenize_pow line 268
theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_zero line 272
theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_mono line 277

theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_mul line 284

Source documentation

Multiplication adds lower bounds in the actual affine coordinate rings.

theorem multiplicityAtLeast_mul {F G : MvPolynomial (Fin 3) ℂ}
    {p : PlanePoint} {m n : ℕ} (hF : multiplicityAtLeast F p m)
    (hG : multiplicityAtLeast G p n) : multiplicityAtLeast (F * G) p (m + n) := by
…

Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint

theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_pow line 291
def OAI.Nagata.FullNagata line 312
Source documentation
The strict, simultaneous Nagata inequality in homogeneous coordinates, equivalent to the effective-cycle formulation FullNagataEffectiveCurves.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:338 (same statement text; different proof or body). Qualify references as OAI.Nagata.FullNagata@path.
```
def FullNagata : Prop :=
…
```
def OAI.Nagata.ProjectiveGeometry.chartIndexEquiv line 338
Source documentation
Ordered enumeration of the two coordinates different from c.
```
def chartIndexEquiv (c : Fin 3) : Fin 2 ≃ ChartVariables c :=
…
```
theorem OAI.Nagata.ProjectiveGeometry.chartIndexEquiv_val line 347
theorem OAI.Nagata.ProjectiveGeometry.chartIndexEquiv_symm_succAbove line 350
def OAI.Nagata.ProjectiveGeometry.chartCoordinates₂ line 354
def OAI.Nagata.ProjectiveGeometry.chartDehomogenize₂ line 359
Source documentation
The same genuine affine chart equation with its two variables enumerated by Fin 2, for the finite jet matrix interface.
```
def chartDehomogenize₂ (c : Fin 3) (F : MvPolynomial (Fin 3) ℂ) :
    MvPolynomial (Fin 2) ℂ :=
…
```
theorem OAI.Nagata.ProjectiveGeometry.chartDehomogenize₂_eq_eval₂_insertNth line 365
Source documentation
Identification with the direct two-variable chart substitution used by the global homogeneous coefficient matrix.
```
theorem chartDehomogenize₂_eq_eval₂_insertNth (c : Fin 3)
    (F : MvPolynomial (Fin 3) ℂ) :
    chartDehomogenize₂ c F =
      MvPolynomial.eval₂ MvPolynomial.C (c.insertNth 1 MvPolynomial.X) F := by
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.chartDehomogenize₂
theorem OAI.Nagata.ProjectiveGeometry.orderAtLeast_chartDehomogenize₂_iff line 385
def OAI.Nagata.ProjectiveGeometry.chartVector₂ line 404
theorem OAI.Nagata.ProjectiveGeometry.chartVector₂_ne_zero line 406
def OAI.Nagata.ProjectiveGeometry.chartPoint₂ line 411
theorem OAI.Nagata.ProjectiveGeometry.chartPoint₂_coordinate_ne_zero line 414
theorem OAI.Nagata.ProjectiveGeometry.chartCoordinates₂_chartPoint₂ line 425
theorem OAI.Nagata.ProjectiveGeometry.chartPoint₂_injective line 433
theorem OAI.Nagata.ProjectiveGeometry.chartPoint₂_chartCoordinates₂ line 438
abbrev OAI.Nagata.ProjectiveGeometry.ConfigurationChart line 452
def OAI.Nagata.ProjectiveGeometry.InConfigurationChart line 454
def OAI.Nagata.ProjectiveGeometry.configurationChartCoordinates₂ line 458
Source documentation
Explicit affine coordinates in a simultaneous product chart.
```
def configurationChartCoordinates₂ {r : ℕ} (c : ConfigurationChart r)
    (p : Fin r → PlanePoint) : Fin r × Fin 2 → ℂ :=
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.ConfigurationChart, OAI.Nagata.ProjectiveGeometry.PlanePoint
def OAI.Nagata.ProjectiveGeometry.configurationChartEmbedding line 462
theorem OAI.Nagata.ProjectiveGeometry.configurationChartEmbedding_mem line 466
theorem OAI.Nagata.ProjectiveGeometry.configurationChartCoordinates₂_embedding line 470
theorem OAI.Nagata.ProjectiveGeometry.configurationChartEmbedding_coordinates line 476
theorem OAI.Nagata.ProjectiveGeometry.configurationChartEmbedding_injective line 482
theorem OAI.Nagata.ProjectiveGeometry.range_configurationChartEmbedding line 488
theorem OAI.Nagata.ProjectiveGeometry.configurationChartCoordinates₂_eq line 497
theorem OAI.Nagata.ProjectiveGeometry.configurationChart_cover line 503
Source documentation
The simultaneous charts cover every actual projective tuple.
```
theorem configurationChart_cover {r : ℕ} (p : Fin r → PlanePoint) :
    ∃ c : ConfigurationChart r, InConfigurationChart c p := by
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint, OAI.Nagata.ProjectiveGeometry.ConfigurationChart, OAI.Nagata.ProjectiveGeometry.InConfigurationChart
theorem OAI.Nagata.ProjectiveGeometry.multihomogeneous_eval_scale line 529
theorem OAI.Nagata.ProjectiveGeometry.equationVanishes_iff_eval_rep line 550
Source documentation
Vanishing on one chosen representative is equivalent to the intrinsic representative-independent definition used in the configuration Zariski sets.
```
theorem equationVanishes_iff_eval_rep {r : ℕ} (F : MultihomogeneousEquation r)
    (p : Fin r → PlanePoint) :
    equationVanishes F p ↔
      MvPolynomial.eval (fun ij => (p ij.1).rep ij.2) F.polynomial = 0 := by
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.PlanePoint
theorem OAI.Nagata.ProjectiveGeometry.equationVanishes_iff_eval_mk line 570