NYLL
Module

Polar.lean

Nyll.AlgebraicCurves.Differentials.Polar
30 declarations indexed from sourceView source ↗

Module documentation

Polar

Imports3
Imported by17

Declarations

def

IsRegularAt

L34 ↗
AlgebraicCurve.Place.IsRegularAt
Documentation

Regularity of a differential expressed using an integral coefficient in a local coordinate.

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
Lean source · statement
def IsRegularAt (ω : Ω[F⁄K]) : Prop
def

HasSimplePoleAt

L38 ↗
AlgebraicCurve.Place.HasSimplePoleAt
Documentation

The condition that a differential has at most a simple pole at the place.

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
Lean source · statement
def HasSimplePoleAt (ω : Ω[F⁄K]) : Prop
def

HasSimpleResidue

L43 ↗
AlgebraicCurve.Place.HasSimpleResidue
Documentation

The condition that a differential has the specified simple residue in the chosen local coordinate.

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
Lean source · statement
def HasSimpleResidue (ω : Ω[F⁄K]) (a : K) : Prop
theorem

uniformizer_mem_toValuationSubring

L49 ↗
AlgebraicCurve.Place.uniformizer_mem_toValuationSubring
Source context 8 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) in
Lean source · statement
theorem uniformizer_mem_toValuationSubring : v.uniformizer ∈ v.toValuationSubring
theorem

irreducible_mk_uniformizer

L53 ↗
AlgebraicCurve.Place.irreducible_mk_uniformizer
Source context 9 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) in
variable (v) in
Lean source · statement
theorem irreducible_mk_uniformizer :
    Irreducible (⟨v.uniformizer, v.uniformizer_mem_toValuationSubring⟩ : v.toValuationSubring)
theorem

hasSimplePoleAt

L58 ↗
AlgebraicCurve.Place.IsRegularAt.hasSimplePoleAt
Source context 9 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) in
variable (v) in
Lean source · statement
theorem IsRegularAt.hasSimplePoleAt {ω : Ω[F⁄K]} (h : v.IsRegularAt ω) : v.HasSimplePoleAt ω
theorem

hasSimplePoleAt

L62 ↗
AlgebraicCurve.Place.HasSimpleResidue.hasSimplePoleAt
Source context 9 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) in
variable (v) in
Lean source · statement
theorem HasSimpleResidue.hasSimplePoleAt {ω : Ω[F⁄K]} {a : K} (h : v.HasSimpleResidue ω a) :
    v.HasSimplePoleAt ω
theorem

isRegularAt_zero

L68 ↗
AlgebraicCurve.Place.isRegularAt_zero
Source context 10 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) in
variable (v) in
variable (v) in
Lean source · statement
theorem isRegularAt_zero : v.IsRegularAt (0 : Ω[F⁄K])
theorem

add

L71 ↗
AlgebraicCurve.Place.IsRegularAt.add
Source context 10 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) in
variable (v) in
variable (v) in
Lean source · statement
theorem IsRegularAt.add {ω η : Ω[F⁄K]} (hω : v.IsRegularAt ω) (hη : v.IsRegularAt η) :
    v.IsRegularAt (ω + η)
theorem

smul

L77 ↗
AlgebraicCurve.Place.IsRegularAt.smul
Source context 10 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) in
variable (v) in
variable (v) in
Lean source · statement
theorem IsRegularAt.smul (c : K) {ω : Ω[F⁄K]} (hω : v.IsRegularAt ω) : v.IsRegularAt (c • ω)
theorem

hasSimplePoleAt_zero

L83 ↗
AlgebraicCurve.Place.hasSimplePoleAt_zero
Source context 11 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) in
variable (v) in
variable (v) in
variable (v) in
Lean source · statement
theorem hasSimplePoleAt_zero : v.HasSimplePoleAt (0 : Ω[F⁄K])
theorem

add

L86 ↗
AlgebraicCurve.Place.HasSimplePoleAt.add
Source context 11 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) in
variable (v) in
variable (v) in
variable (v) in
Lean source · statement
theorem HasSimplePoleAt.add {ω η : Ω[F⁄K]} (hω : v.HasSimplePoleAt ω) (hη : v.HasSimplePoleAt η) :
    v.HasSimplePoleAt (ω + η)
theorem

smul

