NYLL
Module

TateChainRule.lean

Nyll.AlgebraicCurves.Differentials.Residues.TateChainRule
121 declarations indexed from sourceView source ↗

Module documentation

The chain rule for Tate residue constructions.

Imports44
Imported by3

Declarations

theorem

maximalIdeal_le

L179 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.IsLocalRing.maximalIdeal_le
Source context 5 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
open scoped _root_.IsLocalRing in
Lean source · statement
theorem IsLocalRing.maximalIdeal_le {R : Type*} [CommSemiring R] [IsLocalRing R] {J : Ideal R}
    (hJ : J ≠ ⊤) (h : IsLocalRing.maximalIdeal R ≤ J) :
    J.IsMaximal
instance

instAlgebraSubtypeMemValuationSubring_fLT

L184 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.instAlgebraSubtypeMemValuationSubring_fLT
Source context 4 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
Lean source · full declaration
instance instAlgebraSubtypeMemValuationSubring_fLT {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
theorem

ord_nonneg_of_mem

L345 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem
Source context 17 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem {f : F} (hf : f ∈
    v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L362 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg
Source context 18 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤
    v.ord f) :
    f ∈ v.toValuationSubring
theorem

mem_iff_ord_nonneg

L372 ↗
AlgebraicCurve.Place.mem_iff_ord_nonneg
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f
theorem

exists_ord_pos

L377 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.AlgebraicCurve.Place.exists_ord_pos
Source context 20 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem exists_ord_pos : ∃ f : F, f ≠ 0 ∧ 0 < v.ord f
theorem

algebraMap_ne_zero

L391 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.AlgebraicCurve.Place.algebraMap_ne_zero
Source context 17 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
Lean source · statement
theorem algebraMap_ne_zero {f : F} (hf : f ≠ 0) : algebraMap F F' f ≠ 0
theorem

comap_algebraMap_ne_top

L396 ↗
AlgebraicCurve.Place.comap_algebraMap_ne_top
Source context 18 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
Lean source · statement
theorem _root_.AlgebraicCurve.Place.comap_algebraMap_ne_top [Algebra.IsIntegral F F'] :
    w.toValuationSubring.comap (algebraMap F F') ≠ ⊤
theorem

mem_comap_iff_ord_nonneg

L414 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.AlgebraicCurve.Place.mem_comap_iff_ord_nonneg
Source context 20 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
Lean source · statement
theorem mem_comap_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ w.toValuationSubring.comap (algebraMap F F') ↔
      0 ≤ w.ord (algebraMap F F' f)
theorem

isUnit_mk_comap_iff

L421 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.AlgebraicCurve.Place.isUnit_mk_comap_iff
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
Lean source · statement
theorem isUnit_mk_comap_iff {f : F} (hf : f ≠ 0)
    (hmem : f ∈ w.toValuationSubring.comap (algebraMap F F')) :
    IsUnit (⟨f, hmem⟩ : w.toValuationSubring.comap (algebraMap F F')) ↔
      w.ord (algebraMap F F' f) = 0
theorem

exists_ord_algebraMap_pos

L446 ↗
AlgebraicCurve.Place.exists_ord_algebraMap_pos
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_ord_algebraMap_pos [Algebra.IsIntegral F F'] :
    ∃ f : F, f ≠ 0 ∧ 0 < w.ord (algebraMap F F' f)
theorem

ramificationIndex_set_nonempty

L463 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.AlgebraicCurve.Place.ramificationIndex_set_nonempty
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
variable [Algebra.IsIntegral F F']
Lean source · statement
theorem ramificationIndex_set_nonempty :
    {n : ℕ | 0 < n ∧ ∃ f : F, f ≠ 0 ∧ w.ord (algebraMap F F' f) = n}.Nonempty
theorem

isPrincipalIdealRing_comap

L468 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.AlgebraicCurve.Place.isPrincipalIdealRing_comap
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place
variable {w} in
variable {w} in
open _root_.AlgebraicCurve.Place
variable [Algebra.IsIntegral F F']
Lean source · statement
theorem isPrincipalIdealRing_comap :
    IsPrincipalIdealRing (w.toValuationSubring.comap (algebraMap F F'))
theorem

valued_eq_one_of_isUnit

L539 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ValuationSubring.valued_eq_one_of_isUnit
Source context 8 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
section
variable {F : Type*} [Field F]
open scoped _root_.ValuationSubring in
Lean source · statement
theorem ValuationSubring.valued_eq_one_of_isUnit {K : Type*} [Field K] {Γ₀ : Type*}
    [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : hv.v.valuationSubring)
    (hx : IsUnit x) : Valued.v x.val = 1
theorem

isUnit_of_valued_eq_one

L550 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ValuationSubring.isUnit_of_valued_eq_one
Source context 8 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
section
variable {F : Type*} [Field F]
open scoped _root_.ValuationSubring in
Lean source · statement
theorem ValuationSubring.isUnit_of_valued_eq_one {K : Type*} [Field K] {Γ₀ : Type*}
    [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : hv.v.valuationSubring)
    (hx : Valued.v x.val = 1) : IsUnit x
theorem

isUnit_iff_valued_eq_one

L561 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ValuationSubring.isUnit_iff_valued_eq_one
Source context 8 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
section
variable {F : Type*} [Field F]
open scoped _root_.ValuationSubring in
Lean source · statement
theorem ValuationSubring.isUnit_iff_valued_eq_one {K : Type*} [Field K] {Γ₀ : Type*}
    [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀] (x : hv.v.valuationSubring) :
    IsUnit x ↔ Valued.v x.val = 1
theorem

kaehlerPullback_D

L755 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.AlgebraicCurve.kaehlerPullback_D
Source context 18 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.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]
variable {K F E}
Lean source · statement
theorem
    kaehlerPullback_D (e : E) :
    kaehlerPullback K F E (KaehlerDifferential.D K E e)
      = KaehlerDifferential.D K F (algebraMap E F e)
theorem

mem_adicIntegersKSubmod_iff

L840 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.mem_adicIntegersKSubmod_iff
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateProj
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem mem_adicIntegersKSubmod_iff (x : u.adicCompletion) :
    x ∈ adicIntegersKSubmod u ↔ x ∈ u.adicCompletionIntegers
theorem

tateProj_mem_integers

L843 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateProj_mem_integers
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateProj
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem tateProj_mem_integers (x : u.adicCompletion) :
    tateProj u x ∈ u.adicCompletionIntegers
theorem

tateProj_of_mem

L850 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateProj_of_mem
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateProj
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem tateProj_of_mem {x : u.adicCompletion} (hx : x ∈ u.adicCompletionIntegers) :
    tateProj u x = x
theorem

tateProj_idem

L858 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateProj_idem
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateProj
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem tateProj_idem : tateProj u ∘ₗ tateProj u = tateProj u
theorem

range_tateProj

L863 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.range_tateProj
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateProj
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem range_tateProj : LinearMap.range (tateProj u) = adicIntegersKSubmod u
def

poleWindowKSubmod

L925 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.poleWindowKSubmod
Documentation

The sections whose product with the chosen uniformizer power is integral.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindow
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · full declaration
def poleWindowKSubmod (πh : u.adicCompletionIntegers) (M : ℕ) :
    Submodule K u.adicCompletion where
  carrier := {x | (πh : u.adicCompletion)^M * x ∈ u.adicCompletionIntegers}
  add_mem' {a b} ha hb := by
    simp only [Set.mem_ofPred_eq, mul_add] at ha hb ⊢; exact add_mem ha hb
  zero_mem' := by simp only [Set.mem_ofPred_eq, mul_zero]; exact zero_mem _
  smul_mem' c x hx := by
    simp only [Set.mem_ofPred_eq] at hx ⊢
    rw [Algebra.smul_def, IsScalarTower.algebraMap_apply K L u.adicCompletion, mul_left_comm]
    exact mul_mem ((kwHgfV352_algebraMap_mem_adicCompletionIntegers_iff u _).mpr
      (u.algebraMap_mem' c)) hx
theorem

mem_poleWindowKSubmod_iff

L937 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.mem_poleWindowKSubmod_iff
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindow
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem mem_poleWindowKSubmod_iff (πh : u.adicCompletionIntegers) (M : ℕ)
    (x : u.adicCompletion) :
    x ∈ poleWindowKSubmod u πh M ↔ (πh : u.adicCompletion)^M * x ∈ u.adicCompletionIntegers
theorem

adicIntegersKSubmod_le_poleWindowKSubmod

L942 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.adicIntegersKSubmod_le_poleWindowKSubmod
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindow
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem adicIntegersKSubmod_le_poleWindowKSubmod (πh : u.adicCompletionIntegers) (M : ℕ) :
    adicIntegersKSubmod u ≤ poleWindowKSubmod u πh M
theorem

kwF4gRRTate_clearPole

L946 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.kwF4gRRTate_clearPole
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindow
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem kwF4gRRTate_clearPole (πh : u.adicCompletionIntegers) (hπh : Irreducible πh)
    (fh : u.adicCompletion) :
    ∃ M : ℕ, (πh : u.adicCompletion)^M * fh ∈ u.adicCompletionIntegers
def

KwF4gRRTatePoleWindowFinite

L973 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.KwF4gRRTatePoleWindowFinite
Documentation

Finite dimensionality of each bounded pole window modulo integral sections.

Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindow
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (K L) in
Lean source · statement
def KwF4gRRTatePoleWindowFinite : Prop
theorem

isOpen_setOf_valued_le

L1013 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.isOpen_setOf_valued_le
Source context 18 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open scoped _root_.WithZero _root_.Multiplicative _root_.Topology
open _root_.Filter
namespace IsDedekindDomain
open _root_.IsDedekindDomain
namespace HeightOneSpectrum
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsDedekindDomain
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
namespace adicCompletion
open _root_.IsDedekindDomain.HeightOneSpectrum.adicCompletion
open _root_.IsDedekindDomain.HeightOneSpectrum.adicCompletion
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
Lean source · statement
theorem
_root_.AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.isOpen_setOf_valued_le
    {γ : ℤᵐ⁰} (hγ : γ ≠ 0) :
    IsOpen {y : v.adicCompletion K | Valued.v y ≤ γ}
instance

kwF4R1V410a_subsingletonHeightOneSpectrumDVR

L1068 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4R1V410a.kwF4R1V410a_subsingletonHeightOneSpectrumDVR
Source context 16 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V410a
open _root_.ModularCurve
Lean source · statement
instance kwF4R1V410a_subsingletonHeightOneSpectrumDVR
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] :
    Subsingleton (HeightOneSpectrum O)
theorem

kwF4R1V410a_algebraMap_mem_completionIdeal_pow_iff

L1084 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4R1V410a.kwF4R1V410a_algebraMap_mem_completionIdeal_pow_iff
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V410a
open _root_.ModularCurve
section Bridge
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
local notation "O_w" => w.toValuationSubring
local notation "𝔪_w" => IsLocalRing.maximalIdeal w.toValuationSubring
local notation "O_W" => w.adicCompletionIntegers
local notation "𝔪_W" => w.heightOneSpectrum.completionIdeal F
Lean source · statement
theorem kwF4R1V410a_algebraMap_mem_completionIdeal_pow_iff (n : ℕ) (x : O_w) :
    algebraMap (O_w) (O_W) x ∈ (𝔪_W) ^ n ↔ x ∈ (𝔪_w) ^ n
theorem

kwF4R1V410a_exists_sub_mem_completionIdeal_pow

L1095 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4R1V410a.kwF4R1V410a_exists_sub_mem_completionIdeal_pow
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V410a
open _root_.ModularCurve
section Bridge
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
local notation "O_w" => w.toValuationSubring
local notation "𝔪_w" => IsLocalRing.maximalIdeal w.toValuationSubring
local notation "O_W" => w.adicCompletionIntegers
local notation "𝔪_W" => w.heightOneSpectrum.completionIdeal F
Lean source · statement
theorem kwF4R1V410a_exists_sub_mem_completionIdeal_pow (n : ℕ) (y : O_W) :
    ∃ x : O_w, y - algebraMap (O_w) (O_W) x ∈ (𝔪_W) ^ n
def

kwF4R1V410a_quotientEquiv

L1137 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.kwF4R1V410a_quotientEquiv
Documentation

The quotient ring equivalence induced by completion modulo powers of the maximal ideal.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V410a
open _root_.ModularCurve
section Bridge
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
local notation "O_w" => w.toValuationSubring
local notation "𝔪_w" => IsLocalRing.maximalIdeal w.toValuationSubring
local notation "O_W" => w.adicCompletionIntegers
local notation "𝔪_W" => w.heightOneSpectrum.completionIdeal F
Lean source · statement
def _root_.AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.kwF4R1V410a_quotientEquiv
    (n : ℕ) :
    (O_w) ⧸ (𝔪_w) ^ n ≃+* (O_W) ⧸ (𝔪_W) ^ n
theorem

kwF4R1V410a_quotientEquiv_mk

L1157 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.kwF4R1V410a_quotientEquiv_mk
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V410a
open _root_.ModularCurve
section Bridge
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
local notation "O_w" => w.toValuationSubring
local notation "𝔪_w" => IsLocalRing.maximalIdeal w.toValuationSubring
local notation "O_W" => w.adicCompletionIntegers
local notation "𝔪_W" => w.heightOneSpectrum.completionIdeal F
Lean source · statement
theorem
_root_.AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.kwF4R1V410a_quotientEquiv_mk
    (n : ℕ) (x : O_w) :
    TateChainRule.kwF4R1V410a_quotientEquiv
      w n (Ideal.Quotient.mk _ x)
      = Ideal.Quotient.mk _ (algebraMap (O_w) (O_W) x)
theorem

coe_smul_K

L1199 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.coe_smul_K
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem coe_smul_K (c : K) (x : u.adicCompletionIntegers) :
    ((c • x : u.adicCompletionIntegers) : u.adicCompletion) = c • (x : u.adicCompletion)
def

poleWindowShift

L1205 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.poleWindowShift
Documentation

Multiplication by the uniformizer power from the bounded pole window to integral sections.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · full declaration
def poleWindowShift (πh : u.adicCompletionIntegers) (M : ℕ) :
    poleWindowKSubmod u πh M →ₗ[K] u.adicCompletionIntegers where
  toFun x := ⟨(πh : u.adicCompletion)^M * (x : u.adicCompletion), x.2⟩
  map_add' x y := by apply Subtype.ext; push_cast; ring
  map_smul' c x := by
    apply Subtype.ext
    rw [coe_smul_K]
    change (πh : u.adicCompletion)^M * (c • (x : u.adicCompletion))
        = c • ((πh : u.adicCompletion)^M * (x : u.adicCompletion))
    rw [mul_smul_comm]
theorem

poleWindowShift_injective

L1216 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.poleWindowShift_injective
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem poleWindowShift_injective (πh : u.adicCompletionIntegers) (hπh : Irreducible πh)
    (M : ℕ) : Function.Injective (poleWindowShift u πh M)
theorem

poleWindowShift_surjective

L1231 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.poleWindowShift_surjective
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem poleWindowShift_surjective (πh : u.adicCompletionIntegers) (hπh : Irreducible πh)
    (M : ℕ) : Function.Surjective (poleWindowShift u πh M)
def

poleWindowShiftEquiv

L1246 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.poleWindowShiftEquiv
Documentation

The linear equivalence between a bounded pole window and integral sections given by multiplication.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
def poleWindowShiftEquiv (πh : u.adicCompletionIntegers) (hπh : Irreducible πh) (M : ℕ) :
    poleWindowKSubmod u πh M ≃ₗ[K] u.adicCompletionIntegers
def

piPowKSubmod

L1252 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.piPowKSubmod
Documentation

The submodule of integral sections divisible by the chosen uniformizer power.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · full declaration
def piPowKSubmod (πh : u.adicCompletionIntegers) (M : ℕ) :
    Submodule K u.adicCompletionIntegers where
  carrier := {y | ∃ x : u.adicCompletionIntegers, y = πh^M * x}
  add_mem' := by rintro a b ⟨xa, rfl⟩ ⟨xb, rfl⟩; exact ⟨xa + xb, by ring⟩
  zero_mem' := ⟨0, by ring⟩
  smul_mem' c y := by
    rintro ⟨x, rfl⟩
    exact ⟨c • x, by rw [Algebra.smul_def, Algebra.smul_def, mul_left_comm]⟩
theorem

poleWindowShift_image_integers

L1261 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.poleWindowShift_image_integers
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem poleWindowShift_image_integers (πh : u.adicCompletionIntegers) (M : ℕ) :
    Submodule.map (poleWindowShift u πh M)
        ((adicIntegersKSubmod u).comap (poleWindowKSubmod u πh M).subtype)
      = piPowKSubmod u πh M
def

KwF4gRRTateDVRQuotPowKFinite

L1277 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.KwF4gRRTateDVRQuotPowKFinite
Documentation

Finite dimensionality of integral sections modulo each uniformizer power.

Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (K L) in
Lean source · statement
def KwF4gRRTateDVRQuotPowKFinite : Prop
theorem

kwF4gRRTate_poleWindowFinite_of_DVRQuotPowKFinite

L1282 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.kwF4gRRTate_poleWindowFinite_of_DVRQuotPowKFinite
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section PoleWindowShift
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (K L) in
Lean source · statement
theorem kwF4gRRTate_poleWindowFinite_of_DVRQuotPowKFinite
    (hDVR : KwF4gRRTateDVRQuotPowKFinite K L) :
    KwF4gRRTatePoleWindowFinite K L
theorem

range_comp_map_left

L1328 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.range_comp_map_left
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section FinrankTraceCyclicity
variable {K M N : Type*} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N]
Lean source · statement
theorem range_comp_map_left (f : M →ₗ[K] N) (g : N →ₗ[K] M) :
    ∀ x ∈ LinearMap.range (g ∘ₗ f), f x ∈ LinearMap.range (f ∘ₗ g)
theorem

finrankTrace_comp_comm

L1333 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finrankTrace_comp_comm
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section FinrankTraceCyclicity
variable {K M N : Type*} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N]
Lean source · statement
theorem finrankTrace_comp_comm (f : M →ₗ[K] N) (g : N →ₗ[K] M)
    [FiniteDimensional K (LinearMap.range (g ∘ₗ f))]
    [FiniteDimensional K (LinearMap.range (f ∘ₗ g))] :
    finrankTrace (g ∘ₗ f) = finrankTrace (f ∘ₗ g)
theorem

finrankTrace_eq_trace_on_superspace

L1381 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finrankTrace_eq_trace_on_superspace
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TraceOnSuperspace
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · full declaration
theorem finrankTrace_eq_trace_on_superspace
    (φ : V →ₗ[K] V) (W : Submodule K V) [FiniteDimensional K W]
    (hrange : LinearMap.range φ ≤ W) (hW : ∀ x ∈ W, φ x ∈ W) :
    have : FiniteDimensional K (LinearMap.range φ) :=
      Submodule.finiteDimensional_of_le hrange
    finrankTrace φ = LinearMap.trace K W (φ.restrict hW) := by
  have : FiniteDimensional K (LinearMap.range φ) := Submodule.finiteDimensional_of_le hrange
  let i : LinearMap.range φ →ₗ[K] W := Submodule.inclusion hrange
  let π : W →ₗ[K] LinearMap.range φ :=
    { toFun := fun w => ⟨φ (w : V), LinearMap.mem_range_self φ (w : V)⟩
      map_add' := fun w₁ w₂ => by simp
      map_smul' := fun c w => by simp }
  have hip : i ∘ₗ π = φ.restrict hW := by
    apply LinearMap.ext; intro w; apply Subtype.ext; rfl
  have hpi : π ∘ₗ i = φ.restrict (fun x _ => LinearMap.mem_range_self φ x) := by
    apply LinearMap.ext; intro x; apply Subtype.ext; rfl
  unfold finrankTrace
  rw [← hpi, ← hip, LinearMap.trace_comp_comm']
theorem

finrankTrace_sub_eq

L1406 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finrankTrace_sub_eq
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Additivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · full declaration
theorem finrankTrace_sub_eq
    (φ ψ : V →ₗ[K] V)
    [FiniteDimensional K (LinearMap.range φ)]
    [FiniteDimensional K (LinearMap.range ψ)] :
    have : FiniteDimensional K
        ((LinearMap.range φ ⊔ LinearMap.range ψ : Submodule K V) : Type _) :=
      Submodule.finiteDimensional_sup _ _
    finrankTrace φ - finrankTrace ψ
      = LinearMap.trace K (LinearMap.range φ ⊔ LinearMap.range ψ : Submodule K V)
          ((φ - ψ).restrict
            (p := (LinearMap.range φ ⊔ LinearMap.range ψ : Submodule K V))
            (fun x _ => sub_mem
              (Submodule.mem_sup_left (LinearMap.mem_range_self φ x))
              (Submodule.mem_sup_right (LinearMap.mem_range_self ψ x)))) := by
  set W' : Submodule K V := LinearMap.range φ ⊔ LinearMap.range ψ with hW'
  have : FiniteDimensional K W' := Submodule.finiteDimensional_sup _ _
  have hφW : ∀ x ∈ W', φ x ∈ W' := fun x _ =>
    Submodule.mem_sup_left (LinearMap.mem_range_self φ x)
  have hψW : ∀ x ∈ W', ψ x ∈ W' := fun x _ =>
    Submodule.mem_sup_right (LinearMap.mem_range_self ψ x)
  rw [finrankTrace_eq_trace_on_superspace φ W' le_sup_left hφW,
    finrankTrace_eq_trace_on_superspace ψ W' le_sup_right hψW,
    ← map_sub]
  refine congrArg (LinearMap.trace K W') (LinearMap.ext fun x => Subtype.ext ?_)
  rfl
theorem

piPowKSubmod_eq_restrictScalars

L1468 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.piPowKSubmod_eq_restrictScalars
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRQuotDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem piPowKSubmod_eq_restrictScalars (πh : u.adicCompletionIntegers) (M : ℕ) :
    piPowKSubmod u πh M
      = (Ideal.span {πh^M} : Ideal u.adicCompletionIntegers).restrictScalars K
def

quotPiPowEquivIdealQuot

L1477 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.quotPiPowEquivIdealQuot
Documentation

The linear equivalence identifying the divisibility quotient with the principal ideal quotient.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRQuotDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
def quotPiPowEquivIdealQuot (πh : u.adicCompletionIntegers) (M : ℕ) :
    (u.adicCompletionIntegers ⧸ piPowKSubmod u πh M)
      ≃ₗ[K] (u.adicCompletionIntegers ⧸ (Ideal.span {πh^M} : Ideal u.adicCompletionIntegers))
def

KwF4gRRTateDVRCotangentKFinite

L1485 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.KwF4gRRTateDVRCotangentKFinite
Documentation

Finite dimensionality of integral sections modulo a uniformizer.

Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRQuotDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (K L) in
Lean source · statement
def KwF4gRRTateDVRCotangentKFinite : Prop
theorem

range_mulLeft_eq_restrictScalars_span

L1490 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.range_mulLeft_eq_restrictScalars_span
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRQuotDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (K L) in
Lean source · statement
theorem range_mulLeft_eq_restrictScalars_span (a : u.adicCompletionIntegers) :
    LinearMap.range (LinearMap.mulLeft K a)
      = (Ideal.span {a} : Ideal u.adicCompletionIntegers).restrictScalars K
theorem

finiteDimensional_restrictScalarsQuot_pow

L1499 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finiteDimensional_restrictScalarsQuot_pow
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRQuotDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (K L) in
Lean source · statement
theorem finiteDimensional_restrictScalarsQuot_pow [u.FiniteResidue]
    (hCot : KwF4gRRTateDVRCotangentKFinite K L)
    (πh : u.adicCompletionIntegers) (hπh : Irreducible πh) (M : ℕ) :
    FiniteDimensional K (u.adicCompletionIntegers ⧸
      (Ideal.span {πh^M} : Ideal u.adicCompletionIntegers).restrictScalars K)
theorem

finiteDimensional_idealQuot_pow

L1561 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finiteDimensional_idealQuot_pow
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRQuotDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (K L) in
Lean source · statement
theorem finiteDimensional_idealQuot_pow [u.FiniteResidue]
    (hCot : KwF4gRRTateDVRCotangentKFinite K L)
    (πh : u.adicCompletionIntegers) (hπh : Irreducible πh) (M : ℕ) :
    FiniteDimensional K
      (u.adicCompletionIntegers ⧸ (Ideal.span {πh^M} : Ideal u.adicCompletionIntegers))
theorem

kwF4gRRTate_DVRQuotPowKFinite_of_cotangent

L1569 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.kwF4gRRTate_DVRQuotPowKFinite_of_cotangent
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRQuotDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (K L) in
Lean source · statement
theorem kwF4gRRTate_DVRQuotPowKFinite_of_cotangent
    (hCot : KwF4gRRTateDVRCotangentKFinite K L) :
    KwF4gRRTateDVRQuotPowKFinite K L
instance

instIsScalarTower_K_toValuationSubring_adicCompletionIntegers

L1612 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.instIsScalarTower_K_toValuationSubring_adicCompletionIntegers
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRCotangentDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
instance instIsScalarTower_K_toValuationSubring_adicCompletionIntegers :
    IsScalarTower K u.toValuationSubring u.adicCompletionIntegers
theorem

span_irreducible_eq_completionIdeal_pow_one

L1621 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.span_irreducible_eq_completionIdeal_pow_one
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRCotangentDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem span_irreducible_eq_completionIdeal_pow_one
    (πh : u.adicCompletionIntegers) (hπh : Irreducible πh) :
    (Ideal.span {πh} : Ideal u.adicCompletionIntegers)
      = (u.heightOneSpectrum.completionIdeal L) ^ 1
def

quotientEquivKAlg

L1628 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.quotientEquivKAlg
Documentation

The completion quotient equivalence as an algebra equivalence over the base field.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRCotangentDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
def quotientEquivKAlg (n : ℕ) :
    (u.toValuationSubring ⧸ (IsLocalRing.maximalIdeal u.toValuationSubring) ^ n)
      ≃ₐ[K] (u.adicCompletionIntegers ⧸ (u.heightOneSpectrum.completionIdeal L) ^ n)
def

quotSpanIrreducibleEquivResidueField

L1645 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.quotSpanIrreducibleEquivResidueField
Documentation

The linear equivalence from the quotient by a uniformizer to the residue field.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRCotangentDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
def quotSpanIrreducibleEquivResidueField (πh : u.adicCompletionIntegers) (hπh : Irreducible πh) :
    (u.adicCompletionIntegers ⧸ (Ideal.span {πh} : Ideal u.adicCompletionIntegers))
      ≃ₗ[K] u.ResidueField
theorem

kwF4gRRTate_DVRCotangentKFinite

L1654 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.kwF4gRRTate_DVRCotangentKFinite
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DVRCotangentDischarge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem kwF4gRRTate_DVRCotangentKFinite : KwF4gRRTateDVRCotangentKFinite K L
def

KwF4gRRTatePoleWindowImageFinite

L1701 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.KwF4gRRTatePoleWindowImageFinite
Documentation

Finite dimensionality of multiplication images of integral sections modulo integral sections.

Source context 20 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TermRangeFinite
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable [u.FiniteResidue]
Lean source · statement
def KwF4gRRTatePoleWindowImageFinite : Prop
theorem

kwF4gRRTate_poleWindowFinite

L1746 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.kwF4gRRTate_poleWindowFinite
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Composite
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem kwF4gRRTate_poleWindowFinite : KwF4gRRTatePoleWindowFinite K L
theorem

lmul_adicIntegers_subset_poleWindow

L1757 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.lmul_adicIntegers_subset_poleWindow
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Subset
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem lmul_adicIntegers_subset_poleWindow (fh : u.adicCompletion)
    (πh : u.adicCompletionIntegers) (M : ℕ)
    (hfhM : (πh : u.adicCompletion) ^ M * fh ∈ u.adicCompletionIntegers) :
    Submodule.map (lmulK u fh) (adicIntegersKSubmod u) ≤ poleWindowKSubmod u πh M
theorem

kwF4gRRTate_poleWindowImageFinite

L1775 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.kwF4gRRTate_poleWindowImageFinite
Source context 20 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Discharge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable [u.FiniteResidue]
Lean source · statement
theorem kwF4gRRTate_poleWindowImageFinite :
    KwF4gRRTatePoleWindowImageFinite u
theorem

finrankTrace_congr

L1831 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finrankTrace_congr
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Additivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem finrankTrace_congr {φ ψ : V →ₗ[K] V}
    [hφ : FiniteDimensional K (LinearMap.range φ)]
    [hψ : FiniteDimensional K (LinearMap.range ψ)]
    (h : φ = ψ) : finrankTrace φ = finrankTrace ψ
theorem

range_sub_le

L1837 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.range_sub_le
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Additivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem range_sub_le (φ ψ : V →ₗ[K] V) :
    LinearMap.range (φ - ψ) ≤ LinearMap.range φ ⊔ LinearMap.range ψ
instance

instFinDimRangeSub

L1843 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.instFinDimRangeSub
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Additivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
instance instFinDimRangeSub (φ ψ : V →ₗ[K] V)
    [FiniteDimensional K (LinearMap.range φ)]
    [FiniteDimensional K (LinearMap.range ψ)] :
    FiniteDimensional K (LinearMap.range (φ - ψ))
theorem

finrankTrace_sub

L1852 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finrankTrace_sub
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Additivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem finrankTrace_sub (φ ψ : V →ₗ[K] V)
    [FiniteDimensional K (LinearMap.range φ)]
    [FiniteDimensional K (LinearMap.range ψ)] :
    finrankTrace φ - finrankTrace ψ = finrankTrace (φ - ψ)
def

alphaMap

L1878 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.alphaMap
Documentation

Multiplication on the range of the Tate projection, followed by the quotient by that range.

Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TermMaps
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
def alphaMap (c : u.adicCompletion) :
    LinearMap.range (tateProj u) →ₗ[K] (u.adicCompletion ⧸ LinearMap.range (tateProj u))
theorem

finiteDimensional_range_alphaMap

L1884 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finiteDimensional_range_alphaMap
Source context 20 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TermMaps
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable [u.FiniteResidue]
Lean source · statement
theorem finiteDimensional_range_alphaMap (c : u.adicCompletion) :
    FiniteDimensional K (LinearMap.range (alphaMap u c))
instance

instFinDimRangeNeg

L1956 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.instFinDimRangeNeg
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Additivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
instance instFinDimRangeNeg (φ : V →ₗ[K] V) [FiniteDimensional K (LinearMap.range φ)] :
    FiniteDimensional K (LinearMap.range (-φ))
instance

instFinDimRangeZero

L1964 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.instFinDimRangeZero
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Additivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
instance instFinDimRangeZero : FiniteDimensional K (LinearMap.range (0 : V →ₗ[K] V))
theorem

finrankTrace_zero

L1967 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finrankTrace_zero
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Additivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem finrankTrace_zero : finrankTrace (0 : V →ₗ[K] V) = 0
theorem

finrankTrace_neg

L1975 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finrankTrace_neg
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Additivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem finrankTrace_neg (φ : V →ₗ[K] V) [FiniteDimensional K (LinearMap.range φ)] :
    finrankTrace (-φ) = -finrankTrace φ
instance

instFinDimRangeAdd

L1983 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.instFinDimRangeAdd
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Additivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
instance instFinDimRangeAdd (φ ψ : V →ₗ[K] V)
    [FiniteDimensional K (LinearMap.range φ)]
    [FiniteDimensional K (LinearMap.range ψ)] :
    FiniteDimensional K (LinearMap.range (φ + ψ))
theorem

finrankTrace_add

L1990 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finrankTrace_add
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Additivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem finrankTrace_add (φ ψ : V →ₗ[K] V)
    [FiniteDimensional K (LinearMap.range φ)]
    [FiniteDimensional K (LinearMap.range ψ)] :
    finrankTrace (φ + ψ) = finrankTrace φ + finrankTrace ψ
theorem

tateComm_add_fst

L2006 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateComm_add_fst
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateCommAddFst
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateComm_add_fst (pA φ₁ φ₂ ψ : V →ₗ[K] V) :
    tateComm pA (φ₁ + φ₂) ψ = tateComm pA φ₁ ψ + tateComm pA φ₂ ψ
theorem

tateCommRestrict_add_fst

L2013 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateCommRestrict_add_fst
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateCommAddFst
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateCommRestrict_add_fst (pA φ₁ φ₂ ψ : V →ₗ[K] V) :
    tateCommRestrict pA (φ₁ + φ₂) ψ
      = tateCommRestrict pA φ₁ ψ + tateCommRestrict pA φ₂ ψ
theorem

tateCommTrace_add_fst

L2022 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateCommTrace_add_fst
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateCommAddFst
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · full declaration
theorem tateCommTrace_add_fst (pA φ₁ φ₂ ψ : V →ₗ[K] V)
    [FiniteDimensional K (LinearMap.range (tateCommRestrict pA φ₁ ψ))]
    [FiniteDimensional K (LinearMap.range (tateCommRestrict pA φ₂ ψ))] :
    have : FiniteDimensional K (LinearMap.range (tateCommRestrict pA (φ₁ + φ₂) ψ)) := by
      rw [tateCommRestrict_add_fst]; exact instFinDimRangeAdd _ _
    tateCommTrace pA (φ₁ + φ₂) ψ = tateCommTrace pA φ₁ ψ + tateCommTrace pA φ₂ ψ := by
  have : FiniteDimensional K (LinearMap.range (tateCommRestrict pA (φ₁ + φ₂) ψ)) := by
    rw [tateCommRestrict_add_fst]; exact instFinDimRangeAdd _ _
  unfold tateCommTrace
  rw [← finrankTrace_add]
  exact finrankTrace_congr (tateCommRestrict_add_fst pA φ₁ φ₂ ψ)
theorem

tateRes_add_fst

L2040 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateRes_add_fst
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResAddFst
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · full declaration
theorem tateRes_add_fst (fh₁ fh₂ gh : u.adicCompletion)
    [FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u fh₁) (lmulK u gh)))]
    [FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u fh₂) (lmulK u gh)))] :
    have : FiniteDimensional K (LinearMap.range
        (tateCommRestrict (tateProj u) (lmulK u (fh₁ + fh₂)) (lmulK u gh))) := by
      have heq : lmulK u (fh₁ + fh₂) = lmulK u fh₁ + lmulK u fh₂ := map_add _ _ _
      rw [heq, tateCommRestrict_add_fst]; exact instFinDimRangeAdd _ _
    tateRes u (fh₁ + fh₂) gh = tateRes u fh₁ gh + tateRes u fh₂ gh := by
  have heq : lmulK u (fh₁ + fh₂) = lmulK u fh₁ + lmulK u fh₂ := map_add _ _ _
  have : FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u (fh₁ + fh₂)) (lmulK u gh))) := by
    rw [heq, tateCommRestrict_add_fst]; exact instFinDimRangeAdd _ _
  have : FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u fh₁ + lmulK u fh₂) (lmulK u gh))) := by
    rw [tateCommRestrict_add_fst]; exact instFinDimRangeAdd _ _
  unfold tateRes
  have hct := tateCommTrace_add_fst (tateProj u) (lmulK u fh₁) (lmulK u fh₂) (lmulK u gh)
  unfold tateCommTrace at hct ⊢
  rw [← hct]
  exact finrankTrace_congr (by rw [heq])
theorem

tateComm_add_snd

L2111 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateComm_add_snd
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section AddSnd
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateComm_add_snd (pA φ ψ₁ ψ₂ : V →ₗ[K] V) :
    tateComm pA φ (ψ₁ + ψ₂) = tateComm pA φ ψ₁ + tateComm pA φ ψ₂
theorem

tateCommRestrict_add_snd

L2118 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateCommRestrict_add_snd
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section AddSnd
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateCommRestrict_add_snd (pA φ ψ₁ ψ₂ : V →ₗ[K] V) :
    tateCommRestrict pA φ (ψ₁ + ψ₂)
      = tateCommRestrict pA φ ψ₁ + tateCommRestrict pA φ ψ₂
theorem

tateCommTrace_add_snd

L2127 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateCommTrace_add_snd
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section AddSnd
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · full declaration
theorem tateCommTrace_add_snd (pA φ ψ₁ ψ₂ : V →ₗ[K] V)
    [FiniteDimensional K (LinearMap.range (tateCommRestrict pA φ ψ₁))]
    [FiniteDimensional K (LinearMap.range (tateCommRestrict pA φ ψ₂))] :
    have : FiniteDimensional K (LinearMap.range (tateCommRestrict pA φ (ψ₁ + ψ₂))) := by
      rw [tateCommRestrict_add_snd]; exact instFinDimRangeAdd _ _
    tateCommTrace pA φ (ψ₁ + ψ₂) = tateCommTrace pA φ ψ₁ + tateCommTrace pA φ ψ₂ := by
  have : FiniteDimensional K (LinearMap.range (tateCommRestrict pA φ (ψ₁ + ψ₂))) := by
    rw [tateCommRestrict_add_snd]; exact instFinDimRangeAdd _ _
  unfold tateCommTrace
  rw [← finrankTrace_add]
  exact finrankTrace_congr (tateCommRestrict_add_snd pA φ ψ₁ ψ₂)
instance

instFinDimRangeCompRight

L2145 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.instFinDimRangeCompRight
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section CommutatorVanish
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
instance instFinDimRangeCompRight (φ ψ : V →ₗ[K] V)
    [FiniteDimensional K (LinearMap.range ψ)] :
    FiniteDimensional K (LinearMap.range (φ ∘ₗ ψ))
instance

instFinDimRangeCompLeft

L2150 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.instFinDimRangeCompLeft
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section CommutatorVanish
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
instance instFinDimRangeCompLeft (φ ψ : V →ₗ[K] V)
    [FiniteDimensional K (LinearMap.range ψ)] :
    FiniteDimensional K (LinearMap.range (ψ ∘ₗ φ))
theorem

finrankTrace_commutator_eq_zero

L2155 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finrankTrace_commutator_eq_zero
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section CommutatorVanish
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem finrankTrace_commutator_eq_zero (φ ψ : V →ₗ[K] V)
    [FiniteDimensional K (LinearMap.range ψ)] :
    finrankTrace (φ ∘ₗ ψ - ψ ∘ₗ φ) = 0
def

piRestrict

L2167 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.piRestrict
Documentation

The projected endomorphism restricted to the range of the projection.

Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section LeibnizAbstract
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
def piRestrict (pA φ : V →ₗ[K] V) : LinearMap.range pA →ₗ[K] LinearMap.range pA
theorem

piRestrict_apply

L2170 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.piRestrict_apply
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section LeibnizAbstract
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem piRestrict_apply (pA φ : V →ₗ[K] V) (a : LinearMap.range pA) :
    (piRestrict pA φ a : V) = pA (φ (a : V))
def

epsRestrict

L2174 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.epsRestrict
Documentation

The intermediate complementary projection term restricted to the projection range.

Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section LeibnizAbstract
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
def epsRestrict (pA φ ψ : V →ₗ[K] V) : LinearMap.range pA →ₗ[K] LinearMap.range pA
theorem

epsRestrict_apply

L2178 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.epsRestrict_apply
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section LeibnizAbstract
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem epsRestrict_apply (pA φ ψ : V →ₗ[K] V) (a : LinearMap.range pA) :
    (epsRestrict pA φ ψ a : V) = pA (φ (ψ (a : V) - pA (ψ (a : V))))
theorem

piRestrict_comp_eq

L2183 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.piRestrict_comp_eq
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section LeibnizAbstract
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem piRestrict_comp_eq (pA φ ψ : V →ₗ[K] V) :
    piRestrict pA (φ ∘ₗ ψ) = piRestrict pA φ ∘ₗ piRestrict pA ψ + epsRestrict pA φ ψ
theorem

tateCommRestrict_eq_bracket

L2191 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateCommRestrict_eq_bracket
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section LeibnizAbstract
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateCommRestrict_eq_bracket (pA f g : V →ₗ[K] V) :
    tateCommRestrict pA f g
      = piRestrict pA f ∘ₗ piRestrict pA g - piRestrict pA g ∘ₗ piRestrict pA f
theorem

bracket_leibniz_defect

L2199 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.bracket_leibniz_defect
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section LeibnizAbstract
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem bracket_leibniz_defect {R W : Type*} [CommRing R] [AddCommGroup W] [Module R W]
    (F G H : W →ₗ[R] W) :
    (F ∘ₗ (G ∘ₗ H) - (G ∘ₗ H) ∘ₗ F)
      - ((F ∘ₗ G) ∘ₗ H - H ∘ₗ (F ∘ₗ G))
      - ((F ∘ₗ H) ∘ₗ G - G ∘ₗ (F ∘ₗ H))
      = G ∘ₗ (F ∘ₗ H - H ∘ₗ F) - (F ∘ₗ H - H ∘ₗ F) ∘ₗ G
theorem

tateCommTrace_leibniz_snd

L2209 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateCommTrace_leibniz_snd
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section LeibnizAbstract
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateCommTrace_leibniz_snd (pA f g h : V →ₗ[K] V)
    (hfin_fh : FiniteDimensional K (LinearMap.range (tateCommRestrict pA f h)))
    (hfin_gh : FiniteDimensional K (LinearMap.range (epsRestrict pA g h)))
    (hfin_fg : FiniteDimensional K (LinearMap.range (epsRestrict pA f g)))
    (hfin_fh' : FiniteDimensional K (LinearMap.range (epsRestrict pA f h)))
    [FiniteDimensional K (LinearMap.range (tateCommRestrict pA f (g ∘ₗ h)))]
    [FiniteDimensional K (LinearMap.range (tateCommRestrict pA (f ∘ₗ g) h))]
    [FiniteDimensional K (LinearMap.range (tateCommRestrict pA (f ∘ₗ h) g))] :
    tateCommTrace pA f (g ∘ₗ h)
      = tateCommTrace pA (f ∘ₗ g) h + tateCommTrace pA (f ∘ₗ h) g
theorem

finiteDimensional_range_epsRestrict_lmulK

L2328 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finiteDimensional_range_epsRestrict_lmulK
Source context 20 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResLeibniz
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable [u.FiniteResidue]
Lean source · statement
theorem finiteDimensional_range_epsRestrict_lmulK (φ ψ : u.adicCompletion) :
    FiniteDimensional K (LinearMap.range
      (epsRestrict (tateProj u) (lmulK u φ) (lmulK u ψ)))
theorem

tateRes_leibniz_snd

L2352 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateRes_leibniz_snd
Source context 20 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResLeibniz
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable [u.FiniteResidue]
Lean source · full declaration
theorem tateRes_leibniz_snd (hfin : KwF4gRRTateCommFinite K L)
    (f g h : u.adicCompletion) :
    let := hfin u f (g * h)
    let := hfin u (f * g) h
    let := hfin u (f * h) g
    tateRes u f (g * h) = tateRes u (f * g) h + tateRes u (f * h) g := by
  let := hfin u f (g * h)
  let := hfin u (f * g) h
  let := hfin u (f * h) g
  let := hfin u f h
  change tateRes u f (g * h) = tateRes u (f * g) h + tateRes u (f * h) g
  have hlmul : ∀ x y : u.adicCompletion, lmulK u (x * y) = lmulK u x ∘ₗ lmulK u y := by
    intro x y
    apply LinearMap.ext; intro z
    change (x * y) * z = x * (y * z)
    ring
  have hL : FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u f) (lmulK u g ∘ₗ lmulK u h))) := by
    rw [← hlmul g h]; exact hfin u f (g * h)
  have hR₁ : FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u f ∘ₗ lmulK u g) (lmulK u h))) := by
    rw [← hlmul f g]; exact hfin u (f * g) h
  have hR₂ : FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u f ∘ₗ lmulK u h) (lmulK u g))) := by
    rw [← hlmul f h]; exact hfin u (f * h) g
  have hleib := tateCommTrace_leibniz_snd (tateProj u) (lmulK u f) (lmulK u g) (lmulK u h)
    (hfin u f h)
    (finiteDimensional_range_epsRestrict_lmulK u g h)
    (finiteDimensional_range_epsRestrict_lmulK u f g)
    (finiteDimensional_range_epsRestrict_lmulK u f h)
  unfold tateRes tateCommTrace at hleib ⊢
  simpa only [hlmul] using hleib
