Module

Mem_principalRepartitions_iff_coe_mem_globalSub.lean

Nyll.AlgebraicCurves.Cohomology.Mem_principalRepartitions_iff_coe_mem_globalSub

5 declarations indexed from sourceView source ↗

Module documentation

Mem principal Repartitions iff coe mem global Sub

Imports3

Imported by2

theorem

mem_repartitionsOf_iff_coe_mem_adeleBdd

L33 ↗

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

L54 ↗

AlgebraicCurve.mem_principalRepartitions_iff_coe_mem_globalSub

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.MemPrincipalRepartitionsIffCoe
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Cohomology.Proofs.MemPrincipalRepartitionsIffCoe.AlgebraicCurve WithZero in

Lean source · statement

theorem _root_.AlgebraicCurve.mem_principalRepartitions_iff_coe_mem_globalSub {K F : Type*} [Field
  K] [Field F] [Algebra K F] {α : ↥(repartitions K F)} :
    α ∈ principalRepartitions K F ↔ (α : Place K F → F) ∈ globalSub K F

Module documentation

Mem principal Repartitions iff coe mem global Sub

Declarations

mem_repartitionsOf_iff_coe_mem_adeleBdd

mem_repartitions_of_mem_adeleBdd

mem_repartitions_of_mem_adeleSpace

diagonalHom_eq_coe_algebraMap

mem_principalRepartitions_iff_coe_mem_globalSub