L92 ↗
AlgebraicCurve.Place.HasSimplePoleAt.smul
Source context 11 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) in
variable (v) in
variable (v) in
variable (v) in
Lean source · statement
theorem HasSimplePoleAt.smul (c : K) {ω : Ω[F⁄K]} (hω : v.HasSimplePoleAt ω) :
    v.HasSimplePoleAt (c • ω)
theorem

hasSimpleResidue_zero_of_mem

L99 ↗
AlgebraicCurve.Place.hasSimpleResidue_zero_of_mem
Source context 11 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) in
variable (v) in
variable (v) in
variable (v) in
Lean source · statement
theorem hasSimpleResidue_zero_of_mem {f : F} (hf : f ∈ v.toValuationSubring) :
    v.HasSimpleResidue (f • v.dCoord) 0
def

polarDifferentials

L118 ↗
AlgebraicCurve.polarDifferentials
Documentation

The space of differentials regular off the selected places and with at most simple poles there.

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Polar
variable (K F)
Lean source · full declaration
def polarDifferentials (S : Set (Place K F)) : Submodule K Ω[F⁄K] where
  carrier := {ω | ∀ v : Place K F, (v ∉ S → v.IsRegularAt ω) ∧ (v ∈ S → v.HasSimplePoleAt ω)}
  zero_mem' v := ⟨fun _ => v.isRegularAt_zero, fun _ => v.hasSimplePoleAt_zero⟩
  add_mem' hω hη v :=
    ⟨fun hv => ((hω v).1 hv).add ((hη v).1 hv), fun hv => ((hω v).2 hv).add ((hη v).2 hv)⟩
  smul_mem' c _ hω v := ⟨fun hv => ((hω v).1 hv).smul c, fun hv => ((hω v).2 hv).smul c⟩
theorem

mem_polarDifferentials_iff

L127 ↗
AlgebraicCurve.mem_polarDifferentials_iff
Source context 7 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Polar
variable (K F)
variable {K F}
Lean source · statement
theorem mem_polarDifferentials_iff {S : Set (Place K F)} {ω : Ω[F⁄K]} :
    ω ∈ polarDifferentials K F S ↔
      ∀ v : Place K F, (v ∉ S → v.IsRegularAt ω) ∧ (v ∈ S → v.HasSimplePoleAt ω)
theorem

hasSimplePoleAt_of_mem_polarDifferentials

L132 ↗
AlgebraicCurve.hasSimplePoleAt_of_mem_polarDifferentials
Source context 7 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Polar
variable (K F)
variable {K F}
Lean source · statement
theorem hasSimplePoleAt_of_mem_polarDifferentials {S : Set (Place K F)} {ω : Ω[F⁄K]}
    (h : ω ∈ polarDifferentials K F S) (v : Place K F) : v.HasSimplePoleAt ω
theorem

regularDifferentials_le_polarDifferentials

L138 ↗
AlgebraicCurve.regularDifferentials_le_polarDifferentials
Source context 7 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Polar
variable (K F)
variable {K F}
Lean source · statement
theorem regularDifferentials_le_polarDifferentials (S : Set (Place K F)) :
    regularDifferentials K F ≤ polarDifferentials K F S
theorem

polarDifferentials_mono

L142 ↗
AlgebraicCurve.polarDifferentials_mono
Source context 7 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Polar
variable (K F)
variable {K F}
Lean source · statement
theorem polarDifferentials_mono {S T : Set (Place K F)} (h : S ⊆ T) :
    polarDifferentials K F S ≤ polarDifferentials K F T
theorem

polarDifferentials_empty

L146 ↗
AlgebraicCurve.polarDifferentials_empty
Source context 7 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Polar
variable (K F)
variable {K F}
Lean source · statement
theorem polarDifferentials_empty : polarDifferentials K F ∅ = regularDifferentials K F
def

IsGluedPolarPair

L157 ↗
AlgebraicCurve.IsGluedPolarPair
Documentation

Pairs of polar differentials whose residues sum to zero at each specified pair of places.

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Glued
variable (K F)
Lean source · statement
def IsGluedPolarPair (S : Set (Place K F × Place K F)) (ω : Ω[F⁄K] × Ω[F⁄K]) : Prop
def

gluedPolarDifferentials

L163 ↗
AlgebraicCurve.gluedPolarDifferentials
Documentation