theorem

tateRes_congr_fst

L2391 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateRes_congr_fst
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResCongr
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem tateRes_congr_fst {fh₁ fh₂ gh : u.adicCompletion} (heq : fh₁ = fh₂)
    [h₁ : FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u fh₁) (lmulK u gh)))]
    [h₂ : FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u fh₂) (lmulK u gh)))] :
    tateRes u fh₁ gh = tateRes u fh₂ gh
def

KwF4gRRTateDerivationFactorSnd

L2407 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.KwF4gRRTateDerivationFactorSnd
Documentation

The equality expressing the second Tate residue argument through its differential coefficient.

Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DerivationFactor
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def KwF4gRRTateDerivationFactorSnd [HasPrincipalDivisors K F] [Nontrivial Ω[F⁄K]]
    (hfinF : KwF4gRRTateCommFinite K F) : Prop
theorem

kwF4gRRTate_chainRule_of_derivationFactor

L2429 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.kwF4gRRTate_chainRule_of_derivationFactor
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Reprice
variable {K F E : Type*} [Field K] [Field F] [Algebra K F]
variable [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E]
omit [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E] in
Lean source · statement
theorem kwF4gRRTate_chainRule_of_derivationFactor
    (hfinF : KwF4gRRTateCommFinite K F)
    (hDF : ∀ [HasPrincipalDivisors K F] [Nontrivial Ω[F⁄K]],
      KwF4gRRTateDerivationFactorSnd K F hfinF) :
    KwF4gRRTateChainRule K F E hfinF
