Module

ClassGroup.lean

Nyll.AlgebraicCurves.Divisors.ClassGroup

72 declarations indexed from sourceView source ↗

Module documentation

Places, divisors and divisor class groups of a field extension. The valuation orders define principal divisors and the degree-zero Picard group.

Imports10

Mathlib.RingTheory.DedekindDomain.AdicValuation
Mathlib.RingTheory.Valuation.Discrete.Basic
Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.Data.Finsupp.SMul
Mathlib.Algebra.BigOperators.Finsupp.Basic
Mathlib.Algebra.Module.Torsion.Basic
Mathlib.Algebra.Ring.Subring.Pointwise
Mathlib.LinearAlgebra.FiniteDimensional.Defs
Mathlib.RingTheory.Bezout

Imported by374

structure

Place

L38 ↗

AlgebraicCurve.Place

Documentation

A proper principal valuation subring of F containing the image of the base field K.

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · full declaration

structure Place where
  /-- The valuation subring defining the place. -/
  toValuationSubring : ValuationSubring F
  /-- Every scalar from the base field belongs to the valuation subring. -/
  algebraMap_mem' : ∀ a : K, algebraMap K F a ∈ toValuationSubring
  /-- The valuation subring is a proper subring of the ambient field. -/
  ne_top' : toValuationSubring ≠ ⊤
  /-- The valuation subring is a principal ideal ring. -/
  isPrincipalIdealRing' : IsPrincipalIdealRing toValuationSubring

theorem

not_isField_of_ne_top

L48 ↗

ValuationSubring.not_isField_of_ne_top

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem _root_.ValuationSubring.not_isField_of_ne_top {A : ValuationSubring F} (hA : A ≠ ⊤) :
    ¬IsField A

theorem

toValuationSubring_injective

L74 ↗

AlgebraicCurve.Place.toValuationSubring_injective

Source context 6 commands

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

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

Lean source · statement

theorem toValuationSubring_injective :
    Function.Injective (toValuationSubring (K := K) (F := F))

theorem

ext

L79 ↗

AlgebraicCurve.Place.ext

Source context 6 commands

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

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

Lean source · statement

theorem ext {v w : Place K F} (h : v.toValuationSubring = w.toValuationSubring) : v = w

instance

(anonymous instance)

L84 ↗

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

instance : IsPrincipalIdealRing v.toValuationSubring

instance

(anonymous instance)

L86 ↗

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · full declaration

instance : IsDiscreteValuationRing v.toValuationSubring where
  not_a_field' := by
    rw [ne_eq, ← IsLocalRing.isField_iff_maximalIdeal_eq]
    exact ValuationSubring.not_isField_of_ne_top F v.ne_top'

instance

(anonymous instance)

L91 ↗

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

instance : Algebra K v.toValuationSubring

theorem

coe_algebraMap

L94 ↗

AlgebraicCurve.Place.coe_algebraMap

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem coe_algebraMap (a : K) :
    (algebraMap K v.toValuationSubring a : F) = algebraMap K F a

instance

(anonymous instance)

L97 ↗

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

instance : IsScalarTower K v.toValuationSubring F

abbrev

ResidueField

L101 ↗

AlgebraicCurve.Place.ResidueField

Documentation

The residue field of the valuation subring at the place.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

abbrev ResidueField : Type _

def

deg

L104 ↗

AlgebraicCurve.Place.deg

Documentation

The degree of the residue field over the base field.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

def deg : ℕ

class

FiniteResidue

L107 ↗

AlgebraicCurve.Place.FiniteResidue

Documentation

The residue field at a place is a finite module over the base field.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · full declaration

class FiniteResidue : Prop where
  /-- Finiteness of the residue field as a module over the base field. -/
  finite : Module.Finite K v.ResidueField

def

heightOneSpectrum

L112 ↗

AlgebraicCurve.Place.heightOneSpectrum

Documentation

The maximal ideal of the discrete valuation ring, viewed as a height-one prime.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

def heightOneSpectrum : HeightOneSpectrum v.toValuationSubring

theorem

heightOneSpectrum_asIdeal

L115 ↗

AlgebraicCurve.Place.heightOneSpectrum_asIdeal

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem heightOneSpectrum_asIdeal :
    v.heightOneSpectrum.asIdeal = IsLocalRing.maximalIdeal v.toValuationSubring

