Module

RiemannGenusReached_of_stichtenothGenusExists.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RiemannGenusReached_of_stichtenothGenusExists

169 declarations indexed from sourceView source ↗

Module documentation

Riemann Genus Reached of stichtenoth Genus Exists

Imports20

Imported by1

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.All

theorem

ord_nonneg_of_mem

L53 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.Place.ord_nonneg_of_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
  restrict_placeOfPrime placeOfPrime
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_nonneg_of_mem {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f

theorem

mem_of_ord_nonneg

L67 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.Place.mem_of_ord_nonneg

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
  restrict_placeOfPrime placeOfPrime
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring

theorem

mem_iff_ord_nonneg

L74 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.Place.mem_iff_ord_nonneg

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
  restrict_placeOfPrime placeOfPrime
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem mem_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f

theorem

degree_eq_sum_support

L89 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.Divisor.degree_eq_sum_support

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Divisor in

Lean source · statement

theorem Divisor.degree_eq_sum_support (D : Divisor K F) :
    Divisor.degree D = ∑ v ∈ D.support, D v * (v.deg : ℤ)

theorem

degree_nonneg_of_nonneg

L95 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.Divisor.degree_nonneg_of_nonneg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}
open scoped _root_.AlgebraicCurve.Divisor in

Lean source · statement

theorem Divisor.degree_nonneg_of_nonneg [IsCurveOver K F]
    {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) : 0 ≤ Divisor.degree D

theorem

lSpace_eq_bot_of_degree_neg

L99 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.lSpace_eq_bot_of_degree_neg

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}

Lean source · statement

theorem lSpace_eq_bot_of_degree_neg [IsCurveOver K F]
    (hD : Divisor.degree D < 0) : LSpace D = ⊥

theorem

ell_eq_zero_of_degree_neg

L115 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.ell_eq_zero_of_degree_neg

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}

Lean source · statement

theorem ell_eq_zero_of_degree_neg [IsCurveOver K F] (hD : Divisor.degree D < 0) :
    ell D = 0

theorem

mk_mem_maximalIdeal_iff

L142 ↗

AlgebraicCurve.Place.mk_mem_maximalIdeal_iff

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
  restrict_placeOfPrime placeOfPrime
variable (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mk_mem_maximalIdeal_iff {f : F} (hf : f ∈
  v.toValuationSubring) :
    (⟨f, hf⟩ : v.toValuationSubring) ∈ IsLocalRing.maximalIdeal v.toValuationSubring
      ↔ f = 0 ∨ 0 < v.ord f

theorem

ell_le_ell_sub_single_add_deg

L172 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.ell_le_ell_sub_single_add_deg

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_ell_sub_single_add_deg [IsCurveOver K F] (D : Divisor K F) (P : Place K F) :
    ell D ≤ ell (D - Finsupp.single P 1) + P.deg

theorem

one_le_deg

L264 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.one_le_deg

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem one_le_deg [IsCurveOver K F] (P : Place K F) : 1 ≤ P.deg

theorem

ell_le_degree_add_ellZero

L268 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.ell_le_degree_add_ellZero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_degree_add_ellZero [IsCurveOver K F] {D : Divisor K F}
    (hD : ∀ v, 0 ≤ D v) :
    (ell D : ℤ) ≤ Divisor.degree D + ell (0 : Divisor K F)

theorem

ell_le_degree_add_one_of_effective

L305 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.ell_le_degree_add_one_of_effective

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_degree_add_one_of_effective [IsCurveOver K F]
    (hC : ConstantsAreBase K F) {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) :
    (ell D : ℤ) ≤ Divisor.degree D + 1

def

lSpaceShiftEquiv

L314 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.lSpaceShiftEquiv

Documentation

Multiplication by the inverse of g identifies the spaces for divisors differing by its divisor.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def lSpaceShiftEquiv (D : Divisor K F) {g : F} (hg : g ≠ 0)
    {Dg : Divisor K F} (hDg : ∀ v, Dg v = v.ord g) :
    LSpace D ≃ₗ[K] LSpace (D + Dg) where
  toFun h := ⟨(h : F) * g⁻¹, by
    rw [mem_lSpace_iff_ord]
    rcases eq_or_ne (h : F) 0 with hh0 | hh0
    · left; rw [hh0, zero_mul]
    · right; intro v
      rw [Finsupp.add_apply, hDg, v.ord_mul hh0 (inv_ne_zero hg), v.ord_inv]
      have := (mem_lSpace_iff_ord.mp h.2).resolve_left hh0 v
      linarith⟩
  invFun k := ⟨(k : F) * g, by
    rw [mem_lSpace_iff_ord]
    rcases eq_or_ne (k : F) 0 with hk0 | hk0
    · left; rw [hk0, zero_mul]
    · right; intro v
      have := (mem_lSpace_iff_ord.mp k.2).resolve_left hk0 v
      rw [Finsupp.add_apply, hDg] at this
      rw [v.ord_mul hk0 hg]
      linarith⟩
  map_add' h₁ h₂ := by apply Subtype.ext; push_cast; ring
  map_smul' c h := by
    apply Subtype.ext
    simp only [RingHom.id_apply, SetLike.val_smul, Algebra.smul_def]
    ring
  left_inv h := by
    apply Subtype.ext
    change (h : F) * g⁻¹ * g = (h : F)
    rw [mul_assoc, inv_mul_cancel₀ hg, mul_one]
  right_inv k := by
    apply Subtype.ext
    change (k : F) * g * g⁻¹ = (k : F)
    rw [mul_assoc, mul_inv_cancel₀ hg, mul_one]

theorem

ell_le_degree_add_one

L348 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.ell_le_degree_add_one

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_degree_add_one [IsCurveOver K F] (hC : ConstantsAreBase K F)
    {D : Divisor K F} (hD : 0 ≤ Divisor.degree D) :
    (ell D : ℤ) ≤ Divisor.degree D + 1

def

nestedComapMapMkQEquiv

L387 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.Submodule.nestedComapMapMkQEquiv

Documentation

Identify the image of B in the quotient of C by A with the induced quotient of B.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

def nestedComapMapMkQEquiv {A B C : Submodule K X} (_hAB : A ≤ B) (hBC : B ≤ C) :
    ((B.comap C.subtype).map (A.comap C.subtype).mkQ : Submodule K _)
      ≃ₗ[K] B ⧸ A.comap B.subtype

theorem

finrank_quotient_chain

L415 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.Submodule.finrank_quotient_chain

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem finrank_quotient_chain {A B C : Submodule K X} (hAB : A ≤ B) (hBC : B ≤ C)
    [hCB : Module.Finite K (C ⧸ B.comap C.subtype)]
    [hBA : Module.Finite K (B ⧸ A.comap B.subtype)] :
    Module.Finite K (C ⧸ A.comap C.subtype) ∧
      finrank K (C ⧸ A.comap C.subtype)
        = finrank K (C ⧸ B.comap C.subtype) + finrank K (B ⧸ A.comap B.subtype)

theorem

finrank_quotient_chain'

L434 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.Submodule.finrank_quotient_chain'

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem finrank_quotient_chain' {A B C : Submodule K X} (hAB : A ≤ B) (hBC : B ≤ C)
    [hCA : Module.Finite K (C ⧸ A.comap C.subtype)] :
    Module.Finite K (C ⧸ B.comap C.subtype) ∧
      finrank K (C ⧸ B.comap C.subtype)
        = finrank K (C ⧸ A.comap C.subtype) - finrank K (B ⧸ A.comap B.subtype)

def

adeleBddQuotSingleEquivResidueField

L461 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.adeleBddQuotSingleEquivResidueField

Documentation

The quotient obtained by lowering the bound at one place is linearly equivalent to its residue field.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def adeleBddQuotSingleEquivResidueField (D : Divisor K F) (P : Place K F) :
    (adeleBdd D ⧸ (adeleBdd (D - Finsupp.single P 1)).comap (adeleBdd D).subtype)
      ≃ₗ[K] P.ResidueField

theorem

finrank_adeleBdd_quotient_single

L572 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.finrank_adeleBdd_quotient_single

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBdd_quotient_single [IsCurveOver K F] (D : Divisor K F) (P : Place K F) :
    Module.Finite K
        (adeleBdd D ⧸ (adeleBdd (D - Finsupp.single P 1)).comap (adeleBdd D).subtype) ∧
      finrank K
          (adeleBdd D ⧸ (adeleBdd (D - Finsupp.single P 1)).comap (adeleBdd D).subtype)
        = P.deg

theorem

finrank_adeleBdd_quotient

L582 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.finrank_adeleBdd_quotient

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBdd_quotient [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    Module.Finite K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype) ∧
      (finrank K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype) : ℤ)
        = Divisor.degree D₂ - Divisor.degree D₁

