Module

CechH1ToH1_bijective.lean

Nyll.AlgebraicCurves.Cohomology.CechH1ToH1_bijective

5 declarations indexed from sourceView source ↗

Module documentation

Bijectivity of the map from divisor-section Cech cohomology to adelic cohomology.

Imports8

Imported by3

theorem

finite_setOf_not_adicValuation_le_of_mem_adeleBdd

L36 ↗

AlgebraicCurves.Cohomology.Proofs.CechH1ToH1_bijective.AlgebraicCurve.finite_setOf_not_adicValuation_le_of_mem_adeleBdd

Source context 6 commands

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

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

Lean source · statement

theorem finite_setOf_not_adicValuation_le_of_mem_adeleBdd {E : Divisor K F} {β : Place K F → F}
    (hβ : β ∈ adeleBdd E) (D : Divisor K F) :
    {v : Place K F | ¬ v.adicValuation (β v) ≤ WithZero.exp (D v)}.Finite

theorem

finite_setOf_not_adicValuation_le_of_mem_adeleSpace

L48 ↗

AlgebraicCurves.Cohomology.Proofs.CechH1ToH1_bijective.AlgebraicCurve.finite_setOf_not_adicValuation_le_of_mem_adeleSpace

Source context 6 commands

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

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

Lean source · statement

theorem finite_setOf_not_adicValuation_le_of_mem_adeleSpace {β : Place K F → F}
    (hβ : β ∈ adeleSpace K F) (D : Divisor K F) :
    {v : Place K F | ¬ v.adicValuation (β v) ≤ WithZero.exp (D v)}.Finite

theorem

cechH1ToH1_injective

L60 ↗

AlgebraicCurves.Cohomology.Proofs.CechH1ToH1_bijective.AlgebraicCurve.cechH1ToH1_injective

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.CechH1ToH1_bijective
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem cechH1ToH1_injective {K F : Type*} [Field K] [Field F] [Algebra K F]
    {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ) (D : Divisor K F) :
    Function.Injective (cechH1ToH1 hcover D)

theorem

cechH1ToH1_surjective

L99 ↗

AlgebraicCurves.Cohomology.Proofs.CechH1ToH1_bijective.AlgebraicCurve.cechH1ToH1_surjective

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.CechH1ToH1_bijective
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem cechH1ToH1_surjective {K F : Type*} [Field K] [Field F] [Algebra K F] [IsCurveOver K F]
    [FiniteDimensional K ↥(LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ) (h₀ : ∃ v, v ∉ S₀) (h₁ : ∃ v, v ∉ S₁)
    (D : Divisor K F) :
    Function.Surjective (cechH1ToH1 hcover D)

theorem