Module

Repartitions.lean

Nyll.AlgebraicCurves.Cohomology.Adelic.Repartitions

19 declarations indexed from sourceView source ↗

Module documentation

Repartitions and Riemann--Roch spaces defined by valuation bounds. Principal repartitions give the quotient used for the first cohomology space.

Imports1

Nyll.AlgebraicCurves.Divisors.ClassGroup

Imported by192

theorem

adicValuation_le_one_of_mem

L30 ↗

AlgebraicCurve.Place.adicValuation_le_one_of_mem

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem adicValuation_le_one_of_mem {x : F} (hx : x ∈ v.toValuationSubring) :
    v.adicValuation x ≤ 1

theorem

adicValuation_algebraMap_le_one

L36 ↗

AlgebraicCurve.Place.adicValuation_algebraMap_le_one

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem adicValuation_algebraMap_le_one (a : K) :
    v.adicValuation (algebraMap K F a) ≤ 1

theorem

adicValuation_eq_exp_neg_ord

L40 ↗

AlgebraicCurve.Place.adicValuation_eq_exp_neg_ord

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem adicValuation_eq_exp_neg_ord {f : F} (hf : f ≠ 0) :
    v.adicValuation f = exp (-v.ord f)

theorem

adicValuation_le_exp_iff

L45 ↗

AlgebraicCurve.Place.adicValuation_le_exp_iff

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem adicValuation_le_exp_iff {f : F} {n : ℤ} :
    v.adicValuation f ≤ exp n ↔ f = 0 ∨ -n ≤ v.ord f

theorem

adicValuation_le_one_iff

L51 ↗

AlgebraicCurve.Place.adicValuation_le_one_iff

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem adicValuation_le_one_iff {f : F} :
    v.adicValuation f ≤ 1 ↔ f = 0 ∨ 0 ≤ v.ord f

theorem

not_adicValuation_le_one_iff

L55 ↗

AlgebraicCurve.Place.not_adicValuation_le_one_iff

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem not_adicValuation_le_one_iff {f : F} :
    ¬v.adicValuation f ≤ 1 ↔ v.ord f < 0

def

repartitions

L67 ↗

AlgebraicCurve.repartitions

Documentation

The algebra generated by families integral at all but finitely many places.

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · statement

def repartitions : Subalgebra F (Place K F → F)

theorem

mem_repartitions_of_finite

L73 ↗

AlgebraicCurve.mem_repartitions_of_finite

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}

Lean source · statement

theorem mem_repartitions_of_finite {α : Place K F → F}
    (hα : {v : Place K F | ¬v.adicValuation (α v) ≤ 1}.Finite) :
    α ∈ repartitions K F

theorem

mem_repartitions_of_finite_ord

L78 ↗

AlgebraicCurve.mem_repartitions_of_finite_ord

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}

Lean source · statement

theorem mem_repartitions_of_finite_ord {α : Place K F → F}
    (hα : {v : Place K F | v.ord (α v) < 0}.Finite) :
    α ∈ repartitions K F

theorem

mem_repartitions_of_forall_le_exp

L86 ↗

AlgebraicCurve.mem_repartitions_of_forall_le_exp

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}

Lean source · statement

theorem mem_repartitions_of_forall_le_exp (D : Divisor K F) (α : Place K F → F)
    (h : ∀ v : Place K F, v.adicValuation (α v) ≤ exp (D v)) :
    α ∈ repartitions K F

def

repartitionsOf

L95 ↗

AlgebraicCurve.repartitionsOf

Documentation

The repartitions satisfying the valuation bounds specified by a divisor.

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}

Lean source · full declaration