theorem

module_finite_adeleBdd_quotient

L643 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.module_finite_adeleBdd_quotient

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem module_finite_adeleBdd_quotient [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    Module.Finite K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype)

theorem

finrank_adeleBdd_quotient_eq

L647 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.finrank_adeleBdd_quotient_eq

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBdd_quotient_eq [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    (finrank K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype) : ℤ)
      = Divisor.degree D₂ - Divisor.degree D₁

def

lSpaceQuotientToAdeleBddQuotient

L653 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.lSpaceQuotientToAdeleBddQuotient

Documentation

The map between divisor-bounded quotients induced by the diagonal embedding into adeles.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def lSpaceQuotientToAdeleBddQuotient {D₁ D₂ : Divisor K F} (_hD : D₁ ≤ D₂) :
    (LSpace D₂ ⧸ (LSpace D₁).comap (LSpace D₂).subtype)
      →ₗ[K] (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype)

theorem

lSpaceQuotientToAdeleBddQuotient_injective

L664 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.lSpaceQuotientToAdeleBddQuotient_injective

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpaceQuotientToAdeleBddQuotient_injective {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    Function.Injective (lSpaceQuotientToAdeleBddQuotient hD)

theorem

ell_sub_ell_le_degree_sub_degree

L677 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.ell_sub_ell_le_degree_sub_degree

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_sub_ell_le_degree_sub_degree [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂)
    [FiniteDimensional K (LSpace D₂)] :
    (ell D₂ : ℤ) - (ell D₁ : ℤ) ≤ Divisor.degree D₂ - Divisor.degree D₁

theorem

adeleBdd_inf_sup_globalSub

L696 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.adeleBdd_inf_sup_globalSub

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBdd_inf_sup_globalSub {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    adeleBdd D₂ ⊓ (adeleBdd D₁ ⊔ globalSub K F)
      = adeleBdd D₁ ⊔ adeleBdd D₂ ⊓ globalSub K F

theorem

map_diagonal_lSpace_inf_adeleBdd

L701 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.map_diagonal_lSpace_inf_adeleBdd

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem map_diagonal_lSpace_inf_adeleBdd {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    (LSpace D₂).map (diagonalHom K F) ⊓ adeleBdd D₁ = (LSpace D₁).map (diagonalHom K F)

theorem

gate_finrank_adeleBdd_quotient_single_point

L706 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_finrank_adeleBdd_quotient_single_point

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_finrank_adeleBdd_quotient_single_point [IsCurveOver K F] (P : Place K F) :
    (finrank K (adeleBdd (Finsupp.single P 1 : Divisor K F)
        ⧸ (adeleBdd (0 : Divisor K F)).comap (adeleBdd (Finsupp.single P 1)).subtype) : ℤ)
      = (P.deg : ℤ)

theorem

comap_subtype_sup_of_le_of_le

L730 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.Submodule.comap_subtype_sup_of_le_of_le

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem comap_subtype_sup_of_le_of_le {S T C : Submodule K X} (hS : S ≤ C) (hT : T ≤ C) :
    S.comap C.subtype ⊔ T.comap C.subtype = (S ⊔ T).comap C.subtype

theorem

finrank_quotient_chain_top

L737 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.Submodule.finrank_quotient_chain_top

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem finrank_quotient_chain_top {M : Type*} [AddCommGroup M] [Module K M]
    {A B : Submodule K M} (hAB : A ≤ B)
    [hMB : Module.Finite K (M ⧸ B)] [hBA : Module.Finite K (B ⧸ A.comap B.subtype)] :
    Module.Finite K (M ⧸ A) ∧
      finrank K (M ⧸ A) = finrank K (M ⧸ B) + finrank K (B ⧸ A.comap B.subtype)

theorem

globalSub_le_adeleSpace

L768 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.globalSub_le_adeleSpace

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem globalSub_le_adeleSpace [HasPrincipalDivisors K F] :
    globalSub K F ≤ adeleSpace K F

theorem

adeleBdd_sup_globalSub_le_adeleSpace

L773 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.adeleBdd_sup_globalSub_le_adeleSpace

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBdd_sup_globalSub_le_adeleSpace [HasPrincipalDivisors K F] (D : Divisor K F) :
    adeleBdd D ⊔ globalSub K F ≤ adeleSpace K F

theorem

adeleBddPrincipal_eq_comap

L777 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.adeleBddPrincipal_eq_comap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBddPrincipal_eq_comap [HasPrincipalDivisors K F] (D : Divisor K F) :
    adeleBddPrincipal K F D = (adeleBdd D ⊔ globalSub K F).comap (adeleSpace K F).subtype

theorem

adeleBddPrincipal_mono

L781 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.adeleBddPrincipal_mono

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBddPrincipal_mono {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    adeleBddPrincipal K F D₁ ≤ adeleBddPrincipal K F D₂

theorem

finiteDimensional_lSpace

L790 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.finiteDimensional_lSpace

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section FiniteLSpace
variable [IsCurveOver K F] [Nonempty (Place K F)]
omit [Nonempty (Place K F)] in

Lean source · statement

theorem finiteDimensional_lSpace [hL0 : FiniteDimensional K (LSpace (0 : Divisor K F))]
    (D : Divisor K F) : FiniteDimensional K (LSpace D)

theorem

range_lSpaceQuotientToAdeleBddQuotient

L810 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.range_lSpaceQuotientToAdeleBddQuotient

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem range_lSpaceQuotientToAdeleBddQuotient {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    LinearMap.range (lSpaceQuotientToAdeleBddQuotient hD)
      = ((adeleBdd D₁ ⊔ globalSub K F).comap (adeleBdd D₂).subtype).map
          ((adeleBdd D₁).comap (adeleBdd D₂).subtype).mkQ

theorem

finrank_adeleBddSup_quotient

L851 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.finrank_adeleBddSup_quotient

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBddSup_quotient [IsCurveOver K F] [Nonempty (Place K F)]
    {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) [hL : FiniteDimensional K (LSpace D₂)] :
    Module.Finite K (↥(adeleBdd D₂ ⊔ globalSub K F)
        ⧸ (adeleBdd D₁ ⊔ globalSub K F).comap (adeleBdd D₂ ⊔ globalSub K F).subtype) ∧
      (finrank K (↥(adeleBdd D₂ ⊔ globalSub K F)
          ⧸ (adeleBdd D₁ ⊔ globalSub K F).comap (adeleBdd D₂ ⊔ globalSub K F).subtype) : ℤ)
        = (Divisor.degree D₂ - ell D₂) - (Divisor.degree D₁ - ell D₁)

theorem

adeleBddSup_eq_of_degree_sub_ell_eq

L922 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.adeleBddSup_eq_of_degree_sub_ell_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Index
variable [IsCurveOver K F] [Nonempty (Place K F)]

Lean source · statement

theorem adeleBddSup_eq_of_degree_sub_ell_eq {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂)
    [FiniteDimensional K (LSpace D₂)]
    (heq : Divisor.degree D₂ - ell D₂ = Divisor.degree D₁ - ell D₁) :
    adeleBdd D₂ ⊔ globalSub K F = adeleBdd D₁ ⊔ globalSub K F

theorem

eq_of_ge

L950 ↗

AlgebraicCurve.RiemannGenusReachedAt.eq_of_ge

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace RiemannGenusReachedAt
open scoped _root_.AlgebraicCurve.RiemannGenusReachedAt in

Lean source · statement

theorem _root_.AlgebraicCurve.RiemannGenusReachedAt.eq_of_ge [IsCurveOver K F] [Nonempty
  (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    {D : Divisor K F} (hD : D₀ ≤ D) :
    Divisor.degree D - ell D = γ - 1

theorem

adeleSpace_eq_of_genusReached

L965 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.adeleSpace_eq_of_genusReached

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem adeleSpace_eq_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    adeleSpace K F = adeleBdd D₀ ⊔ globalSub K F

theorem

indexOfSpecialty_eq_zero_of_genusReached

L981 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.indexOfSpecialty_eq_zero_of_genusReached

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem indexOfSpecialty_eq_zero_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    indexOfSpecialty D₀ = 0

theorem

indexOfSpecialty_eq_of_genusReached

L992 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.indexOfSpecialty_eq_of_genusReached

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem indexOfSpecialty_eq_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) (D : Divisor K F) :
    Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D) ∧
      (indexOfSpecialty D : ℤ) = (ell D : ℤ) - (Divisor.degree D + 1 - γ)

theorem

gate_indexOfSpecialty_at_witness

L1039 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_indexOfSpecialty_at_witness

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_indexOfSpecialty_at_witness [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    (indexOfSpecialty D₀ : ℤ) = 0

theorem

gate_riemannInequality_of_genusReached

L1048 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_riemannInequality_of_genusReached

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_riemannInequality_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) (D : Divisor K F) :
    Divisor.degree D + 1 - γ ≤ (ell D : ℤ)

theorem

adeleSpaceMul_add

L1071 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.adeleSpaceMul_add

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleSpaceMul_add [HasPrincipalDivisors K F] (f g : F) :
    adeleSpaceMul K F (f + g) = adeleSpaceMul K F f + adeleSpaceMul K F g

theorem

adeleSpaceMul_zero

L1077 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.adeleSpaceMul_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleSpaceMul_zero [HasPrincipalDivisors K F] :
    adeleSpaceMul K F (0 : F) = 0

theorem

weilSmul_add_left

L1083 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.weilSmul_add_left

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_add_left [HasPrincipalDivisors K F] (f g : F)
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (f + g) φ = weilSmul K F f φ + weilSmul K F g φ

theorem

weilSmul_zero_left

L1089 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.weilSmul_zero_left

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_zero_left [HasPrincipalDivisors K F]
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (0 : F) φ = 0

theorem

weilSmul_neg_left

L1095 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.weilSmul_neg_left

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_neg_left [HasPrincipalDivisors K F] (f : F)
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (-f) φ = -weilSmul K F f φ

theorem

weilSmul_sub_left

L1102 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.weilSmul_sub_left

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_sub_left [HasPrincipalDivisors K F] (f g : F)
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (f - g) φ = weilSmul K F f φ - weilSmul K F g φ

theorem

weilSmul_eq_zero_iff_left

L1107 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.weilSmul_eq_zero_iff_left

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_eq_zero_iff_left [HasPrincipalDivisors K F]
    {f : F} {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ≠ 0) :
    weilSmul K F f φ = 0 ↔ f = 0

theorem

weilSmul_left_injective

L1114 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.weilSmul_left_injective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem weilSmul_left_injective [HasPrincipalDivisors K F]
    {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ≠ 0) :
    Function.Injective (fun f : F => weilSmul K F f φ) := by
  intro f g hfg
  have hsub : weilSmul K F (f - g) φ = 0 := by
    rw [weilSmul_sub_left, sub_eq_zero]; exact hfg
  exact sub_eq_zero.mp ((weilSmul_eq_zero_iff_left hφ).mp hsub)

def

doubleResiduePairing

L1124 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.doubleResiduePairing

Documentation

The sum of the two residue pairings on the product of their spaces of sections.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

def doubleResiduePairing [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W) :
    LSpace (W - D) × LSpace (W - D) →ₗ[K] omegaSpace D

theorem

doubleResiduePairing_apply_coe

L1130 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.doubleResiduePairing_apply_coe

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem doubleResiduePairing_apply_coe [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W) (g h : LSpace (W - D)) :
    (doubleResiduePairing K F W D hφ hμ (g, h) : Module.Dual K (adeleSpace K F))
      = weilSmul K F (g : F) φ + weilSmul K F (h : F) μ

theorem

doubleResiduePairing_injective

L1138 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.doubleResiduePairing_injective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem doubleResiduePairing_injective [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W)
    (hφ0 : φ ≠ 0) (hindep : ∀ f : F, μ ≠ weilSmul K F f φ) :
    Function.Injective (doubleResiduePairing K F W D hφ hμ)

theorem

two_mul_ell_le_indexOfSpecialty

L1165 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.two_mul_ell_le_indexOfSpecialty

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem two_mul_ell_le_indexOfSpecialty [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W)
    (hφ0 : φ ≠ 0) (hindep : ∀ f : F, μ ≠ weilSmul K F f φ)
    [Module.Finite K (omegaSpace (K := K) (F := F) D)]
    [Module.Finite K (LSpace (K := K) (F := F) (W - D))] :
    2 * ell (W - D) ≤ indexOfSpecialty D

theorem

omegaSpace_finite_of_genusReached

L1198 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.omegaSpace_finite_of_genusReached

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Finiteness
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]

Lean source · statement

theorem omegaSpace_finite_of_genusReached
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) (D : Divisor K F) :
    Module.Finite K (omegaSpace (K := K) (F := F) D)

theorem

exists_weilSmul_eq_of_genusReached

L1212 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.exists_weilSmul_eq_of_genusReached

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ParametricRankOne
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]

Lean source · statement

theorem exists_weilSmul_eq_of_genusReached
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    {φ μ : Module.Dual K (adeleSpace K F)} {W : Divisor K F}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W) (hφ0 : φ ≠ 0) :
    ∃ f : F, μ = weilSmul K F f φ

theorem

weilDifferentialRankOne_of_genusReached

L1248 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.weilDifferentialRankOne_of_genusReached

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ParametricRankOne
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]

