NYLL
Module

Card_effective_sub_isPrincipal_of_finite.lean

Nyll.AlgebraicCurves.Divisors.Card_effective_sub_isPrincipal_of_finite
16 declarations indexed from sourceView source ↗

Module documentation

Card effective sub is Principal of finite

Imports4
Imported by1

Declarations

def

divOf

L45 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.divOf
Documentation

A selected principal divisor for a nonzero function, with zero assigned to the zero function.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section DivOf
variable [HasPrincipalDivisors K F]
variable (K) in
open Classical in
Lean source · statement
def divOf (f : F) : Divisor K F
theorem

divOf_apply

L48 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.divOf_apply
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section DivOf
variable [HasPrincipalDivisors K F]
variable (K) in
Lean source · statement
theorem divOf_apply {f : F} (hf : f ≠ 0) (v : Place K F) : divOf K f v = v.ord f
theorem

ord_algebraMap

L52 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.ord_algebraMap
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section DivOf
variable [HasPrincipalDivisors K F]
variable (K) in
omit [HasPrincipalDivisors K F] in
Lean source · statement
theorem ord_algebraMap (v : Place K F) {a : K} (ha : a ≠ 0) : v.ord (algebraMap K F a) = 0
theorem

divOf_smul

L57 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.divOf_smul
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section DivOf
variable [HasPrincipalDivisors K F]
variable (K) in
Lean source · statement
theorem divOf_smul {f : F} (hf : f ≠ 0) {a : K} (ha : a ≠ 0) :
    divOf K (a • f) = divOf K f
theorem

divOf_mul

L64 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.divOf_mul
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section DivOf
variable [HasPrincipalDivisors K F]
variable (K) in
Lean source · statement
theorem divOf_mul {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) :
    divOf K (f * g) = divOf K f + divOf K g
theorem

divOf_inv

L69 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.divOf_inv
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section DivOf
variable [HasPrincipalDivisors K F]
variable (K) in
Lean source · statement
theorem divOf_inv (f : F) : divOf K f⁻¹ = -divOf K f
theorem

nonneg_divOf_add_iff

L76 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.nonneg_divOf_add_iff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section DivOf
variable [HasPrincipalDivisors K F]
variable (K) in
Lean source · statement
theorem nonneg_divOf_add_iff {f : F} (hf : f ≠ 0) (C : Divisor K F) :
    0 ≤ divOf K f + C ↔ f ∈ LSpace C
abbrev

LinSys

L94 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.LinSys
Documentation

The effective divisors linearly equivalent to the specified divisor.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section LinSys
variable [IsCurveOver K F]
Lean source · statement
abbrev LinSys (C : Divisor K F) : Type _
def

toLinSys'

L98 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.toLinSys'
Documentation

The effective divisor obtained by adding the divisor of a nonzero Riemann--Roch section.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section LinSys
variable [IsCurveOver K F]
Lean source · statement
def toLinSys' (C : Divisor K F) (f : {f : LSpace C // f ≠ 0}) : LinSys C
theorem

toLinSys'_wd

L104 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.toLinSys'_wd
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section LinSys
variable [IsCurveOver K F]
Lean source · statement
theorem toLinSys'_wd (C : Divisor K F) (a b : {f : LSpace C // f ≠ 0}) (t : K)
    (h : (a : LSpace C) = t • (b : LSpace C)) : toLinSys' C a = toLinSys' C b
def

toLinSys

L116 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.toLinSys
Documentation

The effective divisor associated with a projective class of nonzero Riemann--Roch sections.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section LinSys
variable [IsCurveOver K F]
Lean source · statement
def toLinSys (C : Divisor K F) : ℙ K (LSpace C) → LinSys C
theorem

toLinSys_mk

L119 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.toLinSys_mk
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section LinSys
variable [IsCurveOver K F]
Lean source · statement
theorem toLinSys_mk (C : Divisor K F) (f : LSpace C) (hf : f ≠ 0) :
    (toLinSys C (Projectivization.mk K f hf) : Divisor K F) = divOf K (f : F) + C
theorem

toLinSys_injective

L123 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.toLinSys_injective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section LinSys
variable [IsCurveOver K F]
Lean source · statement
theorem toLinSys_injective (hC : ConstantsAreBase K F) (C : Divisor K F) :
    Function.Injective (toLinSys C)
theorem

toLinSys_surjective

L154 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.toLinSys_surjective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section LinSys
variable [IsCurveOver K F]
Lean source · statement
theorem toLinSys_surjective (C : Divisor K F) : Function.Surjective (toLinSys C)
theorem

main

L165 ↗
AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite.AlgebraicCurve.CardLinearSystemSol.main
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CardLinearSystemSol
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section LinSys
variable [IsCurveOver K F]
Lean source · statement
theorem main [Finite K] (hC : ConstantsAreBase K F) (C : Divisor K F) :
    (Nat.card K - 1) * Nat.card (LinSys C) + 1 = Nat.card K ^ ell C
theorem

card_effective_sub_isPrincipal_of_finite

L183 ↗
AlgebraicCurve.card_effective_sub_isPrincipal_of_finite
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Card_effective_sub_isPrincipal_of_finite
open _root_.AlgebraicCurve
open scoped LinearAlgebra.Projectivization
Lean source · statement
theorem _root_.AlgebraicCurve.card_effective_sub_isPrincipal_of_finite
    (k F : Type*) [Field k] [Finite k] [Field F] [Algebra k F]
    [AlgebraicCurve.IsCurveOver k F]
    (hC : AlgebraicCurve.ConstantsAreBase k F) (C : AlgebraicCurve.Divisor k F) :
    (Nat.card k - 1) *
        Nat.card {D : AlgebraicCurve.Divisor k F //
          0 ≤ D ∧ AlgebraicCurve.Divisor.IsPrincipal (D - C)} + 1 =
      Nat.card k ^ AlgebraicCurve.ell C

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.