def

DualDom

L2494 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.DualDom
Documentation

The linear dual over the base field of the completed local field.

Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DualDom
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
def DualDom (w : Place K F) : Type _
instance

(anonymous instance)

L2496 ↗
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DualDom
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
instance (w : Place K F) : AddCommGroup (DualDom w)
def

toLM

L2500 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.DualDom.toLM
Documentation

The underlying linear map of an element of the completed local dual.

Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DualDom
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
def DualDom.toLM {w : Place K F} (φ : DualDom w) : w.adicCompletion →ₗ[K] K
theorem

ext

L2502 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.DualDom.ext
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DualDom
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem DualDom.ext {w : Place K F} {φ ψ : DualDom w}
    (h : ∀ x, φ.toLM x = ψ.toLM x) : φ = ψ
theorem

toLM_add

L2505 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.DualDom.toLM_add
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DualDom
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem DualDom.toLM_add {w : Place K F} (φ ψ : DualDom w) :
    (φ + ψ).toLM = φ.toLM + ψ.toLM
instance

(anonymous instance)

L2508 ↗
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DualDom
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
instance (w : Place K F) : Module F (DualDom w) where
  smul h φ := φ.toLM ∘ₗ lmulK w (algebraMap F w.adicCompletion h)
  one_smul φ := DualDom.ext fun x => by
    change φ.toLM (algebraMap F w.adicCompletion 1 * x) = φ.toLM x
    rw [_root_.map_one, one_mul]
  mul_smul a b φ := DualDom.ext fun x => by
    change φ.toLM (algebraMap F _ (a * b) * x) = φ.toLM (algebraMap F _ b * (algebraMap F _ a * x))
    rw [(algebraMap F w.adicCompletion).map_mul, mul_comm (algebraMap F _ a), mul_assoc]
  smul_zero a := DualDom.ext fun _ => rfl
  smul_add a φ ψ := DualDom.ext fun _ => rfl
  add_smul a b φ := DualDom.ext fun x => by
    change φ.toLM (algebraMap F _ (a + b) * x)
      = φ.toLM (algebraMap F _ a * x) + φ.toLM (algebraMap F _ b * x)
    rw [(algebraMap F w.adicCompletion).map_add, add_mul, φ.toLM.map_add]
  zero_smul φ := DualDom.ext fun x => by
    change φ.toLM (algebraMap F _ 0 * x) = 0
    rw [(algebraMap F w.adicCompletion).map_zero, zero_mul, φ.toLM.map_zero]