Lean source · statement

theorem weilDifferentialRankOne_of_genusReached
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    WeilDifferentialRankOne K F

theorem

residuePairing_surjective_of_rankOne_max

L1261 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.residuePairing_surjective_of_rankOne_max

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem residuePairing_surjective_of_rankOne_max [HasPrincipalDivisors K F]
    (hRankOne : WeilDifferentialRankOne K F)
    {W : Divisor K F} {φ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hφ0 : φ ≠ 0)
    (hWmax : ∀ E : Divisor K F, φ ∈ omegaSpace E → E ≤ W) (D : Divisor K F) :
    Function.Surjective (residuePairing K F W D hφ)

theorem

exists_riemannGenusReachedAt_of_bounded

L1306 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.exists_riemannGenusReachedAt_of_bounded

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_riemannGenusReachedAt_of_bounded
    [IsCurveOver K F] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hbdd : RiemannGenusBounded K F) :
    ∃ (γ : ℤ) (D₀ : Divisor K F), RiemannGenusReachedAt γ D₀

theorem

stichtenothGenusExists_of_bounded

L1323 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.stichtenothGenusExists_of_bounded

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem stichtenothGenusExists_of_bounded
    [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hbdd : RiemannGenusBounded K F) :
    StichtenothGenusExists K F

theorem

indexOfSpecialty_sub_of_ge

L1331 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.indexOfSpecialty_sub_of_ge

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem indexOfSpecialty_sub_of_ge [IsCurveOver K F] [Nonempty (Place K F)]
    {D₀ D : Divisor K F} (hD : D₀ ≤ D)
    [FiniteDimensional K (LSpace D)]
    [hfin : Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D₀)] :
    Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D) ∧
      (Divisor.degree D - ell D) - (Divisor.degree D₀ - ell D₀)
        = (indexOfSpecialty D₀ : ℤ) - (indexOfSpecialty D : ℤ)

theorem

degreeSub_ell_le_of_indexFinite

L1375 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.degreeSub_ell_le_of_indexFinite

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem degreeSub_ell_le_of_indexFinite [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {D₀ : Divisor K F}
    (hfin : Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D₀))
    (D : Divisor K F) :
    Divisor.degree D - ell D ≤ (Divisor.degree D₀ - ell D₀) + indexOfSpecialty D₀

theorem

riemannGenusBounded_of_indexFinite

L1392 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.riemannGenusBounded_of_indexFinite

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem riemannGenusBounded_of_indexFinite [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hfin : IndexOfSpecialtyFinite K F) :
    RiemannGenusBounded K F

theorem

stichtenothGenusExists_of_indexFinite

L1400 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.stichtenothGenusExists_of_indexFinite

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem stichtenothGenusExists_of_indexFinite
    [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hfin : IndexOfSpecialtyFinite K F) :
    StichtenothGenusExists K F

theorem

indexOfSpecialtyFinite_of_stichtenothGenusExists

L1407 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.indexOfSpecialtyFinite_of_stichtenothGenusExists

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem indexOfSpecialtyFinite_of_stichtenothGenusExists
    [IsCurveOver K F] (hSG : StichtenothGenusExists K F) :
    IndexOfSpecialtyFinite K F

theorem

stichtenothGenusExists_iff_indexFinite

L1421 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.stichtenothGenusExists_iff_indexFinite

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem stichtenothGenusExists_iff_indexFinite
    [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))] :
    StichtenothGenusExists K F ↔ IndexOfSpecialtyFinite K F

theorem

