Module

Construction.lean

Nyll.AlgebraicCurves.Differentials.Residues.Construction

131 declarations indexed from sourceView source ↗

Module documentation

Results on Construction.

Imports7

Mathlib.RingTheory.AdicCompletion.LocalRing
Mathlib.FieldTheory.RatFunc.Basic
Nyll.AlgebraicCurves.Differentials.Residues.Basic
Nyll.AlgebraicCurves.FunctionFields.CurveOver
Nyll.AlgebraicCurves.Divisors.Maps
Nyll.AlgebraicCurves.Places.Completion
Nyll.AlgebraicCurves.Differentials.Kaehler.Weil

Imported by11

instance

of_perfectField

L31 ↗

AlgebraicCurve.HasSeparableResidue.of_perfectField

Source context 3 commands

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

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

Lean source · full declaration

instance HasSeparableResidue.of_perfectField [PerfectField K]
    [∀ v : Place K F, v.FiniteResidue] : HasSeparableResidue K F where
  trace_ne_zero v :=
    have : Module.Finite K v.ResidueField := Place.FiniteResidue.finite
    Algebra.trace_ne_zero K v.ResidueField

instance

of_perfectField_of_isCurveOver

L37 ↗

AlgebraicCurve.HasSeparableResidue.of_perfectField_of_isCurveOver

Source context 3 commands

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

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

Lean source · statement

instance HasSeparableResidue.of_perfectField_of_isCurveOver [PerfectField K]
    [IsCurveOver K F] : HasSeparableResidue K F

theorem

finiteResidue_of_deg_pos

L116 ↗

AlgebraicCurve.Place.finiteResidue_of_deg_pos

Source context 7 commands

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

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

Lean source · statement

theorem finiteResidue_of_deg_pos (h : 0 < v.deg) : v.FiniteResidue

def

restrictSubringHom

L132 ↗

AlgebraicCurve.Place.restrictSubringHom

Documentation

The valuation-subring homomorphism induced by restricting the place to the smaller field.

Source context 7 commands

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

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

Lean source · statement

def restrictSubringHom : (w.restrict F).toValuationSubring →+* w.toValuationSubring

instance

instIsLocalHom_restrictSubringHom

L138 ↗

AlgebraicCurve.Place.instIsLocalHom_restrictSubringHom

Source context 7 commands

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

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

Lean source · statement

instance instIsLocalHom_restrictSubringHom : IsLocalHom (w.restrictSubringHom (F := F))

def

residueFieldMapRestrict

L158 ↗

AlgebraicCurve.Place.residueFieldMapRestrict

Documentation

The residue-field homomorphism induced by restriction of the valuation subring.

Source context 7 commands

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

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

Lean source · statement

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

instance

instAlgebra_restrictResidueField

L161 ↗

AlgebraicCurve.Place.instAlgebra_restrictResidueField

Source context 7 commands

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

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

Lean source · statement

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

theorem

algebraMap_residueField_residue

L164 ↗

AlgebraicCurve.Place.algebraMap_residueField_residue

Source context 7 commands

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

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

Lean source · statement

theorem algebraMap_residueField_residue (x : (w.restrict F).toValuationSubring) :
    algebraMap (w.restrict F).ResidueField w.ResidueField
        (IsLocalRing.residue _ x)
      = IsLocalRing.residue _ (w.restrictSubringHom x)

instance

instIsScalarTower_restrictResidueField

L170 ↗

AlgebraicCurve.Place.instIsScalarTower_restrictResidueField

Source context 7 commands

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

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

Lean source · statement

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

def

uniformizerSubring

L202 ↗

AlgebraicCurve.Place.uniformizerSubring

Documentation

A chosen irreducible uniformizer in the valuation subring.

Source context 6 commands

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

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

Lean source · statement

def uniformizerSubring : v.toValuationSubring

theorem

coe_uniformizerSubring

L205 ↗

AlgebraicCurve.Place.coe_uniformizerSubring

Source context 6 commands

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

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

Lean source · statement

theorem coe_uniformizerSubring : (v.uniformizerSubring : F) = v.uniformizer

theorem

irreducible_uniformizerSubring

L207 ↗

AlgebraicCurve.Place.irreducible_uniformizerSubring

Source context 6 commands

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

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

Lean source · statement

theorem irreducible_uniformizerSubring : Irreducible v.uniformizerSubring

theorem

ord_nonneg_of_mem

