Module

Mem_adeleSpace_iff_mem_repartitions.lean

Nyll.AlgebraicCurves.Cohomology.Mem_adeleSpace_iff_mem_repartitions

7 declarations indexed from sourceView source ↗

Module documentation

Adelic families are precisely repartitions, using a divisor bound for their valuations.

Imports3

Imported by4

theorem

mem_repartitionsOf_iff_coe_mem_adeleBdd

L33 ↗

AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions.AlgebraicCurve.mem_repartitionsOf_iff_coe_mem_adeleBdd

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_repartitionsOf_iff_coe_mem_adeleBdd {D : Divisor K F} {α : ↥(repartitions K F)} :
    α ∈ repartitionsOf D ↔ (α : Place K F → F) ∈ adeleBdd D

theorem

mem_repartitions_of_mem_adeleBdd

L36 ↗

AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions.AlgebraicCurve.mem_repartitions_of_mem_adeleBdd

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_repartitions_of_mem_adeleBdd {D : Divisor K F} {α : Place K F → F} (hα : α ∈ adeleBdd
    D) :
    α ∈ repartitions K F

theorem

mem_repartitions_of_mem_adeleSpace

L41 ↗

AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions.AlgebraicCurve.mem_repartitions_of_mem_adeleSpace

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_repartitions_of_mem_adeleSpace {α : Place K F → F} (hα : α ∈ adeleSpace K F) :
    α ∈ repartitions K F

theorem

diagonalHom_eq_coe_algebraMap

L46 ↗

AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions.AlgebraicCurve.diagonalHom_eq_coe_algebraMap

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem diagonalHom_eq_coe_algebraMap (f : F) :
    diagonalHom K F f = ((algebraMap F ↥(repartitions K F) f : ↥(repartitions K F)) : Place K F →
      F)

theorem

mem_principalRepartitions_iff_coe_mem_globalSub

L50 ↗

AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions.AlgebraicCurve.mem_principalRepartitions_iff_coe_mem_globalSub

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_principalRepartitions_iff_coe_mem_globalSub {α : ↥(repartitions K F)} :
    α ∈ principalRepartitions K F ↔ (α : Place K F → F) ∈ globalSub K F

def

boundedFamilies

L58 ↗

AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions.AlgebraicCurve.boundedFamilies

Documentation

Families bounded at every place by the valuation bound of a single divisor.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Mem_adeleSpace_iff_mem_repartitions
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open WithZero
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def boundedFamilies [HasPrincipalDivisors K F] : Subalgebra F (Place K F → F) where
  carrier := {α | ∃ D : Divisor K F, ∀ v : Place K F, v.adicValuation (α v) ≤ exp (D v)}
  mul_mem' := by
    rintro α β ⟨D, hD⟩ ⟨E, hE⟩
    refine ⟨D + E, fun v => ?_⟩
    rw [Pi.mul_apply, map_mul, Finsupp.add_apply, exp_add]
    exact mul_le_mul' (hD v) (hE v)
  add_mem' := by
    rintro α β ⟨D, hD⟩ ⟨E, hE⟩
    refine ⟨D ⊔ E, fun v => ?_⟩
    rw [Pi.add_apply]
    refine (Valuation.map_add _ _ _).trans (max_le ?_ ?_)
    · exact (hD v).trans (exp_le_exp.mpr (le_sup_left (a := D) (b := E) v))
    · exact (hE v).trans (exp_le_exp.mpr (le_sup_right (a := D) (b := E) v))
  algebraMap_mem' := by
    intro f
    rcases eq_or_ne f 0 with rfl | hf
    · exact ⟨0, fun v => by simp⟩
    · obtain ⟨P, hP, -⟩ := HasPrincipalDivisors.exists_divisor (K := K) f hf
      refine ⟨-P, fun v => ?_⟩
      rw [Pi.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
        v.adicValuation_eq_exp_neg_ord hf, Finsupp.neg_apply, hP]

theorem