Module

Completion.lean

Nyll.AlgebraicCurves.Places.Completion

37 declarations indexed from sourceView source ↗

Module documentation

Completion

Completions at places carry the induced maps of finite extensions, their integral valuation subrings, completed traces, and constant-field maps.

Imports9

Mathlib.Algebra.Order.Ring.IsNonarchimedean
Mathlib.Algebra.Order.Ring.Abs
Mathlib.RingTheory.Henselian
Mathlib.RingTheory.SimpleRing.Principal
Mathlib.Topology.Algebra.Module.FiniteDimension
Mathlib.Topology.Algebra.Valued.NormedValued
Mathlib.Topology.UniformSpace.Uniformizable
Nyll.AlgebraicCurves.Divisors.Maps
Nyll.AlgebraicCurves.Valuations.AdicCompletion

Imported by13

instance

(anonymous instance)

L30 ↗

Lean source · full declaration

instance {K L : Type*} [Field K] [Semiring L] (O : ValuationSubring K) [Algebra K L] :
    Algebra O L where
  smul r x := r.1 • x
  algebraMap := (algebraMap K L).comp (algebraMap O K)
  commutes' _ _ := by simp [Algebra.commutes]
  smul_def' _ _ := by simp [← Algebra.smul_def]; rfl

abbrev

adicCompletion

L48 ↗

AlgebraicCurve.Place.adicCompletion

Documentation

The completion of the function field at the adic valuation of the place.

Source context 5 commands

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

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

Lean source · statement

abbrev adicCompletion : Type _

abbrev

adicCompletionIntegers

L51 ↗

AlgebraicCurve.Place.adicCompletionIntegers

Documentation

The integral valuation subring in the completion at the place.

Source context 5 commands

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

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

Lean source · statement

abbrev adicCompletionIntegers : ValuationSubring V.adicCompletion

theorem

kw_ffgc_adicValuation_algebraMap

L62 ↗

AlgebraicCurve.Place.kw_ffgc_adicValuation_algebraMap

Source context 7 commands

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

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

Lean source · statement