L210 ↗

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 Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (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

L225 ↗

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 Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (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

L233 ↗

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 Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (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

uniformizerSubring_mem_maximalIdeal

L237 ↗

AlgebraicCurve.Place.uniformizerSubring_mem_maximalIdeal

Source context 6 commands

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

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

Lean source · statement

theorem uniformizerSubring_mem_maximalIdeal :
    v.uniformizerSubring ∈ IsLocalRing.maximalIdeal v.toValuationSubring

theorem

uniformizer_mem

L241 ↗

AlgebraicCurve.Place.uniformizer_mem

Source context 6 commands

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

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

Lean source · statement

theorem uniformizer_mem : v.uniformizer ∈ v.toValuationSubring

def

simplePoleSubmodule

L245 ↗

AlgebraicCurve.Place.simplePoleSubmodule

Documentation

Functions whose product with the uniformizer lies in the valuation subring.

Source context 6 commands

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

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

Lean source · full declaration

def simplePoleSubmodule : Submodule K F where
  carrier := {f | v.uniformizer * f ∈ v.toValuationSubring}
  add_mem' {f g} hf hg := by
    simpa only [Set.mem_ofPred_eq, mul_add] using add_mem hf hg
  zero_mem' := by simpa only [Set.mem_ofPred_eq, mul_zero] using zero_mem _
  smul_mem' c f hf := by
    change v.uniformizer * (c • f) ∈ v.toValuationSubring
    rw [Algebra.smul_def, mul_left_comm]
    exact mul_mem (v.algebraMap_mem' c) hf

theorem

mem_simplePoleSubmodule

L255 ↗

AlgebraicCurve.Place.mem_simplePoleSubmodule

Source context 6 commands

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

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

Lean source · statement

theorem mem_simplePoleSubmodule {f : F} :
    f ∈ v.simplePoleSubmodule ↔ v.uniformizer * f ∈ v.toValuationSubring

theorem

mem_simplePoleSubmodule_of_mem

L258 ↗

AlgebraicCurve.Place.mem_simplePoleSubmodule_of_mem

Source context 6 commands

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

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

Lean source · statement

theorem mem_simplePoleSubmodule_of_mem {f : F} (hf : f ∈ v.toValuationSubring) :
    f ∈ v.simplePoleSubmodule

def

simplePoleMulUniformizer

L263 ↗

AlgebraicCurve.Place.simplePoleMulUniformizer

Documentation

The valuation-subring section obtained by clearing a simple pole.

Source context 6 commands

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

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

Lean source · full declaration

def simplePoleMulUniformizer : v.simplePoleSubmodule →ₗ[K] v.toValuationSubring where
  toFun f := ⟨v.uniformizer * f.1, f.2⟩
  map_add' f g := Subtype.ext (mul_add _ _ _)
  map_smul' c f := Subtype.ext <| by
    change v.uniformizer * ((c • f : v.simplePoleSubmodule) : F)
        = ((c • ⟨v.uniformizer * f.1, f.2⟩ : v.toValuationSubring) : F)
    simp only [Algebra.smul_def, MulMemClass.coe_mul, v.coe_algebraMap, Submodule.coe_smul,
      mul_left_comm]

def

simplePoleResidueAux

L273 ↗

AlgebraicCurve.Place.simplePoleResidueAux

Documentation

The residue of a function after clearing its simple pole.

Source context 6 commands

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

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

Lean source · statement

def simplePoleResidueAux : v.simplePoleSubmodule →ₗ[K] v.ResidueField

theorem

simplePoleResidueAux_apply

L277 ↗

AlgebraicCurve.Place.simplePoleResidueAux_apply

Source context 6 commands

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

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

Lean source · statement

theorem simplePoleResidueAux_apply (f : v.simplePoleSubmodule) :
    v.simplePoleResidueAux f = IsLocalRing.residue _ ⟨v.uniformizer * f.1, f.2⟩

theorem

simplePoleResidueAux_eq_zero_of_mem

L280 ↗

AlgebraicCurve.Place.simplePoleResidueAux_eq_zero_of_mem

Source context 6 commands

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

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

Lean source · statement

theorem simplePoleResidueAux_eq_zero_of_mem {f : F} (hf : f ∈ v.toValuationSubring) :
    v.simplePoleResidueAux ⟨f, v.mem_simplePoleSubmodule_of_mem hf⟩ = 0

def

localResidueExtend

L289 ↗

AlgebraicCurve.Place.localResidueExtend

Documentation

A linear extension of the simple-pole residue to the function field.

Source context 6 commands

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

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

Lean source · statement

def localResidueExtend : F →ₗ[K] v.ResidueField

theorem

localResidueExtend_apply_of_mem

L292 ↗

AlgebraicCurve.Place.localResidueExtend_apply_of_mem

Source context 6 commands

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

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

Lean source · statement

theorem localResidueExtend_apply_of_mem {f : F} (hf : f ∈ v.simplePoleSubmodule) :
    v.localResidueExtend f = v.simplePoleResidueAux ⟨f, hf⟩

def

localResidueDataOfExtend

L298 ↗

AlgebraicCurve.Place.localResidueDataOfExtend

Documentation

Local residue data supplied by the chosen linear extension.

Source context 6 commands

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

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

Lean source · full declaration

def localResidueDataOfExtend : v.LocalResidueData where
  res := v.localResidueExtend
  res_of_mem f hf := by
    rw [v.localResidueExtend_apply_of_mem (v.mem_simplePoleSubmodule_of_mem hf),
      v.simplePoleResidueAux_eq_zero_of_mem hf]
  res_simplePole f hf := by
    rw [v.localResidueExtend_apply_of_mem hf, simplePoleResidueAux_apply]

instance

instHasLocalResidue

L308 ↗

AlgebraicCurve.instHasLocalResidue

Source context 4 commands

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

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

Lean source · full declaration

instance instHasLocalResidue : HasLocalResidue K F where
  exists_data v := ⟨v.localResidueDataOfExtend⟩

theorem

gate_hasLocalResidue_uniformizer_inv

L313 ↗

AlgebraicCurve.gate_hasLocalResidue_uniformizer_inv

Source context 5 commands

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

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

Lean source · statement

theorem gate_hasLocalResidue_uniformizer_inv (v : Place K F) :
    v.localResidue v.uniformizer⁻¹ = 1

theorem

gate_uniformizer_inv_mem_simplePoleSubmodule

L318 ↗

AlgebraicCurve.gate_uniformizer_inv_mem_simplePoleSubmodule

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
omit [HasCanonicalLocalResidueKStar K F] in

Lean source · statement

theorem gate_uniformizer_inv_mem_simplePoleSubmodule (v : Place K F) :
    v.uniformizer⁻¹ ∈ v.simplePoleSubmodule ∧ v.uniformizer⁻¹ ∉ v.toValuationSubring

def

poleSubmodule

L345 ↗

AlgebraicCurve.Place.poleSubmodule

Documentation

Functions whose poles are cleared by the specified uniformizer power.

Source context 6 commands

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

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

Lean source · full declaration

def poleSubmodule (n : ℕ) : Submodule K F where
  carrier := {f | v.uniformizer ^ n * f ∈ v.toValuationSubring}
  add_mem' {f g} hf hg := by
    simpa only [Set.mem_ofPred_eq, mul_add] using add_mem hf hg
  zero_mem' := by simpa only [Set.mem_ofPred_eq, mul_zero] using zero_mem _
  smul_mem' c f hf := by
    change v.uniformizer ^ n * (c • f) ∈ v.toValuationSubring
    rw [Algebra.smul_def, mul_left_comm]
    exact mul_mem (v.algebraMap_mem' c) hf

theorem

mem_poleSubmodule

L355 ↗

AlgebraicCurve.Place.mem_poleSubmodule

Source context 6 commands

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

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

Lean source · statement

theorem mem_poleSubmodule {n : ℕ} {f : F} :
    f ∈ v.poleSubmodule n ↔ v.uniformizer ^ n * f ∈ v.toValuationSubring

theorem

uniformizer_pow_ne_zero

L358 ↗

AlgebraicCurve.Place.uniformizer_pow_ne_zero

Source context 6 commands

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

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

Lean source · statement

theorem uniformizer_pow_ne_zero (n : ℕ) : (v.uniformizer ^ n : F) ≠ 0

theorem

ord_uniformizer_pow

L361 ↗

AlgebraicCurve.Place.ord_uniformizer_pow

Source context 6 commands

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

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

Lean source · statement

theorem ord_uniformizer_pow (n : ℕ) : v.ord (v.uniformizer ^ n) = (n : ℤ)

theorem

coe_poleSubmodule_zero

L365 ↗

AlgebraicCurve.Place.coe_poleSubmodule_zero

Source context 6 commands

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

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

Lean source · statement

theorem coe_poleSubmodule_zero :
    (v.poleSubmodule 0 : Set F) = (v.toValuationSubring : Set F)

theorem

poleSubmodule_one

L369 ↗

AlgebraicCurve.Place.poleSubmodule_one

Source context 6 commands

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

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

Lean source · statement

theorem poleSubmodule_one : v.poleSubmodule 1 = v.simplePoleSubmodule

theorem

mem_poleSubmodule_iff_ord

L372 ↗

AlgebraicCurve.Place.mem_poleSubmodule_iff_ord

Source context 6 commands

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

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

Lean source · statement

theorem mem_poleSubmodule_iff_ord {n : ℕ} {f : F} (hf : f ≠ 0) :
    f ∈ v.poleSubmodule n ↔ -(n : ℤ) ≤ v.ord f

theorem

poleSubmodule_mono

L378 ↗

AlgebraicCurve.Place.poleSubmodule_mono

Source context 6 commands

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

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

Lean source · statement

theorem poleSubmodule_mono : Monotone v.poleSubmodule

theorem

iSup_poleSubmodule_eq_top

L386 ↗

AlgebraicCurve.Place.iSup_poleSubmodule_eq_top

Source context 6 commands

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

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

Lean source · statement

theorem iSup_poleSubmodule_eq_top : ⨆ n, v.poleSubmodule n = ⊤

def

poleMulUniformizerPow

L397 ↗

AlgebraicCurve.Place.poleMulUniformizerPow

Documentation

The linear map clearing poles by the specified uniformizer power.

Source context 6 commands

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

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

Lean source · full declaration

def poleMulUniformizerPow (n : ℕ) : v.poleSubmodule n →ₗ[K] v.toValuationSubring where
  toFun f := ⟨v.uniformizer ^ n * f.1, f.2⟩
  map_add' f g := Subtype.ext (mul_add _ _ _)
  map_smul' c f := Subtype.ext <| by
    change v.uniformizer ^ n * ((c • f : v.poleSubmodule n) : F)
        = ((c • ⟨v.uniformizer ^ n * f.1, f.2⟩ : v.toValuationSubring) : F)
    simp only [Algebra.smul_def, MulMemClass.coe_mul, v.coe_algebraMap, Submodule.coe_smul,
      mul_left_comm]

def

laurentTailCoeff

L407 ↗

AlgebraicCurve.Place.laurentTailCoeff

Documentation

The residue of a section after clearing its pole by the specified power.

Source context 6 commands

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

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

Lean source · statement

def laurentTailCoeff (n : ℕ) : v.poleSubmodule n →ₗ[K] v.ResidueField

theorem

laurentTailCoeff_apply

L411 ↗

AlgebraicCurve.Place.laurentTailCoeff_apply

Source context 6 commands

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

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

Lean source · statement

theorem laurentTailCoeff_apply {n : ℕ} (f : v.poleSubmodule n) :
    v.laurentTailCoeff n f = IsLocalRing.residue _ ⟨v.uniformizer ^ n * f.1, f.2⟩

theorem

coe_mul_uniformizer_pow_inv_mem_poleSubmodule

L414 ↗

AlgebraicCurve.Place.coe_mul_uniformizer_pow_inv_mem_poleSubmodule

Source context 6 commands

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

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

Lean source · statement

theorem coe_mul_uniformizer_pow_inv_mem_poleSubmodule {n : ℕ} (c : v.toValuationSubring) :
    (c : F) * (v.uniformizer ^ n)⁻¹ ∈ v.poleSubmodule n

theorem

laurentTail_remainder_mem_poleSubmodule

L419 ↗

AlgebraicCurve.Place.laurentTail_remainder_mem_poleSubmodule

Source context 6 commands

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

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

Lean source · statement

theorem laurentTail_remainder_mem_poleSubmodule {n : ℕ} {f : F}
    (hf : f ∈ v.poleSubmodule (n + 1)) {c : v.toValuationSubring}
    (hc : IsLocalRing.residue _ c = v.laurentTailCoeff (n + 1) ⟨f, hf⟩) :
    f - (c : F) * (v.uniformizer ^ (n + 1))⁻¹ ∈ v.poleSubmodule n

theorem

localResidueData_agree_on_simplePole

L444 ↗

AlgebraicCurve.Place.localResidueData_agree_on_simplePole

Source context 6 commands

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

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

Lean source · statement

theorem localResidueData_agree_on_simplePole (R₁ R₂ : v.LocalResidueData) {f : F}
    (hf : f ∈ v.simplePoleSubmodule) : R₁.res f = R₂.res f

theorem

localResidueData_res_eq_simplePoleResidueAux

L448 ↗

AlgebraicCurve.Place.localResidueData_res_eq_simplePoleResidueAux

Source context 6 commands

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

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

Lean source · statement

theorem localResidueData_res_eq_simplePoleResidueAux (R : v.LocalResidueData) {f : F}
    (hf : f ∈ v.simplePoleSubmodule) : R.res f = v.simplePoleResidueAux ⟨f, hf⟩

theorem

gate_poleSubmodule_strictMono

L454 ↗

AlgebraicCurve.gate_poleSubmodule_strictMono

Source context 4 commands

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

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

Lean source · statement

theorem gate_poleSubmodule_strictMono (v : Place K F) (n : ℕ) :
    (v.uniformizer ^ (n + 1))⁻¹ ∈ v.poleSubmodule (n + 1) ∧
      (v.uniformizer ^ (n + 1))⁻¹ ∉ v.poleSubmodule n

theorem

exists_mem_poleSubmodule

L479 ↗

AlgebraicCurve.Place.exists_mem_poleSubmodule

Source context 6 commands

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

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

Lean source · statement

theorem exists_mem_poleSubmodule (f : F) : ∃ n, f ∈ v.poleSubmodule n

theorem

laurentTailCoeff_coe_mul_uniformizer_pow_inv

L487 ↗

AlgebraicCurve.Place.laurentTailCoeff_coe_mul_uniformizer_pow_inv

Source context 6 commands

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

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

Lean source · statement

theorem laurentTailCoeff_coe_mul_uniformizer_pow_inv {n : ℕ} (c : v.toValuationSubring) :
    v.laurentTailCoeff (n + 1)
        ⟨(c : F) * (v.uniformizer ^ (n + 1))⁻¹,
          v.coe_mul_uniformizer_pow_inv_mem_poleSubmodule c⟩
      = IsLocalRing.residue _ c

theorem

uniformizer_mul_uniformizer_sq_inv

L522 ↗

AlgebraicCurve.Place.uniformizer_mul_uniformizer_sq_inv

Source context 6 commands

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

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

Lean source · statement

theorem uniformizer_mul_uniformizer_sq_inv :
    (v.uniformizer : F) * (v.uniformizer ^ 2)⁻¹ = v.uniformizer⁻¹

theorem

res_algebraMap_mul_uniformizer_pow_inv

L532 ↗

AlgebraicCurve.Place.CanonicalLocalResidueDataK.res_algebraMap_mul_uniformizer_pow_inv

Source context 6 commands

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

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

Lean source · statement

theorem CanonicalLocalResidueDataK.res_algebraMap_mul_uniformizer_pow_inv
    (R : v.CanonicalLocalResidueDataK) {n : ℕ} (hn : 1 ≤ n) (c : K) :
    R.res ((algebraMap K F c) * (v.uniformizer ^ (n + 1))⁻¹) = 0

theorem

res_laurentRecK

L539 ↗

AlgebraicCurve.Place.CanonicalLocalResidueDataK.res_laurentRecK

Source context 6 commands

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

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

Lean source · statement

theorem CanonicalLocalResidueDataK.res_laurentRecK (R : v.CanonicalLocalResidueDataK)
    {n : ℕ} (hn : 1 ≤ n) (f : F) (c : K) :
    R.res (f - (algebraMap K F c) * (v.uniformizer ^ (n + 1))⁻¹) = R.res f

theorem

uniformizer_pow_inv_mem_poleSubmodule_self

L562 ↗

AlgebraicCurve.Place.uniformizer_pow_inv_mem_poleSubmodule_self

Source context 6 commands

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

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

Lean source · statement

theorem uniformizer_pow_inv_mem_poleSubmodule_self (m : ℕ) :
    (v.uniformizer ^ (m + 2))⁻¹ ∈ v.poleSubmodule (m + 2)

theorem

higherPoleMonomial_sum_mem_poleSubmodule

L566 ↗

AlgebraicCurve.Place.higherPoleMonomial_sum_mem_poleSubmodule

Source context 6 commands

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

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

Lean source · statement

theorem higherPoleMonomial_sum_mem_poleSubmodule {s : Finset ℕ} {N : ℕ}
    (hs : ∀ m ∈ s, m < N) (c : ℕ → K) :
    ∑ m ∈ s, c m • (v.uniformizer ^ (m + 2))⁻¹ ∈ v.poleSubmodule (N + 1)

theorem

higherPoleMonomial_coeff_eq_zero_of_mem

L574 ↗

AlgebraicCurve.Place.higherPoleMonomial_coeff_eq_zero_of_mem

Source context 6 commands

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

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

Lean source · statement

theorem higherPoleMonomial_coeff_eq_zero_of_mem (s : Finset ℕ) (c : ℕ → K)
    (hmem : ∑ m ∈ s, c m • (v.uniformizer ^ (m + 2))⁻¹ ∈ v.poleSubmodule 1) :
    ∀ m ∈ s, c m = 0

theorem

linearIndependent_higherPoleMonomial_mkQ

L599 ↗

AlgebraicCurve.Place.linearIndependent_higherPoleMonomial_mkQ

Source context 6 commands

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

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

Lean source · full declaration

theorem linearIndependent_higherPoleMonomial_mkQ :
    LinearIndependent K
      (fun m : ℕ => (v.poleSubmodule 1).mkQ ((v.uniformizer ^ (m + 2))⁻¹)) := by
  rw [linearIndependent_iff']
  intro s c hsum m hm
  refine v.higherPoleMonomial_coeff_eq_zero_of_mem s c ?_ m hm
  have h := hsum
  simp only [← map_smul, ← map_sum] at h
  rwa [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at h

def

higherPoleCorrectionAux

L610 ↗

AlgebraicCurve.Place.higherPoleCorrectionAux

Documentation

The correction on higher-pole monomials modulo the simple-pole submodule.

Source context 6 commands

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

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

Lean source · full declaration

def higherPoleCorrectionAux :
    Submodule.span K
        (Set.range fun m : ℕ => (v.poleSubmodule 1).mkQ ((v.uniformizer ^ (m + 2))⁻¹))
      →ₗ[K] v.ResidueField :=
  (Basis.span v.linearIndependent_higherPoleMonomial_mkQ).constr K
    (fun m => v.localResidueExtend ((v.uniformizer ^ (m + 2))⁻¹))

def

higherPoleCorrection

L618 ↗

AlgebraicCurve.Place.higherPoleCorrection

Documentation

The linear correction extended from higher-pole monomials to the function field.

Source context 6 commands

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

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

Lean source · statement

def higherPoleCorrection : F →ₗ[K] v.ResidueField

theorem

higherPoleCorrection_apply_of_mem

L621 ↗

AlgebraicCurve.Place.higherPoleCorrection_apply_of_mem

Source context 6 commands

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

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

Lean source · statement

theorem higherPoleCorrection_apply_of_mem {f : F} (hf : f ∈ v.poleSubmodule 1) :
    v.higherPoleCorrection f = 0

theorem

higherPoleCorrection_uniformizer_pow_inv

L627 ↗

AlgebraicCurve.Place.higherPoleCorrection_uniformizer_pow_inv

Source context 6 commands

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

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

Lean source · statement

theorem higherPoleCorrection_uniformizer_pow_inv (m : ℕ) :
    v.higherPoleCorrection ((v.uniformizer ^ (m + 2))⁻¹)
      = v.localResidueExtend ((v.uniformizer ^ (m + 2))⁻¹)

def

canonicalLocalResidueDataKOfExtend

L643 ↗

AlgebraicCurve.Place.canonicalLocalResidueDataKOfExtend

Documentation

Residue data corrected to vanish on the higher-pole uniformizer monomials.

Source context 6 commands

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

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

Lean source · full declaration

def canonicalLocalResidueDataKOfExtend : v.CanonicalLocalResidueDataK where
  res := v.localResidueExtend - v.higherPoleCorrection
  res_of_mem f hf := by
    have h1 : f ∈ v.poleSubmodule 1 :=
      v.poleSubmodule_one ▸ v.mem_simplePoleSubmodule_of_mem hf
    rw [LinearMap.sub_apply, v.higherPoleCorrection_apply_of_mem h1, sub_zero,
      v.localResidueExtend_apply_of_mem (v.mem_simplePoleSubmodule_of_mem hf),
      v.simplePoleResidueAux_eq_zero_of_mem hf]
  res_simplePole f hf := by
    have h1 : f ∈ v.poleSubmodule 1 := v.poleSubmodule_one ▸ hf
    rw [LinearMap.sub_apply, v.higherPoleCorrection_apply_of_mem h1, sub_zero,
      v.localResidueExtend_apply_of_mem hf, simplePoleResidueAux_apply]
  res_higherPoleMonomial n hn := by
    obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le hn
    rw [show 1 + m + 1 = m + 2 from by omega, LinearMap.sub_apply,
      v.higherPoleCorrection_uniformizer_pow_inv m, sub_self]

instance

instHasCanonicalLocalResidueK

L662 ↗

AlgebraicCurve.instHasCanonicalLocalResidueK

Source context 4 commands

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

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

Lean source · full declaration

instance instHasCanonicalLocalResidueK : HasCanonicalLocalResidueK K F where
  exists_data v := ⟨v.canonicalLocalResidueDataKOfExtend⟩

theorem

canonicalLocalResidueDataK_agree_on_poleSubmodule_of_surj

L669 ↗

AlgebraicCurve.Place.canonicalLocalResidueDataK_agree_on_poleSubmodule_of_surj

Source context 6 commands

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

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

Lean source · statement

theorem canonicalLocalResidueDataK_agree_on_poleSubmodule_of_surj
    (hsurj : Function.Surjective (algebraMap K v.ResidueField))
    (R₁ R₂ : v.CanonicalLocalResidueDataK) (n : ℕ) {f : F} (hf : f ∈ v.poleSubmodule n) :
    R₁.res f = R₂.res f

structure

CoefficientFieldSection

L713 ↗

AlgebraicCurve.Place.CoefficientFieldSection

Documentation

An algebra section of the valuation-subring residue map.

Source context 6 commands

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

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

Lean source · full declaration

structure CoefficientFieldSection where
  /-- The algebra lift of residue classes to the valuation subring. -/
  lift : v.ResidueField →ₐ[K] v.toValuationSubring
  /-- Taking residue after the lift recovers the original residue class. -/
  residue_lift : ∀ a, IsLocalRing.residue _ (lift a) = a

structure

CanonicalLocalResidueDataS

L720 ↗

AlgebraicCurve.Place.CanonicalLocalResidueDataS

Documentation

Local residue data vanishing on higher-pole monomials lifted through the supplied section.

Source context 6 commands

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

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

Lean source · full declaration

structure CanonicalLocalResidueDataS (σ : v.CoefficientFieldSection)
    extends v.LocalResidueData where
  /-- Higher-pole monomials with coefficients in the supplied section have zero residue. -/
  res_higherPoleSectionMonomial : ∀ (n : ℕ), 1 ≤ n → ∀ a : v.ResidueField,
    res ((σ.lift a : F) * (v.uniformizer ^ (n + 1))⁻¹) = 0

theorem

res_laurentRecS

L730 ↗

AlgebraicCurve.Place.CanonicalLocalResidueDataS.res_laurentRecS

Source context 8 commands

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

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

Lean source · statement

theorem res_laurentRecS {n : ℕ} (hn : 1 ≤ n) (f : F) (a : v.ResidueField) :
    R.res (f - (σ.lift a : F) * (v.uniformizer ^ (n + 1))⁻¹) = R.res f

theorem

canonicalLocalResidueDataS_agree_on_poleSubmodule

L736 ↗

AlgebraicCurve.Place.canonicalLocalResidueDataS_agree_on_poleSubmodule

Source context 6 commands

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

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

Lean source · statement

theorem canonicalLocalResidueDataS_agree_on_poleSubmodule (σ : v.CoefficientFieldSection)
    (R₁ R₂ : v.CanonicalLocalResidueDataS σ) (n : ℕ) {f : F} (hf : f ∈ v.poleSubmodule n) :
    R₁.res f = R₂.res f

def

coefficientFieldSectionOfBijective

L758 ↗

AlgebraicCurve.Place.coefficientFieldSectionOfBijective

Documentation

The coefficient-field section obtained when the base-field residue map is bijective.

Source context 6 commands

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

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

Lean source · full declaration

def coefficientFieldSectionOfBijective
    (hbij : Function.Bijective (algebraMap K v.ResidueField)) :
    v.CoefficientFieldSection where
  lift := (Algebra.ofId K v.toValuationSubring).comp
    (AlgEquiv.ofBijective (Algebra.ofId K v.ResidueField) hbij).symm.toAlgHom
  residue_lift a := by
    simp only [AlgHom.coe_comp, Function.comp_apply]
    set c : K := (AlgEquiv.ofBijective (Algebra.ofId K v.ResidueField) hbij).symm a with hc_def
    change IsLocalRing.residue _ (algebraMap K v.toValuationSubring c) = a
    rw [show IsLocalRing.residue _ (algebraMap K v.toValuationSubring c)
          = algebraMap K v.ResidueField c from by
        rw [IsScalarTower.algebraMap_apply K v.toValuationSubring v.ResidueField,
          IsLocalRing.ResidueField.algebraMap_eq]]
    exact (AlgEquiv.ofBijective (Algebra.ofId K v.ResidueField) hbij).apply_symm_apply a

abbrev

lg37_completion

L902 ↗

ModularCurve.Lg37.lg37_completion

Documentation

The completion of the valuation subring at its maximal ideal.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace ModularCurve.Lg37
open AlgebraicCurve
open ModularCurve.Ldgr36Si
open ModularCurve.Ldgr36Rc
open ModularCurve.Ldgr35Cs
section CompletionCarrier
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev lg37_completion (v : Place K F) : Type _

def

lg37_residueHat

L906 ↗

ModularCurve.Lg37.lg37_residueHat

Documentation

The residue map from the completed valuation subring.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace ModularCurve.Lg37
open AlgebraicCurve
open ModularCurve.Ldgr36Si
open ModularCurve.Ldgr36Rc
open ModularCurve.Ldgr35Cs
section CompletionCarrier
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def lg37_residueHat (v : Place K F) :
    lg37_completion v →+* v.ResidueField

theorem

lg37_residueHat_algebraMap

L910 ↗

ModularCurve.Lg37.lg37_residueHat_algebraMap

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace ModularCurve.Lg37
open AlgebraicCurve
open ModularCurve.Ldgr36Si
open ModularCurve.Ldgr36Rc
open ModularCurve.Ldgr35Cs
section CompletionCarrier
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lg37_residueHat_algebraMap (v : Place K F) (x : v.toValuationSubring) :
    lg37_residueHat v
        (algebraMap v.toValuationSubring (lg37_completion v) x)
      = IsLocalRing.residue v.toValuationSubring x

structure

Lg37CompletionSection

L916 ↗

ModularCurve.Lg37.Lg37CompletionSection

Documentation

An algebra section of the completed valuation-subring residue map.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace ModularCurve.Lg37
open AlgebraicCurve
open ModularCurve.Ldgr36Si
open ModularCurve.Ldgr36Rc
open ModularCurve.Ldgr35Cs
section CompletionCarrier
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

structure Lg37CompletionSection (v : Place K F) where
  /-- The algebra lift of residue classes to the completed valuation subring. -/
  lift : v.ResidueField →ₐ[K] lg37_completion v
  /-- The completed residue map is a left inverse to the lift. -/
  residueHat_lift : ∀ a, lg37_residueHat v (lift a) = a

abbrev

mp72a102_t1_maximalIdealHat

L954 ↗

Mp72a102T1.mp72a102_t1_maximalIdealHat

Documentation

The extension of the valuation-subring maximal ideal to its completion.

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing Polynomial
namespace Mp72a102T1
open AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Ldgr37Ch
open scoped Polynomial
attribute [local instance 2000] RatFunc.instAlgebraOfPolynomial
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

abbrev mp72a102_t1_maximalIdealHat (v : Place K F) :
    Ideal (lg37_completion v)

theorem

mp72a102_t1_isScalarTower

L959 ↗

Mp72a102T1.mp72a102_t1_isScalarTower

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing Polynomial
namespace Mp72a102T1
open AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Ldgr37Ch
open scoped Polynomial
attribute [local instance 2000] RatFunc.instAlgebraOfPolynomial
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t1_isScalarTower (v : Place K F) :
    IsScalarTower K v.toValuationSubring (lg37_completion v)

theorem

mp72a102_t1_isAdicComplete_maximalIdealHat

L963 ↗

Mp72a102T1.mp72a102_t1_isAdicComplete_maximalIdealHat

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing Polynomial
namespace Mp72a102T1
open AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Ldgr37Ch
open scoped Polynomial
attribute [local instance 2000] RatFunc.instAlgebraOfPolynomial
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t1_isAdicComplete_maximalIdealHat (v : Place K F) :
    IsAdicComplete (mp72a102_t1_maximalIdealHat v) (lg37_completion v)

theorem

mp72a102_t1_henselianRing_completion

L971 ↗

Mp72a102T1.mp72a102_t1_henselianRing_completion

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing Polynomial
namespace Mp72a102T1
open AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Ldgr37Ch
open scoped Polynomial
attribute [local instance 2000] RatFunc.instAlgebraOfPolynomial
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t1_henselianRing_completion (v : Place K F) :
    HenselianRing (lg37_completion v) (mp72a102_t1_maximalIdealHat v)

theorem

mp72a102_t1_maximalIdealHat_le_ker_residueHat

L976 ↗

Mp72a102T1.mp72a102_t1_maximalIdealHat_le_ker_residueHat

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing Polynomial
namespace Mp72a102T1
open AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Ldgr37Ch
open scoped Polynomial
attribute [local instance 2000] RatFunc.instAlgebraOfPolynomial
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t1_maximalIdealHat_le_ker_residueHat (v : Place K F) :
    mp72a102_t1_maximalIdealHat v ≤ RingHom.ker (lg37_residueHat v)

theorem

mp72a102_t1_exists_completion_root_of_residue_root

L982 ↗

Mp72a102T1.mp72a102_t1_exists_completion_root_of_residue_root

Source context 9 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing Polynomial
namespace Mp72a102T1
open AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Ldgr37Ch
open scoped Polynomial
attribute [local instance 2000] RatFunc.instAlgebraOfPolynomial
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t1_exists_completion_root_of_residue_root
    (v : Place K F) {p : K[X]} (hpmon : p.Monic) (hpsep : p.Separable)
    {rbar : v.ResidueField} (hrbar : Polynomial.aeval rbar p = 0) :
    ∃ α : lg37_completion v,
      Polynomial.aeval α p = 0 ∧ lg37_residueHat v α = rbar

theorem

mp72a102_t3_evalₐ_zero_depth

L1065 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_evalₐ_zero_depth

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section General
variable {R : Type*} [CommRing R] (I : Ideal R)

Lean source · statement

theorem mp72a102_t3_evalₐ_zero_depth (z : AdicCompletion I R) :
    AdicCompletion.evalₐ I 0 z = 0

theorem

mp72a102_t3_evalₐ_algebraMap

L1071 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_evalₐ_algebraMap

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section General
variable {R : Type*} [CommRing R] (I : Ideal R)

Lean source · statement

theorem mp72a102_t3_evalₐ_algebraMap (n : ℕ) (r : R) :
    AdicCompletion.evalₐ I n (algebraMap R (AdicCompletion I R) r)
      = Ideal.Quotient.mk (I ^ n) r

theorem

mp72a102_t3_evalₐ_factor

L1077 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_evalₐ_factor

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section General
variable {R : Type*} [CommRing R] (I : Ideal R)

Lean source · statement

theorem mp72a102_t3_evalₐ_factor {m n : ℕ} (hmn : m ≤ n) (z : AdicCompletion I R) :
    Ideal.Quotient.factor (Ideal.pow_le_pow_right hmn) (AdicCompletion.evalₐ I n z)
      = AdicCompletion.evalₐ I m z

theorem

mp72a102_t3_exists_rep_of_evalₐ_eq_zero

L1084 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_exists_rep_of_evalₐ_eq_zero

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section General
variable {R : Type*} [CommRing R] (I : Ideal R)

Lean source · statement

theorem mp72a102_t3_exists_rep_of_evalₐ_eq_zero {n : ℕ} {z : AdicCompletion I R}
    (h : AdicCompletion.evalₐ I n z = 0) :
    ∃ w ∈ I ^ n, AdicCompletion.evalₐ I (n + 1) z = Ideal.Quotient.mk (I ^ (n + 1)) w

theorem

mp72a102_t3_evalₐ_succ_mul_eq_zero

L1093 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_evalₐ_succ_mul_eq_zero

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section General
variable {R : Type*} [CommRing R] (I : Ideal R)

Lean source · statement

theorem mp72a102_t3_evalₐ_succ_mul_eq_zero {n : ℕ} {r : R} (hr : r ∈ I)
    {z : AdicCompletion I R} (h : AdicCompletion.evalₐ I n z = 0) :
    AdicCompletion.evalₐ I (n + 1) (algebraMap R (AdicCompletion I R) r * z) = 0

theorem

mp72a102_t3_evalₐ_one_eq_zero_of_evalOneₐ

L1101 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_evalₐ_one_eq_zero_of_evalOneₐ

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section General
variable {R : Type*} [CommRing R] (I : Ideal R)

Lean source · statement

theorem mp72a102_t3_evalₐ_one_eq_zero_of_evalOneₐ {z : AdicCompletion I R}
    (h : AdicCompletion.evalOneₐ I z = 0) : AdicCompletion.evalₐ I 1 z = 0

theorem

mp72a102_t3_evalDepth_add

L1115 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_evalDepth_add

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section Carrier
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t3_evalDepth_add (v : Place K F) (n : ℕ)
    (x y : lg37_completion v) :
    AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) n (x + y)
      = AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) n x
        + AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) n y

theorem

mp72a102_t3_evalDepth_mul

L1122 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_evalDepth_mul

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section Carrier
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t3_evalDepth_mul (v : Place K F) (n : ℕ)
    (x y : lg37_completion v) :
    AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) n (x * y)
      = AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) n x
        * AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) n y

theorem

mp72a102_t3_residueHat_congr_of_depth_one

L1129 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_residueHat_congr_of_depth_one

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section Carrier
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t3_residueHat_congr_of_depth_one (v : Place K F)
    {x y : lg37_completion v}
    (h : AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) 1 x
        = AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) 1 y) :
    lg37_residueHat v x = lg37_residueHat v y