gate_indexOfSpecialty_engine_at_witness

L1428 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_indexOfSpecialty_engine_at_witness

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_indexOfSpecialty_engine_at_witness [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    (indexOfSpecialty D₀ : ℤ) = 0

theorem

gate_stichtenothGenus_le_of_indexFinite

L1434 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_stichtenothGenus_le_of_indexFinite

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_stichtenothGenus_le_of_indexFinite [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {D₀ : Divisor K F}
    (hfin : Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D₀))
    {γ : ℤ} {D₁ : Divisor K F} (h : RiemannGenusReachedAt γ D₁) :
    γ - 1 ≤ (Divisor.degree D₀ - ell D₀) + indexOfSpecialty D₀

theorem

gate_riemannGenusBounded_of_reachedAt

L1443 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_riemannGenusBounded_of_reachedAt

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_riemannGenusBounded_of_reachedAt
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    RiemannGenusBounded K F

theorem

gate_indexOfSpecialtyFinite_at_zero

L1448 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_indexOfSpecialtyFinite_at_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_indexOfSpecialtyFinite_at_zero [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F (0 : Divisor K F))

theorem

mul_mem_lSpace_add

L1469 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.mul_mem_lSpace_add

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mul_mem_lSpace_add {D E : Divisor K F} {f g : F}
    (hf : f ∈ LSpace D) (hg : g ∈ LSpace E) :
    f * g ∈ LSpace (D + E)

theorem

pow_mem_lSpace_nsmul

L1482 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.pow_mem_lSpace_nsmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem pow_mem_lSpace_nsmul {B : Divisor K F} {f : F} (hf : f ∈ LSpace B) (j : ℕ) :
    f ^ j ∈ LSpace (j • B)

theorem

pow_mul_u_mem_lSpace

L1496 ↗

AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace (j : ℕ) (i : Fin
  P.n) :
    P.x ^ j * P.u i ∈ LSpace ((j + P.c) • P.B)

theorem

pow_mul_u_mem_lSpace_of_le

L1504 ↗

AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace_of_le

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)
open _root_.AlgebraicCurve.PoleDivisorPackage

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace_of_le {j m : ℕ} (hjm
  : j + P.c ≤ m) (i : Fin P.n) :
    P.x ^ j * P.u i ∈ LSpace (m • P.B)

theorem

ell_nsmul_poleDivisor_ge

L1516 ↗

AlgebraicCurve.PoleDivisorPackage.ell_nsmul_poleDivisor_ge

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.ell_nsmul_poleDivisor_ge [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))] {m : ℕ} (hm : P.c ≤ m) :
    (P.n : ℤ) * (m - P.c + 1) ≤ ell (m • P.B)

theorem

degree_nsmul_sub_ell_le

L1544 ↗

AlgebraicCurve.PoleDivisorPackage.degree_nsmul_sub_ell_le

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.degree_nsmul_sub_ell_le [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))] {m : ℕ} (hm : P.c ≤ m) :
    Divisor.degree (m • P.B) - ell (m • P.B) ≤ (P.n : ℤ) * (P.c - 1)

theorem

ell_nsmul_sub_pos

L1561 ↗

AlgebraicCurve.PoleDivisorPackage.ell_nsmul_sub_pos

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace PoleDivisorPackage
open scoped _root_.AlgebraicCurve.PoleDivisorPackage in

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.ell_nsmul_sub_pos [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) {A : Divisor K F} (hA : 0 ≤ A) {m : ℕ} (hm : P.c ≤ m)
    (hbig : Divisor.degree A < (P.n : ℤ) * (m - P.c + 1)) :
    0 < ell (m • P.B - A)

theorem

degree_sub_ell_le

L1582 ↗

AlgebraicCurve.PoleDivisorPackage.degree_sub_ell_le

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
namespace PoleDivisorPackage
open scoped _root_.AlgebraicCurve.PoleDivisorPackage in

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.degree_sub_ell_le [IsCurveOver K F]
  [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) (D : Divisor K F) :
    Divisor.degree D - ell D ≤ (P.n : ℤ) * (P.c - 1)

theorem

riemannGenusBounded_of_poleDivisorPackage

L1631 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.riemannGenusBounded_of_poleDivisorPackage

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem riemannGenusBounded_of_poleDivisorPackage [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) :
    RiemannGenusBounded K F

theorem

stichtenothGenusExists_of_poleDivisorPackage

L1637 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.stichtenothGenusExists_of_poleDivisorPackage

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem stichtenothGenusExists_of_poleDivisorPackage [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) :
    StichtenothGenusExists K F

theorem

indexOfSpecialtyFinite_of_poleDivisorPackage

L1643 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.indexOfSpecialtyFinite_of_poleDivisorPackage

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem indexOfSpecialtyFinite_of_poleDivisorPackage [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) :
    IndexOfSpecialtyFinite K F

theorem

indexOfSpecialtyFinite_of_hasPoleDivisorPackage

L1650 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.indexOfSpecialtyFinite_of_hasPoleDivisorPackage

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem indexOfSpecialtyFinite_of_hasPoleDivisorPackage [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (h : HasPoleDivisorPackage K F) :
    IndexOfSpecialtyFinite K F

theorem

stichtenothGenusExists_of_hasPoleDivisorPackage

L1656 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.stichtenothGenusExists_of_hasPoleDivisorPackage

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem stichtenothGenusExists_of_hasPoleDivisorPackage [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (h : HasPoleDivisorPackage K F) :
    StichtenothGenusExists K F

theorem

gate_stichtenothGenus_le_of_poleDivisorPackage

L1662 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_stichtenothGenus_le_of_poleDivisorPackage

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_stichtenothGenus_le_of_poleDivisorPackage [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F)
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    γ ≤ (P.n : ℤ) * (P.c - 1) + 1

theorem

gate_ell_c_nsmul_ge

L1670 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_ell_c_nsmul_ge

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_ell_c_nsmul_ge [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) :
    (P.n : ℤ) ≤ ell (P.c • P.B)

theorem

gate_x_transcendental_of_poleDivisorPackage

L1678 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_x_transcendental_of_poleDivisorPackage

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · full declaration

theorem gate_x_transcendental_of_poleDivisorPackage (P : PoleDivisorPackage K F) :
    LinearIndependent K (fun j : ℕ => P.x ^ j * P.u ⟨0, P.hn_pos⟩) := by
  refine P.lin_indep.comp (fun j => (j, ⟨0, P.hn_pos⟩)) ?_
  intro a b hab
  exact (Prod.mk.injEq .. ▸ hab).1

theorem

gate_u_linearIndependent_of_poleDivisorPackage

L1684 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_u_linearIndependent_of_poleDivisorPackage

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_u_linearIndependent_of_poleDivisorPackage (P : PoleDivisorPackage K F) :
    LinearIndependent K P.u

instance

instSumRamificationInertia_port

L1701 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.instSumRamificationInertia_port

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg

Lean source · statement

instance instSumRamificationInertia_port {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F']
    [Algebra F F'] [IsScalarTower K F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    [HasPrincipalDivisors K F'] : SumRamificationInertia K F F'

theorem

x_ne_zero

L1728 ↗

AlgebraicCurve.TranscendenceTower.x_ne_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.x_ne_zero : T.x ≠ 0

theorem

xF_ne_zero

L1733 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.TranscendenceTower.xF_ne_zero

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] in

Lean source · statement

theorem xF_ne_zero : T.xF ≠ 0

theorem

poleDivisor_apply

L1736 ↗

AlgebraicCurve.TranscendenceTower.poleDivisor_apply

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.poleDivisor_apply (w : Place K F) :
    T.poleDivisor w = (w.ramificationIndex E : ℤ) * (Finsupp.single T.v 1) (w.restrict E)

theorem

poleDivisor_nonneg

L1742 ↗

AlgebraicCurve.TranscendenceTower.poleDivisor_nonneg

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.poleDivisor_nonneg : 0 ≤ T.poleDivisor

theorem

xF_mem_lSpace_poleDivisor

L1752 ↗

AlgebraicCurve.TranscendenceTower.xF_mem_lSpace_poleDivisor

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.xF_mem_lSpace_poleDivisor : T.xF ∈ LSpace
  T.poleDivisor

theorem

degree_poleDivisor_eq_finrank

L1765 ↗

AlgebraicCurve.TranscendenceTower.degree_poleDivisor_eq_finrank

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.degree_poleDivisor_eq_finrank :
    Divisor.degree T.poleDivisor = (Module.finrank E F : ℤ)

theorem

mem_lSpace_nsmul_poleDivisor_of_regular_outside

L1772 ↗

AlgebraicCurve.TranscendenceTower.mem_lSpace_nsmul_poleDivisor_of_regular_outside

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] in

Lean source · statement

theorem
  _root_.AlgebraicCurve.TranscendenceTower.mem_lSpace_nsmul_poleDivisor_of_regular_outside {f : F}
    (hreg : ∀ w : Place K F, w.restrict E ≠ T.v → 0 ≤ w.ord f)
    {c : ℕ} (hc : ∀ w ∈ T.v.fiber F, -(c : ℤ) ≤ w.ord f) :
    f ∈ LSpace (c • T.poleDivisor)

theorem

exists_forall_mem_lSpace_nsmul_poleDivisor

L1794 ↗

AlgebraicCurve.TranscendenceTower.exists_forall_mem_lSpace_nsmul_poleDivisor

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] in