theorem

smul_apply

L2526 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.DualDom.smul_apply
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DualDom
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem DualDom.smul_apply {w : Place K F} (h : F) (φ : DualDom w)
    (x : w.adicCompletion) :
    (h • φ).toLM x = φ.toLM (algebraMap F w.adicCompletion h * x)
instance

(anonymous instance)

L2530 ↗
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DualDom
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
instance (w : Place K F) : Module K (DualDom w)
theorem

k_smul_apply

L2533 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.DualDom.k_smul_apply
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DualDom
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem DualDom.k_smul_apply {w : Place K F} (c : K) (φ : DualDom w)
    (x : w.adicCompletion) :
    (c • φ).toLM x = c • φ.toLM x
instance

(anonymous instance)

L2537 ↗
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section DualDom
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
instance (w : Place K F) : IsScalarTower K F (DualDom w) where
  smul_assoc c h φ := DualDom.ext fun x => by
    change φ.toLM (algebraMap F _ (c • h) * x) = c • φ.toLM (algebraMap F _ h * x)
    rw [Algebra.smul_def, (algebraMap F w.adicCompletion).map_mul,
      ← IsScalarTower.algebraMap_apply K F w.adicCompletion,
      Algebra.algebraMap_eq_smul_one, smul_mul_assoc, one_mul, smul_mul_assoc, φ.toLM.map_smul]
