Module

Finrank_span_pair_mul_riemannRochSpace_add_finrank.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Finrank_span_pair_mul_riemannRochSpace_add_finrank

3 declarations indexed from sourceView source ↗

Module documentation

Finrank span pair mul riemann Roch Space add finrank

Imports1

Nyll.AlgebraicCurves.Cohomology.Adelic.Repartitions

Imported by1

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.All

theorem

ord_neg'

L27 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankSpanPairMulRRSpaceAdd.ProofAuxBrick.ord_neg'

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankSpanPairMulRRSpaceAdd
namespace ProofAuxBrick
open Submodule AlgebraicCurve

Lean source · statement

theorem ord_neg' {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F) (x : F) :
    w.ord (-x) = w.ord x

theorem

mul_mem_riemannRochSpace_add

L31 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankSpanPairMulRRSpaceAdd.ProofAuxBrick.mul_mem_riemannRochSpace_add

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankSpanPairMulRRSpaceAdd
namespace ProofAuxBrick
open Submodule AlgebraicCurve

Lean source · statement

theorem mul_mem_riemannRochSpace_add {K F : Type*} [Field K] [Field F] [Algebra K F]
    {A B : Divisor K F} {f g : F} (hf : f ∈ riemannRochSpace A) (hg : g ∈ riemannRochSpace B) :
    f * g ∈ riemannRochSpace (A + B)

theorem

finrank_span_pair_mul_riemannRochSpace_add_finrank

L47 ↗

AlgebraicCurve.finrank_span_pair_mul_riemannRochSpace_add_finrank

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankSpanPairMulRRSpaceAdd
open Submodule AlgebraicCurve ProofAuxBrick in

Lean source · statement

theorem _root_.AlgebraicCurve.finrank_span_pair_mul_riemannRochSpace_add_finrank
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (L M : AlgebraicCurve.Divisor K F) {f₁ f₂ : F} (hf₁ : f₁ ≠ 0) (hf₂ : f₂ ≠ 0)
    (h₁ : ∀ w : AlgebraicCurve.Place K F, 0 ≤ w.ord f₁ + L w)
    (h₂ : ∀ w : AlgebraicCurve.Place K F, 0 ≤ w.ord f₂ + L w)
    (hbpf : ∀ w : AlgebraicCurve.Place K F, w.ord f₁ + L w = 0 ∨ w.ord f₂ + L w = 0)
    [FiniteDimensional K ↥(AlgebraicCurve.riemannRochSpace M)] :
    Module.finrank K ↥(Submodule.span K {f₁, f₂} * AlgebraicCurve.riemannRochSpace M)
        + Module.finrank K ↥(AlgebraicCurve.riemannRochSpace (M - L))
      = 2 * Module.finrank K ↥(AlgebraicCurve.riemannRochSpace M) ∧
    Submodule.span K {f₁, f₂} * AlgebraicCurve.riemannRochSpace M ≤
      AlgebraicCurve.riemannRochSpace (M + L)

Module documentation

Finrank span pair mul riemann Roch Space add finrank

Declarations

ord_neg'

mul_mem_riemannRochSpace_add

finrank_span_pair_mul_riemannRochSpace_add_finrank