def

adicValuation

L119 ↗

AlgebraicCurve.Place.adicValuation

Documentation

The multiplicative discrete valuation associated with the place.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

def adicValuation : Valuation F ℤᵐ⁰

theorem

adicValuation_ne_zero

L121 ↗

AlgebraicCurve.Place.adicValuation_ne_zero

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem adicValuation_ne_zero {f : F} (hf : f ≠ 0) : v.adicValuation f ≠ 0

theorem

adicValuation_coe

L124 ↗

AlgebraicCurve.Place.adicValuation_coe

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem adicValuation_coe (a : v.toValuationSubring) :
    v.adicValuation (a : F) = v.heightOneSpectrum.intValuation a

theorem

adicValuation_coe_eq_one_iff

L128 ↗

AlgebraicCurve.Place.adicValuation_coe_eq_one_iff

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem adicValuation_coe_eq_one_iff (a : v.toValuationSubring) :
    v.adicValuation (a : F) = 1 ↔ IsUnit a

theorem

adicValuation_coe_irreducible

L133 ↗

AlgebraicCurve.Place.adicValuation_coe_irreducible

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem adicValuation_coe_irreducible {π : v.toValuationSubring} (hπ : Irreducible π) :
    v.adicValuation (π : F) = exp (-1 : ℤ)

def

ord

L140 ↗

AlgebraicCurve.Place.ord

Documentation

The additive valuation order of an element, with order zero assigned to zero.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

def ord (f : F) : ℤ

theorem

ord_zero

L142 ↗

AlgebraicCurve.Place.ord_zero

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem ord_zero : v.ord (0 : F) = 0

theorem

ord_one

L144 ↗

AlgebraicCurve.Place.ord_one

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem ord_one : v.ord (1 : F) = 0

theorem

ord_mul

L146 ↗

AlgebraicCurve.Place.ord_mul

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem ord_mul {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) :
    v.ord (f * g) = v.ord f + v.ord g

theorem

ord_inv

L152 ↗

AlgebraicCurve.Place.ord_inv

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem ord_inv (f : F) : v.ord f⁻¹ = -v.ord f

theorem

ord_coe_unit

L157 ↗

AlgebraicCurve.Place.ord_coe_unit

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem ord_coe_unit (u : v.toValuationSubringˣ) :
    v.ord ((u : v.toValuationSubring) : F) = 0

theorem

ord_coe_irreducible

L161 ↗

AlgebraicCurve.Place.ord_coe_irreducible

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem ord_coe_irreducible {π : v.toValuationSubring} (hπ : Irreducible π) :
    v.ord (π : F) = 1

theorem

ord_zpow

L165 ↗

AlgebraicCurve.Place.ord_zpow

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem ord_zpow (f : F) (n : ℤ) : v.ord (f ^ n) = n * v.ord f

theorem

ord_unit_smul_zpow

L169 ↗

AlgebraicCurve.Place.ord_unit_smul_zpow

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem ord_unit_smul_zpow (u : v.toValuationSubringˣ) {π : v.toValuationSubring}
    (hπ : Irreducible π) (n : ℤ) :
    v.ord (((u : v.toValuationSubring) : F) * ((π : F) ^ n)) = n

theorem

exists_unit_mul_zpow

L179 ↗

AlgebraicCurve.Place.exists_unit_mul_zpow

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable (v : Place K F)

Lean source · statement

theorem exists_unit_mul_zpow {f : F} (hf : f ≠ 0) {π : v.toValuationSubring}
    (hπ : Irreducible π) :
    ∃ u : v.toValuationSubringˣ,
      f = ((u : v.toValuationSubring) : F) * ((π : F) ^ (v.ord f))

abbrev

Divisor

L196 ↗

AlgebraicCurve.Divisor

Documentation

A divisor is a finitely supported integer-valued function on places.

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev Divisor : Type _

def

degree

L203 ↗

AlgebraicCurve.Divisor.degree

Documentation

The degree homomorphism, weighting each coefficient by its residue-field degree.

Source context 6 commands

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

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

Lean source · statement

def degree : Divisor K F →+ ℤ

theorem

degree_single

L206 ↗

AlgebraicCurve.Divisor.degree_single

