CubicGeometry.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Cubic relations, closed embeddings, image containment, and gradients

theorem OAI.Nagata.W21.cubicSectionProduct_mem line 21

theorem OAI.Nagata.W21.exists_cubicRelation_of_degreeNine_dimension line 55

Source documentation

The actual evaluation coordinates satisfy a nonzero homogeneous cubic, conditional only here on the separately proved degree-nine section dimension.

theorem exists_cubicRelation_of_degreeNine_dimension {τ γ : ℂ}
    (b : Fin 3 → automorphicSections τ 3 γ)
    [Module.Finite ℂ (automorphicSections τ 9 (γ ^ 3))]
    (hdim : Module.finrank ℂ (automorphicSections τ 9 (γ ^ 3)) ≤ 9) :
    ∃ P : MvPolynomial (Fin 3) ℂ,
      P ≠ 0 ∧ P.IsHomogeneous 3 ∧
      MvPolynomial.aeval (fun i ↦ (b i).val) P = 0 := by
…

theorem OAI.Nagata.W21.exists_cubicEquation_of_degreeNine_dimension line 70

Source documentation

The cubic equation vanishes at every actual evaluation vector, including all lifts used by the projective quotient map.

theorem exists_cubicEquation_of_degreeNine_dimension {τ γ : ℂ}
    (b : Fin 3 → automorphicSections τ 3 γ)
    [Module.Finite ℂ (automorphicSections τ 9 (γ ^ 3))]
    (hdim : Module.finrank ℂ (automorphicSections τ 9 (γ ^ 3)) ≤ 9) :
    ∃ P : MvPolynomial (Fin 3) ℂ,
      P ≠ 0 ∧ P.IsHomogeneous 3 ∧ ∀ z : ℂ,
      MvPolynomial.aeval (fun i ↦ (b i).val z) P = 0 := by
…

theorem OAI.Nagata.W21.continuous_cubicEvaluationVector line 93

theorem OAI.Nagata.W21.continuous_cubicCoverMap line 104

Source documentation

Continuity into the canonical complex projective topology.

theorem continuous_cubicCoverMap {τ γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2) :
    Continuous (cubicCoverMap b hbase) := by
…

theorem OAI.Nagata.W21.continuous_cubicTorusMap line 117

Source documentation

The descended actual torus map is continuous for both canonical quotient topologies.

theorem continuous_cubicTorusMap (τ : ℂˣ) {γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections (τ : ℂ) 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2) :
    Continuous (cubicTorusMap τ b hbase) :=
…

theorem OAI.Nagata.W21.isCompact_cubicTorusMap_range line 125

Source documentation

The image is compact for every admissible period.

theorem isCompact_cubicTorusMap_range {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    {γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections
      (Nagata.Workers.W05.positivePeriod τ hτ : ℂ) 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval (τ : ℂ) 3 γ z)) = 2) :
    IsCompact (Set.range (cubicTorusMap (Nagata.Workers.W05.positivePeriod τ hτ) b hbase)) := by
…

Mentions: OAI.Nagata.Workers.W05.positivePeriod

theorem OAI.Nagata.W21.cubicTorusMap_on_curve line 146

Source documentation

A homogeneous equation vanishing on the evaluation coordinates vanishes on the canonical representative of every image point.

theorem cubicTorusMap_on_curve (τ : ℂˣ) {γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections (τ : ℂ) 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2)
    {d : ℕ} (G : NonzeroHomogeneousForm d)
    (hG : ∀ z : ℂ, z ≠ 0 → MvPolynomial.eval (cubicEvaluationVector b z) G.polynomial = 0)
    (q : TorusPoint τ) : MvPolynomial.eval (cubicTorusMap τ b hbase q).rep G.polynomial = 0 := by
…

Mentions: OAI.Nagata.W21.TorusPoint

def OAI.Nagata.W21.cubicCurveMap line 164

Source documentation

The actual projective curve-valued map, without a surjectivity claim.

noncomputable def cubicCurveMap (τ : ℂˣ) {γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections (τ : ℂ) 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2)
    {d : ℕ} (G : NonzeroHomogeneousForm d)
    (hG : ∀ z : ℂ, z ≠ 0 → MvPolynomial.eval (cubicEvaluationVector b z) G.polynomial = 0) :
    TorusPoint τ → AssociatedBundle.CurvePoint G :=