theorem kw_ffgc_adicValuation_algebraMap (x : F) :
    W.adicValuation (algebraMap F F' x)
      = (W.restrict F).adicValuation x ^ W.ramificationIndex F

theorem

kw_ffgc_valued_withValMapAlgebraMap

L78 ↗

AlgebraicCurve.Place.kw_ffgc_valued_withValMapAlgebraMap

Source context 7 commands

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

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

Lean source · statement

theorem kw_ffgc_valued_withValMapAlgebraMap
    (x : WithVal ((W.restrict F).heightOneSpectrum.valuation F)) :
    Valued.v (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
      (W.heightOneSpectrum.valuation F') (algebraMap F F') x)
        = Valued.v x ^ W.ramificationIndex F

theorem

kw_ffgc_uniformContinuous_withValMapAlgebraMap

L86 ↗

AlgebraicCurve.Place.kw_ffgc_uniformContinuous_withValMapAlgebraMap

Source context 7 commands

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

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

Lean source · statement

theorem kw_ffgc_uniformContinuous_withValMapAlgebraMap :
    UniformContinuous (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
      (W.heightOneSpectrum.valuation F') (algebraMap F F'))

def

kw_ffgc_adicCompletionComap

L127 ↗

AlgebraicCurve.Place.kw_ffgc_adicCompletionComap

Documentation

The map of completions induced by restricting the place along the field extension.

Source context 7 commands

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

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

Lean source · statement

def kw_ffgc_adicCompletionComap : (W.restrict F).adicCompletion →+* W.adicCompletion

theorem

kw_ffgc_continuous_adicCompletionComap

L137 ↗

AlgebraicCurve.Place.kw_ffgc_continuous_adicCompletionComap

Source context 7 commands

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

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

Lean source · statement

theorem kw_ffgc_continuous_adicCompletionComap :
    Continuous (kw_ffgc_adicCompletionComap F W)

theorem

kw_ffgc_adicCompletionComap_coe

L149 ↗

AlgebraicCurve.Place.kw_ffgc_adicCompletionComap_coe

Source context 7 commands

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

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

Lean source · statement

theorem kw_ffgc_adicCompletionComap_coe
    (x : WithVal ((W.restrict F).heightOneSpectrum.valuation F)) :
    kw_ffgc_adicCompletionComap F W (x : (W.restrict F).adicCompletion)
      = (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
          (W.heightOneSpectrum.valuation F') (algebraMap F F') x : W.adicCompletion)

theorem

kw_ffgc_valued_adicCompletionComap

L160 ↗

AlgebraicCurve.Place.kw_ffgc_valued_adicCompletionComap

Source context 8 commands

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

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

Lean source · statement

theorem kw_ffgc_valued_adicCompletionComap (x : (W.restrict F).adicCompletion) :
    Valued.v (kw_ffgc_adicCompletionComap F W x)
      = Valued.v x ^ W.ramificationIndex F

theorem

kw_ffgc_adicCompletionComap_mem_integers

L197 ↗

AlgebraicCurve.Place.kw_ffgc_adicCompletionComap_mem_integers

Source context 9 commands

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

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

Lean source · statement

theorem kw_ffgc_adicCompletionComap_mem_integers
    {x : (W.restrict F).adicCompletion} (hx : x ∈ (W.restrict F).adicCompletionIntegers) :
    kw_ffgc_adicCompletionComap F W x ∈ W.adicCompletionIntegers

def

kw_ffgc_adicCompletionComapIntegers

L205 ↗

AlgebraicCurve.Place.kw_ffgc_adicCompletionComapIntegers

Documentation

The induced map on integral valuation subrings of the two completions.

Source context 9 commands

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

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

Lean source · statement

def kw_ffgc_adicCompletionComapIntegers :
    (W.restrict F).adicCompletionIntegers →+* W.adicCompletionIntegers

theorem

kw_ffgc_adicCompletionComapIntegers_coe

L210 ↗

AlgebraicCurve.Place.kw_ffgc_adicCompletionComapIntegers_coe

Source context 9 commands

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

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

Lean source · statement

theorem kw_ffgc_adicCompletionComapIntegers_coe
    (x : (W.restrict F).adicCompletionIntegers) :
    (kw_ffgc_adicCompletionComapIntegers F W x : W.adicCompletion)
      = kw_ffgc_adicCompletionComap F W (x : (W.restrict F).adicCompletion)

instance

kw_ffgc_algebraAdicCompletionComap

L231 ↗

AlgebraicCurve.Place.kw_ffgc_algebraAdicCompletionComap

Source context 11 commands

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

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

Lean source · statement

instance kw_ffgc_algebraAdicCompletionComap :
    Algebra (W.restrict F).adicCompletion W.adicCompletion

theorem

kw_ffgc_algebraMap_adicCompletionComap_eq

L235 ↗

AlgebraicCurve.Place.kw_ffgc_algebraMap_adicCompletionComap_eq

Source context 11 commands

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

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

Lean source · statement

theorem kw_ffgc_algebraMap_adicCompletionComap_eq :
    algebraMap (W.restrict F).adicCompletion W.adicCompletion
      = kw_ffgc_adicCompletionComap F W

instance

kw_ffgc_algebraAdicCompletionComapIntegers

L239 ↗

AlgebraicCurve.Place.kw_ffgc_algebraAdicCompletionComapIntegers

Source context 11 commands

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

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

Lean source · statement

instance kw_ffgc_algebraAdicCompletionComapIntegers :
    Algebra (W.restrict F).adicCompletionIntegers W.adicCompletionIntegers

instance

kw_ffgc_algebraAdicCompletionIntegersToCompletion

L243 ↗

AlgebraicCurve.Place.kw_ffgc_algebraAdicCompletionIntegersToCompletion

Source context 11 commands

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

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

Lean source · statement

instance kw_ffgc_algebraAdicCompletionIntegersToCompletion :
    Algebra (W.restrict F).adicCompletionIntegers W.adicCompletion

instance

kw_ffgc_isScalarTower_integersCompletionCompletion

L248 ↗

AlgebraicCurve.Place.kw_ffgc_isScalarTower_integersCompletionCompletion

Source context 11 commands

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

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

Lean source · statement

instance kw_ffgc_isScalarTower_integersCompletionCompletion :
    IsScalarTower (W.restrict F).adicCompletionIntegers
      (W.restrict F).adicCompletion W.adicCompletion

instance

kw_ffgc_isScalarTower_integersIntegersCompletion

L253 ↗

AlgebraicCurve.Place.kw_ffgc_isScalarTower_integersIntegersCompletion

Source context 11 commands

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

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

Lean source · statement

instance kw_ffgc_isScalarTower_integersIntegersCompletion :
    IsScalarTower (W.restrict F).adicCompletionIntegers
      W.adicCompletionIntegers W.adicCompletion

def

kw_ffgc_rankOne_adicCompletion

L270 ↗

AlgebraicCurve.Place.kw_ffgc_rankOne_adicCompletion

Documentation

The rank-one certificate for the discrete valuation on the completion.

Source context 11 commands

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

noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve.Place
section SpectralSetup
open scoped Valued NNReal WithZero
open WithZeroMulInt Valuation.IsRankOneDiscrete
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (V : Place K F)

Lean source · statement

def kw_ffgc_rankOne_adicCompletion :
    (Valued.v : Valuation V.adicCompletion ℤᵐ⁰).RankOne

def

kw_ffgc_absoluteValue

L287 ↗

AlgebraicCurve.Place.kw_ffgc_absoluteValue

Documentation

The absolute value on the extension completion normalized by the ramification index.

Source context 13 commands

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

noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve.Place
section AbsoluteValue
open scoped Valued NNReal WithZero
open WithZeroMulInt Valuation.IsRankOneDiscrete
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

Lean source · statement

def kw_ffgc_absoluteValue : AbsoluteValue W.adicCompletion ℝ

instance

kw_ffgc_continuousSMul_adicCompletionComap

L314 ↗

AlgebraicCurve.Place.kw_ffgc_continuousSMul_adicCompletionComap

Source context 12 commands

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

noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
namespace AlgebraicCurve.Place
section ClosedAdjoin
open scoped Valued NNReal WithZero
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

Lean source · statement

instance kw_ffgc_continuousSMul_adicCompletionComap :
    ContinuousSMul (W.restrict F).adicCompletion W.adicCompletion

theorem

kw_ffgc_adicCompletionComap_algebraMap_algebraMap

L338 ↗

AlgebraicCurve.Place.kw_ffgc_adicCompletionComap_algebraMap_algebraMap

Source context 14 commands

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

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

Lean source · statement

theorem kw_ffgc_adicCompletionComap_algebraMap_algebraMap (c : F) :
    algebraMap F' W.adicCompletion (algebraMap F F' c)
      = algebraMap (W.restrict F).adicCompletion W.adicCompletion
          (algebraMap F (W.restrict F).adicCompletion c)

