AlgebraicCurve.lSpace_nsmul_succ_poleDivisor_le_sup_map_mulLeft_of_ell_eq
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.LSpaceNsmulSuccPoleDivisorLeSup
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.lSpace_nsmul_succ_poleDivisor_le_sup_map_mulLeft_of_ell_eq
{K F : Type*} [Field K] [Field F] [Algebra K F]
(x : F) (D : Divisor K F) (hD : ∀ v : Place K F, D v = max 0 (-v.ord x))
(hFD : ∀ M : ℕ, FiniteDimensional K ↥(LSpace (M • D)))
(M₀ d g₀ : ℕ)
(hell : ∀ N, M₀ ≤ N → (ell (N • D) : ℤ) = N * d + 1 - g₀)
(m : ℕ) (hm : M₀ + 1 ≤ m) :
(LSpace ((m + 1) • D) : Submodule K F)
≤ LSpace (m • D) ⊔ (LSpace (m • D)).map (LinearMap.mulLeft K x)