theorem

derivation_apply_eq_diffCoeff_smul

L2552 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.derivation_apply_eq_diffCoeff_smul
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section GenericFactor
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [Nontrivial Ω[F⁄K]]
variable {M : Type*} [AddCommGroup M] [Module K M] [Module F M] [IsScalarTower K F M]
omit [Nontrivial Ω[F⁄K]] in
Lean source · statement
theorem derivation_apply_eq_diffCoeff_smul (w : Place K F) [w.DCoordGenerates]
    (δ : Derivation K F M) (g : F) :
    δ g = w.differentialCoeff (KaehlerDifferential.D K F g) • δ w.uniformizer
theorem

range_smul_le

L2570 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.range_smul_le
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem range_smul_le {V : Type*} [AddCommGroup V] [Module K V]
    (c : K) (φ : V →ₗ[K] V) : LinearMap.range (c • φ) ≤ LinearMap.range φ
theorem

finDimRangeSMul

L2575 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finDimRangeSMul
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finDimRangeSMul {V : Type*} [AddCommGroup V] [Module K V]
    (c : K) (φ : V →ₗ[K] V) [FiniteDimensional K (LinearMap.range φ)] :
    FiniteDimensional K (LinearMap.range (c • φ))
theorem

finrankTrace_smul

L2580 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.finrankTrace_smul
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
theorem finrankTrace_smul {V : Type*} [AddCommGroup V] [Module K V]
    (c : K) (φ : V →ₗ[K] V) [FiniteDimensional K (LinearMap.range φ)] :
    let := finDimRangeSMul c φ
    finrankTrace (c • φ) = c • finrankTrace φ := by
  let := finDimRangeSMul c φ
  change finrankTrace (c • φ) = c • finrankTrace φ
  have hW : ∀ x ∈ LinearMap.range φ, (c • φ) x ∈ LinearMap.range φ := fun x _ =>
    range_smul_le c φ (LinearMap.mem_range_self _ x)
  rw [finrankTrace_eq_trace_on_superspace (c • φ) (LinearMap.range φ) (range_smul_le c φ) hW]
  unfold finrankTrace
  rw [← LinearMap.map_smul]
  exact congrArg (LinearMap.trace K _) (LinearMap.ext fun x => Subtype.ext rfl)