theorem

kw_ffgc_algebraMap_smul_algebraMap

L350 ↗

AlgebraicCurve.Place.kw_ffgc_algebraMap_smul_algebraMap

Source context 14 commands

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

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

Lean source · statement

theorem kw_ffgc_algebraMap_smul_algebraMap (c : F) (b : F') :
    algebraMap F (W.restrict F).adicCompletion c • algebraMap F' W.adicCompletion b
      = algebraMap F' W.adicCompletion (c • b)

def

kw_ffgc_completionLinearCombination

L357 ↗

AlgebraicCurve.Place.kw_ffgc_completionLinearCombination

Documentation

Linear combinations of the chosen field basis with coefficients in the base completion.

Source context 14 commands

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

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

Lean source · statement

def kw_ffgc_completionLinearCombination {ι : Type*} [Fintype ι] (b : Module.Basis ι F F') :
    (ι → (W.restrict F).adicCompletion)
      →ₗ[(W.restrict F).adicCompletion] W.adicCompletion

theorem

kw_ffgc_denseRange_completionLinearCombination

L363 ↗

AlgebraicCurve.Place.kw_ffgc_denseRange_completionLinearCombination

Source context 14 commands

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

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

Lean source · statement

theorem kw_ffgc_denseRange_completionLinearCombination {ι : Type*} [Fintype ι]
    (b : Module.Basis ι F F') :
    DenseRange (kw_ffgc_completionLinearCombination F W b)

instance

kw_ffgc_finiteDimensional_adicCompletion

L374 ↗

AlgebraicCurve.Place.kw_ffgc_finiteDimensional_adicCompletion

Source context 14 commands

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

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

Lean source · statement

instance kw_ffgc_finiteDimensional_adicCompletion [FiniteDimensional F F'] :
    FiniteDimensional (W.restrict F).adicCompletion W.adicCompletion

abbrev

kw_ffgc_completionTrace

L395 ↗

AlgebraicCurve.Place.kw_ffgc_completionTrace

Documentation

The trace from the extension completion to the base completion.

Source context 14 commands

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

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

Lean source · statement

abbrev kw_ffgc_completionTrace [FiniteDimensional F F'] :
    W.adicCompletion →ₗ[(W.restrict F).adicCompletion] (W.restrict F).adicCompletion

def

kw_ffgc_completionTraceF'

L400 ↗

AlgebraicCurve.Place.kw_ffgc_completionTraceF'

Documentation

The completed trace restricted to the original extension field.

Source context 14 commands

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

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

Lean source · statement

def kw_ffgc_completionTraceF' [FiniteDimensional F F'] : F' →ₗ[F] (W.restrict F).adicCompletion

theorem

kwHgfV352_valued_algebraMap_adicCompletion

L423 ↗

AlgebraicCurve.kwHgfV352_valued_algebraMap_adicCompletion

Source context 14 commands

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

noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
section LocalResidueCompletion
variable {K E : Type*} [Field K] [Field E] [Algebra K E]

Lean source · statement

theorem kwHgfV352_valued_algebraMap_adicCompletion (v : Place K E) (x : E) :
    Valued.v (algebraMap E v.adicCompletion x) = v.heightOneSpectrum.valuation E x

theorem

mem_of_ord_nonneg_placeCompletionAux

L431 ↗

AlgebraicCurve.Place.mem_of_ord_nonneg_placeCompletionAux

Source context 15 commands

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

noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
section LocalResidueCompletion
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
namespace Place

Lean source · statement

theorem mem_of_ord_nonneg_placeCompletionAux {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring

theorem

ord_nonneg_of_mem_placeCompletionAux

L440 ↗

AlgebraicCurve.Place.ord_nonneg_of_mem_placeCompletionAux

Source context 15 commands

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

noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
section LocalResidueCompletion
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
namespace Place

Lean source · statement

theorem ord_nonneg_of_mem_placeCompletionAux {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f

theorem

kwHgfV352_algebraMap_mem_adicCompletionIntegers_iff

L458 ↗

AlgebraicCurve.kwHgfV352_algebraMap_mem_adicCompletionIntegers_iff

Source context 14 commands

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

noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
section LocalResidueCompletion
variable {K E : Type*} [Field K] [Field E] [Algebra K E]

Lean source · statement

theorem kwHgfV352_algebraMap_mem_adicCompletionIntegers_iff (v : Place K E) (x : E) :
    algebraMap E v.adicCompletion x ∈ v.adicCompletionIntegers ↔ x ∈ v.toValuationSubring

theorem

kwHgfV352_exists_sub_mem_adicCompletionIntegers

L476 ↗

AlgebraicCurve.kwHgfV352_exists_sub_mem_adicCompletionIntegers

Source context 14 commands

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

noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
section LocalResidueCompletion
variable {K E : Type*} [Field K] [Field E] [Algebra K E]

Lean source · statement

theorem kwHgfV352_exists_sub_mem_adicCompletionIntegers (v : Place K E)
    (xh : v.adicCompletion) :
    ∃ x : E, algebraMap E v.adicCompletion x - xh ∈ v.adicCompletionIntegers

theorem

algebraMap_K_mem_adicCompletionIntegers

L504 ↗

ModularCurve.KwF4gRRTate.algebraMap_K_mem_adicCompletionIntegers

Source context 17 commands

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

noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing
noncomputable section
namespace ModularCurve.KwF4gRRTate
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)

Lean source · statement

theorem algebraMap_K_mem_adicCompletionIntegers (c : K) :
    algebraMap K u.adicCompletion c ∈ u.adicCompletionIntegers

def

algebraMapKIntegers

L510 ↗

ModularCurve.KwF4gRRTate.algebraMapKIntegers

Documentation

The map from the constant field to the integral valuation subring of the completion.

Source context 17 commands

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

noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing
noncomputable section
namespace ModularCurve.KwF4gRRTate
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)

Lean source · full declaration

def algebraMapKIntegers : K →+* u.adicCompletionIntegers where
  toFun c := ⟨algebraMap K u.adicCompletion c, algebraMap_K_mem_adicCompletionIntegers u c⟩
  map_one' := Subtype.ext (map_one _)
  map_mul' x y := Subtype.ext (map_mul _ x y)
  map_zero' := Subtype.ext (map_zero _)
  map_add' x y := Subtype.ext (map_add _ x y)

instance

instAlgebraKAdicCompletionIntegers

L517 ↗

ModularCurve.KwF4gRRTate.instAlgebraKAdicCompletionIntegers

Source context 17 commands

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

noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom
noncomputable section
open Polynomial IsLocalRing IsDedekindDomain
noncomputable section
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero
open scoped Valued WithZero
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing
noncomputable section
namespace ModularCurve.KwF4gRRTate
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)

Lean source · statement

instance instAlgebraKAdicCompletionIntegers : Algebra K u.adicCompletionIntegers

Module documentation

Completion

Declarations