Source context 6 commands

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

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

Lean source · statement

theorem degree_single (v : Place K F) (n : ℤ) :
    degree (Finsupp.single v n) = n * v.deg

def

degZero

L211 ↗

AlgebraicCurve.Divisor.degZero

Documentation

The subgroup of divisors with degree zero.

Source context 6 commands

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

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

Lean source · statement

def degZero : AddSubgroup (Divisor K F)

theorem

mem_degZero

L213 ↗

AlgebraicCurve.Divisor.mem_degZero

Source context 6 commands

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

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

Lean source · statement

theorem mem_degZero {D : Divisor K F} : D ∈ degZero (K := K) (F := F) ↔ degree D = 0

def

IsPrincipal

L217 ↗

AlgebraicCurve.Divisor.IsPrincipal

Documentation

A divisor is principal if its coefficients are the orders of one nonzero function.

Source context 6 commands

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

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

Lean source · statement

def IsPrincipal (D : Divisor K F) : Prop

def

principal

L220 ↗

AlgebraicCurve.Divisor.principal

Documentation

The additive subgroup of principal divisors.

Source context 6 commands

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

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

Lean source · full declaration

def principal : AddSubgroup (Divisor K F) where
  carrier := {D | IsPrincipal D}
  zero_mem' := ⟨1, one_ne_zero, fun v => by simp⟩
  add_mem' := by
    rintro D E ⟨f, hf, hD⟩ ⟨g, hg, hE⟩
    exact ⟨f * g, mul_ne_zero hf hg, fun v => by
      rw [Finsupp.add_apply, hD v, hE v, v.ord_mul hf hg]⟩
  neg_mem' := by
    rintro D ⟨f, hf, hD⟩
    exact ⟨f⁻¹, inv_ne_zero hf, fun v => by
      rw [Finsupp.neg_apply, hD v, v.ord_inv]⟩

theorem

mem_principal

L232 ↗

AlgebraicCurve.Divisor.mem_principal

Source context 6 commands

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

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

Lean source · statement

theorem mem_principal {D : Divisor K F} :
    D ∈ principal (K := K) (F := F) ↔ IsPrincipal D

class

HasPrincipalDivisors

L238 ↗

AlgebraicCurve.HasPrincipalDivisors

Documentation

Nonzero functions have finitely supported principal divisors of degree zero.

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · full declaration

class HasPrincipalDivisors : Prop where
  /-- A nonzero function admits a divisor with its valuation orders and with degree zero. -/
  exists_divisor : ∀ f : F, f ≠ 0 → ∃ D : Divisor K F,
    (∀ v : Place K F, D v = v.ord f) ∧ Divisor.degree D = 0

abbrev

Pic

L244 ↗

AlgebraicCurve.Pic

Documentation

The divisor class group, obtained by quotienting divisors by principal divisors.

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev Pic : Type _

abbrev

Pic0

L247 ↗

AlgebraicCurve.Pic0

Documentation

Degree-zero divisors modulo the principal divisors lying in the degree-zero subgroup.

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev Pic0 : Type _

def

mk

L256 ↗

AlgebraicCurve.Pic0.mk

Documentation

The quotient map from degree-zero divisors to their divisor classes.

Source context 6 commands

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

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

Lean source · statement

def mk (D : Divisor.degZero (K := K) (F := F)) : Pic0 K F

theorem

mk_surjective

L258 ↗

AlgebraicCurve.Pic0.mk_surjective

Source context 6 commands

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

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

Lean source · statement

theorem mk_surjective : Function.Surjective (mk (K := K) (F := F))

theorem

mk_add

L261 ↗

AlgebraicCurve.Pic0.mk_add

Source context 6 commands

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

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

Lean source · statement

theorem mk_add (D E : Divisor.degZero (K := K) (F := F)) : mk (D + E) = mk D + mk E

theorem

mk_zero

L263 ↗

AlgebraicCurve.Pic0.mk_zero

Source context 6 commands

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

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

Lean source · statement

theorem mk_zero : mk (0 : Divisor.degZero (K := K) (F := F)) = 0

def

torsion

L267 ↗

AlgebraicCurve.Pic0.torsion

Documentation

The subgroup of degree-zero divisor classes annihilated by n.

Source context 7 commands

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

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

Lean source · statement