theorem

tateCommRestrict_smul_snd

L2593 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateCommRestrict_smul_snd
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem tateCommRestrict_smul_snd {V : Type*} [AddCommGroup V] [Module K V]
    (pA φ ψ : V →ₗ[K] V) (c : K) :
    tateCommRestrict pA φ (c • ψ) = c • tateCommRestrict pA φ ψ
theorem

tateCommRestrict_smul_fst

L2603 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateCommRestrict_smul_fst
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem tateCommRestrict_smul_fst {V : Type*} [AddCommGroup V] [Module K V]
    (pA φ ψ : V →ₗ[K] V) (c : K) :
    tateCommRestrict pA (c • φ) ψ = c • tateCommRestrict pA φ ψ
theorem

tateRes_congr_snd

L2613 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateRes_congr_snd
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem tateRes_congr_snd (u : Place K F) {fh gh₁ gh₂ : u.adicCompletion} (heq : gh₁ = gh₂)
    [h₁ : FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u fh) (lmulK u gh₁)))]
    [h₂ : FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u fh) (lmulK u gh₂)))] :
    tateRes u fh gh₁ = tateRes u fh gh₂
theorem

tateRes_add_snd

L2621 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateRes_add_snd
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
theorem tateRes_add_snd (u : Place K F) (hfin : KwF4gRRTateCommFinite K F)
    (f g h : u.adicCompletion) :
    have := hfin u f (g + h); have := hfin u f g; have := hfin u f h
    tateRes u f (g + h) = tateRes u f g + tateRes u f h := by
  have := hfin u f (g + h); have := hfin u f g; have := hfin u f h
  have heq : lmulK u (g + h) = lmulK u g + lmulK u h := map_add _ _ _
  have : FiniteDimensional K (LinearMap.range
      (tateCommRestrict (tateProj u) (lmulK u f) (lmulK u g + lmulK u h))) := by
    rw [← heq]; exact hfin u f (g + h)
  unfold tateRes
  have hct := tateCommTrace_add_snd (tateProj u) (lmulK u f) (lmulK u g) (lmulK u h)
  unfold tateCommTrace at hct ⊢
  have hmap : tateCommRestrict (tateProj u) (lmulK u f) (lmulK u (g + h)) =
      tateCommRestrict (tateProj u) (lmulK u f) (lmulK u g + lmulK u h) :=
    congrArg (tateCommRestrict (tateProj u) (lmulK u f)) heq
  have htrace := finrankTrace_congr hmap
  exact htrace.trans hct