theorem

mp72a102_t3_evalDepth_one_eq_zero_of_residueHat

L1138 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_evalDepth_one_eq_zero_of_residueHat

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section Carrier
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t3_evalDepth_one_eq_zero_of_residueHat (v : Place K F)
    {x : lg37_completion v} (hx : lg37_residueHat v x = 0) :
    AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) 1 x = 0

theorem

mp72a102_t3_eq_uniformizer_mul_of_mem_maximalIdeal

L1143 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_eq_uniformizer_mul_of_mem_maximalIdeal

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section Carrier
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t3_eq_uniformizer_mul_of_mem_maximalIdeal (v : Place K F)
    {w : v.toValuationSubring} (hw : w ∈ maximalIdeal v.toValuationSubring) :
    ∃ u : v.toValuationSubring, w = v.uniformizerSubring * u

theorem

mp72a102_t3_exists_uniformizer_factor

L1149 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_exists_uniformizer_factor

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section Carrier
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t3_exists_uniformizer_factor (v : Place K F)
    {x : lg37_completion v} (hx : lg37_residueHat v x = 0) (n : ℕ) :
    ∃ u : v.toValuationSubring,
      AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) n
        (x - algebraMap v.toValuationSubring (lg37_completion v) v.uniformizerSubring
          * algebraMap v.toValuationSubring (lg37_completion v) u) = 0

