OAI/AlgebraicGeometry/PlaneCurves/CubicMap.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Projective cubic maps, separation, local coordinates, and differentials

  1. def OAI.Nagata.W07.cubicEvaluationVector line 24

    Source documentation

    Three actual evaluation coordinates associated to a basis of D(3,γ).

    def cubicEvaluationVector {τ γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ)) (z : ℂ) : Fin 3 → ℂ :=
…
  2. theorem OAI.Nagata.W07.cubic_basis_finrank line 28
  3. theorem OAI.Nagata.W07.cubicEvaluationVector_ne_zero line 34

    Source documentation

    No base point means the actual coordinate vector is nonzero.

    theorem cubicEvaluationVector_ne_zero {τ γ z : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    (hker : Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2) :
    cubicEvaluationVector b z ≠ 0 := by
…

    Mentions: OAI.Nagata.W07.sectionEval, OAI.Nagata.W07.cubicEvaluationVector

  4. def OAI.Nagata.W07.cubicCoverMap line 48

    Source documentation

    The actual projective map on the nonzero complex covering space.

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

    Mentions: OAI.Nagata.W07.sectionEval

  5. theorem OAI.Nagata.W07.cubicCoverMap_ne_of_kernel line 57

    Source documentation

    Independent values at two lifts force distinct actual projective images.

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

    Mentions: OAI.Nagata.W07.sectionEval, OAI.Nagata.W07.sectionTwoEval, OAI.Nagata.W07.cubicCoverMap

  6. theorem OAI.Nagata.W07.cubicCoverMap_period line 78

    Source documentation

    Common automorphy multipliers give invariance under the period generator.

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

    Mentions: OAI.Nagata.W07.sectionEval, OAI.Nagata.W07.cubicCoverMap

  7. theorem OAI.Nagata.W07.cubicCoverMap_zpow line 89

    Source documentation

    Period invariance holds in both integer directions, without a choice of lift.

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

    Mentions: OAI.Nagata.W07.sectionEval, OAI.Nagata.W07.cubicCoverMap

  8. def OAI.Nagata.W07.cubicTorusMap line 109

    Source documentation

    The map on the actual multiplicative torus quotient.

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

    Mentions: OAI.Nagata.W07.sectionEval

  9. theorem OAI.Nagata.W07.cubicTorusMap_mk line 119
  10. theorem OAI.Nagata.W07.cubicTorusMap_injective line 126

    Source documentation

    The dimension-two divisor input proves injectivity of the genuine torus map.

    theorem cubicTorusMap_injective (τ : ℂˣ) {γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections (τ : ℂ) 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2)
    (hsep : ∀ z w : ℂˣ, ¬ torusOrbitSetoid τ z w →
      Module.finrank ℂ (LinearMap.ker (sectionTwoEval τ 3 γ z w)) = 1) :
    Function.Injective (cubicTorusMap τ b hbase) := by
…

    Mentions: OAI.Nagata.W07.sectionEval, OAI.Nagata.W07.sectionTwoEval, OAI.Nagata.W07.cubicTorusMap

  11. theorem OAI.Nagata.W07.cubic_eval_kernel_dimension line 157
  12. theorem OAI.Nagata.W07.cubic_firstJet_kernel_dimension line 164
  13. theorem OAI.Nagata.W07.cubic_twoEval_kernel_dimension line 171
  14. theorem OAI.Nagata.W07.cubic_no_base_points line 180

    Source documentation

    No base points, using actual D3 and D2 section dimensions alone.

    theorem cubic_no_base_points {τ γ : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (hγ : γ ≠ 0)
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    (h2 : ∀ δ : ℂ, δ ≠ 0 → Module.finrank ℂ (automorphicSections τ 2 δ) = 2)
    {z : ℂ} (hz : z ≠ 0) :
    ∃ f : automorphicSections τ 3 γ, f.val z = 1 :=
…
  15. theorem OAI.Nagata.W07.cubic_ratio_deriv_one_from_dimensions line 190

    Source documentation

    A ratio with actual derivative one, after discharging the double-point divisor kernel.

    theorem cubic_ratio_deriv_one_from_dimensions {τ γ : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (hγ : γ ≠ 0)
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    (h1 : ∀ δ : ℂ, δ ≠ 0 → Module.finrank ℂ (automorphicSections τ 1 δ) = 1)
    (h2 : ∀ δ : ℂ, δ ≠ 0 → Module.finrank ℂ (automorphicSections τ 2 δ) = 2)
    {z : ℂ} (hz : z ≠ 0) :
    ∃ f g : automorphicSections τ 3 γ,
      f.val z = 0 ∧ g.val z = 1 ∧ deriv f.val z = 1 ∧
        deriv (fun w => f.val w / g.val w) z = 1 :=
…
  16. def OAI.Nagata.W07.cubicMapFromDimensions line 204

    Source documentation

    The genuine projective map, with basepoint exclusion obtained from D2 dimensions.

    def cubicMapFromDimensions (τ : ℂˣ) (hτ : ‖(τ : ℂ)‖ < 1) {γ : ℂ} (hγ : γ ≠ 0)
    (b : Module.Basis (Fin 3) ℂ (automorphicSections (τ : ℂ) 3 γ))
    (h2 : ∀ δ : ℂ, δ ≠ 0 → Module.finrank ℂ (automorphicSections (τ : ℂ) 2 δ) = 2) :
    TorusPoint τ → Projectivization ℂ (Fin 3 → ℂ) :=
…
  17. theorem OAI.Nagata.W07.cubicMapFromDimensions_injective line 210
  18. theorem OAI.Nagata.W07.cubic_basis_ratio_deriv_ne_zero line 236

    Source documentation

    For every nonzero basis denominator, some coordinate ratio has nonzero derivative.

    theorem cubic_basis_ratio_deriv_ne_zero {τ γ z : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ)) (hz : z ≠ 0)
    (hker : Module.finrank ℂ (LinearMap.ker (sectionFirstJet τ 3 γ hz)) = 1)
    (j : Fin 3) (hj : (b j).val z ≠ 0) :
    ∃ i : Fin 3, deriv (fun w => (b i).val w / (b j).val w) z ≠ 0 := by
…

    Mentions: OAI.Nagata.W07.sectionFirstJet

  19. theorem OAI.Nagata.W07.cubic_basis_ratio_analyticAt line 264

    Source documentation

    Coordinate ratios are genuine analytic functions wherever the denominator is nonzero.

    theorem cubic_basis_ratio_analyticAt {τ γ z : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    (hz : z ≠ 0) (i j : Fin 3) (hj : (b j).val z ≠ 0) :
    AnalyticAt ℂ (fun w => (b i).val w / (b j).val w) z :=
…
  20. theorem OAI.Nagata.W07.cubic_affine_chart_nonzero_derivative line 272

    Source documentation

    Some actual affine coordinate chart has a nonzero coordinate derivative at every lift.

    theorem cubic_affine_chart_nonzero_derivative {τ γ z : ℂ}
    (hτ : ‖τ‖ < 1) (hτ0 : τ ≠ 0) (hγ : γ ≠ 0)
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    (h1 : ∀ δ : ℂ, δ ≠ 0 → Module.finrank ℂ (automorphicSections τ 1 δ) = 1)
    (h2 : ∀ δ : ℂ, δ ≠ 0 → Module.finrank ℂ (automorphicSections τ 2 δ) = 2)
    (hz : z ≠ 0) :
    ∃ i j : Fin 3, (b j).val z ≠ 0 ∧
      AnalyticAt ℂ (fun w => (b i).val w / (b j).val w) z ∧
      deriv (fun w => (b i).val w / (b j).val w) z ≠ 0 := by
…
  21. theorem OAI.Nagata.W07.cubicCoverMap_chartCoordinates line 301
  22. theorem OAI.Nagata.W07.cubicCoverMap_chart_nonzero line 310
  23. theorem OAI.Nagata.W07.cubic_chart_variable_deriv_ne_zero line 319

    Source documentation

    The witness lies among the two genuine affine chart variables, not the denominator.

    theorem cubic_chart_variable_deriv_ne_zero {τ γ z : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ)) (hz : z ≠ 0)
    (hker : Module.finrank ℂ (LinearMap.ker (sectionFirstJet τ 3 γ hz)) = 1)
    (j : Fin 3) (hj : (b j).val z ≠ 0) :
    ∃ i : ChartVariables j, deriv (fun w => (b i.val).val w / (b j).val w) z ≠ 0 := by
…

    Mentions: OAI.Nagata.W07.sectionFirstJet

  24. def OAI.Nagata.W07.cubicExponentialMap line 335

    Source documentation

    The covering map in a genuine local exponential parameter.

    def cubicExponentialMap {τ γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2)
    (z : ℂˣ) (x : ℂ) : PlanePoint :=
…

    Mentions: OAI.Nagata.W07.sectionEval

  25. theorem OAI.Nagata.W07.cubicExponentialMap_coordinate line 342
  26. theorem OAI.Nagata.W07.cubicExponentialMap_coordinate_deriv_ne_zero line 353

    Source documentation

    Actual projective affine coordinates have a nonzero derivative in the torus chart.

    theorem cubicExponentialMap_coordinate_deriv_ne_zero {τ γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2)
    (z : ℂˣ) (j : Fin 3) (hj : (b j).val z ≠ 0)
    (hker : Module.finrank ℂ (LinearMap.ker (sectionFirstJet τ 3 γ z.ne_zero)) = 1) :
    ∃ i : ChartVariables j,
      deriv (fun x => chartCoordinates j (cubicExponentialMap b hbase z x) i) 0 ≠ 0 := by
…

    Mentions: OAI.Nagata.W07.sectionEval, OAI.Nagata.W07.sectionFirstJet, OAI.Nagata.W07.cubicExponentialMap

  27. theorem OAI.Nagata.W07.pi_fderiv_injective_of_coordinate line 390
  28. theorem OAI.Nagata.W07.cubicExponentialMap_coordinate_differentiableAt line 402
  29. theorem OAI.Nagata.W07.cubicExponentialMap_fderiv_injective line 422

    Source documentation

    This is the actual affine-coordinate tangent map, not an assumed immersion predicate.

    theorem cubicExponentialMap_fderiv_injective {τ γ : ℂ}
    (b : Module.Basis (Fin 3) ℂ (automorphicSections τ 3 γ))
    (hbase : ∀ z : ℂ, z ≠ 0 →
      Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2)
    (z : ℂˣ) (j : Fin 3) (hj : (b j).val z ≠ 0)
    (hker : Module.finrank ℂ (LinearMap.ker (sectionFirstJet τ 3 γ z.ne_zero)) = 1) :
    Function.Injective (fderiv ℂ
      (fun x => chartCoordinates j (cubicExponentialMap b hbase z x)) 0) :=
…

    Mentions: OAI.Nagata.W07.sectionEval, OAI.Nagata.W07.sectionFirstJet, OAI.Nagata.W07.cubicExponentialMap

  30. theorem OAI.Nagata.W07.cubicExponentialMap_chartTwo_differentiableAt line 446
  31. theorem OAI.Nagata.W07.cubicExponentialMap_chartTwo_fderiv_injective line 457
  32. def OAI.Nagata.W07.cubicPeriod line 487

    Source documentation

    The actual nonzero real period as a complex unit.

    def cubicPeriod {τ : ℝ} (hτ : 0 < τ) : ℂˣ :=
…
  33. theorem OAI.Nagata.W07.cubicPeriod_val line 490
  34. theorem OAI.Nagata.W07.realPeriod_norm_lt_one line 493
  35. theorem OAI.Nagata.W07.actualPositiveSection_finrank line 498

    Source documentation

    Actual positive-degree dimensions, with Laurent injectivity discharged.

    theorem actualPositiveSection_finrank {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    {n : ℤ} (hn : 0 < n) {γ : ℂ} (hγ : γ ≠ 0) :
    Module.finrank ℂ (automorphicSections (τ : ℂ) n γ) = n.toNat :=
…
  36. def OAI.Nagata.W07.actualCubicBasis line 505

    Source documentation

    A chosen actual basis of D(3,γ), built from convergent theta sections.

    def actualCubicBasis {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    {γ : ℂ} (hγ : γ ≠ 0) :
    Module.Basis (Fin 3) ℂ (automorphicSections (τ : ℂ) 3 γ) :=
…
  37. theorem OAI.Nagata.W07.actualCubic_eval_kernel_dimension line 512
  38. theorem OAI.Nagata.W07.actualCubic_firstJet_kernel_dimension line 519
  39. theorem OAI.Nagata.W07.actualCubic_no_base_points line 527

    Source documentation

    The complete actual degree-three section space has no base points.

    theorem actualCubic_no_base_points {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    {γ : ℂ} (hγ : γ ≠ 0) {z : ℂ} (hz : z ≠ 0) :
    ∃ f : automorphicSections (τ : ℂ) 3 γ, f.val z = 1 :=
…
  40. def OAI.Nagata.W07.actualCubicMap line 535

    Source documentation

    The genuine projective map on the genuine multiplicative torus quotient.

    def actualCubicMap {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    {γ : ℂ} (hγ : γ ≠ 0) : TorusPoint (cubicPeriod hτ) → PlanePoint :=
…

    Mentions: OAI.Nagata.W07.cubicPeriod

  41. theorem OAI.Nagata.W07.actualCubicMap_injective line 540
  42. def OAI.Nagata.W07.actualCubicExponentialMap line 555

    Source documentation

    Evaluate the actual cubic map in the genuine exponential parameter around a lift.

    def actualCubicExponentialMap {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    {γ : ℂ} (hγ : γ ≠ 0) (z : ℂˣ) : ℂ → PlanePoint :=
…
  43. theorem OAI.Nagata.W07.actualCubicExponentialMap_eq line 560
  44. theorem OAI.Nagata.W07.actualCubicExponentialMap_zero line 567
  45. theorem OAI.Nagata.W07.actualCubicMap_chart_differentiableAt line 577

    Source documentation

    In every target chart containing the image, the actual two-coordinate map is differentiable.

    theorem actualCubicMap_chart_differentiableAt {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    {γ : ℂ} (hγ : γ ≠ 0) (z : ℂˣ) (j : Fin 3)
    (hj : (actualCubicMap hτ hτone hγ (torusPointMk (cubicPeriod hτ) z)).rep j ≠ 0) :
    DifferentiableAt ℂ
      (fun x => chartCoordinates₂ j (actualCubicExponentialMap hτ hτone hγ z x)) 0 := by
…

    Mentions: OAI.Nagata.W07.actualCubicMap, OAI.Nagata.W07.cubicPeriod, OAI.Nagata.W07.actualCubicExponentialMap

  46. theorem OAI.Nagata.W07.actualCubicMap_chart_fderiv_injective line 587

    Source documentation

    The actual complex tangent map is injective in every projective chart containing the point.

    theorem actualCubicMap_chart_fderiv_injective {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
    {γ : ℂ} (hγ : γ ≠ 0) (z : ℂˣ) (j : Fin 3)
    (hj : (actualCubicMap hτ hτone hγ (torusPointMk (cubicPeriod hτ) z)).rep j ≠ 0) :
    Function.Injective (fderiv ℂ
      (fun x => chartCoordinates₂ j (actualCubicExponentialMap hτ hτone hγ z x)) 0) := by
…

    Mentions: OAI.Nagata.W07.actualCubicMap, OAI.Nagata.W07.cubicPeriod, OAI.Nagata.W07.actualCubicExponentialMap