def

tateResFstLM

L2640 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateResFstLM
Documentation

The linear functional in the first Tate residue argument for a fixed second argument.

Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
def tateResFstLM (w : Place K F) (hfin : KwF4gRRTateCommFinite K F)
    (gh : w.adicCompletion) : DualDom w where
  toFun f := have := hfin w f gh; tateRes w f gh
  map_add' f₁ f₂ := by
    have := hfin w f₁ gh; have := hfin w f₂ gh
    exact tateRes_add_fst w f₁ f₂ gh
  map_smul' c f := by
    have := hfin w f gh; have := hfin w (c • f) gh
    change tateRes w (c • f) gh = c • tateRes w f gh
    have heq : tateCommRestrict (tateProj w) (lmulK w (c • f)) (lmulK w gh)
        = c • tateCommRestrict (tateProj w) (lmulK w f) (lmulK w gh) := by
      rw [show lmulK w (c • f) = c • lmulK w f from map_smul _ _ _,
        tateCommRestrict_smul_fst]
    have := finDimRangeSMul c (tateCommRestrict (tateProj w) (lmulK w f) (lmulK w gh))
    unfold tateRes tateCommTrace
    rw [finrankTrace_congr heq, finrankTrace_smul]
theorem

tateResFstLM_apply

L2657 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateResFstLM_apply
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
theorem tateResFstLM_apply (w : Place K F) (hfin : KwF4gRRTateCommFinite K F)
    (gh f : w.adicCompletion) :
    (tateResFstLM w hfin gh).toLM f = have := hfin w f gh; tateRes w f gh := rfl
