OAI/AlgebraicGeometry/PlaneCurves/SectionDimensions.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nagata.Workers.W10.positiveSectionBasis_exists line 23

   Source documentation

   Arbitrary nonzero multipliers admit the actual positive-degree theta basis. Only injectivity of the genuine circle coefficient map remains an explicit input.

   theorem positiveSectionBasis_exists {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
       (hC : ∀ (n : ℤ) (γ : ℂ), Function.Injective (laurentCoefficientMap (τ : ℂ) n γ))
       {n : ℤ} (hn : 0 < n) {γ : ℂ} (hγ : γ ≠ 0) :
       Nonempty (Basis (Fin n.toNat) ℂ (automorphicSections (τ : ℂ) n γ)) := by
   …

2. def OAI.Nagata.Workers.W10.positiveSectionBasisFin line 39
3. theorem OAI.Nagata.Workers.W10.positiveSection_finite line 45
4. theorem OAI.Nagata.Workers.W10.positiveSection_finrank line 51
5. theorem OAI.Nagata.Workers.W10.zeroSection_finrank line 58

   Source documentation

   The constant tip has dimension one unconditionally.

   theorem zeroSection_finrank {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1) :
       Module.finrank ℂ (automorphicSections (τ : ℂ) 0 1) = 1 := by
   …

6. def OAI.Nagata.Workers.W10.thetaLowerIndexEquiv line 77
7. def OAI.Nagata.Workers.W10.thetaSectionBasisAtLower line 81
8. theorem OAI.Nagata.Workers.W10.thetaSectionBasisAtLower_apply line 92
9. theorem OAI.Nagata.Workers.W10.thetaSectionBasisAtLower_local line 103
10. def OAI.Nagata.Workers.W10.automorphicSectionBasis line 129
11. theorem OAI.Nagata.Workers.W10.automorphicSection_finite line 134
12. theorem OAI.Nagata.Workers.W10.automorphicSection_finrank line 139
13. def OAI.Nagata.Workers.W10.actualThetaBasis line 145

    Source documentation

    The exact centered source vectors, retaining their local scalar normalization.

    def actualThetaBasis (n : ℤ) (hn : 0 < n) (σ x₀ : ℝ)
        {ε : ℂ} (hε : ε ≠ 0) (hunit : ‖ε‖ = 1)
        {τ : ℝ} (hτ : 0 < τ) (hτone : τ < 1)
        (hU : σ - x₀ * (n : ℝ) ∉ Set.range (Int.cast : ℤ → ℝ)) :
        Basis (Nagata.W09.thetaIndices (σ - x₀ * (n : ℝ)) n) ℂ
          (automorphicSections (τ : ℂ) n (ε * ((τ ^ σ : ℝ) : ℂ))) :=
    …

    Mentions: OAI.Nagata.W09.thetaIndices

14. theorem OAI.Nagata.Workers.W10.actualThetaBasis_apply line 154