Documentation

Atlas.ArithmeticGeometry.code.RiemannRochP1

theorem RiemannRochSpace.rational_curve_Pic0_and_infinite {C : Type u_4} {F : Type u_5} {k : Type u_6} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (hF : F ≃ₐ[k] RatFunc k) :
(∀ (D : CurveDivisor C), (CurveDivisor.degree C) D = 0∃ (f : Fˣ), CurveWithOrd.principalDivisor f = D) ∃ (f : C), Function.Injective f

A rational curve (function field $\cong k(t)$) has trivial $\mathrm{Pic}^0$ (every degree-$0$ divisor is principal) and infinitely many points.

theorem RiemannRochSpace.rational_curve_inject_nat {C : Type u_4} {F : Type u_5} {k : Type u_6} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (hF : F ≃ₐ[k] RatFunc k) :
∃ (f : C), Function.Injective f

A rational curve admits an injection from $\mathbb{N}$, witnessing it has infinitely many points.

theorem RiemannRochSpace.rational_curve_infinite {C : Type u_4} {F : Type u_5} {k : Type u_6} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (hF : F ≃ₐ[k] RatFunc k) :

A rational curve has infinitely many points.

theorem RiemannRochSpace.degree_zero_divisor_is_principal_of_rational {C : Type u_4} {F : Type u_5} {k : Type u_6} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (hF : F ≃ₐ[k] RatFunc k) (D : CurveDivisor C) (hD : (CurveDivisor.degree C) D = 0) :

Every degree-zero divisor on a rational curve is principal.

theorem RiemannRochSpace.Pic0_trivial_of_rational {C : Type u_4} {F : Type u_5} {k : Type u_6} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (hF : F ≃ₐ[k] RatFunc k) (D : CurveDivisor C) :

$\mathrm{Pic}^0(C) = 0$ for a rational curve: every divisor of degree $0$ is principal.

def RiemannRochSpace.HasPrescribedPoles {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (f : Fˣ) (A : CurveDivisor C) :

A nonzero rational function $f$ has prescribed poles given by an effective divisor $A$ if $\mathrm{div}(f) + A \geq 0$ and $\mathrm{ord}_P(f) = -A(P)$ for every $P$ with $A(P) > 0$.

Instances For
    theorem RiemannRochSpace.exists_point_not_in_support {C : Type u_4} {F : Type u_5} {k : Type u_6} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (hF : F ≃ₐ[k] RatFunc k) (A : CurveDivisor C) :
    ∃ (P₀ : C), P₀A.support

    On a rational curve (hence infinite), any divisor $A$ admits a point $P_0$ outside its support.

    theorem RiemannRochSpace.prescribed_poles_of_rational {C : Type u_4} {F : Type u_5} {k : Type u_6} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (hF : F ≃ₐ[k] RatFunc k) (A : CurveDivisor C) (_hA : A.IsEffective) (hA_pos : (CurveDivisor.degree C) A > 0) :
    ∃ (f : Fˣ), HasPrescribedPoles f A

    On a rational curve, given any effective divisor $A$ of positive degree, there exists a rational function $f$ with prescribed poles equal to $A$.

    theorem RiemannRochSpace.mem_riemannRochSpace_of_prescribed_poles {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] {f : Fˣ} {A : CurveDivisor C} (hf : HasPrescribedPoles f A) :

    A function with prescribed poles bounded by $A$ lies in the Riemann-Roch space $L(A)$.

    If $A \leq B$ as divisors then $\deg B - \deg A \geq 0$.

    theorem RiemannRochSpace.step_eq_aux {C : Type u_4} {F : Type u_5} {k : Type u_6} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (hF : F ≃ₐ[k] RatFunc k) (n : ) {A B : CurveDivisor C} (hAB : A B) (hA : A.IsEffective) [FiniteDimensional k (riemannRochSpace A)] (hn : ((CurveDivisor.degree C) B - (CurveDivisor.degree C) A).toNat = n) :

    Inductive step lemma for Riemann-Roch on $\mathbb{P}^1$: when $A \leq B$ are effective with $\deg B - \deg A = n$, we have $\dim_k L(B) = \dim_k L(A) + (\deg B - \deg A)$, proved by induction on $n$.

    On a rational curve, for effective divisors $A \leq B$, $\dim_k L(B) = \dim_k L(A) + (\deg B - \deg A)$.

    theorem RiemannRochSpace.riemannRochSpace_lower_bound_of_rational {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (hF : F ≃ₐ[k] RatFunc k) (D : CurveDivisor C) (hD : D.IsEffective) :

    On a rational curve, for any effective divisor $D$, the Riemann-Roch space satisfies $\dim_k L(D) \geq \deg D + 1$.

    theorem RiemannRochSpace.divisorDim_eq_degD_add_one_of_rational {C : Type u_1} {F : Type u_2} {k : Type u_3} [Field k] [Field F] [Algebra k F] [RiemannRochData C F k] (hF : F ≃ₐ[k] RatFunc k) (D : CurveDivisor C) (hD : D.IsEffective) :

    Riemann-Roch on $\mathbb{P}^1$: for any effective divisor $D$ on a rational curve, $\ell(D) = \deg D + 1$.