Module

Finite_H1_and_exists_linearEquiv_dual_H1_omegaSpace.lean

Nyll.AlgebraicCurves.Cohomology.Finite_H1_and_exists_linearEquiv_dual_H1_omegaSpace

2 declarations indexed from sourceView source ↗

Module documentation

Finite H1 and exists linear Equiv dual H1 omega Space

Imports6

Imported by2

theorem

finite_H1_and_exists_linearEquiv_dual_H1_omegaSpace'

L53 ↗

AlgebraicCurves.Cohomology.Proofs.FiniteH1ExistsEquivDualH1Omega.AlgebraicCurve.finite_H1_and_exists_linearEquiv_dual_H1_omegaSpace'

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.FiniteH1ExistsEquivDualH1Omega
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem finite_H1_and_exists_linearEquiv_dual_H1_omegaSpace' {K : Type*} {F : Type*} [Field K]
  [Field F] [Algebra K F]
    [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
    (hC : ConstantsAreBase K F) (D : Divisor K F) :
    Module.Finite K (H1 D) ∧
      ∃ e : Module.Dual K (H1 D) ≃ₗ[K] ↥(omegaSpace (K := K) (F := F) D),
        ∀ (φ : Module.Dual K (H1 D)) (a : ↥(adeleSpace K F))
          (ha : (a : Place K F → F) ∈ repartitions K F),
          (e φ : Module.Dual K ↥(adeleSpace K F)) a
            = φ (Submodule.Quotient.mk ⟨(a : Place K F → F), ha⟩)

theorem

finite_H1_and_exists_linearEquiv_dual_H1_omegaSpace

L75 ↗

AlgebraicCurve.finite_H1_and_exists_linearEquiv_dual_H1_omegaSpace

Source context 7 commands