def repartitionsOf (D : Divisor K F) : Submodule K ↥(repartitions K F) where
  carrier :=
    {α | ∀ v : Place K F, v.adicValuation ((α : Place K F → F) v) ≤ exp (D v)}
  zero_mem' := by
    intro v
    change v.adicValuation (0 : F) ≤ exp (D v)
    simp
  add_mem' := by
    intro α β hα hβ v
    exact (Valuation.map_add _ _ _).trans (max_le (hα v) (hβ v))
  smul_mem' := by
    intro c α hα v
    change v.adicValuation (c • (α : Place K F → F) v) ≤ exp (D v)
    rw [Algebra.smul_def, map_mul]
    exact (mul_le_of_le_one_left' (v.adicValuation_algebraMap_le_one c)).trans (hα v)

theorem

mem_repartitionsOf_iff

L111 ↗

AlgebraicCurve.mem_repartitionsOf_iff

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}

Lean source · statement

theorem mem_repartitionsOf_iff {D : Divisor K F} {α : ↥(repartitions K F)} :
    α ∈ repartitionsOf D ↔
      ∀ v : Place K F,
        (α : Place K F → F) v = 0 ∨ -D v ≤ v.ord ((α : Place K F → F) v)

theorem

repartitionsOf_mono

L118 ↗

AlgebraicCurve.repartitionsOf_mono

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}

Lean source · statement

theorem repartitionsOf_mono {D D' : Divisor K F} (h : D ≤ D') :
    repartitionsOf D ≤ repartitionsOf D'

def

riemannRochSpace

L123 ↗

AlgebraicCurve.riemannRochSpace

Documentation

The functions satisfying the valuation bounds specified by a divisor.

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}

Lean source · full declaration

def riemannRochSpace (D : Divisor K F) : Submodule K F where
  carrier := {f | ∀ v : Place K F, v.adicValuation f ≤ exp (D v)}
  zero_mem' := by
    intro v
    simp
  add_mem' := by
    intro f g hf hg v
    exact (Valuation.map_add _ _ _).trans (max_le (hf v) (hg v))
  smul_mem' := by
    intro c f hf v
    change v.adicValuation (c • f) ≤ exp (D v)
    rw [Algebra.smul_def, map_mul]
    exact (mul_le_of_le_one_left' (v.adicValuation_algebraMap_le_one c)).trans (hf v)

theorem

mem_riemannRochSpace_iff

L137 ↗

AlgebraicCurve.mem_riemannRochSpace_iff

Source context 5 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}

Lean source · statement

theorem mem_riemannRochSpace_iff {D : Divisor K F} {f : F} :
    f ∈ riemannRochSpace D ↔ ∀ v : Place K F, f = 0 ∨ -D v ≤ v.ord f

def

principalRepartitions

L144 ↗

AlgebraicCurve.principalRepartitions

Documentation

The submodule of constant repartitions arising from global functions.

Source context 6 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
variable (K F) in

Lean source · statement

def principalRepartitions : Submodule K ↥(repartitions K F)

theorem

mem_principalRepartitions_iff

L147 ↗

AlgebraicCurve.mem_principalRepartitions_iff

Source context 6 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
variable (K F) in

Lean source · full declaration

theorem mem_principalRepartitions_iff {α : ↥(repartitions K F)} :
    α ∈ principalRepartitions K F ↔
      ∃ f : F, (α : Place K F → F) = fun _ => f := by
  simp only [principalRepartitions, Submodule.restrictScalars_mem, LinearMap.mem_range,
    Algebra.linearMap_apply]
  constructor
  · rintro ⟨f, rfl⟩
    exact ⟨f, rfl⟩
  · rintro ⟨f, hf⟩
    exact ⟨f, Subtype.ext hf.symm⟩

abbrev

H1

L159 ↗

AlgebraicCurve.H1

Documentation

Repartitions modulo bounded and principal repartitions for a divisor.

Source context 6 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
variable (K F) in

Lean source · statement

abbrev H1 (D : Divisor K F) : Type _

def

genusFF

L164 ↗

AlgebraicCurve.genusFF

Documentation

The dimension of the first repartition cohomology space for the zero divisor.

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
variable (K F) in
variable (K F) in

Lean source · statement

def genusFF : ℕ

Module documentation

Declarations