theorem

mp72a102_t3_sigma_taylor_expansion

L1172 ↗

ModularCurve.Mp72a102T3.mp72a102_t3_sigma_taylor_expansion

Source context 7 commands

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

noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace ModularCurve.Mp72a102T3
open AlgebraicCurve ModularCurve.Lg37
section Carrier
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t3_sigma_taylor_expansion (v : Place K F)
    (S : Lg37CompletionSection v) (n : ℕ) (x : lg37_completion v) :
    ∃ a : ℕ → v.ResidueField,
      AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) n
        (x - ∑ i ∈ Finset.range n, S.lift (a i)
          * algebraMap v.toValuationSubring (lg37_completion v)
              v.uniformizerSubring ^ i) = 0

theorem

mp72a102_t2_residueHat_algebraMap_base

L1256 ↗

Mp72a102T2.mp72a102_t2_residueHat_algebraMap_base

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing Polynomial
namespace Mp72a102T2
open AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Ldgr35Cs
open scoped Polynomial
section ResidueCalculus
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a102_t2_residueHat_algebraMap_base (v : Place K F) (c : K) :
    lg37_residueHat v (algebraMap K (lg37_completion v) c)
      = algebraMap K v.ResidueField c

def

mp72a102_t2_residueHatAlgHom

