Module

DivisorSections.lean

Nyll.AlgebraicCurves.Cohomology.Cech.DivisorSections

38 declarations indexed from sourceView source ↗

Module documentation

Divisor-bounded functions on two charts and their Cech cohomology. Chart extension maps the first Cech quotient to adelic cohomology.

Imports2

Imported by57

def

lSpaceOn

L30 ↗

AlgebraicCurve.lSpaceOn

Documentation

Functions satisfying the divisor valuation bounds at all places in the specified set.

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def lSpaceOn (S : Set (Place K F)) (D : Divisor K F) : Submodule K F where
  carrier := {f | ∀ v ∈ S, v.adicValuation f ≤ exp (D v)}
  add_mem' := fun {f g} hf hg v hv =>
    (Valuation.map_add _ f g).trans (max_le (hf v hv) (hg v hv))
  zero_mem' := fun v _ => by simp
  smul_mem' := fun c f hf v hv => by
    change v.adicValuation (c • f) ≤ exp (D v)
    rw [Algebra.smul_def, map_mul]
    exact (mul_le_of_le_one_left' (v.adicValuation_algebraMap_le_one c)).trans (hf v hv)

theorem

mem_lSpaceOn_iff

L40 ↗

AlgebraicCurve.mem_lSpaceOn_iff

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_lSpaceOn_iff {S : Set (Place K F)} {D : Divisor K F} {f : F} :
    f ∈ lSpaceOn S D ↔ ∀ v ∈ S, v.adicValuation f ≤ exp (D v)

theorem

mem_lSpaceOn_iff_ord

L43 ↗

AlgebraicCurve.mem_lSpaceOn_iff_ord

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_lSpaceOn_iff_ord {S : Set (Place K F)} {D : Divisor K F} {f : F} :
    f ∈ lSpaceOn S D ↔ ∀ v ∈ S, f = 0 ∨ -D v ≤ v.ord f

theorem

lSpaceOn_univ

L47 ↗

AlgebraicCurve.lSpaceOn_univ

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpaceOn_univ (D : Divisor K F) :
    lSpaceOn (Set.univ : Set (Place K F)) D = riemannRochSpace D

theorem

lSpaceOn_empty

L52 ↗

AlgebraicCurve.lSpaceOn_empty

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpaceOn_empty (D : Divisor K F) :
    lSpaceOn (∅ : Set (Place K F)) D = ⊤

theorem

lSpaceOn_anti

L57 ↗

AlgebraicCurve.lSpaceOn_anti

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpaceOn_anti {S₀ S₁ : Set (Place K F)} (h : S₀ ⊆ S₁) (D : Divisor K F) :
    lSpaceOn S₁ D ≤ lSpaceOn S₀ D

theorem

riemannRochSpace_le_lSpaceOn

L60 ↗

AlgebraicCurve.riemannRochSpace_le_lSpaceOn

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem riemannRochSpace_le_lSpaceOn (S : Set (Place K F)) (D : Divisor K F) :
    riemannRochSpace D ≤ lSpaceOn S D

theorem

lSpaceOn_mono

L63 ↗

AlgebraicCurve.lSpaceOn_mono

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpaceOn_mono {D E : Divisor K F} (hDE : D ≤ E) (S : Set (Place K F)) :
    lSpaceOn S D ≤ lSpaceOn S E

theorem

lSpaceOn_union

L67 ↗

AlgebraicCurve.lSpaceOn_union

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpaceOn_union (S₀ S₁ : Set (Place K F)) (D : Divisor K F) :
    lSpaceOn (S₀ ∪ S₁) D = lSpaceOn S₀ D ⊓ lSpaceOn S₁ D

theorem

lSpaceOn_inf_eq_of_cover

L74 ↗

AlgebraicCurve.lSpaceOn_inf_eq_of_cover

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpaceOn_inf_eq_of_cover {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ)
    (D : Divisor K F) :
    lSpaceOn S₀ D ⊓ lSpaceOn S₁ D = riemannRochSpace D

theorem

lSpaceOn_eq_iInf_singleton

L79 ↗

AlgebraicCurve.lSpaceOn_eq_iInf_singleton

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpaceOn_eq_iInf_singleton (S : Set (Place K F)) (D : Divisor K F) :
    lSpaceOn S D = ⨅ v ∈ S, lSpaceOn {v} D

theorem

mem_lSpaceOn_singleton_iff

L84 ↗

AlgebraicCurve.mem_lSpaceOn_singleton_iff

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_lSpaceOn_singleton_iff {v : Place K F} {D : Divisor K F} {f : F} :
    f ∈ lSpaceOn {v} D ↔ f = 0 ∨ -D v ≤ v.ord f

def

cechSections

L90 ↗

AlgebraicCurve.cechSections

Documentation

The two-chart section system formed from divisor-bounded functions.

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def cechSections (S₀ S₁ : Set (Place K F)) (D : Divisor K F) :
    TwoChartCech.Sections (TwoChartCech.Cover.trivial K)

abbrev

cechDiff

L96 ↗

AlgebraicCurve.cechDiff

Documentation

The difference map from the two chart spaces to the overlap space.

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev cechDiff (S₀ S₁ : Set (Place K F)) (D : Divisor K F) :
    (lSpaceOn S₀ D × lSpaceOn S₁ D) →ₗ[K] lSpaceOn (S₀ ∩ S₁) D

theorem

coe_cechDiff_apply

L100 ↗

AlgebraicCurve.coe_cechDiff_apply

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem coe_cechDiff_apply {S₀ S₁ : Set (Place K F)} {D : Divisor K F}
    (p : lSpaceOn S₀ D × lSpaceOn S₁ D) :
    (cechDiff S₀ S₁ D p : F) = (p.2 : F) - p.1

abbrev

cechH0

L109 ↗

AlgebraicCurve.cechH0

Documentation

Matching pairs of divisor-bounded functions on the two charts.

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev cechH0 (S₀ S₁ : Set (Place K F)) (D : Divisor K F) :
    Submodule K (lSpaceOn S₀ D × lSpaceOn S₁ D)

theorem

cechH0_eq

L113 ↗

AlgebraicCurve.cechH0_eq

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem cechH0_eq (S₀ S₁ : Set (Place K F)) (D : Divisor K F) :
    cechH0 S₀ S₁ D = (cechSections S₀ S₁ D).H0

theorem

mem_cechH0_iff

L116 ↗

AlgebraicCurve.mem_cechH0_iff

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_cechH0_iff {S₀ S₁ : Set (Place K F)} {D : Divisor K F}
    (p : lSpaceOn S₀ D × lSpaceOn S₁ D) :
    p ∈ cechH0 S₀ S₁ D ↔ (p.1 : F) = p.2

abbrev

cechH1

L122 ↗

AlgebraicCurve.cechH1

Documentation

Divisor-bounded functions on the overlap modulo chart differences.

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev cechH1 (S₀ S₁ : Set (Place K F)) (D : Divisor K F) : Type _

theorem

cechH1_eq

L125 ↗

AlgebraicCurve.cechH1_eq

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem cechH1_eq (S₀ S₁ : Set (Place K F)) (D : Divisor K F) :
    cechH1 S₀ S₁ D = (cechSections S₀ S₁ D).H1

theorem

map_subtype_range_cechDiff

L128 ↗

AlgebraicCurve.map_subtype_range_cechDiff

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem map_subtype_range_cechDiff (S₀ S₁ : Set (Place K F)) (D : Divisor K F) :
    (LinearMap.range (cechDiff S₀ S₁ D)).map (lSpaceOn (S₀ ∩ S₁) D).subtype
      = lSpaceOn S₀ D ⊔ lSpaceOn S₁ D

theorem

mem_range_cechDiff_iff

L148 ↗

AlgebraicCurve.mem_range_cechDiff_iff

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_range_cechDiff_iff {S₀ S₁ : Set (Place K F)} {D : Divisor K F}
    (g : lSpaceOn (S₀ ∩ S₁) D) :
    g ∈ LinearMap.range (cechDiff S₀ S₁ D) ↔ (g : F) ∈ lSpaceOn S₀ D ⊔ lSpaceOn S₁ D

def

cechH0Equiv

L160 ↗

AlgebraicCurve.cechH0Equiv

Documentation

Identify matching chart sections with the Riemann--Roch space when the charts cover all places.

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def cechH0Equiv {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ) (D : Divisor K F) :
    cechH0 S₀ S₁ D ≃ₗ[K] riemannRochSpace D where
  toFun p := ⟨((p.1.1 : lSpaceOn S₀ D) : F), by
    rw [← lSpaceOn_inf_eq_of_cover hcover]
    exact ⟨p.1.1.2, ((mem_cechH0_iff p.1).mp p.2).symm ▸ p.1.2.2⟩⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun f := ⟨(⟨f, riemannRochSpace_le_lSpaceOn S₀ D f.2⟩, ⟨f, riemannRochSpace_le_lSpaceOn S₁ D
    f.2⟩),
    (mem_cechH0_iff _).mpr rfl⟩
  left_inv p := by
    apply Subtype.ext
    apply Prod.ext
    · rfl
    · exact Subtype.ext ((mem_cechH0_iff p.1).mp p.2)
  right_inv f := rfl

theorem

coe_cechH0Equiv_apply

L177 ↗

AlgebraicCurve.coe_cechH0Equiv_apply

Source context 4 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem coe_cechH0Equiv_apply {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ)
    (D : Divisor K F) (p : cechH0 S₀ S₁ D) :
    (cechH0Equiv hcover D p : F) = ((p.1.1 : lSpaceOn S₀ D) : F)

def

offChartIndicator

L186 ↗

AlgebraicCurve.offChartIndicator

Documentation

The repartition equal to zero on the chart and one outside it.

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
open Classical in

Lean source · statement

def offChartIndicator (S : Set (Place K F)) : ↥(repartitions K F)

theorem

coe_offChartIndicator_apply

L194 ↗

AlgebraicCurve.coe_offChartIndicator_apply

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
open Classical in

Lean source · full declaration

theorem coe_offChartIndicator_apply (S : Set (Place K F)) (v : Place K F) :
    (offChartIndicator K S : Place K F → F) v = if v ∈ S then 0 else 1 := rfl

def

extendOffChart

L199 ↗

AlgebraicCurve.extendOffChart

Documentation

Extend a function as a repartition supported outside the specified chart.

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in

Lean source · full declaration

def extendOffChart (S₀ : Set (Place K F)) : F →ₗ[K] ↥(repartitions K F) where
  toFun f := offChartIndicator K S₀ * algebraMap F (↥(repartitions K F)) f
  map_add' f g := by rw [map_add, mul_add]
  map_smul' c f := by
    apply Subtype.ext
    funext v
    change (offChartIndicator K S₀ : Place K F → F) v * (c • f)
        = c • ((offChartIndicator K S₀ : Place K F → F) v * f)
    rw [Algebra.smul_def, Algebra.smul_def]
    ring

theorem

coe_extendOffChart_apply

L211 ↗

AlgebraicCurve.coe_extendOffChart_apply

Source context 8 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in
open Classical in

Lean source · full declaration

theorem coe_extendOffChart_apply (S₀ : Set (Place K F)) (f : F) (v : Place K F) :
    (extendOffChart K S₀ f : Place K F → F) v = if v ∈ S₀ then 0 else f := by
  change ((offChartIndicator K S₀ : Place K F → F) * algebraMap F (Place K F → F) f) v = _
  rw [Pi.mul_apply, coe_offChartIndicator_apply, Pi.algebraMap_apply, Algebra.algebraMap_self,
    RingHom.id_apply]
  split_ifs <;> simp

theorem

coe_extendOffChart_apply_of_mem

L218 ↗

AlgebraicCurve.coe_extendOffChart_apply_of_mem

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in

Lean source · statement

theorem coe_extendOffChart_apply_of_mem {S₀ : Set (Place K F)} (f : F) {v : Place K F}
    (hv : v ∈ S₀) : (extendOffChart K S₀ f : Place K F → F) v = 0

theorem

coe_extendOffChart_apply_of_not_mem

L223 ↗

AlgebraicCurve.coe_extendOffChart_apply_of_not_mem

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in

Lean source · statement

theorem coe_extendOffChart_apply_of_not_mem {S₀ : Set (Place K F)} (f : F) {v : Place K F}
    (hv : v ∉ S₀) : (extendOffChart K S₀ f : Place K F → F) v = f

theorem

algebraMap_sub_extendOffChart_mem_repartitionsOf

L228 ↗

AlgebraicCurve.algebraMap_sub_extendOffChart_mem_repartitionsOf

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in

Lean source · statement

theorem algebraMap_sub_extendOffChart_mem_repartitionsOf {S₀ : Set (Place K F)} {D : Divisor K F}
    {f : F} (hf : f ∈ lSpaceOn S₀ D) :
    algebraMap F (↥(repartitions K F)) f - extendOffChart K S₀ f ∈ repartitionsOf D

theorem

extendOffChart_mem_repartitionsOf

L240 ↗

AlgebraicCurve.extendOffChart_mem_repartitionsOf

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in

Lean source · statement

theorem extendOffChart_mem_repartitionsOf {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ)
    {D : Divisor K F} {f : F} (hf : f ∈ lSpaceOn S₁ D) :
    extendOffChart K S₀ f ∈ repartitionsOf D

theorem

algebraMap_mem_principalRepartitions

L253 ↗

AlgebraicCurve.algebraMap_mem_principalRepartitions

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in

Lean source · statement

theorem algebraMap_mem_principalRepartitions (f : F) :
    algebraMap F (↥(repartitions K F)) f ∈ principalRepartitions K F

def

toH1Aux

L258 ↗

AlgebraicCurve.toH1Aux

Documentation

Map an overlap section to adelic cohomology by extending it outside the first chart.

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in

Lean source · statement

def toH1Aux (S₀ S₁ : Set (Place K F)) (D : Divisor K F) : ↥(lSpaceOn (S₀ ∩ S₁) D) →ₗ[K] H1 D

theorem

toH1Aux_apply

L262 ↗

AlgebraicCurve.toH1Aux_apply

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in

Lean source · statement

theorem toH1Aux_apply {S₀ S₁ : Set (Place K F)} {D : Divisor K F} (f : lSpaceOn (S₀ ∩ S₁) D) :
    toH1Aux S₀ S₁ D f = Submodule.Quotient.mk (extendOffChart K S₀ (f : F))

theorem

range_cechDiff_le_ker_toH1Aux

L265 ↗

AlgebraicCurve.range_cechDiff_le_ker_toH1Aux

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in

Lean source · statement

theorem range_cechDiff_le_ker_toH1Aux {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ)
    (D : Divisor K F) :
    LinearMap.range (cechDiff S₀ S₁ D) ≤ LinearMap.ker (toH1Aux S₀ S₁ D)

def

cechH1ToH1

L279 ↗

AlgebraicCurve.cechH1ToH1

Documentation

The induced map from first Cech cohomology to adelic cohomology.

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in

Lean source · statement

def cechH1ToH1 {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ) (D : Divisor K F) :
    cechH1 S₀ S₁ D →ₗ[K] H1 D

theorem

cechH1ToH1_mk

L284 ↗

AlgebraicCurve.cechH1ToH1_mk

Source context 7 commands

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

noncomputable section
open WithZero
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ToH1
variable (K) in
variable (K) in

Lean source · statement

theorem cechH1ToH1_mk {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ)
    (D : Divisor K F) (f : lSpaceOn (S₀ ∩ S₁) D) :
    cechH1ToH1 hcover D (Submodule.Quotient.mk f)
      = Submodule.Quotient.mk (extendOffChart K S₀ (f : F))

Module documentation

Declarations