AssociatedBundles.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

Associated line bundles of multiplier actions

abbrev OAI.Nagata.W16.AssociatedBundle.CurvePoint line 31
Source documentation
Actual points on the projective zero locus of G.
```
abbrev CurvePoint := {p : PlanePoint // MvPolynomial.eval p.rep G.polynomial = 0}
```
structure OAI.Nagata.W16.AssociatedBundle.BundleVector line 34
Source documentation
Representatives of the weight-k associated bundle.
```
structure BundleVector (k : ℕ) where
…
```
def OAI.Nagata.W16.AssociatedBundle.Equivalent line 43
Source documentation
The orbit relation for (x,w) ↦ (λx,λ^k w).
```
def Equivalent {k : ℕ} (a b : BundleVector G k) : Prop :=
…
```
Mentions: OAI.Nagata.W16.AssociatedBundle.BundleVector
theorem OAI.Nagata.W16.AssociatedBundle.equivalent_refl line 46
theorem OAI.Nagata.W16.AssociatedBundle.equivalent_symm line 49
theorem OAI.Nagata.W16.AssociatedBundle.equivalent_trans line 58
def OAI.Nagata.W16.AssociatedBundle.bundleSetoid line 68
def OAI.Nagata.W16.AssociatedBundle.TotalSpace line 73
Source documentation
The genuine quotient total space of the associated bundle.
```
def TotalSpace (G : NonzeroHomogeneousForm n) (k : ℕ) := Quotient (bundleSetoid G k)
```
Mentions: OAI.Nagata.W16.AssociatedBundle.bundleSetoid
def OAI.Nagata.W16.AssociatedBundle.mk line 75
theorem OAI.Nagata.W16.AssociatedBundle.mk_eq_mk_iff line 77
def OAI.Nagata.W16.AssociatedBundle.base line 80
theorem OAI.Nagata.W16.AssociatedBundle.base_mk line 87
theorem OAI.Nagata.W16.AssociatedBundle.base_on_curve line 91
Source documentation
The quotient base actually lies on the homogeneous curve.
```
theorem base_on_curve {k : ℕ} (t : TotalSpace G k) :
    MvPolynomial.eval (base t).rep G.polynomial = 0 := by
…
```
Mentions: OAI.Nagata.W16.AssociatedBundle.TotalSpace, OAI.Nagata.W16.AssociatedBundle.base
def OAI.Nagata.W16.AssociatedBundle.curveBase line 101
theorem OAI.Nagata.W16.AssociatedBundle.equivalent_fiberCoordinate line 103
def OAI.Nagata.W16.AssociatedBundle.fiberCoordinate line 112
Source documentation
Fiber coordinate w/x_c^k; used as a trivialization on the chart x_c ≠ 0. The quotient function itself is defined everywhere.
```
def fiberCoordinate {k : ℕ} (c : Fin 3) : TotalSpace G k → ℂ :=
…
```
Mentions: OAI.Nagata.W16.AssociatedBundle.TotalSpace
theorem OAI.Nagata.W16.AssociatedBundle.fiberCoordinate_mk line 116
theorem OAI.Nagata.W16.AssociatedBundle.base_mk_chart_iff line 119
def OAI.Nagata.W16.AssociatedBundle.vectorOfBase line 125
theorem OAI.Nagata.W16.AssociatedBundle.base_vectorOfBase line 131
theorem OAI.Nagata.W16.AssociatedBundle.fiberCoordinate_vectorOfBase line 135
abbrev OAI.Nagata.W16.AssociatedBundle.CurveChart line 140
Source documentation
Coordinates on the curve's actual projective affine chart.
```
abbrev CurveChart (G : NonzeroHomogeneousForm n) (c : Fin 3) :=
…
```
abbrev OAI.Nagata.W16.AssociatedBundle.BundleChart line 144
Source documentation
The part of the associated total space above that affine chart.
```
abbrev BundleChart (G : NonzeroHomogeneousForm n) (k : ℕ) (c : Fin 3) :=
…
```
def OAI.Nagata.W16.AssociatedBundle.reconstruct line 148
Source documentation
Reconstruct from a projective base point and a normalized chart fiber.
```
def reconstruct {k : ℕ} (c : Fin 3) (p : CurvePoint G) (z : ℂ) : TotalSpace G k :=
…
```
Mentions: OAI.Nagata.W16.AssociatedBundle.CurvePoint, OAI.Nagata.W16.AssociatedBundle.TotalSpace
theorem OAI.Nagata.W16.AssociatedBundle.base_reconstruct line 151
theorem OAI.Nagata.W16.AssociatedBundle.fiberCoordinate_reconstruct line 155
theorem OAI.Nagata.W16.AssociatedBundle.reconstruct_fiberCoordinate line 161
def OAI.Nagata.W16.AssociatedBundle.chartTrivialization line 183
Source documentation
Each actual projective affine chart trivializes the quotient fiber.
```
def chartTrivialization (G : NonzeroHomogeneousForm n) (k : ℕ) (c : Fin 3) :
    BundleChart G k c ≃ CurveChart G c × ℂ where
…
```
Mentions: OAI.Nagata.W16.AssociatedBundle.BundleChart, OAI.Nagata.W16.AssociatedBundle.CurveChart
theorem OAI.Nagata.W16.AssociatedBundle.fiberCoordinate_overlap line 199
Source documentation
The transition factor between two containing chart fiber coordinates.
```
theorem fiberCoordinate_overlap {k : ℕ} (t : TotalSpace G k) (b c : Fin 3)
    (hb : (base t).rep b ≠ 0) (hc : (base t).rep c ≠ 0) :
    fiberCoordinate c t = ((base t).rep b / (base t).rep c) ^ k * fiberCoordinate b t := by
…
```
Mentions: OAI.Nagata.W16.AssociatedBundle.TotalSpace, OAI.Nagata.W16.AssociatedBundle.base, OAI.Nagata.W16.AssociatedBundle.fiberCoordinate
def OAI.Nagata.W16.AssociatedBundle.weightedEval line 212
Source documentation
The actual finite polynomial evaluated on homogeneous base and fiber coordinates.
```
def weightedEval (s : Finset ℕ) (T : ℕ → PlanePolynomial) (j : ℕ → ℕ)
    (x : Fin 3 → ℂ) (w : ℂ) : ℂ :=
…
```
Mentions: OAI.Nagata.W16.PlanePolynomial
theorem OAI.Nagata.W16.AssociatedBundle.weightedEval_scale line 216
def OAI.Nagata.W16.AssociatedBundle.polynomialVector line 234
def OAI.Nagata.W16.AssociatedBundle.polynomialMap line 243
Source documentation
Evaluation of a weighted polynomial gives an actual map from the weight-k total space to the weight-d total space over the same curve.
```
def polynomialMap {k : ℕ} (s : Finset ℕ) (T : ℕ → PlanePolynomial)
    (j : ℕ → ℕ) (d : ℕ)
    (hdeg : ∀ a ∈ s, (T a).IsHomogeneous (d - k * j a))
    (hkj : ∀ a ∈ s, k * j a ≤ d) : TotalSpace G k → TotalSpace G d :=
…
```
Mentions: OAI.Nagata.W16.PlanePolynomial, OAI.Nagata.W16.AssociatedBundle.TotalSpace
theorem OAI.Nagata.W16.AssociatedBundle.polynomialMap_mk line 256
theorem OAI.Nagata.W16.AssociatedBundle.polynomialMap_base line 262
def OAI.Nagata.W16.AssociatedBundle.homogeneousSection line 273
Source documentation
A homogeneous polynomial gives a section of the corresponding actual associated bundle; its local expression is computed from representatives.
```
def homogeneousSection {e : ℕ} (T : PlanePolynomial) (_hT : T.IsHomogeneous e)
    (p : CurvePoint G) : TotalSpace G e :=
…
```
Mentions: OAI.Nagata.W16.PlanePolynomial, OAI.Nagata.W16.AssociatedBundle.CurvePoint, OAI.Nagata.W16.AssociatedBundle.TotalSpace
theorem OAI.Nagata.W16.AssociatedBundle.homogeneousSection_base line 277
theorem OAI.Nagata.W16.AssociatedBundle.homogeneousSection_representative line 281
def OAI.Nagata.W16.AssociatedBundle.IsZeroFiber line 296
Source documentation
The zero fiber is independent of the representative.
```
def IsZeroFiber {k : ℕ} : TotalSpace G k → Prop :=
…
```
Mentions: OAI.Nagata.W16.AssociatedBundle.TotalSpace
theorem OAI.Nagata.W16.AssociatedBundle.isZeroFiber_mk line 304

