Module

IndexOfSpecialty_eq_finrank_H1.lean

Nyll.AlgebraicCurves.Cohomology.IndexOfSpecialty_eq_finrank_H1

10 declarations indexed from sourceView source ↗

Module documentation

The index of specialty is the dimension of first adelic cohomology. The adelic and repartition models are identified by their common bounded families.

Imports3

Imported by12

theorem

mem_repartitionsOf_iff_coe_mem_adeleBdd

L34 ↗

AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1.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.IndexOfSpecialty_eq_finrank_H1
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

L37 ↗

AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1.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.IndexOfSpecialty_eq_finrank_H1
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

L42 ↗

AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1.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.IndexOfSpecialty_eq_finrank_H1
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

L47 ↗

AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1.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.IndexOfSpecialty_eq_finrank_H1
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

L51 ↗

AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1.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.IndexOfSpecialty_eq_finrank_H1
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

L59 ↗

AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1.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.IndexOfSpecialty_eq_finrank_H1
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

mem_adeleSpace_iff_mem_repartitions

L82 ↗

AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1.AlgebraicCurve.mem_adeleSpace_iff_mem_repartitions

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1
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_adeleSpace_iff_mem_repartitions [HasPrincipalDivisors K F] {α : Place K F → F} :
    α ∈ adeleSpace K F ↔ α ∈ repartitions K F

theorem

adeleSpace_eq_restrictScalars_repartitions

L110 ↗

AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1.AlgebraicCurve.adeleSpace_eq_restrictScalars_repartitions

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1
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 adeleSpace_eq_restrictScalars_repartitions [HasPrincipalDivisors K F] :
    adeleSpace K F = (Subalgebra.toSubmodule (repartitions K F)).restrictScalars K

def

adeleSpaceEquivRepartitions

L116 ↗

AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1.AlgebraicCurve.adeleSpaceEquivRepartitions

Documentation

Identify the adelic space with repartitions by their common underlying bounded families.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.IndexOfSpecialty_eq_finrank_H1
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 adeleSpaceEquivRepartitions [HasPrincipalDivisors K F] :
    ↥(adeleSpace K F) ≃ₗ[K] ↥(repartitions K F) where
  toFun α := ⟨α, mem_adeleSpace_iff_mem_repartitions.mp α.2⟩
  invFun α := ⟨α, mem_adeleSpace_iff_mem_repartitions.mpr α.2⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv _ := rfl
  right_inv _ := rfl

theorem