def

tateResSndDer

L2664 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateResSndDer
Documentation

The derivation in the second Tate residue argument with values in the completed local dual.

Source context 20 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasPrincipalDivisors K F] [Nontrivial Ω[F⁄K]]
Lean source · statement
def tateResSndDer (w : Place K F) [w.DCoordGenerates] [w.FiniteResidue]
    (hfin : KwF4gRRTateCommFinite K F) : Derivation K F (DualDom w)
theorem

tateResSndDer_apply

L2708 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.tateResSndDer_apply
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section TateResDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasPrincipalDivisors K F] [Nontrivial Ω[F⁄K]]
omit [HasPrincipalDivisors K F] [Nontrivial Ω[F⁄K]] in
Lean source · full declaration
theorem tateResSndDer_apply (w : Place K F) [w.DCoordGenerates] [w.FiniteResidue]
    (hfin : KwF4gRRTateCommFinite K F) (g : F) (f : w.adicCompletion) :
    ((tateResSndDer w hfin) g).toLM f
      = have := hfin w f (algebraMap F _ g); tateRes w f (algebraMap F _ g) := rfl
theorem

kwTateRR2_derivationFactorSnd

L2720 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule.ModularCurve.KwF4gRRTate.kwTateRR2_derivationFactorSnd
Source context 20 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Headline
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasPrincipalDivisors K F] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem kwTateRR2_derivationFactorSnd [∀ w : Place K F, w.FiniteResidue]
    (hfinF : KwF4gRRTateCommFinite K F) :
    KwF4gRRTateDerivationFactorSnd K F hfinF
theorem

tateChainRule

L2762 ↗
AlgebraicCurve.tateChainRule
Source context 3 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateChainRule
Lean source · statement
theorem _root_.AlgebraicCurve.tateChainRule {K F : Type*} [Field K] [Field F] [Algebra K F] {E :
    Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F] [Algebra.IsIntegral E F]
      [AlgebraicCurve.HasCanonicalLocalResidueKStar K F]
        [AlgebraicCurve.HasCanonicalLocalResidueKStar K E] [∀ w : AlgebraicCurve.Place K F,
          w.FiniteResidue] (hfinF : ModularCurve.KwF4gRRTate.KwF4gRRTateCommFinite K F) :
            ModularCurve.KwF4gRRTate.KwF4gRRTateChainRule K F E hfinF

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