Lean source · statement

theorem
  _root_.AlgebraicCurve.TranscendenceTower.exists_forall_mem_lSpace_nsmul_poleDivisor {n : ℕ} (u :
  Fin n → F)
    (hreg : ∀ i, ∀ w : Place K F, w.restrict E ≠ T.v → 0 ≤ w.ord (u i)) :
    ∃ c : ℕ, ∀ i, u i ∈ LSpace (c • T.poleDivisor)

def

ofRegularOutside

L1828 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.IntegralBasisInLSpace.ofRegularOutside

Documentation

The integral-basis package built from a basis regular away from the tower place.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section PrincipalDivisors
variable [HasPrincipalDivisors K F]
open scoped _root_.AlgebraicCurve.IntegralBasisInLSpace in

Lean source · full declaration

def IntegralBasisInLSpace.ofRegularOutside (T : TranscendenceTower K E F)
    (u : Fin (Module.finrank E F) → F) (hu_indep : LinearIndependent E u)
    (hreg : ∀ i, ∀ w : Place K F, w.restrict E ≠ T.v → 0 ≤ w.ord (u i)) :
    IntegralBasisInLSpace T where
  c := (T.exists_forall_mem_lSpace_nsmul_poleDivisor u hreg).choose
  u := u
  hu_indep := hu_indep
  hu_mem := (T.exists_forall_mem_lSpace_nsmul_poleDivisor u hreg).choose_spec

theorem

hasIntegralBasisInLSpace_of_regularOutside

L1837 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.hasIntegralBasisInLSpace_of_regularOutside

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section PrincipalDivisors
variable [HasPrincipalDivisors K F]
omit [FiniteDimensional E F] in

Lean source · statement

theorem hasIntegralBasisInLSpace_of_regularOutside (T : TranscendenceTower K E F)
    (h : HasIntegralBasisRegularOutside K E F T) :
    HasIntegralBasisInLSpace K E F T

theorem

linearIndependent_pow_mul

L1843 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.linearIndependent_pow_mul

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section PrincipalDivisors
variable [HasPrincipalDivisors K F]
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] in

Lean source · full declaration

theorem linearIndependent_pow_mul {x : E} {n : ℕ} {u : Fin n → F}
    (hx : LinearIndependent K (fun j : ℕ => x ^ j)) (hu : LinearIndependent E u) :
    LinearIndependent K (fun p : ℕ × Fin n => (algebraMap E F x) ^ p.1 * u p.2) := by
  have heq : (fun p : ℕ × Fin n => (algebraMap E F x) ^ p.1 * u p.2)
      = (fun p : ℕ × Fin n => (x ^ p.1) • u p.2) := by
    funext p
    rw [Algebra.smul_def, map_pow]
  rw [heq]
  exact linearIndependent_smul (R := K) (S := E) (A := F) hx hu

def

ofTranscendenceTower

L1855 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.PoleDivisorPackage.ofTranscendenceTower

Documentation

The pole-divisor data obtained from a transcendence tower and its integral basis.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section PrincipalDivisors
variable [HasPrincipalDivisors K F]
open scoped _root_.AlgebraicCurve.PoleDivisorPackage in

Lean source · full declaration

def PoleDivisorPackage.ofTranscendenceTower (T : TranscendenceTower K E F)
    (IB : IntegralBasisInLSpace T) :
    PoleDivisorPackage K F where
  x := T.xF
  B := T.poleDivisor
  hB_eff := T.poleDivisor_nonneg
  hx_mem := T.xF_mem_lSpace_poleDivisor
  n := Module.finrank E F
  hn_pos := Module.finrank_pos
  degB_eq := T.degree_poleDivisor_eq_finrank
  c := IB.c
  u := IB.u
  hu_mem := IB.hu_mem
  lin_indep := linearIndependent_pow_mul T.hx_indep IB.hu_indep

theorem

hasPoleDivisorPackage_of_transcendenceTower

L1870 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.hasPoleDivisorPackage_of_transcendenceTower

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section PrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem hasPoleDivisorPackage_of_transcendenceTower
    (T : TranscendenceTower K E F) (IB : IntegralBasisInLSpace T) :
    HasPoleDivisorPackage K F

theorem

hasPoleDivisorPackage_of_hasIntegralBasisInLSpace

L1875 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.hasPoleDivisorPackage_of_hasIntegralBasisInLSpace

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section PrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem hasPoleDivisorPackage_of_hasIntegralBasisInLSpace
    (T : TranscendenceTower K E F) (h : HasIntegralBasisInLSpace K E F T) :
    HasPoleDivisorPackage K F

theorem

hasPoleDivisorPackage_of_hasIntegralBasisRegularOutside

L1880 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.hasPoleDivisorPackage_of_hasIntegralBasisRegularOutside

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section PrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem hasPoleDivisorPackage_of_hasIntegralBasisRegularOutside
    (T : TranscendenceTower K E F) (h : HasIntegralBasisRegularOutside K E F T) :
    HasPoleDivisorPackage K F

theorem

indexOfSpecialtyFinite_of_transcendenceTower

L1888 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.indexOfSpecialtyFinite_of_transcendenceTower

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]

Lean source · statement

theorem indexOfSpecialtyFinite_of_transcendenceTower [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (T : TranscendenceTower K E F) (IB : IntegralBasisInLSpace T) :
    IndexOfSpecialtyFinite K F

theorem

stichtenothGenusExists_of_transcendenceTower

L1895 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.stichtenothGenusExists_of_transcendenceTower

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]

Lean source · statement

theorem stichtenothGenusExists_of_transcendenceTower [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (T : TranscendenceTower K E F) (IB : IntegralBasisInLSpace T) :
    StichtenothGenusExists K F

theorem

gate_ofTranscendenceTower_n_eq

L1905 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_ofTranscendenceTower_n_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section PrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem gate_ofTranscendenceTower_n_eq (T : TranscendenceTower K E F)
    (IB : IntegralBasisInLSpace T) :
    (PoleDivisorPackage.ofTranscendenceTower T IB).n = Module.finrank E F

theorem

gate_ofTranscendenceTower_B_eq

L1909 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_ofTranscendenceTower_B_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section PrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem gate_ofTranscendenceTower_B_eq (T : TranscendenceTower K E F)
    (IB : IntegralBasisInLSpace T) :
    (PoleDivisorPackage.ofTranscendenceTower T IB).B = T.poleDivisor

theorem

gate_ofTranscendenceTower_x_transcendental

L1913 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_ofTranscendenceTower_x_transcendental

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section PrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · full declaration

theorem gate_ofTranscendenceTower_x_transcendental (T : TranscendenceTower K E F)
    (IB : IntegralBasisInLSpace T) :
    LinearIndependent K
      (fun j : ℕ => T.xF ^ j *
        (PoleDivisorPackage.ofTranscendenceTower T IB).u ⟨0, Module.finrank_pos⟩) :=
  gate_x_transcendental_of_poleDivisorPackage
    (PoleDivisorPackage.ofTranscendenceTower T IB)

theorem

gate_degree_pullback_single_of_deg_eq

L1921 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_degree_pullback_single_of_deg_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section PrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem gate_degree_pullback_single_of_deg_eq (v : Place K E) (d : ℕ) (hd : v.deg = d) :
    Divisor.degree (Divisor.pullback F (Finsupp.single v (1 : ℤ)))
      = (Module.finrank E F : ℤ) * d

theorem

gate_stichtenothGenus_le_of_transcendenceTower

L1928 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_stichtenothGenus_le_of_transcendenceTower

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]

Lean source · statement

