Module

Maps.lean

Nyll.AlgebraicCurves.Divisors.Maps

71 declarations indexed from sourceView source ↗

Module documentation

Algebra, divisors, and base change

Restriction of places and residue fields, ramification indices, and divisor pullback and pushforward over field extensions.

Imports6

Nyll.AlgebraicCurves.Divisors.ClassGroup
Mathlib.RingTheory.Valuation.LocalSubring
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.Norm.Basic
Mathlib.LinearAlgebra.Dimension.Free

Imported by136

theorem

ord_nonneg_of_mem

L39 ↗

AlgebraicCurve.Place.ord_nonneg_of_mem

Source context 6 commands

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

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

Lean source · statement

theorem ord_nonneg_of_mem {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f

theorem

mem_of_ord_nonneg

L54 ↗

AlgebraicCurve.Place.mem_of_ord_nonneg

Source context 6 commands

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

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

Lean source · statement

theorem mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring

theorem

mem_iff_ord_nonneg

L62 ↗

AlgebraicCurve.Place.mem_iff_ord_nonneg

Source context 6 commands

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

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

Lean source · statement

theorem mem_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f

theorem

exists_ord_pos

L66 ↗

AlgebraicCurve.Place.exists_ord_pos

Source context 6 commands

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

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

Lean source · statement

theorem exists_ord_pos : ∃ f : F, f ≠ 0 ∧ 0 < v.ord f

theorem

algebraMap_ne_zero

L80 ↗

AlgebraicCurve.Place.algebraMap_ne_zero

Source context 6 commands

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

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

Lean source · statement

theorem algebraMap_ne_zero {f : F} (hf : f ≠ 0) : algebraMap F F' f ≠ 0

theorem

comap_algebraMap_ne_top

L85 ↗

AlgebraicCurve.Place.comap_algebraMap_ne_top

Source context 7 commands

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

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

Lean source · statement

theorem comap_algebraMap_ne_top [Algebra.IsIntegral F F'] :
    w.toValuationSubring.comap (algebraMap F F') ≠ ⊤

theorem

mem_comap_iff_ord_nonneg

L102 ↗

AlgebraicCurve.Place.mem_comap_iff_ord_nonneg

Source context 8 commands

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

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

Lean source · statement

theorem mem_comap_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ w.toValuationSubring.comap (algebraMap F F') ↔
      0 ≤ w.ord (algebraMap F F' f)

theorem

isUnit_mk_comap_iff

L109 ↗

AlgebraicCurve.Place.isUnit_mk_comap_iff

Source context 9 commands

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

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

Lean source · statement

theorem isUnit_mk_comap_iff {f : F} (hf : f ≠ 0)
    (hmem : f ∈ w.toValuationSubring.comap (algebraMap F F')) :
    IsUnit (⟨f, hmem⟩ : w.toValuationSubring.comap (algebraMap F F')) ↔
      w.ord (algebraMap F F' f) = 0

theorem

exists_ord_algebraMap_pos

L134 ↗

AlgebraicCurve.Place.exists_ord_algebraMap_pos

Source context 9 commands

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

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

Lean source · statement

theorem exists_ord_algebraMap_pos [Algebra.IsIntegral F F'] :
    ∃ f : F, f ≠ 0 ∧ 0 < w.ord (algebraMap F F' f)

def

ramificationIndex

L149 ↗

AlgebraicCurve.Place.ramificationIndex

Documentation

The least positive order attained by a nonzero function from the base field.

Source context 9 commands

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

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

Lean source · statement

def ramificationIndex (F : Type*) [Field F] [Algebra F F'] : ℕ

theorem

ramificationIndex_le_ord

L152 ↗

AlgebraicCurve.Place.ramificationIndex_le_ord

Source context 9 commands

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

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

Lean source · statement

theorem ramificationIndex_le_ord {f : F} (hf : f ≠ 0)
    (hpos : 0 < w.ord (algebraMap F F' f)) :
    (ramificationIndex (F := F) w : ℤ) ≤ w.ord (algebraMap F F' f)

theorem

ramificationIndex_set_nonempty

L163 ↗

AlgebraicCurve.Place.ramificationIndex_set_nonempty

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']

Lean source · statement

theorem ramificationIndex_set_nonempty :
    {n : ℕ | 0 < n ∧ ∃ f : F, f ≠ 0 ∧ w.ord (algebraMap F F' f) = n}.Nonempty

theorem

ramificationIndex_pos

L168 ↗

AlgebraicCurve.Place.ramificationIndex_pos

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']

Lean source · statement

theorem ramificationIndex_pos : 0 < ramificationIndex (F := F) w

theorem

exists_ord_eq_ramificationIndex

L171 ↗

AlgebraicCurve.Place.exists_ord_eq_ramificationIndex

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']

Lean source · statement

theorem exists_ord_eq_ramificationIndex :
    ∃ f : F, f ≠ 0 ∧ w.ord (algebraMap F F' f) = ramificationIndex (F := F) w

theorem

ramificationIndex_dvd_ord

L175 ↗

AlgebraicCurve.Place.ramificationIndex_dvd_ord

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']

Lean source · statement

theorem ramificationIndex_dvd_ord {f : F} (hf : f ≠ 0) :
    (ramificationIndex (F := F) w : ℤ) ∣ w.ord (algebraMap F F' f)

theorem

irreducible_mk_comap

L203 ↗

AlgebraicCurve.Place.irreducible_mk_comap

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']

Lean source · statement

theorem irreducible_mk_comap {g : F} (hg0 : g ≠ 0)
    (hmem : g ∈ w.toValuationSubring.comap (algebraMap F F'))
    (hge : w.ord (algebraMap F F' g) = ramificationIndex (F := F) w) :
    Irreducible (⟨g, hmem⟩ : w.toValuationSubring.comap (algebraMap F F'))

theorem

isPrincipalIdealRing_comap

L234 ↗

AlgebraicCurve.Place.isPrincipalIdealRing_comap

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']

Lean source · statement

theorem isPrincipalIdealRing_comap :
    IsPrincipalIdealRing (w.toValuationSubring.comap (algebraMap F F'))

def

restrict

L283 ↗

AlgebraicCurve.Place.restrict

Documentation

The place obtained by comapping the valuation ring along the field inclusion.

Source context 13 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']
section RestrictDef
variable [Algebra K F] [IsScalarTower K F F']
variable (F) in

Lean source · full declaration

def restrict : Place K F where
  toValuationSubring := w.toValuationSubring.comap (algebraMap F F')
  algebraMap_mem' a := by
    rw [ValuationSubring.mem_comap, ← IsScalarTower.algebraMap_apply]
    exact w.algebraMap_mem' a
  ne_top' := w.comap_algebraMap_ne_top
  isPrincipalIdealRing' := w.isPrincipalIdealRing_comap

theorem

restrict_toValuationSubring

L291 ↗

AlgebraicCurve.Place.restrict_toValuationSubring

Source context 13 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']
section RestrictDef
variable [Algebra K F] [IsScalarTower K F F']
variable (F) in

Lean source · statement

theorem restrict_toValuationSubring :
    (w.restrict F).toValuationSubring = w.toValuationSubring.comap (algebraMap F F')

theorem

mem_restrict_iff

L294 ↗

AlgebraicCurve.Place.mem_restrict_iff

Source context 13 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']
section RestrictDef
variable [Algebra K F] [IsScalarTower K F F']
variable (F) in

Lean source · statement

theorem mem_restrict_iff {f : F} :
    f ∈ (w.restrict F).toValuationSubring ↔ algebraMap F F' f ∈ w.toValuationSubring

theorem

ord_restrict

L298 ↗

AlgebraicCurve.Place.ord_restrict

Source context 13 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']
section RestrictDef
variable [Algebra K F] [IsScalarTower K F F']
variable (F) in

Lean source · statement

theorem ord_restrict (f : F) :
    w.ord (algebraMap F F' f) = ramificationIndex (F := F) w * (w.restrict F).ord f

theorem

ord_algebraMap_ne_zero_of_restrict_eq

L329 ↗

AlgebraicCurve.Place.ord_algebraMap_ne_zero_of_restrict_eq

Source context 13 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']
section RestrictDef
variable [Algebra K F] [IsScalarTower K F F']
variable (F) in

Lean source · statement

theorem ord_algebraMap_ne_zero_of_restrict_eq {v : Place K F} {f : F}
    (hford : v.ord f ≠ 0) (hw : w.restrict F = v) :
    w.ord (algebraMap F F' f) ≠ 0

theorem

restrict_fiber_finite

L336 ↗

AlgebraicCurve.Place.restrict_fiber_finite

Source context 13 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
namespace Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in
variable {w} in
variable [Algebra.IsIntegral F F']
section RestrictDef
variable [Algebra K F] [IsScalarTower K F F']
variable (F) in

Lean source · statement

theorem restrict_fiber_finite [HasPrincipalDivisors K F'] (v : Place K F) :
    {w : Place K F' | w.restrict F = v}.Finite

def

restrictInclusion

L370 ↗

AlgebraicCurve.Place.restrictInclusion

Documentation

The inclusion of the restricted valuation ring into the original valuation ring.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (w : Place K F')
variable (F) in

Lean source · full declaration

def restrictInclusion : (w.restrict F).toValuationSubring →+* w.toValuationSubring where
  toFun a := ⟨algebraMap F F' (a : F), ValuationSubring.mem_comap.mp a.2⟩
  map_one' := Subtype.ext (map_one (algebraMap F F'))
  map_mul' a b := Subtype.ext (map_mul (algebraMap F F') (a : F) (b : F))
  map_zero' := Subtype.ext (map_zero (algebraMap F F'))
  map_add' a b := Subtype.ext (map_add (algebraMap F F') (a : F) (b : F))

theorem

coe_restrictInclusion

L377 ↗

AlgebraicCurve.Place.coe_restrictInclusion

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (w : Place K F')
variable (F) in

Lean source · statement

theorem coe_restrictInclusion (a : (w.restrict F).toValuationSubring) :
    ((restrictInclusion F w a : w.toValuationSubring) : F') = algebraMap F F' (a : F)

instance

instIsLocalHomRestrictInclusion

L380 ↗

AlgebraicCurve.Place.instIsLocalHomRestrictInclusion

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (w : Place K F')
variable (F) in

Lean source · full declaration

instance instIsLocalHomRestrictInclusion : IsLocalHom (restrictInclusion F w) where
  map_nonunit a ha := by
    have hord : w.ord (algebraMap F F' (a : F)) = 0 := by
      have h := w.ord_coe_unit ha.unit
      rwa [IsUnit.unit_spec, coe_restrictInclusion] at h
    have ha0 : (a : F) ≠ 0 := by
      rintro h0
      obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.mp ha
      have hb' : algebraMap F F' (a : F) * (b : F') = 1 := congrArg Subtype.val hb
      rw [h0, map_zero, zero_mul] at hb'
      exact zero_ne_one hb'
    exact (isUnit_mk_comap_iff ha0 a.2).mpr hord

def

restrictResidueMap

L395 ↗

AlgebraicCurve.Place.restrictResidueMap

Documentation

The residue-field map induced by the inclusion of the restricted valuation ring.

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (w : Place K F')
variable (F) in
variable (F) in

Lean source · statement

def restrictResidueMap : (w.restrict F).ResidueField →+* w.ResidueField

theorem

restrictResidueMap_residue

L398 ↗

AlgebraicCurve.Place.restrictResidueMap_residue

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (w : Place K F')
variable (F) in
variable (F) in

Lean source · statement

theorem restrictResidueMap_residue (a : (w.restrict F).toValuationSubring) :
    restrictResidueMap F w (IsLocalRing.residue _ a) =
      IsLocalRing.residue _ (restrictInclusion F w a)

instance

instAlgebraResidueFieldRestrictPushforward

L403 ↗

AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (w : Place K F')
variable (F) in
variable (F) in

Lean source · statement

instance instAlgebraResidueFieldRestrictPushforward :
    Algebra (w.restrict F).ResidueField w.ResidueField

theorem

algebraMap_residueField_eq

L407 ↗

AlgebraicCurve.Place.algebraMap_residueField_eq

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (w : Place K F')
variable (F) in
variable (F) in

Lean source · statement

theorem algebraMap_residueField_eq :
    algebraMap (w.restrict F).ResidueField w.ResidueField = restrictResidueMap F w

instance

instIsScalarTowerResidueFieldRestrictPushforward

L410 ↗

AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (w : Place K F')
variable (F) in
variable (F) in

Lean source · statement

instance instIsScalarTowerResidueFieldRestrictPushforward :
    IsScalarTower K (w.restrict F).ResidueField w.ResidueField

def

inertiaDeg

L423 ↗

AlgebraicCurve.Place.inertiaDeg

Documentation

The finrank of the residue-field extension over the restricted place.

Source context 11 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (w : Place K F')
variable (F) in
variable (F) in
variable (F) in

Lean source · statement

def inertiaDeg : ℕ

theorem

deg_restrict_mul_inertiaDeg

L425 ↗

AlgebraicCurve.Place.deg_restrict_mul_inertiaDeg

Source context 11 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
namespace Place
variable (w : Place K F')
variable (F) in
variable (F) in
variable (F) in

Lean source · statement

theorem deg_restrict_mul_inertiaDeg : (w.restrict F).deg * w.inertiaDeg F = w.deg

def

mapRestrict

L435 ↗

AlgebraicCurve.Divisor.mapRestrict

Documentation

The divisor homomorphism that sends each place to its restriction, preserving its coefficient.

Source context 8 commands

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

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

Lean source · statement

def mapRestrict : Divisor K F' →+ Divisor K F

theorem

mapRestrict_single

L438 ↗

AlgebraicCurve.Divisor.mapRestrict_single

Source context 8 commands

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

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

Lean source · statement

theorem mapRestrict_single (w : Place K F') (n : ℤ) :
    mapRestrict F (Finsupp.single w n) = Finsupp.single (w.restrict F) n

def

pushforward

L444 ↗

AlgebraicCurve.Divisor.pushforward

Documentation

Divisor pushforward, multiplying each coefficient by its residue-field inertia degree.

Source context 9 commands

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

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

Lean source · statement

def pushforward : Divisor K F' →+ Divisor K F

theorem

pushforward_single

L448 ↗

AlgebraicCurve.Divisor.pushforward_single

Source context 9 commands

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

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

Lean source · statement

theorem pushforward_single (w : Place K F') (n : ℤ) :
    pushforward F (Finsupp.single w n) =
      Finsupp.single (w.restrict F) (n * w.inertiaDeg F)

theorem

degree_pushforward

L453 ↗

AlgebraicCurve.Divisor.degree_pushforward

Source context 9 commands

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

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

Lean source · statement

theorem degree_pushforward (D : Divisor K F') :
    degree (pushforward F D) = degree D

theorem

pushforward_mem_degZero

L463 ↗

AlgebraicCurve.Divisor.pushforward_mem_degZero

Source context 9 commands

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

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

Lean source · statement

theorem pushforward_mem_degZero {D : Divisor K F'} (hD : D ∈ degZero (K := K) (F := F')) :
    pushforward F D ∈ degZero (K := K) (F := F)

theorem

pushforward_apply

L467 ↗

AlgebraicCurve.Divisor.pushforward_apply

Source context 9 commands

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

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

Lean source · full declaration

theorem pushforward_apply [DecidableEq (Place K F)] (D : Divisor K F') (v : Place K F) :
    pushforward F D v =
      ∑ w ∈ D.support, if w.restrict F = v then D w * (w.inertiaDeg F : ℤ) else 0 := by
  classical
  rw [pushforward, Finsupp.liftAddHom_apply, Finsupp.sum_apply, Finsupp.sum]
  refine Finset.sum_congr rfl fun w _ => ?_
  simp [Finsupp.single_apply]

def

PushforwardNormFormula

L478 ↗

AlgebraicCurve.Divisor.PushforwardNormFormula

Documentation

Pushforward of the order divisor of a nonzero function equals the order divisor of its field norm.

Source context 10 commands

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

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

Lean source · statement

def PushforwardNormFormula [Module.Finite F F'] : Prop

theorem

pushforward_eq_of_normFormula

L482 ↗

AlgebraicCurve.Divisor.pushforward_eq_of_normFormula

Source context 10 commands

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

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

Lean source · statement

theorem pushforward_eq_of_normFormula [Module.Finite F F']
    (H : PushforwardNormFormula K F F') {f : F'} (hf : f ≠ 0)
    {D : Divisor K F'} (hD : ∀ w, D w = w.ord f)
    {E : Divisor K F} (hE : ∀ v, E v = v.ord (Algebra.norm F f)) :
    pushforward F D = E

theorem

isPrincipal_pushforward_of_normFormula

L489 ↗

AlgebraicCurve.Divisor.isPrincipal_pushforward_of_normFormula

Source context 10 commands

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

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

Lean source · statement

theorem isPrincipal_pushforward_of_normFormula [Module.Finite F F']
    (H : PushforwardNormFormula K F F') {D : Divisor K F'} (hD : IsPrincipal D) :
    IsPrincipal (pushforward F D)

def

fiber

L511 ↗

AlgebraicCurve.Place.fiber

Documentation

The finite set of places that restrict to the given base place.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Place
variable (F') in

Lean source · statement

def fiber (v : Place K F) : Finset (Place K F')

theorem

mem_fiber

L514 ↗

AlgebraicCurve.Place.mem_fiber

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Place
variable (F') in

Lean source · statement

theorem mem_fiber {v : Place K F} {w : Place K F'} :
    w ∈ v.fiber F' ↔ w.restrict F = v

theorem

restrict_mem_fiber

L518 ↗

AlgebraicCurve.Place.restrict_mem_fiber

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Place
variable (F') in

Lean source · statement

theorem restrict_mem_fiber (w : Place K F') : w ∈ (w.restrict F).fiber F'

def

pullbackSingleHom

L527 ↗

AlgebraicCurve.Divisor.pullbackSingleHom

Documentation

Pullback of a single place divisor, weighted by the ramification indices of its fibre.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Divisor
variable (F') in

Lean source · full declaration

def pullbackSingleHom (v : Place K F) : ℤ →+ Divisor K F' where
  toFun n := ∑ w ∈ v.fiber F', Finsupp.single w (n * w.ramificationIndex F)
  map_zero' := by simp
  map_add' m n := by
    rw [← Finset.sum_add_distrib]
    exact Finset.sum_congr rfl fun w _ => by rw [add_mul, Finsupp.single_add]

theorem

pullbackSingleHom_apply

L534 ↗

AlgebraicCurve.Divisor.pullbackSingleHom_apply

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Divisor
variable (F') in

Lean source · statement

theorem pullbackSingleHom_apply (v : Place K F) (n : ℤ) :
    pullbackSingleHom F' v n
      = ∑ w ∈ v.fiber F', Finsupp.single w (n * w.ramificationIndex F)

def

pullback

L541 ↗

AlgebraicCurve.Divisor.pullback

Documentation

The additive divisor pullback obtained by extending pullback of single place divisors.

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Divisor
variable (F') in
variable (F') in

Lean source · statement

def pullback : Divisor K F →+ Divisor K F'

theorem

pullback_single

L544 ↗

AlgebraicCurve.Divisor.pullback_single

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Divisor
variable (F') in
variable (F') in

Lean source · statement

theorem pullback_single (v : Place K F) (n : ℤ) :
    pullback F' (Finsupp.single v n)
      = ∑ w ∈ v.fiber F', Finsupp.single w (n * w.ramificationIndex F)

theorem

pullback_single_apply_of_restrict_eq

L549 ↗

AlgebraicCurve.Divisor.pullback_single_apply_of_restrict_eq

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Divisor
variable (F') in
variable (F') in

Lean source · statement

theorem pullback_single_apply_of_restrict_eq {v : Place K F} {w : Place K F'}
    (hw : w.restrict F = v) (n : ℤ) :
    pullback F' (Finsupp.single v n) w = n * w.ramificationIndex F

theorem

pullback_single_apply_of_restrict_ne

L559 ↗

AlgebraicCurve.Divisor.pullback_single_apply_of_restrict_ne

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Divisor
variable (F') in
variable (F') in

Lean source · statement

theorem pullback_single_apply_of_restrict_ne {v : Place K F} {w : Place K F'}
    (hw : w.restrict F ≠ v) (n : ℤ) :
    pullback F' (Finsupp.single v n) w = 0

theorem

pullback_apply

L566 ↗

AlgebraicCurve.Divisor.pullback_apply

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Divisor
variable (F') in
variable (F') in

Lean source · statement

theorem pullback_apply (D : Divisor K F) (w : Place K F') :
    pullback F' D w = w.ramificationIndex F * D (w.restrict F)

theorem

restrict_mem_support_of_mem_support_pullback

L579 ↗

AlgebraicCurve.Divisor.restrict_mem_support_of_mem_support_pullback

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Divisor
variable (F') in
variable (F') in

Lean source · statement

theorem restrict_mem_support_of_mem_support_pullback {D : Divisor K F} {w : Place K F'}
    (hw : w ∈ (pullback F' D).support) : w.restrict F ∈ D.support

theorem

pullback_apply_eq_ord

L585 ↗

AlgebraicCurve.Divisor.pullback_apply_eq_ord

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Divisor
variable (F') in
variable (F') in

Lean source · statement

theorem pullback_apply_eq_ord {f : F} {D : Divisor K F}
    (hD : ∀ v : Place K F, D v = v.ord f) (w : Place K F') :
    pullback F' D w = w.ord (algebraMap F F' f)

theorem

isPrincipal_pullback

L590 ↗

AlgebraicCurve.Divisor.isPrincipal_pullback

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Divisor
variable (F') in
variable (F') in

Lean source · statement

theorem isPrincipal_pullback {D : Divisor K F} (hD : D.IsPrincipal) :
    (pullback F' D).IsPrincipal

theorem

pullback_mem_principal

L595 ↗

AlgebraicCurve.Divisor.pullback_mem_principal

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
namespace Divisor
variable (F') in
variable (F') in

Lean source · statement

theorem pullback_mem_principal {D : Divisor K F} (hD : D ∈ principal (K := K) (F := F)) :
    pullback F' D ∈ principal (K := K) (F := F')

class

FundamentalIdentity

L604 ↗

AlgebraicCurve.FundamentalIdentity

Documentation

The ramification-weighted sum of degrees over a place fibre equals the extension degree times the base-place degree.

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · full declaration

class FundamentalIdentity : Prop where
  /-- The degree-weighted ramification sum over every place fibre. -/
  sum_ramificationIndex_mul_deg : ∀ v : Place K F,
    ∑ w ∈ v.fiber F', (w.ramificationIndex F : ℤ) * (w.deg : ℤ)
      = (Module.finrank F F' : ℤ) * (v.deg : ℤ)

theorem

degree_pullback_single

L612 ↗

AlgebraicCurve.Divisor.degree_pullback_single

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in
namespace Divisor

Lean source · statement

theorem degree_pullback_single [FundamentalIdentity K F F'] (v : Place K F) (n : ℤ) :
    degree (pullback F' (Finsupp.single v n))
      = (Module.finrank F F' : ℤ) * degree (Finsupp.single v n)

theorem

degree_pullback

L621 ↗

AlgebraicCurve.Divisor.degree_pullback

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in
namespace Divisor

Lean source · statement

theorem degree_pullback [FundamentalIdentity K F F'] (D : Divisor K F) :
    degree (pullback F' D) = (Module.finrank F F' : ℤ) * degree D

theorem

pullback_mem_degZero

L628 ↗

AlgebraicCurve.Divisor.pullback_mem_degZero

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in
namespace Divisor

Lean source · statement

theorem pullback_mem_degZero [FundamentalIdentity K F F'] {D : Divisor K F}
    (hD : D ∈ degZero (K := K) (F := F)) :
    pullback F' D ∈ degZero (K := K) (F := F')

class

SumRamificationInertia

L649 ↗

AlgebraicCurve.SumRamificationInertia

Documentation

The ramification and inertia degree products sum to the field-extension degree over each base place.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · full declaration

class SumRamificationInertia : Prop where
  /-- The sum of ramification indices times inertia degrees over a place fibre. -/
  sum_ramificationIndex_mul_inertiaDeg : ∀ v : Place K F,
    ∑ w ∈ v.fiber F', (w.ramificationIndex F : ℤ) * (w.inertiaDeg F : ℤ)
      = (Module.finrank F F' : ℤ)

instance

instFundamentalIdentityOfSumRamificationInertia

L655 ↗

AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
noncomputable section
namespace AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K F']
variable (K F F') in

Lean source · full declaration

instance (priority := 100) instFundamentalIdentityOfSumRamificationInertia
    [SumRamificationInertia K F F'] : FundamentalIdentity K F F' where
  sum_ramificationIndex_mul_deg v := by
    have key := SumRamificationInertia.sum_ramificationIndex_mul_inertiaDeg
      (K := K) (F := F) (F' := F') v
    calc
      ∑ w ∈ v.fiber F', (w.ramificationIndex F : ℤ) * (w.deg : ℤ)
          = ∑ w ∈ v.fiber F',
              (v.deg : ℤ) * ((w.ramificationIndex F : ℤ) * (w.inertiaDeg F : ℤ)) := by
            refine Finset.sum_congr rfl fun w hw => ?_
            have htower : ((w.restrict F).deg : ℤ) * (w.inertiaDeg F : ℤ) = (w.deg : ℤ) := by
              exact_mod_cast congrArg (Nat.cast (R := ℤ))
                (w.deg_restrict_mul_inertiaDeg (F := F))
            rw [Place.mem_fiber.mp hw] at htower
            rw [← htower]; ring
      _ = (v.deg : ℤ) * ∑ w ∈ v.fiber F',
              (w.ramificationIndex F : ℤ) * (w.inertiaDeg F : ℤ) := by
            rw [Finset.mul_sum]
      _ = (Module.finrank F F' : ℤ) * (v.deg : ℤ) := by rw [key]; ring

def

pullbackDegZeroHom

L679 ↗

AlgebraicCurve.Pic0.pullbackDegZeroHom

Documentation

Divisor pullback restricted to degree-zero divisors.

Source context 11 commands

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

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

Lean source · statement

def pullbackDegZeroHom [FundamentalIdentity K F F'] :
    Divisor.degZero (K := K) (F := F) →+ Divisor.degZero (K := K) (F := F')

theorem

coe_pullbackDegZeroHom

L684 ↗

AlgebraicCurve.Pic0.coe_pullbackDegZeroHom

Source context 11 commands

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

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

Lean source · statement

theorem coe_pullbackDegZeroHom [FundamentalIdentity K F F']
    (D : Divisor.degZero (K := K) (F := F)) :
    (pullbackDegZeroHom F' D : Divisor K F') = Divisor.pullback F' (D : Divisor K F)

def

pullbackHom

L690 ↗

AlgebraicCurve.Pic0.pullbackHom

Documentation

The degree-zero Picard homomorphism induced by divisor pullback.

Source context 12 commands

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

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

Lean source · statement

def pullbackHom [FundamentalIdentity K F F'] : Pic0 K F →+ Pic0 K F'

theorem

pullbackHom_mk

L696 ↗

AlgebraicCurve.Pic0.pullbackHom_mk

Source context 12 commands

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

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

Lean source · statement

theorem pullbackHom_mk [FundamentalIdentity K F F']
    (D : Divisor.degZero (K := K) (F := F)) :
    pullbackHom F' (mk D) = mk (pullbackDegZeroHom F' D)

def

pushforwardDegZeroHom

L702 ↗

AlgebraicCurve.Pic0.pushforwardDegZeroHom

Documentation

Divisor pushforward restricted to degree-zero divisors.

Source context 13 commands

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

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

Lean source · statement

def pushforwardDegZeroHom :
    Divisor.degZero (K := K) (F := F') →+ Divisor.degZero (K := K) (F := F)

theorem

coe_pushforwardDegZeroHom

L709 ↗

AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom

Source context 14 commands

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

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

Lean source · statement

theorem coe_pushforwardDegZeroHom (D : Divisor.degZero (K := K) (F := F')) :
    (pushforwardDegZeroHom F D : Divisor K F) = Divisor.pushforward F (D : Divisor K F')

def

pushforwardHom

L714 ↗

AlgebraicCurve.Pic0.pushforwardHom

Documentation

The degree-zero Picard homomorphism induced by divisor pushforward and the norm formula.

Source context 14 commands

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

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

Lean source · statement

def pushforwardHom [Module.Finite F F'] (H : Divisor.PushforwardNormFormula K F F') :
    Pic0 K F' →+ Pic0 K F

theorem

pushforwardHom_mk

L722 ↗

AlgebraicCurve.Pic0.pushforwardHom_mk

Source context 15 commands

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

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

Lean source · statement

theorem pushforwardHom_mk [Module.Finite F F'] (H : Divisor.PushforwardNormFormula K F F')
    (D : Divisor.degZero (K := K) (F := F')) :
    pushforwardHom K F F' H (mk D) = mk (pushforwardDegZeroHom F D)

Module documentation

Algebra, divisors, and base change

Declarations