L1266 ↗

Mp72a102T2.mp72a102_t2_residueHatAlgHom

Documentation

The completed residue map as a base-field algebra homomorphism.

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing Polynomial
namespace Mp72a102T2
open AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Ldgr35Cs
open scoped Polynomial
section ResidueCalculus
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def mp72a102_t2_residueHatAlgHom (v : Place K F) :
    lg37_completion v →ₐ[K] v.ResidueField where
  toRingHom := lg37_residueHat v
  commutes' := mp72a102_t2_residueHat_algebraMap_base v

def

residueFieldAdjoinRootEquiv

L1292 ↗

ModularCurve.KwNo6Section.residueFieldAdjoinRootEquiv

Documentation

The algebra equivalence identifying the residue field with the primitive-root presentation.

Source context 4 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
namespace ModularCurve.KwNo6Section
section GenericIso
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

def residueFieldAdjoinRootEquiv {ᾱ : v.ResidueField} (hint : IsIntegral K ᾱ)
    (htop : K⟮ᾱ⟯ = ⊤) :
    AdjoinRoot (minpoly K ᾱ) ≃ₐ[K] v.ResidueField

theorem

residueFieldAdjoinRootEquiv_root

L1298 ↗

ModularCurve.KwNo6Section.residueFieldAdjoinRootEquiv_root