theorem gate_stichtenothGenus_le_of_transcendenceTower [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (T : TranscendenceTower K E F) (IB : IntegralBasisInLSpace T)
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    γ ≤ (Module.finrank E F : ℤ) * (IB.c - 1) + 1

theorem

mem_of_isIntegral

L1956 ↗

AlgebraicCurve.Place.mem_of_isIntegral

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
  restrict_placeOfPrime placeOfPrime
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_of_isIntegral {f : F} (hf : IsIntegral
  w.toValuationSubring f) :
    f ∈ w.toValuationSubring

theorem

ord_nonneg_of_isIntegral

L1964 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.Place.ord_nonneg_of_isIntegral

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
  restrict_placeOfPrime placeOfPrime
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem ord_nonneg_of_isIntegral {f : F} (hf : IsIntegral w.toValuationSubring f) :
    0 ≤ w.ord f

theorem

mem_of_isIntegral_of_algebraMap_mem

L1968 ↗

AlgebraicCurve.Place.mem_of_isIntegral_of_algebraMap_mem

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
  restrict_placeOfPrime placeOfPrime
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_of_isIntegral_of_algebraMap_mem {A : Type*}
  [CommRing A] [Algebra A F]
    (hA : ∀ a : A, algebraMap A F a ∈ w.toValuationSubring)
    {f : F} (hf : IsIntegral A f) : f ∈ w.toValuationSubring

theorem

ord_nonneg_of_isIntegral_of_algebraMap_mem

L1980 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.Place.ord_nonneg_of_isIntegral_of_algebraMap_mem

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
  restrict_placeOfPrime placeOfPrime
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem ord_nonneg_of_isIntegral_of_algebraMap_mem {A : Type*} [CommRing A] [Algebra A F]
    (hA : ∀ a : A, algebraMap A F a ∈ w.toValuationSubring)
    {f : F} (hf : IsIntegral A f) : 0 ≤ w.ord f

theorem

mem_of_isIntegral_of_restrict

L1998 ↗

AlgebraicCurve.Place.mem_of_isIntegral_of_restrict

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Bridge
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable {A : Type*} [CommRing A] [Algebra A E] [Algebra A F] [IsScalarTower A E F]
namespace Place
open scoped _root_.AlgebraicCurve.Place in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_of_isIntegral_of_restrict [Algebra.IsIntegral E F]
  (w : Place K F)
    {u : Place K E} (hw : w.restrict E = u)
    (hA : ∀ a : A, algebraMap A E a ∈ u.toValuationSubring)
    {f : F} (hf : IsIntegral A f) : f ∈ w.toValuationSubring

theorem

ord_nonneg_of_isIntegral_of_restrict

L2011 ↗

AlgebraicCurve.Place.ord_nonneg_of_isIntegral_of_restrict

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Bridge
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable {A : Type*} [CommRing A] [Algebra A E] [Algebra A F] [IsScalarTower A E F]
open _root_.AlgebraicCurve
namespace Place
open scoped _root_.AlgebraicCurve.Place in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_isIntegral_of_restrict
  [Algebra.IsIntegral E F] (w : Place K F)
    {u : Place K E} (hw : w.restrict E = u)
    (hA : ∀ a : A, algebraMap A E a ∈ u.toValuationSubring)
    {f : F} (hf : IsIntegral A f) : 0 ≤ w.ord f

theorem

ord_nonneg_of_isIntegral_of_regularOutside

L2025 ↗

AlgebraicCurve.TranscendenceTower.ord_nonneg_of_isIntegral_of_regularOutside

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Bridge
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable {A : Type*} [CommRing A] [Algebra A E] [Algebra A F] [IsScalarTower A E F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace TranscendenceTower
open scoped _root_.AlgebraicCurve.TranscendenceTower in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.ord_nonneg_of_isIntegral_of_regularOutside
    [Algebra.IsIntegral E F] (T : TranscendenceTower K E F) (hA : T.RegularOutside A)
    {f : F} (hf : IsIntegral A f) :
    ∀ w : Place K F, w.restrict E ≠ T.v → 0 ≤ w.ord f

theorem

linearIndependent_reindex_basis

L2042 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.linearIndependent_reindex_basis

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] in

Lean source · full declaration

theorem linearIndependent_reindex_basis {s : Finset F} (b : Basis s E F) :
    LinearIndependent E (fun i : Fin (Module.finrank E F) =>
      b ((Fintype.equivFinOfCardEq (Module.finrank_eq_card_basis b).symm).symm i)) :=
  b.linearIndependent.comp _ (Equiv.injective _)

theorem

hasIntegralBasisRegularOutside_of_isFractionRing

L2047 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.hasIntegralBasisRegularOutside_of_isFractionRing

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem hasIntegralBasisRegularOutside_of_isFractionRing
    {A : Type*} [CommRing A] [IsDomain A] [Algebra A E] [IsFractionRing A E]
    [Algebra A F] [IsScalarTower A E F]
    (T : TranscendenceTower K E F) (hA : T.RegularOutside A) :
    HasIntegralBasisRegularOutside K E F T

theorem

hasIntegralBasisRegularOutside_of_hasRegularFractionSubring

L2058 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.hasIntegralBasisRegularOutside_of_hasRegularFractionSubring

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem hasIntegralBasisRegularOutside_of_hasRegularFractionSubring
    (T : TranscendenceTower K E F) (h : HasRegularFractionSubring K E F T) :
    HasIntegralBasisRegularOutside K E F T

theorem

hasPoleDivisorPackage_of_isFractionRing

L2066 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.hasPoleDivisorPackage_of_isFractionRing

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]

Lean source · statement

theorem hasPoleDivisorPackage_of_isFractionRing
    {A : Type*} [CommRing A] [IsDomain A] [Algebra A E] [IsFractionRing A E]
    [Algebra A F] [IsScalarTower A E F]
    (T : TranscendenceTower K E F) (hA : T.RegularOutside A) :
    HasPoleDivisorPackage K F

theorem

stichtenothGenusExists_of_isFractionRing

L2074 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.stichtenothGenusExists_of_isFractionRing

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem stichtenothGenusExists_of_isFractionRing [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {A : Type*} [CommRing A] [IsDomain A] [Algebra A E] [IsFractionRing A E]
    [Algebra A F] [IsScalarTower A E F]
    (T : TranscendenceTower K E F) (hA : T.RegularOutside A) :
    StichtenothGenusExists K F

theorem

hasPoleDivisorPackage_of_hasRegularFractionSubring

L2083 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.hasPoleDivisorPackage_of_hasRegularFractionSubring

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]

Lean source · statement

theorem hasPoleDivisorPackage_of_hasRegularFractionSubring
    (T : TranscendenceTower K E F) (h : HasRegularFractionSubring K E F T) :
    HasPoleDivisorPackage K F

theorem

stichtenothGenusExists_of_hasRegularFractionSubring

L2089 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.stichtenothGenusExists_of_hasRegularFractionSubring

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem stichtenothGenusExists_of_hasRegularFractionSubring [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (T : TranscendenceTower K E F) (h : HasRegularFractionSubring K E F T) :
    StichtenothGenusExists K F

theorem

adjoin_x_regularOutside

L2099 ↗

AlgebraicCurve.TranscendenceTower.adjoin_x_regularOutside

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
namespace TranscendenceTower
open scoped _root_.AlgebraicCurve.TranscendenceTower in
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.adjoin_x_regularOutside (T :
  TranscendenceTower K E F) :
    ∀ u : Place K E, u ≠ T.v →
      ∀ a ∈ Algebra.adjoin K {T.x}, a ∈ u.toValuationSubring

theorem

hasRegularFractionSubring_of_adjoin_x_isFractionRing

L2118 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.hasRegularFractionSubring_of_adjoin_x_isFractionRing

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] in

Lean source · statement

theorem hasRegularFractionSubring_of_adjoin_x_isFractionRing
    (T : TranscendenceTower K E F)
    (hfrac : IsFractionRing (Algebra.adjoin K {T.x}) E) :
    HasRegularFractionSubring K E F T

theorem

hasIntegralBasisRegularOutside_of_adjoin_x_isFractionRing

L2124 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.hasIntegralBasisRegularOutside_of_adjoin_x_isFractionRing

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem hasIntegralBasisRegularOutside_of_adjoin_x_isFractionRing
    (T : TranscendenceTower K E F)
    (hfrac : IsFractionRing (Algebra.adjoin K {T.x}) E) :
    HasIntegralBasisRegularOutside K E F T

theorem

stichtenothGenusExists_of_adjoin_x_isFractionRing

