Module

Exists_linearEquiv_adeleSpaceQuot_H1.lean

Nyll.AlgebraicCurves.Cohomology.Exists_linearEquiv_adeleSpaceQuot_H1

1 declaration indexed from sourceView source ↗

Module documentation

Exists linear Equiv adele Space Quot H1

Imports6

Imported by2

theorem

exists_linearEquiv_adeleSpaceQuot_H1

L29 ↗

AlgebraicCurve.exists_linearEquiv_adeleSpaceQuot_H1

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Exists_linearEquiv_adeleSpaceQuot_H1
open AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.exists_linearEquiv_adeleSpaceQuot_H1 {K F : Type*} [Field K] [Field
  F] [Algebra K F]
    [HasPrincipalDivisors K F] (D : Divisor K F) :
    ∃ e : (↥(adeleSpace K F) ⧸ adeleBddPrincipal K F D) ≃ₗ[K] H1 D,
      ∀ (a : ↥(adeleSpace K F)) (ha : (a : Place K F → F) ∈ repartitions K F),
        e (Submodule.Quotient.mk a) = Submodule.Quotient.mk ⟨(a : Place K F → F), ha⟩

Module documentation

Exists linear Equiv adele Space Quot H1

Declarations

exists_linearEquiv_adeleSpaceQuot_H1