Module

Ell_add_of_forall_eq_ord.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_add_of_forall_eq_ord

3 declarations indexed from sourceView source ↗

Module documentation

Dimensions of Riemann--Roch spaces under translation by the divisor of a nonzero function.

Imports1

Nyll.AlgebraicCurves.Cohomology.Adelic.Index

Imported by3

theorem

lSpace_add_map_mulLeft

L33 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_add_of_forall_eq_ord.RRSol.lSpace_add_map_mulLeft

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_add_of_forall_eq_ord
open AlgebraicCurve
universe u v
namespace RRSol
section principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpace_add_map_mulLeft {D P : Divisor K F} {f : F} (hf : f ≠ 0)
    (hP : ∀ v : Place K F, P v = v.ord f) :
    (LSpace (D + P)).map (LinearMap.mulLeft K f) = LSpace D

theorem

ell_add_of_forall_eq_ord

L64 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_add_of_forall_eq_ord.RRSol.ell_add_of_forall_eq_ord

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_add_of_forall_eq_ord
open AlgebraicCurve
universe u v
namespace RRSol
section principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_add_of_forall_eq_ord {D P : Divisor K F} {f : F} (hf : f ≠ 0)
    (hP : ∀ v : Place K F, P v = v.ord f) : ell (D + P) = ell D

theorem

ell_add_of_forall_eq_ord

L75 ↗

AlgebraicCurve.ell_add_of_forall_eq_ord

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_add_of_forall_eq_ord
open AlgebraicCurve
universe u v

Lean source · statement

theorem _root_.AlgebraicCurve.ell_add_of_forall_eq_ord
    {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] (D : Divisor K F) {P : Divisor K F}
    {f : F} (hf : f ≠ 0) (hP : ∀ v : Place K F, P v = v.ord f) :
    ell (D + P) = ell D

Module documentation

Declarations

lSpace_add_map_mulLeft

ell_add_of_forall_eq_ord

ell_add_of_forall_eq_ord