L2131 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.stichtenothGenusExists_of_adjoin_x_isFractionRing

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem stichtenothGenusExists_of_adjoin_x_isFractionRing [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (T : TranscendenceTower K E F)
    (hfrac : IsFractionRing (Algebra.adjoin K {T.x}) E) :
    StichtenothGenusExists K F

theorem

gate_mem_of_isIntegral_recovers_comap

L2145 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_mem_of_isIntegral_recovers_comap

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_mem_of_isIntegral_recovers_comap (w : Place K F) (E : Type*) [Field E]
    [Algebra E F] [Algebra.IsIntegral E F]
    (hE : ∀ a : E, algebraMap E F a ∈ w.toValuationSubring) (f : F) :
    f ∈ w.toValuationSubring

theorem

gate_bridge_recovers_hxreg

L2157 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_bridge_recovers_hxreg

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]

Lean source · statement

theorem gate_bridge_recovers_hxreg [Algebra.IsIntegral E F]
    (T : TranscendenceTower K E F) (w : Place K F) (hw : w.restrict E ≠ T.v) :
    0 ≤ w.ord T.xF

theorem

gate_regularOutside_mono

L2163 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_regularOutside_mono

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]

Lean source · statement

theorem gate_regularOutside_mono (T : TranscendenceTower K E F) {A A' : Subalgebra K E}
    (hle : A ≤ A')
    (hA' : ∀ u : Place K E, u ≠ T.v → ∀ a ∈ A', a ∈ u.toValuationSubring) :
    ∀ u : Place K E, u ≠ T.v → ∀ a ∈ A, a ∈ u.toValuationSubring

theorem

gate_bot_regularOutside

L2169 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_bot_regularOutside

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]

Lean source · statement

theorem gate_bot_regularOutside (T : TranscendenceTower K E F) :
    ∀ u : Place K E, u ≠ T.v → ∀ a ∈ (⊥ : Subalgebra K E), a ∈ u.toValuationSubring

theorem

gate_adjoin_x_not_regular_at_v

L2175 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.gate_adjoin_x_not_regular_at_v

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]

Lean source · statement

theorem gate_adjoin_x_not_regular_at_v (T : TranscendenceTower K E F) :
    ¬ ∀ a ∈ Algebra.adjoin K {T.x}, a ∈ T.v.toValuationSubring

theorem

linearIndependent_pow_of_transcendental

L2201 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.linearIndependent_pow_of_transcendental

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Transcendental
variable {K A : Type*} [CommRing K] [CommRing A] [Algebra K A]

Lean source · full declaration

theorem linearIndependent_pow_of_transcendental {x : A} (hx : Transcendental K x) :
    LinearIndependent K (fun j : ℕ => x ^ j) := by
  have hinj : Function.Injective (Polynomial.aeval x : K[X] →ₐ[K] A) :=
    transcendental_iff_injective.mp hx
  have hXj : LinearIndependent K (fun j : ℕ => (X : K[X]) ^ j) := by
    have hb := (Polynomial.basisMonomials K).linearIndependent
    simp only [Polynomial.coe_basisMonomials] at hb
    convert hb using 2 with j
    exact (Polynomial.monomial_one_right_eq_X_pow j).symm
  have heq : (fun j : ℕ => x ^ j)
      = (fun j : ℕ => (Polynomial.aeval x : K[X] →ₐ[K] A) (X ^ j)) := by
    funext j; simp
  rw [heq]
  exact hXj.map' (Polynomial.aeval x).toLinearMap
    (LinearMap.ker_eq_bot_of_injective hinj)

theorem

transcendental_of_linearIndependent_pow

L2217 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.transcendental_of_linearIndependent_pow

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Transcendental
variable {K A : Type*} [CommRing K] [CommRing A] [Algebra K A]

Lean source · full declaration

theorem transcendental_of_linearIndependent_pow {x : A}
    (hx : LinearIndependent K (fun j : ℕ => x ^ j)) :
    Transcendental K x := by
  rw [transcendental_iff]
  intro p hp
  rw [Polynomial.aeval_eq_sum_range, ← Fin.sum_univ_eq_sum_range] at hp
  ext j
  rcases lt_or_ge j (p.natDegree + 1) with hj | hj
  · exact (Fintype.linearIndependent_iff.mp
      (hx.comp (Fin.val : Fin (p.natDegree + 1) → ℕ) Fin.val_injective))
      (fun i => p.coeff i) hp ⟨j, hj⟩
  · exact p.coeff_eq_zero_of_natDegree_lt (Nat.lt_of_succ_le hj)

theorem

ord_placeInfty_X

L2238 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.ord_placeInfty_X

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem ord_placeInfty_X : (placeInfty K).ord (RatFunc.X : RatFunc K) = -1

theorem

algebraMap_polynomial_mem_of_ne_placeInfty

L2241 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.algebraMap_polynomial_mem_of_ne_placeInfty

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem algebraMap_polynomial_mem_of_ne_placeInfty
    {u : Place K (RatFunc K)} (hu : u ≠ placeInfty K) (q : K[X]) :
    algebraMap K[X] (RatFunc K) q ∈ u.toValuationSubring

theorem

ord_X_nonneg_of_ne_placeInfty

L2248 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.ord_X_nonneg_of_ne_placeInfty

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem ord_X_nonneg_of_ne_placeInfty
    {u : Place K (RatFunc K)} (hu : u ≠ placeInfty K) :
    0 ≤ u.ord (RatFunc.X : RatFunc K)

def

transcendenceTower

L2258 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.transcendenceTower

Documentation

The rational-function-field tower with the standard variable and the place at infinity.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]

Lean source · full declaration

def transcendenceTower : TranscendenceTower K (RatFunc K) F where
  x := RatFunc.X
  hx_indep := linearIndependent_pow_of_transcendental RatFunc.transcendental_X
  v := placeInfty K
  hvdeg := deg_placeInfty K
  hxv := ord_placeInfty_X K
  hxreg := fun _ hu => ord_X_nonneg_of_ne_placeInfty K hu

theorem

transcendenceTower_x

L2266 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.transcendenceTower_x

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]

Lean source · statement

theorem transcendenceTower_x : (transcendenceTower K F).x = RatFunc.X

theorem

transcendenceTower_v

L2268 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.transcendenceTower_v

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]

Lean source · statement

theorem transcendenceTower_v : (transcendenceTower K F).v = placeInfty K

theorem

aeval_X_eq_algebraMap

L2270 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.aeval_X_eq_algebraMap

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem aeval_X_eq_algebraMap (q : K[X]) :
    (Polynomial.aeval (R := K) (RatFunc.X : RatFunc K)) q
      = algebraMap K[X] (RatFunc K) q

theorem

algebraMap_polynomial_mem_adjoin_X

L2278 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.algebraMap_polynomial_mem_adjoin_X

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem algebraMap_polynomial_mem_adjoin_X (q : K[X]) :
    algebraMap K[X] (RatFunc K) q ∈ Algebra.adjoin K {(RatFunc.X : RatFunc K)}

theorem

isFractionRing_adjoin_X

L2283 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.isFractionRing_adjoin_X

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem isFractionRing_adjoin_X :
    IsFractionRing (Algebra.adjoin K {(RatFunc.X : RatFunc K)}) (RatFunc K)

theorem

hasRegularFractionSubring

L2291 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.hasRegularFractionSubring

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]

Lean source · statement

theorem hasRegularFractionSubring :
    HasRegularFractionSubring K (RatFunc K) F (transcendenceTower K F)

theorem

hasIntegralBasisRegularOutside

L2298 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.hasIntegralBasisRegularOutside

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
variable [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]

Lean source · statement

theorem hasIntegralBasisRegularOutside :
    HasIntegralBasisRegularOutside K (RatFunc K) F (transcendenceTower K F)

theorem

hasPoleDivisorPackage_of_ratFunc_tower

L2306 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.hasPoleDivisorPackage_of_ratFunc_tower

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
variable [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]
variable [HasPrincipalDivisors K F]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem hasPoleDivisorPackage_of_ratFunc_tower :
    HasPoleDivisorPackage K F

theorem

stichtenothGenusExists_of_ratFunc_tower

L2316 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.stichtenothGenusExists_of_ratFunc_tower

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
variable [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]
variable [HasPrincipalDivisors K F]
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]
omit [HasPrincipalDivisors K F] in
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem stichtenothGenusExists_of_ratFunc_tower :
    StichtenothGenusExists K F

theorem

indexOfSpecialtyFinite_of_ratFunc_tower