theorem OAI.Nagata.W16.AssociatedBundle.polynomialMap_not_identically_zero line 309

Source documentation

Distinct powers cannot cancel a coefficient known to be nonzero at an actual curve vector. The resulting nonzero value lies in the genuine bundle.

theorem polynomialMap_not_identically_zero {k : ℕ} (s : Finset ℕ)
    (T : ℕ → PlanePolynomial) (j : ℕ → ℕ) (d : ℕ)
    (hdeg : ∀ a ∈ s, (T a).IsHomogeneous (d - k * j a))
    (hkj : ∀ a ∈ s, k * j a ≤ d)
    (hinj : Set.InjOn j (↑s : Set ℕ))
    (x : Fin 3 → ℂ) (hx : x ≠ 0) (hGx : MvPolynomial.eval x G.polynomial = 0)
    (hcoeff : ∃ a ∈ s, MvPolynomial.eval x (T a) ≠ 0) :
    ∃ t : TotalSpace G k, ¬ IsZeroFiber (polynomialMap s T j d hdeg hkj t) := by
…

Mentions: OAI.Nagata.W16.PlanePolynomial, OAI.Nagata.W16.AssociatedBundle.TotalSpace, OAI.Nagata.W16.AssociatedBundle.IsZeroFiber, OAI.Nagata.W16.AssociatedBundle.polynomialMap