NYLL
Module

TateTrace.lean

Nyll.AlgebraicCurves.Differentials.Residues.TateTrace
27 declarations indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

Finite-rank traces and Tate commutators on completions, with residue agreement and completed trace identities.

Imports14
Imported by13

Declarations

def

finrankTrace

L46 ↗
ModularCurve.KwF4gRRTate.finrankTrace
Documentation

The trace of an endomorphism restricted to its finite-dimensional range.

Source context 5 commands

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

open LinearMap Submodule
noncomputable section
namespace ModularCurve.KwF4gRRTate
section FinrankTrace
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
def finrankTrace (φ : V →ₗ[K] V) [FiniteDimensional K (LinearMap.range φ)] : K
def

tateComm

L57 ↗
ModularCurve.KwF4gRRTate.tateComm
Documentation

The difference of the two projected composites defining the Tate commutator.

Source context 5 commands

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

open LinearMap Submodule
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateComm
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
def tateComm (pA φ ψ : V →ₗ[K] V) : V →ₗ[K] V
theorem

tateComm_apply

L60 ↗
ModularCurve.KwF4gRRTate.tateComm_apply
Source context 5 commands

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

open LinearMap Submodule
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateComm
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateComm_apply (pA φ ψ : V →ₗ[K] V) (x : V) :
    tateComm pA φ ψ x = pA (φ (pA (ψ x))) - pA (ψ (pA (φ x)))
theorem

tateComm_mem_range

L63 ↗
ModularCurve.KwF4gRRTate.tateComm_mem_range
Source context 5 commands

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

open LinearMap Submodule
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateComm
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateComm_mem_range (pA φ ψ : V →ₗ[K] V) (x : V) :
    tateComm pA φ ψ x ∈ LinearMap.range pA
theorem

tateComm_antisymm

L67 ↗
ModularCurve.KwF4gRRTate.tateComm_antisymm
Source context 5 commands

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

open LinearMap Submodule
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateComm
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateComm_antisymm (pA φ ψ : V →ₗ[K] V) :
    tateComm pA φ ψ = - tateComm pA ψ φ
def

tateCommRestrict

L72 ↗
ModularCurve.KwF4gRRTate.tateCommRestrict
Documentation

The Tate commutator restricted to the range of the projection.

Source context 5 commands

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

open LinearMap Submodule
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateComm
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
def tateCommRestrict (pA φ ψ : V →ₗ[K] V) :
    LinearMap.range pA →ₗ[K] LinearMap.range pA
theorem

tateCommRestrict_apply

L76 ↗
ModularCurve.KwF4gRRTate.tateCommRestrict_apply
Source context 5 commands

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

open LinearMap Submodule
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateComm
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateCommRestrict_apply (pA φ ψ : V →ₗ[K] V) (a : LinearMap.range pA) :
    (tateCommRestrict pA φ ψ a : V) = tateComm pA φ ψ (a : V)
def

tateCommTrace

L80 ↗
ModularCurve.KwF4gRRTate.tateCommTrace
Documentation

The trace of the Tate commutator on the finite-dimensional range of its restriction.

Source context 5 commands

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

open LinearMap Submodule
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateComm
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
def tateCommTrace (pA φ ψ : V →ₗ[K] V)
    [FiniteDimensional K (LinearMap.range (tateCommRestrict pA φ ψ))] : K
theorem

tateComm_eq_of_commute

L90 ↗
ModularCurve.KwF4gRRTate.tateComm_eq_of_commute
Source context 5 commands

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

open LinearMap Submodule
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateFactoring
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateComm_eq_of_commute {pA φ ψ : V →ₗ[K] V}
    (hcomm : φ ∘ₗ ψ = ψ ∘ₗ φ) (a : V) :
    tateComm pA φ ψ a
      = pA (ψ (φ a - pA (φ a))) - pA (φ (ψ a - pA (ψ a)))
def

kaehlerPullback

L119 ↗
AlgebraicCurve.kaehlerPullback
Documentation

Pullback of a Kähler differential along the scalar tower.

Source context 7 commands

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