L2322 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.indexOfSpecialtyFinite_of_ratFunc_tower

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
variable [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]
variable [HasPrincipalDivisors K F]
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]
omit [HasPrincipalDivisors K F] in
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem indexOfSpecialtyFinite_of_ratFunc_tower :
    IndexOfSpecialtyFinite K F

theorem

exists_restrict_eq

L2369 ↗

AlgebraicCurve.RationalFunctionField.exists_restrict_eq

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
section LyingOver
variable [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]
omit [DecidableEq (RatFunc K)] in
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem _root_.AlgebraicCurve.RationalFunctionField.exists_restrict_eq (v : Place K
  (RatFunc K)) :
    ∃ w : Place K F, w.restrict (RatFunc K) = v

theorem

nonempty_place_of_ratFunc_tower

L2377 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.nonempty_place_of_ratFunc_tower

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
section LyingOver
variable [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]
open _root_.AlgebraicCurve.RationalFunctionField
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem nonempty_place_of_ratFunc_tower : Nonempty (Place K F)

theorem

finiteDimensional_lSpace_zero_of_constantsAreBase

L2383 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.finiteDimensional_lSpace_zero_of_constantsAreBase

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
omit [DecidableEq (RatFunc K)] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] in

Lean source · statement

theorem finiteDimensional_lSpace_zero_of_constantsAreBase (hC : ConstantsAreBase K F) :
    FiniteDimensional K (LSpace (0 : Divisor K F))

theorem

stichtenothGenusExists

L2392 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.stichtenothGenusExists

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
variable [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]
variable [IsCurveOver K F]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem stichtenothGenusExists (hC : ConstantsAreBase K F) :
    StichtenothGenusExists K F

theorem

indexOfSpecialtyFinite

L2398 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.indexOfSpecialtyFinite

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
variable [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]
variable [IsCurveOver K F]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem indexOfSpecialtyFinite (hC : ConstantsAreBase K F) :
    IndexOfSpecialtyFinite K F

theorem

riemannGenusBounded

L2402 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.riemannGenusBounded

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module Polynomial IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F]
  [IsScalarTower K (RatFunc K) F]
variable [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]
variable [IsCurveOver K F]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem riemannGenusBounded (hC : ConstantsAreBase K F) : RiemannGenusBounded K F

theorem

finrank_omegaSpace_eq_ell_canonical_sub_of_genusReached

L2444 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.finrank_omegaSpace_eq_ell_canonical_sub_of_genusReached

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Identification
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]
  [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [HasCanonicalLocalResidueKStar K F]

Lean source · statement

theorem finrank_omegaSpace_eq_ell_canonical_sub_of_genusReached
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    (hWK : WeilKaehlerAgree K F) {ω : Ω[F⁄K]} (hω : ω ≠ 0) (D : Divisor K F) :
    Module.finrank K (omegaSpace (K := K) (F := F) D) = ell (canonicalDivisorOf hω - D)

theorem

ell_canonicalDivisor_eq_stichtenothGenus

L2454 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.ell_canonicalDivisor_eq_stichtenothGenus

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Identification
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]
  [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [HasCanonicalLocalResidueKStar K F]

Lean source · statement

theorem ell_canonicalDivisor_eq_stichtenothGenus
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    (hWK : WeilKaehlerAgree K F) (hC : ConstantsAreBase K F)
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) :
    (ell (canonicalDivisorOf hω) : ℤ) = γ

theorem

degree_canonicalDivisor_eq_of_genusReached

L2466 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.degree_canonicalDivisor_eq_of_genusReached

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Identification
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]
  [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [HasCanonicalLocalResidueKStar K F]

Lean source · statement

theorem degree_canonicalDivisor_eq_of_genusReached
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    (hWK : WeilKaehlerAgree K F) (hC : ConstantsAreBase K F)
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) :
    Divisor.degree (canonicalDivisorOf hω) = 2 * γ - 2

theorem

stichtenothGenus_nonneg

L2481 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.stichtenothGenus_nonneg

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Identification
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]
  [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [HasCanonicalLocalResidueKStar K F]
omit [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [HasCanonicalLocalResidueKStar K F] in

Lean source · statement

theorem stichtenothGenus_nonneg
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    (hC : ConstantsAreBase K F) : 0 ≤ γ

theorem

genus_eq_degree_div

L2490 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.genus_eq_degree_div

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Identification
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]
  [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [HasCanonicalLocalResidueKStar K F]
omit [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
  [∀ v : Place K F, v.DCoordGenerates] [HasCanonicalLocalResidueKStar K F] in

Lean source · statement

theorem genus_eq_degree_div :
    ∃ (ω₀ : Ω[F⁄K]) (hω₀ : ω₀ ≠ 0),
      genus K F = (Divisor.degree (canonicalDivisorOf hω₀) + 2).toNat / 2

theorem

stichtenothGenus_eq_genus

L2497 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.stichtenothGenus_eq_genus

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Identification
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]
  [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [HasCanonicalLocalResidueKStar K F]

Lean source · statement

theorem stichtenothGenus_eq_genus
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    (hWK : WeilKaehlerAgree K F) (hC : ConstantsAreBase K F) :
    γ = (genus K F : ℤ)

theorem

riemannGenusReached_of_stichtenothGenusExists_port

L2511 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.riemannGenusReached_of_stichtenothGenusExists_port

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem riemannGenusReached_of_stichtenothGenusExists_port
    [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)]
    [∀ v : Place K F, v.DCoordGenerates] [HasCanonicalLocalResidueKStar K F]
    (hSG : StichtenothGenusExists K F)
    (hWK : WeilKaehlerAgree K F) (hC : ConstantsAreBase K F) :
    RiemannGenusReached K F (genus K F)

theorem

indexOfSpecialty_eq_of_stichtenothGenusExists

L2522 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.indexOfSpecialty_eq_of_stichtenothGenusExists

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem indexOfSpecialty_eq_of_stichtenothGenusExists
    [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)]
    [∀ v : Place K F, v.DCoordGenerates] [HasCanonicalLocalResidueKStar K F]
    (hSG : StichtenothGenusExists K F)
    (hWK : WeilKaehlerAgree K F) (hC : ConstantsAreBase K F) (D : Divisor K F) :
    (indexOfSpecialty D : ℤ) = (ell D : ℤ) - (Divisor.degree D + 1 - (genus K F : ℤ))

theorem

riemannIndexFormula_of_genusReached

L2546 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.riemannIndexFormula_of_genusReached

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem riemannIndexFormula_of_genusReached
    (hg : ∀ [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)],
      RiemannGenusReached K F (genus K F)) :
    RiemannIndexFormula K F

theorem

riemannGenusReached

L2577 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.riemannGenusReached

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
variable [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]
variable [IsCurveOver K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [HasCanonicalLocalResidueKStar K F]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem riemannGenusReached (hWK : WeilKaehlerAgree K F) (hC : ConstantsAreBase K F) :
    RiemannGenusReached K F (genus K F)

theorem

indexOfSpecialty_eq

L2581 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth.AlgebraicCurve.RationalFunctionField.indexOfSpecialty_eq

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
noncomputable section
open Module IsDedekindDomain WithZero KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
variable (F : Type*) [Field F] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
variable [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]
variable [IsCurveOver K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [HasCanonicalLocalResidueKStar K F]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem indexOfSpecialty_eq (hWK : WeilKaehlerAgree K F) (hC : ConstantsAreBase K F)
    (D : Divisor K F) :
    (indexOfSpecialty D : ℤ) = (ell D : ℤ) - (Divisor.degree D + 1 - (genus K F : ℤ))

theorem

riemannGenusReached_of_stichtenothGenusExists

L2599 ↗

AlgebraicCurve.riemannGenusReached_of_stichtenothGenusExists

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RiemannGenusReachedStichtenoth
open Polynomial IsLocalRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs in
open _root_.AlgebraicCurve hiding
  Place.ord_nonneg_of_mem
  Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg in
open RiemannGenusReachedStichtenoth.AlgebraicCurve in
open KaehlerDifferential in

Lean source · statement

theorem _root_.AlgebraicCurve.riemannGenusReached_of_stichtenothGenusExists {K : Type*} {F :
  Type*} [Field K] [Field F] [Algebra K F]
    [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)]
    [∀ v : Place K F, v.DCoordGenerates] [HasCanonicalLocalResidueKStar K F]
    (hSG : StichtenothGenusExists K F)
    (hWK : WeilKaehlerAgree K F) (hC : ConstantsAreBase K F) :
    RiemannGenusReached K F (genus K F)

Module documentation

Riemann Genus Reached of stichtenoth Genus Exists

Declarations