Source context 4 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
namespace ModularCurve.KwNo6Section
section GenericIso
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem residueFieldAdjoinRootEquiv_root {ᾱ : v.ResidueField} (hint : IsIntegral K ᾱ)
    (htop : K⟮ᾱ⟯ = ⊤) :
    residueFieldAdjoinRootEquiv v hint htop (AdjoinRoot.root (minpoly K ᾱ)) = ᾱ

def

sectionOfPrimitiveRoot

L1312 ↗

ModularCurve.KwNo6Section.sectionOfPrimitiveRoot

Documentation

The completion section induced by a primitive root and its supplied completion lift.

Source context 4 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
namespace ModularCurve.KwNo6Section
section GenericSection
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · full declaration

def sectionOfPrimitiveRoot {ᾱ : v.ResidueField} (hint : IsIntegral K ᾱ)
    (htop : K⟮ᾱ⟯ = ⊤) (αhat : lg37_completion v)
    (hroot : (aeval αhat) (minpoly K ᾱ) = 0)
    (hres : lg37_residueHat v αhat = ᾱ) :
    Lg37CompletionSection v where
  lift :=
    (AdjoinRoot.liftAlgHom (minpoly K ᾱ) (Algebra.ofId K (lg37_completion v)) αhat
      (by rw [aeval_def] at hroot; exact hroot)).comp
      (residueFieldAdjoinRootEquiv v hint htop).symm.toAlgHom
  residueHat_lift a := by
    have hres' : lg37_residueHat v αhat
        = residueFieldAdjoinRootEquiv v hint htop (AdjoinRoot.root (minpoly K ᾱ)) :=
      hres.trans (residueFieldAdjoinRootEquiv_root v hint htop).symm
    have hkey : (mp72a102_t2_residueHatAlgHom v).comp
          (AdjoinRoot.liftAlgHom (minpoly K ᾱ) (Algebra.ofId K (lg37_completion v)) αhat
            (by rw [aeval_def] at hroot; exact hroot))
        = (residueFieldAdjoinRootEquiv v hint htop).toAlgHom := by
      refine AdjoinRoot.algHom_ext ?_
      exact (congrArg (mp72a102_t2_residueHatAlgHom v)
        (AdjoinRoot.liftAlgHom_root (minpoly K ᾱ) (Algebra.ofId K (lg37_completion v)) αhat
          (by rw [aeval_def] at hroot; exact hroot))).trans hres'
    have h1 := DFunLike.congr_fun hkey ((residueFieldAdjoinRootEquiv v hint htop).symm a)
    rw [AlgHom.comp_apply] at h1
    have h2 : (residueFieldAdjoinRootEquiv v hint htop).toAlgHom
        ((residueFieldAdjoinRootEquiv v hint htop).symm a) = a :=
      (residueFieldAdjoinRootEquiv v hint htop).apply_symm_apply a
    exact h1.trans h2