def torsion (n : ℕ) : AddSubgroup (Pic0 K F)

theorem

mem_torsion

L270 ↗

AlgebraicCurve.Pic0.mem_torsion

Source context 7 commands

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

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

Lean source · statement

theorem mem_torsion {n : ℕ} {x : Pic0 K F} : x ∈ torsion K F n ↔ (n : ℤ) • x = 0

def

AbelJacobiCard

L276 ↗

AlgebraicCurve.AbelJacobiCard

Documentation

The prescribed cardinalities of the prime-power torsion subgroups of Pic0.

Source context 4 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · statement

def AbelJacobiCard (p : ℕ) (g : ℕ) : Prop

def

smulRingEquiv

L287 ↗

AlgebraicCurve.Place.smulRingEquiv

Documentation

Restrict a field automorphism to the corresponding transported valuation subring.

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
open scoped Pointwise
variable {K F}
variable (σ : F ≃ₐ[K] F)

Lean source · full declaration

def smulRingEquiv (A : ValuationSubring F) : A ≃+* (σ • A : ValuationSubring F) where
  toFun x := ⟨σ x, by
    simpa [AlgEquiv.smul_def] using
      ValuationSubring.smul_mem_pointwise_smul σ (x : F) A x.2⟩
  invFun y := ⟨σ.symm y, by
    have := (ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem (g := σ)
      (S := A) (x := (y : F))).mp y.2
    simpa [AlgEquiv.smul_def, AlgEquiv.aut_inv] using this⟩
  left_inv x := by ext; simp
  right_inv y := by ext; simp
  map_mul' x y := by ext; simp
  map_add' x y := by ext; simp

theorem

coe_smulRingEquiv_apply

L300 ↗

AlgebraicCurve.Place.coe_smulRingEquiv_apply

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
open scoped Pointwise
variable {K F}
variable (σ : F ≃ₐ[K] F)

Lean source · statement

theorem coe_smulRingEquiv_apply (A : ValuationSubring F) (x : A) :
    ((smulRingEquiv σ A x : (σ • A : ValuationSubring F)) : F) = σ x

theorem

pointwise_smul_top

L303 ↗

ValuationSubring.pointwise_smul_top

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
open scoped Pointwise
variable {K F}
variable (σ : F ≃ₐ[K] F)

Lean source · statement

theorem _root_.ValuationSubring.pointwise_smul_top :
    σ • (⊤ : ValuationSubring F) = ⊤

instance

(anonymous instance)

L309 ↗

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
open scoped Pointwise
variable {K F}
variable (σ : F ≃ₐ[K] F)

Lean source · full declaration