The submodule generated by polar differential pairs satisfying the residue gluing condition.

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Glued
variable (K F)
Lean source · statement
def gluedPolarDifferentials (S : Set (Place K F × Place K F)) : Submodule K (Ω[F⁄K] × Ω[F⁄K])
theorem

mem_gluedPolarDifferentials_of_isGluedPolarPair

L168 ↗
AlgebraicCurve.mem_gluedPolarDifferentials_of_isGluedPolarPair
Source context 7 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Glued
variable (K F)
variable {K F}
Lean source · statement
theorem mem_gluedPolarDifferentials_of_isGluedPolarPair {S : Set (Place K F × Place K F)}
    {ω : Ω[F⁄K] × Ω[F⁄K]} (h : IsGluedPolarPair K F S ω) : ω ∈ gluedPolarDifferentials K F S
theorem

gluedPolarDifferentials_eq_span

L172 ↗
AlgebraicCurve.gluedPolarDifferentials_eq_span
Source context 7 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Glued
variable (K F)
variable {K F}
Lean source · statement
theorem gluedPolarDifferentials_eq_span (S : Set (Place K F × Place K F)) :
    gluedPolarDifferentials K F S = Submodule.span K {ω | IsGluedPolarPair K F S ω}
theorem

gluedPolarDifferentials_le_prod

L176 ↗
AlgebraicCurve.gluedPolarDifferentials_le_prod
Source context 7 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Glued
variable (K F)
variable {K F}
Lean source · statement
theorem gluedPolarDifferentials_le_prod (S : Set (Place K F × Place K F)) :
    gluedPolarDifferentials K F S ≤
      (polarDifferentials K F (Prod.fst '' S)).prod (polarDifferentials K F (Prod.snd '' S))
def

fst

L185 ↗
AlgebraicCurve.gluedPolarDifferentials.fst
Documentation

Projection of a glued polar differential pair onto its first polar differential.

Source context 8 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Glued
variable (K F)
variable {K F}
variable (K F) in
Lean source · statement
def gluedPolarDifferentials.fst (S : Set (Place K F × Place K F)) :
    gluedPolarDifferentials K F S →ₗ[K] polarDifferentials K F (Prod.fst '' S)
def

snd

L192 ↗
AlgebraicCurve.gluedPolarDifferentials.snd
Documentation

Projection of a glued polar differential pair onto its second polar differential.

Source context 9 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Glued
variable (K F)
variable {K F}
variable (K F) in
variable (K F) in
Lean source · statement
def gluedPolarDifferentials.snd (S : Set (Place K F × Place K F)) :
    gluedPolarDifferentials K F S →ₗ[K] polarDifferentials K F (Prod.snd '' S)
theorem

coe_fst_apply

L197 ↗
AlgebraicCurve.gluedPolarDifferentials.coe_fst_apply
Source context 9 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Glued
variable (K F)
variable {K F}
variable (K F) in
variable (K F) in
Lean source · statement
theorem gluedPolarDifferentials.coe_fst_apply (S : Set (Place K F × Place K F))
    (ω : gluedPolarDifferentials K F S) :
    (gluedPolarDifferentials.fst K F S ω : Ω[F⁄K]) = (ω : Ω[F⁄K] × Ω[F⁄K]).1
theorem

coe_snd_apply

L202 ↗
AlgebraicCurve.gluedPolarDifferentials.coe_snd_apply
Source context 9 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Glued
variable (K F)
variable {K F}
variable (K F) in
variable (K F) in
Lean source · statement
theorem gluedPolarDifferentials.coe_snd_apply (S : Set (Place K F × Place K F))
    (ω : gluedPolarDifferentials K F S) :
    (gluedPolarDifferentials.snd K F S ω : Ω[F⁄K]) = (ω : Ω[F⁄K] × Ω[F⁄K]).2
theorem

prod_regularDifferentials_le_gluedPolarDifferentials_empty

L207 ↗
AlgebraicCurve.prod_regularDifferentials_le_gluedPolarDifferentials_empty
Source context 9 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Glued
variable (K F)
variable {K F}
variable (K F) in
variable (K F) in
Lean source · statement
theorem prod_regularDifferentials_le_gluedPolarDifferentials_empty :
    (regularDifferentials K F).prod (regularDifferentials K F) ≤
      gluedPolarDifferentials K F (∅ : Set (Place K F × Place K F))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.