theorem

mp72a103_t2_evalDepth_of_uniformizer_mul

L1360 ↗

Mp72a103T2.mp72a103_t2_evalDepth_of_uniformizer_mul

Source context 10 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
noncomputable section
open IsDedekindDomain IsLocalRing Polynomial
open scoped Polynomial
namespace Mp72a103T2
open AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3
open Mp72a102T2
section Calculus
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a103_t2_evalDepth_of_uniformizer_mul (v : Place K F) {n : ℕ}
    {z : lg37_completion v}
    (h : AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) (n + 1)
        (algebraMap v.toValuationSubring (lg37_completion v)
            v.uniformizerSubring * z) = 0) :
    AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) n z = 0

theorem

mp72a103_t2_lift_eq_zero_of_depth_one

L1385 ↗

Mp72a103T2.mp72a103_t2_lift_eq_zero_of_depth_one

Source context 10 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
noncomputable section
open IsDedekindDomain IsLocalRing Polynomial
open scoped Polynomial
namespace Mp72a103T2
open AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3
open Mp72a102T2
section Calculus
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a103_t2_lift_eq_zero_of_depth_one (v : Place K F)
    (S : Lg37CompletionSection v) {c : v.ResidueField}
    (h : AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) 1 (S.lift c) = 0) :
    c = 0

theorem

mp72a103_t2_taylor_coeff_eq_zero_of_depth

L1393 ↗

Mp72a103T2.mp72a103_t2_taylor_coeff_eq_zero_of_depth

Source context 10 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
noncomputable section
open IsDedekindDomain IsLocalRing Polynomial
open scoped Polynomial
namespace Mp72a103T2
open AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3
open Mp72a102T2
section Calculus
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mp72a103_t2_taylor_coeff_eq_zero_of_depth (v : Place K F)
    (S : Lg37CompletionSection v) :
    ∀ (n : ℕ) (a : ℕ → v.ResidueField),
      AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) n
        (∑ i ∈ Finset.range n, S.lift (a i)
          * algebraMap v.toValuationSubring (lg37_completion v)
              v.uniformizerSubring ^ i) = 0 →
      ∀ i < n, a i = 0

theorem

maximalIdeal_fg

L1474 ↗

ModularCurve.KwNo6Pin.maximalIdeal_fg

Source context 6 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem maximalIdeal_fg (v : Place K F) :
    (maximalIdeal v.toValuationSubring).FG

theorem

isAdicComplete_map

L1478 ↗

ModularCurve.KwNo6Pin.isAdicComplete_map

Source context 6 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem isAdicComplete_map (v : Place K F) :
    IsAdicComplete
        ((maximalIdeal v.toValuationSubring).map
          (algebraMap v.toValuationSubring (lg37_completion v)))
        (lg37_completion v)

theorem

residueHat_surjective

L1485 ↗

ModularCurve.KwNo6Pin.residueHat_surjective

Source context 6 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem residueHat_surjective (v : Place K F) :
    Function.Surjective (lg37_residueHat v)

theorem

ker_residueHat

L1491 ↗

ModularCurve.KwNo6Pin.ker_residueHat

Source context 6 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ker_residueHat (v : Place K F) :
    RingHom.ker (lg37_residueHat v)
      = (maximalIdeal v.toValuationSubring).map
          (algebraMap v.toValuationSubring (lg37_completion v))

theorem

map_isMaximal

L1531 ↗

ModularCurve.KwNo6Pin.map_isMaximal

Source context 6 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem map_isMaximal (v : Place K F) :
    ((maximalIdeal v.toValuationSubring).map
        (algebraMap v.toValuationSubring (lg37_completion v))).IsMaximal

instance

isLocalRing_completion

L1537 ↗

ModularCurve.KwNo6Pin.isLocalRing_completion

Source context 6 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

instance isLocalRing_completion (v : Place K F) :
    IsLocalRing (lg37_completion v)

theorem

ker_residueHat_eq_maximalIdeal

L1545 ↗

ModularCurve.KwNo6Pin.ker_residueHat_eq_maximalIdeal

Source context 6 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ker_residueHat_eq_maximalIdeal (v : Place K F) :
    RingHom.ker (lg37_residueHat v)
      = maximalIdeal (lg37_completion v)

theorem

hensel_unique

L1551 ↗

ModularCurve.KwNo6Pin.hensel_unique

Source context 6 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem hensel_unique (v : Place K F) {p : K[X]} (hsep : p.Separable)
    {α β : lg37_completion v}
    (hα : aeval α p = 0) (hβ : aeval β p = 0)
    (hres : lg37_residueHat v α = lg37_residueHat v β) : α = β

theorem

section_unique

L1583 ↗

ModularCurve.KwNo6Pin.section_unique