instance : SMul (F ≃ₐ[K] F) (Place K F) where
  smul σ v :=
    { toValuationSubring := σ • v.toValuationSubring
      algebraMap_mem' := fun a => by
        have h := ValuationSubring.smul_mem_pointwise_smul σ (algebraMap K F a)
          v.toValuationSubring (v.algebraMap_mem' a)
        rwa [AlgEquiv.smul_def, σ.commutes] at h
      ne_top' := fun h => v.ne_top' <| by
        have := congrArg (σ⁻¹ • ·) h
        simpa [ValuationSubring.pointwise_smul_top] using this
      isPrincipalIdealRing' :=
        IsPrincipalIdealRing.of_surjective
          (smulRingEquiv σ v.toValuationSubring : _ ≃+* _)
          (smulRingEquiv σ v.toValuationSubring).surjective }

theorem

smul_toValuationSubring

L327 ↗

AlgebraicCurve.Place.smul_toValuationSubring

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
open scoped Pointwise
variable {K F}
variable (σ : F ≃ₐ[K] F)
variable (v : Place K F)

Lean source · statement

theorem smul_toValuationSubring : (σ • v).toValuationSubring = σ • v.toValuationSubring

instance

(anonymous instance)

L329 ↗

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
open scoped Pointwise
variable {K F}
variable (σ : F ≃ₐ[K] F)
variable (v : Place K F)

Lean source · full declaration

instance : MulAction (F ≃ₐ[K] F) (Place K F) where
  one_smul v := by
    ext1
    rw [smul_toValuationSubring, one_smul]
  mul_smul σ τ v := by
    ext1
    simp only [smul_toValuationSubring]
    rw [mul_smul]

theorem

ord_smul

L338 ↗

AlgebraicCurve.Place.ord_smul

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
open scoped Pointwise
variable {K F}
variable (σ : F ≃ₐ[K] F)
variable (v : Place K F)

Lean source · statement

theorem ord_smul (f : F) : (σ • v).ord (σ f) = v.ord f

def

smulResidueAlgEquiv

L358 ↗

AlgebraicCurve.Place.smulResidueAlgEquiv

Documentation

The residue-field algebra equivalence induced by a field automorphism of a place.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
open scoped Pointwise
variable {K F}
variable (σ : F ≃ₐ[K] F)
variable (v : Place K F)

Lean source · statement

def smulResidueAlgEquiv : v.ResidueField ≃ₐ[K] (σ • v).ResidueField

theorem

deg_smul

L370 ↗

AlgebraicCurve.Place.deg_smul

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
open scoped Pointwise
variable {K F}
variable (σ : F ≃ₐ[K] F)
variable (v : Place K F)

Lean source · statement

theorem deg_smul : (σ • v).deg = v.deg

instance

(anonymous instance)

L381 ↗

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Divisor
open scoped Pointwise
variable {K F}

Lean source · statement

instance : DistribMulAction (F ≃ₐ[K] F) (Divisor K F)

theorem

smul_def

L383 ↗

AlgebraicCurve.Divisor.smul_def

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Divisor
open scoped Pointwise
variable {K F}

Lean source · statement

theorem smul_def (σ : F ≃ₐ[K] F) (D : Divisor K F) :
    σ • D = Finsupp.mapDomain (σ • ·) D

theorem

smul_single

L386 ↗

AlgebraicCurve.Divisor.smul_single

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Divisor
open scoped Pointwise
variable {K F}

Lean source · statement

theorem smul_single (σ : F ≃ₐ[K] F) (v : Place K F) (n : ℤ) :
    σ • Finsupp.single v n = Finsupp.single (σ • v) n

theorem

smul_apply_smul

L390 ↗

AlgebraicCurve.Divisor.smul_apply_smul

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Divisor
open scoped Pointwise
variable {K F}

Lean source · statement

theorem smul_apply_smul (σ : F ≃ₐ[K] F) (D : Divisor K F) (v : Place K F) :
    (σ • D) (σ • v) = D v

theorem

smul_apply

L395 ↗

AlgebraicCurve.Divisor.smul_apply

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Divisor
open scoped Pointwise
variable {K F}

Lean source · statement

theorem smul_apply (σ : F ≃ₐ[K] F) (D : Divisor K F) (w : Place K F) :
    (σ • D) w = D (σ⁻¹ • w)

theorem

degree_smul

L400 ↗

AlgebraicCurve.Divisor.degree_smul

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Divisor
open scoped Pointwise
variable {K F}

Lean source · statement

theorem degree_smul (σ : F ≃ₐ[K] F) (D : Divisor K F) : degree (σ • D) = degree D

theorem

smul_mem_degZero

L407 ↗

AlgebraicCurve.Divisor.smul_mem_degZero

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Divisor
open scoped Pointwise
variable {K F}

Lean source · statement

theorem smul_mem_degZero (σ : F ≃ₐ[K] F) {D : Divisor K F}
    (hD : D ∈ degZero (K := K) (F := F)) : σ • D ∈ degZero (K := K) (F := F)

theorem

smul_mem_principal

L411 ↗

AlgebraicCurve.Divisor.smul_mem_principal

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Divisor
open scoped Pointwise
variable {K F}

Lean source · statement

theorem smul_mem_principal (σ : F ≃ₐ[K] F) {D : Divisor K F}
    (hD : D ∈ principal (K := K) (F := F)) : σ • D ∈ principal (K := K) (F := F)

def

degZeroSMulHom

L429 ↗

AlgebraicCurve.Pic0.degZeroSMulHom

Documentation

The additive action of a field automorphism restricted to degree-zero divisors.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Pic0
open scoped Pointwise
variable {K F}

Lean source · statement

def degZeroSMulHom (σ : F ≃ₐ[K] F) :
    Divisor.degZero (K := K) (F := F) →+ Divisor.degZero (K := K) (F := F)

theorem

coe_degZeroSMulHom

L435 ↗

AlgebraicCurve.Pic0.coe_degZeroSMulHom

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Pic0
open scoped Pointwise
variable {K F}

Lean source · statement

theorem coe_degZeroSMulHom (σ : F ≃ₐ[K] F) (D : Divisor.degZero (K := K) (F := F)) :
    (degZeroSMulHom σ D : Divisor K F) = σ • (D : Divisor K F)

instance

(anonymous instance)

L438 ↗

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Pic0
open scoped Pointwise
variable {K F}

Lean source · full declaration

instance : SMul (F ≃ₐ[K] F) (Pic0 K F) where
  smul σ := QuotientAddGroup.map _ _ (degZeroSMulHom σ) (by
    rintro ⟨D, hD0⟩ hD
    simp only [AddSubgroup.mem_addSubgroupOf] at hD ⊢
    exact Divisor.smul_mem_principal σ hD)

theorem

smul_mk

L444 ↗

AlgebraicCurve.Pic0.smul_mk

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Pic0
open scoped Pointwise
variable {K F}

Lean source · statement

theorem smul_mk (σ : F ≃ₐ[K] F) (D : Divisor.degZero (K := K) (F := F)) :
    σ • (mk D) = mk (degZeroSMulHom σ D)

instance

(anonymous instance)

L447 ↗

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Pic0
open scoped Pointwise
variable {K F}

Lean source · full declaration

instance : DistribMulAction (F ≃ₐ[K] F) (Pic0 K F) where
  one_smul x := by
    obtain ⟨D, rfl⟩ := mk_surjective x
    rw [smul_mk]
    exact congrArg mk (Subtype.ext (by rw [coe_degZeroSMulHom, one_smul]))
  mul_smul σ τ x := by
    obtain ⟨D, rfl⟩ := mk_surjective x
    rw [smul_mk, smul_mk, smul_mk]
    exact congrArg mk (Subtype.ext (by simp only [coe_degZeroSMulHom]; rw [mul_smul]))
  smul_zero σ := by
    change σ • mk 0 = mk 0
    rw [smul_mk]
    exact congrArg mk (map_zero _)
  smul_add σ x y := by
    obtain ⟨D, rfl⟩ := mk_surjective x
    obtain ⟨E, rfl⟩ := mk_surjective y
    change σ • mk (D + E) = mk (degZeroSMulHom σ D) + mk (degZeroSMulHom σ E)
    rw [smul_mk]
    exact congrArg mk (map_add _ _ _)

theorem

isPrincipalIdealRing_valuationSubring

L475 ↗

AlgebraicCurve.Place.isPrincipalIdealRing_valuationSubring

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
open IsDedekindDomain.HeightOneSpectrum in

Lean source · statement

theorem isPrincipalIdealRing_valuationSubring (w : HeightOneSpectrum R) :
    IsPrincipalIdealRing ((w.valuation F).valuationSubring)

def

ofHeightOneSpectrum

L483 ↗

AlgebraicCurve.Place.ofHeightOneSpectrum

Documentation

Construct a place from the prime-adic valuation of a height-one prime.

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
open IsDedekindDomain.HeightOneSpectrum in

Lean source · full declaration

def ofHeightOneSpectrum [Algebra K R] [IsScalarTower K R F] (w : HeightOneSpectrum R) :
    Place K F where
  toValuationSubring := (w.valuation F).valuationSubring
  algebraMap_mem' := fun a => by
    rw [Valuation.mem_valuationSubring_iff, IsScalarTower.algebraMap_apply K R F]
    exact w.valuation_le_one (algebraMap K R a)
  ne_top' := by
    simp only [ne_eq, Valuation.valuationSubring_eq_top_iff, not_not]
    infer_instance
  isPrincipalIdealRing' := isPrincipalIdealRing_valuationSubring w

theorem

ofHeightOneSpectrum_toValuationSubring

L494 ↗

AlgebraicCurve.Place.ofHeightOneSpectrum_toValuationSubring

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]

Lean source · statement

theorem ofHeightOneSpectrum_toValuationSubring [Algebra K R] [IsScalarTower K R F]
    (w : HeightOneSpectrum R) :
    (ofHeightOneSpectrum (K := K) w).toValuationSubring = (w.valuation F).valuationSubring

Module documentation

Declarations