open LinearMap Submodule
noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
section CorrectedCarrier
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (E : Type*) [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
Lean source · statement
def kaehlerPullback (ωE : Ω[E⁄K]) : Ω[F⁄K]
def

regularSubmodule

L146 ↗
AlgebraicCurve.Place.regularSubmodule
Documentation

Functions whose product with the differential coefficient is integral at the chosen place.

Source context 6 commands

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

open LinearMap Submodule
noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
namespace Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
def regularSubmodule (w : Place K F) (ωF : Ω[F⁄K]) : Submodule K F where
  carrier := {f : F | f * w.differentialCoeff ωF ∈ w.toValuationSubring}
  zero_mem' := by simp only [Set.mem_ofPred_eq, zero_mul]; exact zero_mem _
  add_mem' {f g} hf hg := by
    simp only [Set.mem_ofPred_eq, add_mul]; exact add_mem hf hg
  smul_mem' c f hf := by
    simp only [Set.mem_ofPred_eq, Algebra.smul_def, mul_assoc]
    exact mul_mem (w.algebraMap_mem' c) hf
abbrev

kaehlerCotrace

L173 ↗
AlgebraicCurve.kaehlerCotrace
Documentation

The scalar-linear Kähler differential map along the field extension.

Source context 6 commands

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

open LinearMap Submodule
noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
section KaehlerCotrace
variable (K E F : Type*) [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
Lean source · statement
abbrev kaehlerCotrace : Ω[E⁄K] →ₗ[E] Ω[F⁄K]
def

kwHgfV352_localResidueCompletion

L198 ↗
AlgebraicCurve.kwHgfV352_localResidueCompletion
Documentation

The residue of a chosen field representative of a completion element modulo the completion integers.

Source context 7 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
section LocalResidueCompletion
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
variable [HasCanonicalLocalResidueKStar K E]
Lean source · statement
def kwHgfV352_localResidueCompletion (v : Place K E) (xh : v.adicCompletion) :
    v.ResidueField
def

kwHgfV352_completionTraceAt

L211 ↗
AlgebraicCurve.kwHgfV352_completionTraceAt
Documentation

The completed field trace at a place, transported to the completion of its base place.

Source context 8 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
section CompletionTraceAt
variable {K : Type*} [Field K] {F : Type*} [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
Lean source · statement
def kwHgfV352_completionTraceAt [FiniteDimensional E F]
    (v : Place K E) (w' : Place K F) (hw' : w' ∈ v.fiber F) (g : F) :
    v.adicCompletion
def

KwHgfV352R3MPGKPowBasisLocal

L227 ↗
AlgebraicCurve.KwHgfV352R3MPGKPowBasisLocal
Documentation

The local residue and completed-trace identity for powers of an integral element multiplied by inverse uniformizer powers.

Source context 9 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
section MPGKPowBasisLocalMint
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (E : Type*) [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [HasCanonicalLocalResidueKStar K E] [HasCanonicalLocalResidueKStar K F]
variable [Algebra.IsIntegral E F]
Lean source · statement
def KwHgfV352R3MPGKPowBasisLocal : Prop
def

KwHgfV352CompletionTraceSum

L255 ↗
AlgebraicCurve.KwHgfV352CompletionTraceSum
Documentation

The field trace in a base completion equals the sum of the completed traces over its place fibre.

Source context 8 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
section CompletionTraceSumMint
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (E : Type*) [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
def KwHgfV352CompletionTraceSum : Prop
def

adicIntegersKSubmod

L277 ↗
ModularCurve.KwF4gRRTate.adicIntegersKSubmod
Documentation

The completion integers viewed as a submodule over the base field.

Source context 9 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateProj
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · full declaration
def adicIntegersKSubmod : Submodule K u.adicCompletion where
  carrier := u.adicCompletionIntegers
  add_mem' := add_mem
  zero_mem' := zero_mem _
  smul_mem' c x hx := by
    rw [Algebra.smul_def]
    exact mul_mem (by
      rw [IsScalarTower.algebraMap_apply K L u.adicCompletion]
      exact (kwHgfV352_algebraMap_mem_adicCompletionIntegers_iff u _).mpr
        (u.algebraMap_mem' c)) hx
def

tateProj

L289 ↗
ModularCurve.KwF4gRRTate.tateProj
Documentation

A projection onto the completion integers along a chosen complementary submodule.

Source context 9 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateProj
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
def tateProj : u.adicCompletion →ₗ[K] u.adicCompletion
abbrev

lmulK

L302 ↗
ModularCurve.KwF4gRRTate.lmulK
Documentation

Multiplication by a completion element as a base-field linear endomorphism.

Source context 9 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateResDef
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
abbrev lmulK (fh : u.adicCompletion) : u.adicCompletion →ₗ[K] u.adicCompletion
def

tateRes

L307 ↗
ModularCurve.KwF4gRRTate.tateRes
Documentation

The Tate commutator trace of two multiplication endomorphisms with respect to the integer projection.

Source context 9 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateResDef
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
def tateRes (fh gh : u.adicCompletion)
    [FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u fh) (lmulK u gh)))] : K
def

KwF4gRRTateCommFinite

L319 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTateCommFinite
Documentation

All the projected Tate commutators have finite-dimensional range.

Source context 9 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateAtoms
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
Lean source · statement
def KwF4gRRTateCommFinite : Prop
def

KwF4gRRTateAgreement

L328 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTateAgreement
Documentation

The Tate residue against the uniformizer agrees with the traced local completion residue.

Source context 10 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateAtoms
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
Lean source · statement
def KwF4gRRTateAgreement (hfin : KwF4gRRTateCommFinite K L) : Prop
def

KwF4gRRTateChainRule

L340 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTateChainRule
Documentation

The Tate residue transforms by the pulled-back differential coefficient under a place extension.

Source context 13 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateAtoms
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
variable (F E : Type*) [Field F] [Algebra K F] [Field E] [Algebra K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
variable [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E]
Lean source · statement
def KwF4gRRTateChainRule (hfinF : KwF4gRRTateCommFinite K F) : Prop
def

KwF4gRRTateTraceCompat

L356 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTateTraceCompat
Documentation

The upstairs Tate residue agrees with the downstairs Tate residue of the completed trace.

Source context 13 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve.KwF4gRRTate
section TateAtoms
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
variable (F E : Type*) [Field F] [Algebra K F] [Field E] [Algebra K E]
variable [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
variable [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E]
Lean source · statement
def KwF4gRRTateTraceCompat (hfinF : KwF4gRRTateCommFinite K F)
    (hfinE : KwF4gRRTateCommFinite K E) : Prop
def

KwF4R1V391aResidueTraceCompletionCommute

L390 ↗
ModularCurve.KwF4R1V391a.KwF4R1V391aResidueTraceCompletionCommute
Documentation

A pulled-back coordinate differential residue equals the base completion residue of the completed trace.

Source context 13 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open ModularCurve.KwF4gRRTate
open AlgebraicCurve AlgebraicCurve.Place KaehlerDifferential
noncomputable section
namespace ModularCurve.KwF4R1V391a
section Mint
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (E : Type*) [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable [HasCanonicalLocalResidueKStar K E] [HasCanonicalLocalResidueKStar K F]
Lean source · statement
def KwF4R1V391aResidueTraceCompletionCommute
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F] : Prop
def

FiberKaehlerCotraceResidueIdentityK

L419 ↗
AlgebraicCurve.FiberKaehlerCotraceResidueIdentityK
Documentation

An upstairs canonical residue family induces a base residue family compatible with differential pullback and the trace over each place fibre.

Source context 15 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open ModularCurve.KwF4gRRTate
open AlgebraicCurve AlgebraicCurve.Place KaehlerDifferential
noncomputable section
noncomputable section
namespace AlgebraicCurve
open scoped Polynomial
section KCurrencyRow
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (E : Type*) [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [HasCanonicalLocalResidueKStar K E] [HasCanonicalLocalResidueKStar K F]
variable [Algebra.IsIntegral E F]
Lean source · statement
def FiberKaehlerCotraceResidueIdentityK : Prop
def

CotraceResidueIdentityOnFiberLocalizedK

L450 ↗
AlgebraicCurve.CotraceResidueIdentityOnFiberLocalizedK
Documentation

A base canonical residue family satisfies the fibre trace identity for functions singular at at most one place of each fibre.

Source context 15 commands

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

open LinearMap Submodule
open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain
noncomputable section
open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open ModularCurve.KwF4gRRTate
open AlgebraicCurve AlgebraicCurve.Place KaehlerDifferential
noncomputable section
noncomputable section
namespace AlgebraicCurve
open scoped Polynomial
section KCurrencyRowA
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (E : Type*) [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [HasCanonicalLocalResidueKStar K E] [HasCanonicalLocalResidueKStar K F]
variable [Algebra.IsIntegral E F]
Lean source · statement
def CotraceResidueIdentityOnFiberLocalizedK : Prop

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