Source context 6 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem section_unique (v : Place K F)
    [FiniteDimensional K v.ResidueField] [Algebra.IsSeparable K v.ResidueField]
    (S S' : Lg37CompletionSection v) : S.lift = S'.lift

def

aCoeff

L1609 ↗

ModularCurve.KwNo6Pin.aCoeff

Documentation

The chosen Taylor coefficient in the completion with respect to the supplied residue section.

Source context 6 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def aCoeff (v : Place K F) (S : Lg37CompletionSection v)
    (n : ℕ) (x : lg37_completion v) : v.ResidueField

theorem

aCoeff_section_indep

L1613 ↗

ModularCurve.KwNo6Pin.aCoeff_section_indep

Source context 6 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem aCoeff_section_indep (v : Place K F)
    [FiniteDimensional K v.ResidueField] [Algebra.IsSeparable K v.ResidueField]
    (S S' : Lg37CompletionSection v) (n : ℕ) (x : lg37_completion v) :
    aCoeff v S n x = aCoeff v S' n x

theorem

aCoeff_zero

L1660 ↗

ModularCurve.KwNo6Pin.aCoeff_zero

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem aCoeff_zero (v : Place K F) (S : Lg37CompletionSection v)
    (x : lg37_completion v) :
    aCoeff v S 0 x = lg37_residueHat v x

theorem

aCoeff_add

L1672 ↗

ModularCurve.KwNo6Pin.aCoeff_add

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem aCoeff_add (v : Place K F) (S : Lg37CompletionSection v) (m : ℕ)
    (x y : lg37_completion v) :
    aCoeff v S m (x + y) = aCoeff v S m x + aCoeff v S m y

theorem

aCoeff_smul

L1722 ↗

ModularCurve.KwNo6Pin.aCoeff_smul

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem aCoeff_smul (v : Place K F) (S : Lg37CompletionSection v) (m : ℕ) (c : K)
    (x : lg37_completion v) :
    aCoeff v S m (algebraMap K (lg37_completion v) c * x)
      = algebraMap K v.ResidueField c * aCoeff v S m x

theorem

aCoeff_shift

L1781 ↗

ModularCurve.KwNo6Pin.aCoeff_shift

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem aCoeff_shift (v : Place K F) (S : Lg37CompletionSection v) (n : ℕ)
    (x : lg37_completion v) :
    aCoeff v S (n + 1)
        (algebraMap v.toValuationSubring (lg37_completion v) v.uniformizerSubring * x)
      = aCoeff v S n x

theorem

aCoeff_shift_pow

L1848 ↗

ModularCurve.KwNo6Pin.aCoeff_shift_pow

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem aCoeff_shift_pow (v : Place K F) (S : Lg37CompletionSection v) (n k : ℕ)
    (x : lg37_completion v) :
    aCoeff v S (n + k)
        ((algebraMap v.toValuationSubring (lg37_completion v) v.uniformizerSubring) ^ k
          * x)
      = aCoeff v S n x

theorem

aCoeff_one_eq_zero

L1865 ↗

ModularCurve.KwNo6Pin.aCoeff_one_eq_zero

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem aCoeff_one_eq_zero (v : Place K F) (S : Lg37CompletionSection v)
    {n : ℕ} (hn : 1 ≤ n) : aCoeff v S n 1 = 0

theorem

clearPow_mem

L1907 ↗

ModularCurve.KwNo6Pin.clearPow_mem

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem clearPow_mem (v : Place K F) (f : F) {N : ℕ} (hN : (-v.ord f).toNat ≤ N) :
    v.uniformizer ^ (N + 1) * f ∈ v.toValuationSubring

def

clearedHat

L1918 ↗

ModularCurve.KwNo6Pin.clearedHat

Documentation

The completed section obtained by clearing a function-field pole.

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def clearedHat (v : Place K F) (f : F) {N : ℕ} (hN : (-v.ord f).toNat ≤ N) :
    lg37_completion v

def

resStar

L1924 ↗

ModularCurve.KwNo6Pin.resStar

Documentation

The residue coefficient of the completed section obtained by clearing the pole.

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def resStar (v : Place K F) (S : Lg37CompletionSection v) (f : F) :
    v.ResidueField

theorem

aCoeff_clearedHat_of_le

L1928 ↗

ModularCurve.KwNo6Pin.aCoeff_clearedHat_of_le

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem aCoeff_clearedHat_of_le (v : Place K F) (S : Lg37CompletionSection v) (f : F)
    {N : ℕ} (hN : (-v.ord f).toNat ≤ N) :
    aCoeff v S N (clearedHat v f hN) = resStar v S f

theorem

resStar_add

L1943 ↗

ModularCurve.KwNo6Pin.resStar_add

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resStar_add (v : Place K F) (S : Lg37CompletionSection v) (f g : F) :
    resStar v S (f + g) = resStar v S f + resStar v S g

theorem

resStar_smul

L1959 ↗

ModularCurve.KwNo6Pin.resStar_smul

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resStar_smul (v : Place K F) (S : Lg37CompletionSection v) (c : K) (f : F) :
    resStar v S (c • f) = c • resStar v S f

def

resStarₗ

L1975 ↗

ModularCurve.KwNo6Pin.resStarₗ

Documentation

The residue coefficient map regarded as a base-field linear map.

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def resStarₗ (v : Place K F) (S : Lg37CompletionSection v) :
    F →ₗ[K] v.ResidueField where
  toFun := resStar v S
  map_add' := resStar_add v S
  map_smul' c f := by rw [RingHom.id_apply]; exact resStar_smul v S c f

theorem

resStar_simplePole

L1981 ↗

ModularCurve.KwNo6Pin.resStar_simplePole

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resStar_simplePole (v : Place K F) (S : Lg37CompletionSection v) (f : F)
    (hf : v.uniformizer * f ∈ v.toValuationSubring) :
    resStar v S f = IsLocalRing.residue _ ⟨v.uniformizer * f, hf⟩

theorem

resStar_of_mem

L2001 ↗

ModularCurve.KwNo6Pin.resStar_of_mem

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resStar_of_mem (v : Place K F) (S : Lg37CompletionSection v) {f : F}
    (hf : f ∈ v.toValuationSubring) : resStar v S f = 0

theorem

resStar_higherPoleMonomial

L2009 ↗

ModularCurve.KwNo6Pin.resStar_higherPoleMonomial

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem resStar_higherPoleMonomial (v : Place K F) (S : Lg37CompletionSection v)
    {n : ℕ} (hn : 1 ≤ n) : resStar v S (v.uniformizer ^ (n + 1))⁻¹ = 0

def

canonicalLocalResidueDataKStar

L2031 ↗

ModularCurve.KwNo6Pin.canonicalLocalResidueDataKStar

Documentation

Canonical local residue data obtained from completion coefficients.

Source context 9 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
namespace ModularCurve.KwNo6Pin
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def canonicalLocalResidueDataKStar (v : Place K F)
    (S : Lg37CompletionSection v) : v.CanonicalLocalResidueDataK where
  res := resStarₗ v S
  res_of_mem _f hf := resStar_of_mem v S hf
  res_simplePole f hf := resStar_simplePole v S f hf
  res_higherPoleMonomial _n hn := resStar_higherPoleMonomial v S hn

theorem

completionSection_nonempty_generic

L2055 ↗

AlgebraicCurve.completionSection_nonempty_generic

Source context 12 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.KwNo6Section ModularCurve.KwNo6Pin
open Mp72a102T1
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem completionSection_nonempty_generic (v : Place K F)
    [FiniteDimensional K v.ResidueField] [Algebra.IsSeparable K v.ResidueField] :
    Nonempty (Lg37CompletionSection v)

instance

instHasCanonicalLocalResidueKStar

L2067 ↗

AlgebraicCurve.instHasCanonicalLocalResidueKStar

Source context 12 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.KwNo6Section ModularCurve.KwNo6Pin
open Mp72a102T1
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

instance instHasCanonicalLocalResidueKStar [IsCurveOver K F] [PerfectField K] :
    HasCanonicalLocalResidueKStar K F where
  dataKStar v :=
    have : FiniteDimensional K v.ResidueField := Place.FiniteResidue.finite
    have : Algebra.IsSeparable K v.ResidueField :=
      Algebra.IsAlgebraic.isSeparable_of_perfectField
    canonicalLocalResidueDataKStar v
      (Classical.choice (completionSection_nonempty_generic v))

theorem

localResidue_eq_resStar

L2076 ↗

AlgebraicCurve.localResidue_eq_resStar

Source context 12 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.KwNo6Section ModularCurve.KwNo6Pin
open Mp72a102T1
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem localResidue_eq_resStar [IsCurveOver K F] [PerfectField K] (v : Place K F)
    (S : Lg37CompletionSection v) (f : F) :
    v.localResidue f = resStar v S f

theorem

localResidue_eq_resStarₗ

L2086 ↗

AlgebraicCurve.localResidue_eq_resStarₗ

Source context 12 commands

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

open AlgebraicCurve ModularCurve.Lg37 Polynomial IntermediateField Mp72a102T1 Mp72a102T2
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.Mp72a102T3 Mp72a103T2 Mp72a102T1
open ModularCurve.KwNo6Section
open Polynomial IsLocalRing AlgebraicCurve
open ModularCurve.Lg37 ModularCurve.KwNo6Section ModularCurve.KwNo6Pin
open Mp72a102T1
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem localResidue_eq_resStarₗ [IsCurveOver K F] [PerfectField K] (v : Place K F)
    (S : Lg37CompletionSection v) :
    v.localResidue = resStarₗ v S

Module documentation

Declarations