…

Mentions: OAI.Nagata.W21.TorusPoint

theorem OAI.Nagata.W21.continuous_cubicCurveMap line 173

theorem OAI.Nagata.W21.exists_cubicForm_of_degreeNine_dimension line 184

Source documentation

The dimension argument supplies an actual nonzero homogeneous cubic with the pointwise vanishing needed by the curve-valued map.

theorem exists_cubicForm_of_degreeNine_dimension {τ γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    [Module.Finite ℂ (automorphicSections τ 9 (γ ^ 3))]
    (hdim : Module.finrank ℂ (automorphicSections τ 9 (γ ^ 3)) ≤ 9) :
    ∃ G : NonzeroHomogeneousForm 3, ∀ z : ℂ, z ≠ 0 →
      MvPolynomial.eval (cubicEvaluationVector b z) G.polynomial = 0 := by
…

def OAI.Nagata.W21.sectionLinePolynomial line 208

Source documentation

The literal projective linear equation corresponding to a section.

def sectionLinePolynomial {τ γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    (f : automorphicSections τ 3 γ) : MvPolynomial (Fin 3) ℂ :=
…

theorem OAI.Nagata.W21.sectionLinePolynomial_homogeneous line 213

theorem OAI.Nagata.W21.sectionLinePolynomial_eval line 221

Source documentation

Evaluating the actual linear equation recovers the section itself.

theorem sectionLinePolynomial_eval {τ γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    (f : automorphicSections τ 3 γ) (z : ℂ) :
    MvPolynomial.eval (cubicEvaluationVector b z) (sectionLinePolynomial b f) = f.val z := by
…

Mentions: OAI.Nagata.W21.sectionLinePolynomial

theorem OAI.Nagata.W21.sectionLinePolynomial_ne_zero line 232

Source documentation

A nonzero actual section gives a nonzero projective line equation.

theorem sectionLinePolynomial_ne_zero {τ γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    {f : automorphicSections τ 3 γ} (hf : f ≠ 0) : sectionLinePolynomial b f ≠ 0 := by
…

Mentions: OAI.Nagata.W21.sectionLinePolynomial

theorem OAI.Nagata.W21.sectionLinePolynomial_vanishes_at_image line 244

Source documentation

A zero of the section maps to a point on the literal projective line.

theorem sectionLinePolynomial_vanishes_at_image (τ : ℂˣ) {γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections (τ : ℂ) 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2)
    (f : automorphicSections (τ : ℂ) 3 γ) (z : ℂˣ) (hz : f.val z = 0) :
    MvPolynomial.eval (cubicCoverMap b hbase z).rep (sectionLinePolynomial b f) = 0 := by
…

Mentions: OAI.Nagata.W21.sectionLinePolynomial

theorem OAI.Nagata.W21.cubicTorusMap_isClosedEmbedding line 273

Source documentation

Compactness and actual projective Hausdorffness turn the proved injectivity into a closed embedding, with both spaces carrying their canonical topologies.

theorem cubicTorusMap_isClosedEmbedding {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    {γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections (positivePeriod τ hτ : ℂ) 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval (τ : ℂ) 3 γ z)) = 2)
    (hsep : ∀ z w : ℂˣ, ¬ torusOrbitSetoid (positivePeriod τ hτ) z w →
      Module.finrank ℂ (LinearMap.ker (sectionTwoEval (τ : ℂ) 3 γ z w)) = 1) :
    Topology.IsClosedEmbedding (cubicTorusMap (positivePeriod τ hτ) b hbase) := by
…

Mentions: OAI.Nagata.W21.torusOrbitSetoid

theorem OAI.Nagata.W21.cubicTorusMap_range_isConnected line 286

Source documentation

The actual image is connected, independently of any Chow theorem.

theorem cubicTorusMap_range_isConnected (τ : ℂˣ) {γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections (τ : ℂ) 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2) :
    IsConnected (Set.range (cubicTorusMap τ b hbase)) := by
…

theorem OAI.Nagata.W21.positivePeriod_norm_lt line 294

theorem OAI.Nagata.W21.cubicMapFromDimensions_isClosedEmbedding line 301

Source documentation

The closed embedding statement with all divisor-kernel hypotheses reduced to the actual D1/D2/D3 section dimensions. These dimensions remain explicit.

theorem cubicMapFromDimensions_isClosedEmbedding {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    {γ : ℂ} (hγ : γ ≠ 0)
    (b : Module.Basis (Fin 3) ℂ (automorphicSections (positivePeriod τ hτ : ℂ) 3 γ))
    (h1 : ∀ δ : ℂ, δ ≠ 0 → Module.finrank ℂ (automorphicSections (τ : ℂ) 1 δ) = 1)
    (h2 : ∀ δ : ℂ, δ ≠ 0 → Module.finrank ℂ (automorphicSections (τ : ℂ) 2 δ) = 2) :
    Topology.IsClosedEmbedding
      (cubicMapFromDimensions (positivePeriod τ hτ) (positivePeriod_norm_lt hτ hτ1) hγ b h2) := by
…

Mentions: OAI.Nagata.W21.positivePeriod_norm_lt

theorem OAI.Nagata.W21.continuous_actualCubicMap line 325
theorem OAI.Nagata.W21.actualCubicMap_isClosedEmbedding line 331
Source documentation
The actual theta map is a topological closed embedding; all section dimension assumptions have been discharged by the genuine Laurent basis.
```
theorem actualCubicMap_isClosedEmbedding {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    {γ : ℂ} (hγ : γ ≠ 0) : Topology.IsClosedEmbedding (actualCubicMap hτ hτone hγ) := by
…
```
theorem OAI.Nagata.W21.actualCubicMap_range_isConnected line 338

theorem OAI.Nagata.W21.exists_actualCubicForm line 345

Source documentation

An actual nonzero homogeneous cubic vanishes on every evaluation vector, with no dimension, finiteness or basis assumption left.

theorem exists_actualCubicForm {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    {γ : ℂ} (hγ : γ ≠ 0) :
    ∃ G : NonzeroHomogeneousForm 3, ∀ z : ℂ, z ≠ 0 →
      MvPolynomial.eval (cubicEvaluationVector (actualCubicBasis hτ hτone hγ) z)
        G.polynomial = 0 := by
…

theorem OAI.Nagata.W21.exists_actualCubic_image_containment line 360

Source documentation

The closed embedded torus is contained in the actual cubic zero locus. This is containment only, not equality or smoothness of that zero locus.

theorem exists_actualCubic_image_containment {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    {γ : ℂ} (hγ : γ ≠ 0) :
    ∃ G : NonzeroHomogeneousForm 3, ∀ q : TorusPoint (cubicPeriod hτ),
      MvPolynomial.eval (actualCubicMap hτ hτone hγ q).rep G.polynomial = 0 := by
…

Mentions: OAI.Nagata.W21.TorusPoint

theorem OAI.Nagata.W21.cubic_gradient_scale_iff line 379
theorem OAI.Nagata.W21.cubic_gradient_mk_rep_iff line 390
theorem OAI.Nagata.W21.actualCubicMap_gradient_iff line 399

theorem OAI.Nagata.W21.exists_threePointLine_through_image line 422

Source documentation

Through every image point there is an actual line with three distinct image points. The line does not vanish identically on the torus.

theorem exists_threePointLine_through_image {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    {γ : ℂ} (hγ : γ ≠ 0) (q : TorusPoint (cubicPeriod hτ)) :
    ∃ (L : MvPolynomial (Fin 3) ℂ) (p : Fin 3 → PlanePoint),
      L ≠ 0 ∧ L.IsHomogeneous 1 ∧ Function.Injective p ∧
      p 0 = actualCubicMap hτ hτone hγ q ∧
      (∀ i, p i ∈ Set.range (actualCubicMap hτ hτone hγ)) ∧
      (∀ i, MvPolynomial.eval (p i).rep L = 0) ∧
      ∃ z : ℂ, z ≠ 0 ∧
        MvPolynomial.eval (cubicEvaluationVector (actualCubicBasis hτ hτone hγ) z) L ≠ 0 := by
…

Mentions: OAI.Nagata.W21.TorusPoint