CubicEvaluation.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of cubic theta sections

def OAI.Nagata.W07.sectionEval line 28

Source documentation

Evaluation in the actual covering-space frame.

def sectionEval (τ : ℂ) (n : ℤ) (γ z : ℂ) :
    automorphicSections τ n γ →ₗ[ℂ] ℂ where
…

theorem OAI.Nagata.W07.sectionEval_apply line 34

def OAI.Nagata.W07.sectionDeriv line 38

Source documentation

Actual complex derivative at a point of the punctured plane.

def sectionDeriv (τ : ℂ) (n : ℤ) (γ : ℂ) {z : ℂ} (hz : z ≠ 0) :
    automorphicSections τ n γ →ₗ[ℂ] ℂ where
…

theorem OAI.Nagata.W07.sectionDeriv_apply line 44

def OAI.Nagata.W07.sectionFirstJet line 49

Source documentation

Value and actual first derivative in one fixed local frame.

def sectionFirstJet (τ : ℂ) (n : ℤ) (γ : ℂ) {z : ℂ} (hz : z ≠ 0) :
    automorphicSections τ n γ →ₗ[ℂ] ℂ × ℂ :=
…

def OAI.Nagata.W07.sectionTwoEval line 54

Source documentation

Values at two specified covering points.

def sectionTwoEval (τ : ℂ) (n : ℤ) (γ z w : ℂ) :
    automorphicSections τ n γ →ₗ[ℂ] ℂ × ℂ :=
…

theorem OAI.Nagata.W07.mem_sectionEval_ker line 58
theorem OAI.Nagata.W07.mem_sectionTwoEval_ker line 62
theorem OAI.Nagata.W07.mem_sectionFirstJet_ker line 68

theorem OAI.Nagata.W07.linearMap_surjective_of_kernel_codimension line 76

Source documentation

Rank-nullity gives surjectivity when the actual kernel has the expected codimension.

theorem linearMap_surjective_of_kernel_codimension
    {V W : Type*} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
    (L : V →ₗ[ℂ] W)
    (hdim : Module.finrank ℂ (LinearMap.ker L) + Module.finrank ℂ W =
      Module.finrank ℂ V) : Function.Surjective L := by
…

theorem OAI.Nagata.W07.cubic_eval_surjective line 88

Source documentation

Dimension three and a two-dimensional vanishing kernel exclude a base point.

theorem cubic_eval_surjective (τ γ z : ℂ)
    (h3 : Module.finrank ℂ (automorphicSections τ 3 γ) = 3)
    (hker : Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2) :
    Function.Surjective (sectionEval τ 3 γ z) := by
…

Mentions: OAI.Nagata.W07.sectionEval

theorem OAI.Nagata.W07.cubic_exists_section_eval_one line 97

theorem OAI.Nagata.W07.cubic_twoEval_surjective line 104

Source documentation

A one-dimensional simultaneous vanishing kernel allows independent values.

theorem cubic_twoEval_surjective (τ γ z w : ℂ)
    (h3 : Module.finrank ℂ (automorphicSections τ 3 γ) = 3)
    (hker : Module.finrank ℂ (LinearMap.ker (sectionTwoEval τ 3 γ z w)) = 1) :
    Function.Surjective (sectionTwoEval τ 3 γ z w) := by
…

Mentions: OAI.Nagata.W07.sectionTwoEval

theorem OAI.Nagata.W07.cubic_exists_section_separating line 113

theorem OAI.Nagata.W07.cubic_firstJet_surjective line 121

Source documentation

The double-point kernel of dimension one implies full first-jet separation.

theorem cubic_firstJet_surjective (τ γ : ℂ) {z : ℂ} (hz : z ≠ 0)
    (h3 : Module.finrank ℂ (automorphicSections τ 3 γ) = 3)
    (hker : Module.finrank ℂ (LinearMap.ker (sectionFirstJet τ 3 γ hz)) = 1) :
    Function.Surjective (sectionFirstJet τ 3 γ hz) := by
…

Mentions: OAI.Nagata.W07.sectionFirstJet

theorem OAI.Nagata.W07.cubic_exists_ratio_deriv_one line 132

Source documentation

An actual ratio of genuine sections is a local coordinate with derivative one. The denominator is chosen to have value one, so the quotient is holomorphic near the point.

theorem cubic_exists_ratio_deriv_one (τ γ : ℂ) {z : ℂ} (hz : z ≠ 0)
    (h3 : Module.finrank ℂ (automorphicSections τ 3 γ) = 3)
    (hker1 : Module.finrank ℂ (LinearMap.ker (sectionEval τ 3 γ z)) = 2)
    (hker2 : Module.finrank ℂ (LinearMap.ker (sectionFirstJet τ 3 γ hz)) = 1) :
    ∃ 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 := by
…

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