NYLL
Module

TateTraceCompat_of_isSeparable.lean

Nyll.AlgebraicCurves.Differentials.Residues.TateTraceCompat_of_isSeparable
163 declarations indexed from sourceView source ↗

Module documentation

Compatibility of Tate residues with trace in separable function field extensions.

Imports64
Imported by3

Declarations

theorem

maximalIdeal_le

L240 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L245 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L406 ↗
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.TateTraceCompat_of_isSeparable
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

L423 ↗
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.TateTraceCompat_of_isSeparable
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

L433 ↗
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.TateTraceCompat_of_isSeparable
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

L438 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L452 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L457 ↗
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.TateTraceCompat_of_isSeparable
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

L475 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L482 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L507 ↗
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.TateTraceCompat_of_isSeparable
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

L524 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L529 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L600 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L611 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L622 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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
instance

kw_ffgc_isIntegrallyClosed_adicCompletionIntegers

L804 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.AlgebraicCurve.Place.kw_ffgc_isIntegrallyClosed_adicCompletionIntegers
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.TateTraceCompat_of_isSeparable
section
section
noncomputable section
open _root_.Polynomial
open _root_.IsLocalRing
open _root_.IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section CompletionAlgebra
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
instance kw_ffgc_isIntegrallyClosed_adicCompletionIntegers :
    IsIntegrallyClosed (W.restrict F).adicCompletionIntegers
theorem

kw_ffgc_adicCompletionComapIntegers_injective

L813 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.kw_ffgc_adicCompletionComapIntegers_injective
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.TateTraceCompat_of_isSeparable
section
section
noncomputable section
open _root_.Polynomial
open _root_.IsLocalRing
open _root_.IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section CompletionAlgebra
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
open TateTraceCompat_of_isSeparable.AlgebraicCurve.Place in
with_weak_namespace
    _root_.AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable
Lean source · statement
theorem kw_ffgc_adicCompletionComapIntegers_injective :
    Function.Injective (kw_ffgc_adicCompletionComapIntegers F W)
instance

comapTorsionFree

L819 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.comapTorsionFree
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.TateTraceCompat_of_isSeparable
section
section
noncomputable section
open _root_.Polynomial
open _root_.IsLocalRing
open _root_.IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section CompletionAlgebra
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
instance
_root_.AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.comapTorsionFree
    :
    Module.IsTorsionFree (W.restrict F).adicCompletionIntegers W.adicCompletionIntegers
theorem

kw_ffgc_norm_adicCompletion_eq

L845 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.AlgebraicCurve.Place.kw_ffgc_norm_adicCompletion_eq
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.TateTraceCompat_of_isSeparable
section
section
noncomputable section
open _root_.Polynomial
open _root_.IsLocalRing
open _root_.IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section SpectralSetup
open scoped _root_.Valued _root_.NNReal _root_.WithZero
open _root_.WithZeroMulInt
open _root_.Valuation.IsRankOneDiscrete
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (V : Place K F)
Lean source · full declaration
theorem kw_ffgc_norm_adicCompletion_eq (x : V.adicCompletion) :
    let := kw_ffgc_rankOne_adicCompletion V
    ‖x‖ = (WithZeroMulInt.toNNReal (two_ne_zero) (Valued.v x) : ℝ) := by
  let := kw_ffgc_rankOne_adicCompletion V
  have h := valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective
    (V.heightOneSpectrum.valuedAdicCompletion_surjective F) x
  simp only [Valued.toNormedField.norm_def, Valuation.RankOne.hom]
  rw [← h]; rfl
theorem

kw_ffgc_absoluteValue_extends

L867 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.AlgebraicCurve.Place.kw_ffgc_absoluteValue_extends
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.TateTraceCompat_of_isSeparable
section
section
noncomputable section
open _root_.Polynomial
open _root_.IsLocalRing
open _root_.IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section AbsoluteValue
open scoped _root_.Valued _root_.NNReal _root_.WithZero
open _root_.WithZeroMulInt
open _root_.Valuation.IsRankOneDiscrete
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · full declaration
theorem kw_ffgc_absoluteValue_extends (c : (W.restrict F).adicCompletion) :
    let := kw_ffgc_rankOne_adicCompletion (W.restrict F)
    kw_ffgc_absoluteValue F W
      (algebraMap (W.restrict F).adicCompletion W.adicCompletion c) = ‖c‖ := by
  let := kw_ffgc_rankOne_adicCompletion (W.restrict F)
  let := kw_ffgc_rankOne_adicCompletion W
  have hr : (0 : ℝ) < (W.ramificationIndex F : ℝ) :=
    Nat.cast_pos.mpr (W.ramificationIndex_pos (F := F))
  change ‖algebraMap (W.restrict F).adicCompletion W.adicCompletion c‖
      ^ ((W.ramificationIndex F : ℝ))⁻¹ = ‖c‖
  rw [kw_ffgc_norm_adicCompletion_eq W, kw_ffgc_norm_adicCompletion_eq (W.restrict F),
    kw_ffgc_algebraMap_adicCompletionComap_eq, kw_ffgc_valued_adicCompletionComap,
    map_pow, NNReal.coe_pow, ← Real.rpow_natCast, ← Real.rpow_mul (NNReal.coe_nonneg _),
    mul_inv_cancel₀ hr.ne', Real.rpow_one]
theorem

kw_ffgc_isIntegral_adicCompletionIntegers_of_algebraic

L892 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.AlgebraicCurve.Place.kw_ffgc_isIntegral_adicCompletionIntegers_of_algebraic
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.TateTraceCompat_of_isSeparable
section
section
noncomputable section
open _root_.Polynomial
open _root_.IsLocalRing
open _root_.IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section IntegralClosure
open scoped _root_.Valued _root_.NNReal _root_.WithZero
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
Lean source · statement
theorem kw_ffgc_isIntegral_adicCompletionIntegers_of_algebraic
    [Algebra.IsAlgebraic (W.restrict F).adicCompletion W.adicCompletion]
    (x : W.adicCompletionIntegers) :
    _root_.IsIntegral (W.restrict F).adicCompletionIntegers x
theorem

kw_ffgc_isIntegralClosure_adicCompletionIntegers

L939 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.kw_ffgc_isIntegralClosure_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.TateTraceCompat_of_isSeparable
section
section
noncomputable section
open _root_.Polynomial
open _root_.IsLocalRing
open _root_.IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section IntegralClosure
open scoped _root_.Valued _root_.NNReal _root_.WithZero
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
open TateTraceCompat_of_isSeparable.AlgebraicCurve.Place in
with_weak_namespace
    _root_.AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable
Lean source · full declaration
theorem kw_ffgc_isIntegralClosure_adicCompletionIntegers
    [Algebra.IsAlgebraic (W.restrict F).adicCompletion W.adicCompletion] :
    IsIntegralClosure W.adicCompletionIntegers (W.restrict F).adicCompletionIntegers
      W.adicCompletion where
  algebraMap_injective := Subtype.val_injective
  isIntegral_iff {x} := by
    constructor
    · intro hx
      have hxW : _root_.IsIntegral W.adicCompletionIntegers x := hx.tower_top
      have : IsIntegrallyClosed W.adicCompletionIntegers :=
        Valuation.Integers.isIntegrallyClosed
          (HeightOneSpectrum.adicCompletionIntegers.integers
            (K := F') (v := W.heightOneSpectrum))
      exact IsIntegrallyClosed.isIntegral_iff.mp hxW
    · rintro ⟨y, rfl⟩
      exact (kw_ffgc_isIntegral_adicCompletionIntegers_of_algebraic F W y).map
        (IsScalarTower.toAlgHom (W.restrict F).adicCompletionIntegers
          W.adicCompletionIntegers W.adicCompletion)
theorem

kw_ffgc_completionTraceF'_apply

L1022 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.kw_ffgc_completionTraceF'_apply
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.TateTraceCompat_of_isSeparable
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open scoped _root_.Valued _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section CompletionTrace
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')
open TateTraceCompat_of_isSeparable.AlgebraicCurve.Place in
with_weak_namespace
    _root_.AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable
Lean source · statement
theorem kw_ffgc_completionTraceF'_apply [FiniteDimensional F F'] (g : F') :
    kw_ffgc_completionTraceF' F W g
      = Algebra.trace (W.restrict F).adicCompletion W.adicCompletion
          (algebraMap F' W.adicCompletion g)
def

uniformizerSubring

L1128 ↗
AlgebraicCurve.Place.uniformizerSubring
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.TateTraceCompat_of_isSeparable
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
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
Lean source · statement
def _root_.AlgebraicCurve.Place.uniformizerSubring : v.toValuationSubring
theorem

uniformizer_mem

L1132 ↗
AlgebraicCurve.Place.uniformizer_mem
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.TateTraceCompat_of_isSeparable
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
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.uniformizer_mem : v.uniformizer ∈
    v.toValuationSubring
theorem

mem_adicIntegersKSubmod_iff

L1247 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1250 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1257 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1265 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1270 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1332 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.poleWindowKSubmod
Documentation

The K-submodule of completed elements whose poles are cleared by the chosen power of πh.

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.TateTraceCompat_of_isSeparable
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

L1344 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1349 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1353 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1381 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.KwF4gRRTatePoleWindowFinite
Documentation

Each pole window modulo the completed integers is finite dimensional over K at a place with finite residue.

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.TateTraceCompat_of_isSeparable
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

L1424 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.isOpen_setOf_valued_le
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.TateTraceCompat_of_isSeparable
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) ℤᵐ⁰)
open TateTraceCompat_of_isSeparable.IsDedekindDomain.HeightOneSpectrum.adicCompletion in
with_weak_namespace
    _root_.AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable
Lean source · statement
theorem isOpen_setOf_valued_le {γ : ℤᵐ⁰} (hγ : γ ≠ 0) :
    IsOpen {y : v.adicCompletion K | Valued.v y ≤ γ}
instance

kwF4R1V410a_subsingletonHeightOneSpectrumDVR

L1477 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1493 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1504 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1549 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.kwF4R1V410a_quotientEquiv
Documentation

Completion induces a ring equivalence modulo corresponding powers of the local maximal ideals.

Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable
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
open TateTraceCompat_of_isSeparable.ModularCurve.KwF4R1V410a in
with_weak_namespace
    _root_.AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable
Lean source · statement
def kwF4R1V410a_quotientEquiv (n : ℕ) :
    (O_w) ⧸ (𝔪_w) ^ n ≃+* (O_W) ⧸ (𝔪_W) ^ n
theorem

kwF4R1V410a_quotientEquiv_mk

L1571 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.kwF4R1V410a_quotientEquiv_mk
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable
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
open TateTraceCompat_of_isSeparable.ModularCurve.KwF4R1V410a in
with_weak_namespace
    _root_.AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable
Lean source · statement
theorem kwF4R1V410a_quotientEquiv_mk (n : ℕ) (x : O_w) :
    TateTraceCompat_of_isSeparable.kwF4R1V410a_quotientEquiv w n (Ideal.Quotient.mk _ x)
      = Ideal.Quotient.mk _ (algebraMap (O_w) (O_W) x)
theorem

coe_smul_K

L1610 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1616 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.poleWindowShift
Documentation

Multiplication by πh to the power M sends the pole window to the completed 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.TateTraceCompat_of_isSeparable
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

L1627 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1642 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1657 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.poleWindowShiftEquiv
Documentation

Multiplication by an irreducible πh to the power M identifies the pole window with the completed 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.TateTraceCompat_of_isSeparable
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

L1663 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.piPowKSubmod
Documentation

The K-submodule of completed integers divisible by πh to the power M.

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.TateTraceCompat_of_isSeparable
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

L1672 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1689 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.KwF4gRRTateDVRQuotPowKFinite
Documentation

Quotients of completed integers by powers of an irreducible element are finite dimensional over K.

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.TateTraceCompat_of_isSeparable
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

L1694 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

principalPart_mul_zero_of_mem_integers

L1740 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.principalPart_mul_zero_of_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.TateTraceCompat_of_isSeparable
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 AgreementReduce
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem principalPart_mul_zero_of_mem_integers
    {gh : u.adicCompletion} (hgh : gh ∈ u.adicCompletionIntegers)
    {a : u.adicCompletion} (ha : a ∈ u.adicCompletionIntegers) :
    gh * a - tateProj u (gh * a) = 0
theorem

tateCommRestrict_single_term

L1746 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.tateCommRestrict_single_term
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.TateTraceCompat_of_isSeparable
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 AgreementReduce
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem tateCommRestrict_single_term
    {gh : u.adicCompletion} (hgh : gh ∈ u.adicCompletionIntegers)
    (fh : u.adicCompletion) (a : LinearMap.range (tateProj u)) :
    (tateCommRestrict (tateProj u) (lmulK u fh) (lmulK u gh) a : u.adicCompletion)
      = tateProj u (gh * (fh * (a : u.adicCompletion)
          - tateProj u (fh * (a : u.adicCompletion))))
theorem

range_comp_map_left

L1795 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L1800 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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)
structure

SameRangeIdemProjectors

L1850 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.SameRangeIdemProjectors
Documentation

Two idempotent linear projectors with the same range.

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.TateTraceCompat_of_isSeparable
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 DeltaLemmas
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
variable (pA pA' : V →ₗ[K] V)
Lean source · full declaration
structure SameRangeIdemProjectors : Prop where
  /-- The first projector is idempotent. -/
  idem_pA : ∀ x, pA (pA x) = pA x
  /-- The second projector is idempotent. -/
  idem_pA' : ∀ x, pA' (pA' x) = pA' x
  /-- The two projectors have the same range. -/
  range_eq : LinearMap.range pA = LinearMap.range pA'
theorem

pA_fixes_range

L1860 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.pA_fixes_range
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.TateTraceCompat_of_isSeparable
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 DeltaLemmas
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
variable (pA pA' : V →ₗ[K] V)
variable {pA pA'}
Lean source · statement
theorem pA_fixes_range (h : SameRangeIdemProjectors pA pA') :
    ∀ x ∈ LinearMap.range pA, pA x = x
theorem

pA'_fixes_range

L1864 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.pA'_fixes_range
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.TateTraceCompat_of_isSeparable
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 DeltaLemmas
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
variable (pA pA' : V →ₗ[K] V)
variable {pA pA'}
Lean source · statement
theorem pA'_fixes_range (h : SameRangeIdemProjectors pA pA') :
    ∀ x ∈ LinearMap.range pA, pA' x = x
theorem

delta_zero_on_range

L1871 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.delta_zero_on_range
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.TateTraceCompat_of_isSeparable
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 DeltaLemmas
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
variable (pA pA' : V →ₗ[K] V)
variable {pA pA'}
Lean source · statement
theorem delta_zero_on_range (h : SameRangeIdemProjectors pA pA')
    {x : V} (hx : x ∈ LinearMap.range pA) :
    (pA - pA') x = 0
theorem

delta_range_subset

L1876 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.delta_range_subset
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.TateTraceCompat_of_isSeparable
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 DeltaLemmas
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
variable (pA pA' : V →ₗ[K] V)
variable {pA pA'}
Lean source · statement
theorem delta_range_subset (h : SameRangeIdemProjectors pA pA')
    (x : V) : (pA - pA') x ∈ LinearMap.range pA
def

KwF4gRRTateProjectorIndep

L1890 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.KwF4gRRTateProjectorIndep
Documentation

Tate commutator traces are independent of the idempotent projector with the prescribed range when the second multiplier is integral.

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.TateTraceCompat_of_isSeparable
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 Mint
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
Lean source · statement
def KwF4gRRTateProjectorIndep : Prop
theorem

tateCommRestrict_diff

L1908 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.tateCommRestrict_diff
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.TateTraceCompat_of_isSeparable
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 DiffComputation
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (pA' : u.adicCompletion →ₗ[K] u.adicCompletion)
Lean source · statement
theorem tateCommRestrict_diff
    (h : SameRangeIdemProjectors (tateProj u) pA')
    {gh : u.adicCompletion} (hgh : gh ∈ u.adicCompletionIntegers)
    (fh : u.adicCompletion) (a : LinearMap.range (tateProj u)) :
    (tateCommRestrict (tateProj u) (lmulK u fh) (lmulK u gh) a : u.adicCompletion)
      - tateComm pA' (lmulK u fh) (lmulK u gh) (a : u.adicCompletion)
      = (tateProj u - pA') (gh * fh * (a : u.adicCompletion))
        - gh * (tateProj u - pA') (fh * (a : u.adicCompletion))
theorem

finrankTrace_eq_trace_on_superspace

L1988 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2013 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2075 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2084 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.quotPiPowEquivIdealQuot
Documentation

Identifies the quotient by the K-submodule of multiples of πh to the power M with the corresponding 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.TateTraceCompat_of_isSeparable
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

L2093 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.KwF4gRRTateDVRCotangentKFinite
Documentation

The quotient of completed integers by an irreducible element is finite dimensional over K at each place with finite residue.

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.TateTraceCompat_of_isSeparable
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

L2098 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2107 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2169 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2177 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2220 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2229 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2237 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.quotientEquivKAlg
Documentation

Completion induces a K-algebra equivalence modulo corresponding powers of the local maximal ideals.

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.TateTraceCompat_of_isSeparable
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

L2255 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.quotSpanIrreducibleEquivResidueField
Documentation

Identifies the quotient of completed integers by an irreducible element with the residue field over 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.TateTraceCompat_of_isSeparable
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

L2264 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

deltaQuotFactor

L2305 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.deltaQuotFactor
Documentation

The difference of the two projectors factors through the quotient by their common range and takes values in that range.

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.TateTraceCompat_of_isSeparable
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 DeltaQuotFactor
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
variable {pA pA' : V →ₗ[K] V}
Lean source · statement
def deltaQuotFactor (h : SameRangeIdemProjectors pA pA') :
    (V ⧸ LinearMap.range pA) →ₗ[K] LinearMap.range pA
theorem

deltaQuotFactor_apply

L2313 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.deltaQuotFactor_apply
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.TateTraceCompat_of_isSeparable
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 DeltaQuotFactor
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
variable {pA pA' : V →ₗ[K] V}
Lean source · statement
theorem deltaQuotFactor_apply (h : SameRangeIdemProjectors pA pA') (x : V) :
    (deltaQuotFactor h (Submodule.Quotient.mk x) : V) = (pA - pA') x
def

KwF4gRRTatePoleWindowImageFinite

L2325 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.KwF4gRRTatePoleWindowImageFinite
Documentation

Multiplication by any completed element has finite dimensional image modulo the completed integers.

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.TateTraceCompat_of_isSeparable
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
def

KwF4gRRTateCommFiniteGen

L2339 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.KwF4gRRTateCommFiniteGen
Documentation

Finite dimensionality of Tate commutator ranges for projectors with the same range as the Tate projector.

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.TateTraceCompat_of_isSeparable
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 DiffTraceZero
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (pA' : u.adicCompletion →ₗ[K] u.adicCompletion)
Lean source · statement
def KwF4gRRTateCommFiniteGen : Prop
theorem

kwF4gRRTate_poleWindowFinite

L2377 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2388 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2406 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

ker_pA'_inf_integers

L2463 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.ker_pA'_inf_integers
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.TateTraceCompat_of_isSeparable
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 KerInf
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (pA' : u.adicCompletion →ₗ[K] u.adicCompletion)
Lean source · statement
theorem ker_pA'_inf_integers (h : SameRangeIdemProjectors (tateProj u) pA') :
    LinearMap.ker pA' ⊓ adicIntegersKSubmod u = ⊥
theorem

finiteDimensional_ker_pA'_inf_poleWindow

L2473 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.finiteDimensional_ker_pA'_inf_poleWindow
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.TateTraceCompat_of_isSeparable
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 KerInf
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (pA' : u.adicCompletion →ₗ[K] u.adicCompletion)
Lean source · statement
theorem finiteDimensional_ker_pA'_inf_poleWindow
    (h : SameRangeIdemProjectors (tateProj u) pA')
    [u.FiniteResidue] (πh : u.adicCompletionIntegers) (hπh : Irreducible πh) (M : ℕ) :
    FiniteDimensional K
      ((LinearMap.ker pA' ⊓ poleWindowKSubmod u πh M : Submodule K _))
theorem

finiteDimensional_principalPart_pA'_range

L2506 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.finiteDimensional_principalPart_pA'_range
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.TateTraceCompat_of_isSeparable
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 (pA' : u.adicCompletion →ₗ[K] u.adicCompletion)
variable [∀ u : Place K L, u.FiniteResidue]
Lean source · statement
theorem finiteDimensional_principalPart_pA'_range
    (h : SameRangeIdemProjectors (tateProj u) pA') (fh : u.adicCompletion) :
    FiniteDimensional K
      (LinearMap.range
        ((LinearMap.id - pA') ∘ₗ lmulK u fh ∘ₗ (adicIntegersKSubmod u).subtype))
theorem

kwF4gRRTate_commFiniteGen

L2531 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.kwF4gRRTate_commFiniteGen
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.TateTraceCompat_of_isSeparable
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 (pA' : u.adicCompletion →ₗ[K] u.adicCompletion)
variable [∀ u : Place K L, u.FiniteResidue]
Lean source · statement
theorem kwF4gRRTate_commFiniteGen :
    KwF4gRRTateCommFiniteGen u pA'
theorem

finrankTrace_congr

L2603 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2609 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2615 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2624 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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 (φ - ψ)
theorem

range_conj_eq_map

L2643 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.range_conj_eq_map
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.TateTraceCompat_of_isSeparable
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 ConjInvariance
variable {K M N : Type*} [Field K] [AddCommGroup M] [Module K M]
variable [AddCommGroup N] [Module K N]
Lean source · statement
theorem range_conj_eq_map (e : M ≃ₗ[K] N) (φ : M →ₗ[K] M) :
    LinearMap.range (e.conj φ) = (LinearMap.range φ).map (e : M →ₗ[K] N)
theorem

finrankTrace_conj

L2648 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.finrankTrace_conj
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.TateTraceCompat_of_isSeparable
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 ConjInvariance
variable {K M N : Type*} [Field K] [AddCommGroup M] [Module K M]
variable [AddCommGroup N] [Module K N]
Lean source · full declaration
theorem finrankTrace_conj (e : M ≃ₗ[K] N) (φ : M →ₗ[K] M)
    [hφ : FiniteDimensional K (LinearMap.range φ)] :
    have : FiniteDimensional K (LinearMap.range (e.conj φ)) := by
      rw [range_conj_eq_map]
      exact (Submodule.equivMapOfInjective _ e.injective _).finiteDimensional
    finrankTrace (e.conj φ) = finrankTrace φ := by
  have hgf : ((e : M →ₗ[K] N) ∘ₗ φ) ∘ₗ (e.symm : N →ₗ[K] M) = e.conj φ := by
    apply LinearMap.ext; intro x
    simp only [LinearMap.comp_apply, LinearEquiv.coe_coe, LinearEquiv.conj_apply]
  have hfg : (e.symm : N →ₗ[K] M) ∘ₗ ((e : M →ₗ[K] N) ∘ₗ φ) = φ := by
    apply LinearMap.ext; intro x
    simp only [LinearMap.comp_apply, LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply]
  have : FiniteDimensional K
      (LinearMap.range (((e : M →ₗ[K] N) ∘ₗ φ) ∘ₗ (e.symm : N →ₗ[K] M))) := by
    rw [hgf, range_conj_eq_map]
    exact (Submodule.equivMapOfInjective _ e.injective _).finiteDimensional
  have : FiniteDimensional K
      (LinearMap.range ((e.symm : N →ₗ[K] M) ∘ₗ ((e : M →ₗ[K] N) ∘ₗ φ))) := by
    rw [hfg]; exact hφ
  have hcyc := finrankTrace_comp_comm (e.symm : N →ₗ[K] M) ((e : M →ₗ[K] N) ∘ₗ φ)
  have hconj : FiniteDimensional K (LinearMap.range (e.conj φ)) := by
    rw [range_conj_eq_map]
    exact (Submodule.equivMapOfInjective _ e.injective _).finiteDimensional
  exact (finrankTrace_congr hgf.symm).trans (hcyc.trans (finrankTrace_congr hfg))
def

alphaMap

L2681 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.alphaMap
Documentation

Multiplication on the range of the Tate projector, followed by passage to 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.TateTraceCompat_of_isSeparable
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

alphaMap_apply

L2685 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.alphaMap_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.TateTraceCompat_of_isSeparable
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
theorem alphaMap_apply (c : u.adicCompletion) (a : LinearMap.range (tateProj u)) :
    alphaMap u c a = Submodule.Quotient.mk (c * (a : u.adicCompletion))
def

mulOnRange

L2690 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.mulOnRange
Documentation

Multiplication by an integral completed element restricted to the range of the Tate projector.

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.TateTraceCompat_of_isSeparable
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 mulOnRange {gh : u.adicCompletion} (hgh : gh ∈ u.adicCompletionIntegers) :
    LinearMap.range (tateProj u) →ₗ[K] LinearMap.range (tateProj u)
theorem

mulOnRange_apply

L2699 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.mulOnRange_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.TateTraceCompat_of_isSeparable
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
theorem mulOnRange_apply {gh : u.adicCompletion} (hgh : gh ∈ u.adicCompletionIntegers)
    (a : LinearMap.range (tateProj u)) :
    (mulOnRange u hgh a : u.adicCompletion) = gh * (a : u.adicCompletion)
theorem

finiteDimensional_range_alphaMap

L2705 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

instFinDimRangeDeltaAlpha

L2737 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.instFinDimRangeDeltaAlpha
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.TateTraceCompat_of_isSeparable
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 Cyclicity
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable [u.FiniteResidue]
variable {pA' : u.adicCompletion →ₗ[K] u.adicCompletion}
Lean source · statement
instance instFinDimRangeDeltaAlpha (h : SameRangeIdemProjectors (tateProj u) pA')
    (c : u.adicCompletion) :
    FiniteDimensional K (LinearMap.range (deltaQuotFactor h ∘ₗ alphaMap u c))
instance

instFinDimRangeMulDeltaAlpha

L2744 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.instFinDimRangeMulDeltaAlpha
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.TateTraceCompat_of_isSeparable
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 Cyclicity
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable [u.FiniteResidue]
variable {pA' : u.adicCompletion →ₗ[K] u.adicCompletion}
Lean source · statement
instance instFinDimRangeMulDeltaAlpha (h : SameRangeIdemProjectors (tateProj u) pA')
    (c : u.adicCompletion) {gh : u.adicCompletion} (hgh : gh ∈ u.adicCompletionIntegers) :
    FiniteDimensional K
      (LinearMap.range (mulOnRange u hgh ∘ₗ deltaQuotFactor h ∘ₗ alphaMap u c))
theorem

finrankTrace_term_eq

L2752 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.finrankTrace_term_eq
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.TateTraceCompat_of_isSeparable
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 Cyclicity
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable [u.FiniteResidue]
variable {pA' : u.adicCompletion →ₗ[K] u.adicCompletion}
Lean source · statement
theorem finrankTrace_term_eq (h : SameRangeIdemProjectors (tateProj u) pA')
    (fh : u.adicCompletion) {gh : u.adicCompletion} (hgh : gh ∈ u.adicCompletionIntegers) :
    finrankTrace (deltaQuotFactor h ∘ₗ alphaMap u (gh * fh))
      = finrankTrace (mulOnRange u hgh ∘ₗ deltaQuotFactor h ∘ₗ alphaMap u fh)
theorem

kwF4gRRTate_projectorIndep

L2793 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.kwF4gRRTate_projectorIndep
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.TateTraceCompat_of_isSeparable
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 L : Type*} [Field K] [Field L] [Algebra K L]
variable [∀ u : Place K L, u.FiniteResidue]
Lean source · statement
theorem kwF4gRRTate_projectorIndep : KwF4gRRTateProjectorIndep K L
instance

instFinDimRangeNeg

L2879 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2887 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2890 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2898 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2906 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2913 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2929 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2936 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2945 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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

L2963 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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])
def

tateCommDual

L3035 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.tateCommDual
Documentation

The ambient linear commutator obtained by alternating multiplication and 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.TateTraceCompat_of_isSeparable
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 DualAmbient
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
def tateCommDual (pA φ ψ : V →ₗ[K] V) : V →ₗ[K] V
theorem

tateCommDual_apply

L3038 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.tateCommDual_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.TateTraceCompat_of_isSeparable
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 DualAmbient
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateCommDual_apply (pA φ ψ : V →ₗ[K] V) (x : V) :
    tateCommDual pA φ ψ x = φ (pA (ψ (pA x))) - ψ (pA (φ (pA x)))
theorem

tateCommTrace_eq_finrankTrace_tateCommDual

L3041 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.tateCommTrace_eq_finrankTrace_tateCommDual
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.TateTraceCompat_of_isSeparable
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 DualAmbient
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem tateCommTrace_eq_finrankTrace_tateCommDual {pA φ ψ : V →ₗ[K] V}
    [hR : FiniteDimensional K (LinearMap.range (tateCommRestrict pA φ ψ))]
    [hD : FiniteDimensional K (LinearMap.range (tateCommDual pA φ ψ))] :
    tateCommTrace pA φ ψ = finrankTrace (tateCommDual pA φ ψ)
instance

instFinDimRangeSum

L3077 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.instFinDimRangeSum
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.TateTraceCompat_of_isSeparable
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 FinsetAdditivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
instance instFinDimRangeSum {ι : Type*} (s : Finset ι) (f : ι → V →ₗ[K] V)
    [∀ i, FiniteDimensional K (LinearMap.range (f i))] :
    FiniteDimensional K (LinearMap.range (∑ i ∈ s, f i))
theorem

finrankTrace_sum

L3085 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.finrankTrace_sum
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.TateTraceCompat_of_isSeparable
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 FinsetAdditivity
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem finrankTrace_sum {ι : Type*} (s : Finset ι) (f : ι → V →ₗ[K] V)
    [∀ i, FiniteDimensional K (LinearMap.range (f i))] :
    finrankTrace (∑ i ∈ s, f i) = ∑ i ∈ s, finrankTrace (f i)
theorem

finiteDimensional_range_comp_middle

L3110 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.finiteDimensional_range_comp_middle
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.TateTraceCompat_of_isSeparable
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 LemmaC
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
Lean source · statement
theorem finiteDimensional_range_comp_middle
    {M₁ M₂ M₃ M₄ : Type*} [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃]
    [AddCommGroup M₄] [Module K M₁] [Module K M₂] [Module K M₃] [Module K M₄]
    (A : M₃ →ₗ[K] M₄) (δ : M₂ →ₗ[K] M₃) (B : M₁ →ₗ[K] M₂)
    [FiniteDimensional K (LinearMap.range δ)] :
    FiniteDimensional K (LinearMap.range (A ∘ₗ δ ∘ₗ B))
theorem

finiteDimensional_range_tateCommDual_tateProj

L3127 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.finiteDimensional_range_tateCommDual_tateProj
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.TateTraceCompat_of_isSeparable
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 AmbientFinite
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable [u.FiniteResidue]
Lean source · statement
theorem finiteDimensional_range_tateCommDual_tateProj
    (fh : u.adicCompletion) {gh : u.adicCompletion} (hgh : gh ∈ u.adicCompletionIntegers) :
    FiniteDimensional K
      (LinearMap.range (tateCommDual (tateProj u) (lmulK u fh) (lmulK u gh)))
theorem

tateRes_congr_fst

L3158 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.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.TateTraceCompat_of_isSeparable
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 TateResSum
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₂)
    [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)))] :
    tateRes u fh₁ gh = tateRes u fh₂ gh
theorem

tateRes_sum_fst

L3167 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.tateRes_sum_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.TateTraceCompat_of_isSeparable
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 TateResSum
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · full declaration
theorem tateRes_sum_fst {ι : Type*} (s : Finset ι) (f : ι → u.adicCompletion)
    (gh : u.adicCompletion) (hfin : KwF4gRRTateCommFinite K L) :
    let := fun i => hfin u (f i) gh
    let := hfin u (∑ i ∈ s, f i) gh
    ∑ i ∈ s, tateRes u (f i) gh = tateRes u (∑ i ∈ s, f i) gh := by
  let := fun i => hfin u (f i) gh
  let := hfin u (∑ i ∈ s, f i) gh
  change ∑ i ∈ s, tateRes u (f i) gh = tateRes u (∑ i ∈ s, f i) gh
  classical
  induction s using Finset.induction_on with
  | empty =>
    let := hfin u (0 : u.adicCompletion) gh
    simp only [Finset.sum_empty]
    unfold tateRes tateCommTrace
    have h0 : tateCommRestrict (tateProj u) (lmulK u 0) (lmulK u gh) = 0 := by
      apply LinearMap.ext; intro a; apply Subtype.ext
      rw [tateCommRestrict_apply, tateComm_apply]
      simp [lmulK]
    rw [finrankTrace_congr h0, finrankTrace_zero]
  | insert a s ha ih =>
    let := hfin u (∑ i ∈ s, f i) gh
    let := hfin u (∑ i ∈ insert a s, f i) gh
    let := hfin u (f a + ∑ i ∈ s, f i) gh
    conv_lhs => rw [Finset.sum_insert ha]
    calc
      tateRes u (f a) gh + ∑ i ∈ s, tateRes u (f i) gh =
          tateRes u (f a) gh + tateRes u (∑ i ∈ s, f i) gh := by rw [ih]
      _ = tateRes u (f a + ∑ i ∈ s, f i) gh :=
        (tateRes_add_fst u (f a) (∑ i ∈ s, f i) gh).symm
      _ = tateRes u (∑ i ∈ insert a s, f i) gh :=
        tateRes_congr_fst u (Finset.sum_insert ha).symm
def

KwF4gRRTateTraceCompatBlockSum

L3209 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.KwF4gRRTateTraceCompatBlockSum
Documentation

The local Tate residue equals the sum of the Tate residues of diagonal matrix entries over the restricted completion.

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.TateTraceCompat_of_isSeparable
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 BlockSumMint
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable (E : Type*) [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
def KwF4gRRTateTraceCompatBlockSum (hfinF : KwF4gRRTateCommFinite K F)
    (hfinE : KwF4gRRTateCommFinite K E) : Prop
theorem

kwF4gRRTate_traceCompat_of_blockSum

L3236 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.kwF4gRRTate_traceCompat_of_blockSum
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.TateTraceCompat_of_isSeparable
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 {E : Type*} [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_traceCompat_of_blockSum
    (hfinF : KwF4gRRTateCommFinite K F) (hfinE : KwF4gRRTateCommFinite K E)
    (hBS : KwF4gRRTateTraceCompatBlockSum K F E hfinF hfinE) :
    KwF4gRRTateTraceCompat K F E hfinF hfinE
theorem

tateCommDual_conj

L3303 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.tateCommDual_conj
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.TateTraceCompat_of_isSeparable
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 ConjNaturality
variable {K M N : Type*} [Field K] [AddCommGroup M] [Module K M]
variable [AddCommGroup N] [Module K N]
Lean source · statement
theorem tateCommDual_conj (e : M ≃ₗ[K] N) (pA φ ψ : M →ₗ[K] M) :
    e.conj (tateCommDual pA φ ψ) = tateCommDual (e.conj pA) (e.conj φ) (e.conj ψ)
def

prodTateProj

L3316 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.prodTateProj
Documentation

The linear projector obtained by applying the Tate projector in each coordinate.

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.TateTraceCompat_of_isSeparable
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 ProdProj
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (v : Place K L)
Lean source · statement
def prodTateProj (ι : Type*) :
    (ι → v.adicCompletion) →ₗ[K] (ι → v.adicCompletion)
theorem

prodTateProj_apply

L3320 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.prodTateProj_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.TateTraceCompat_of_isSeparable
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 ProdProj
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (v : Place K L)
Lean source · statement
theorem prodTateProj_apply {ι : Type*} (x : ι → v.adicCompletion) (i : ι) :
    prodTateProj v ι x i = tateProj v (x i)
theorem

prodTateProj_idem

L3323 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.prodTateProj_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.TateTraceCompat_of_isSeparable
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 ProdProj
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (v : Place K L)
Lean source · statement
theorem prodTateProj_idem {ι : Type*} (x : ι → v.adicCompletion) :
    prodTateProj v ι (prodTateProj v ι x) = prodTateProj v ι x
def

matMulLin

L3335 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.matMulLin
Documentation

The K-linear map on completion-valued vectors given by multiplication by the matrix.

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.TateTraceCompat_of_isSeparable
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 BlockDecomp
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (v : Place K L)
variable {n : ℕ}
Lean source · statement
def matMulLin (M : Matrix (Fin n) (Fin n) v.adicCompletion) :
    (Fin n → v.adicCompletion) →ₗ[K] (Fin n → v.adicCompletion)
theorem

matMulLin_apply

L3339 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.matMulLin_apply
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.TateTraceCompat_of_isSeparable
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 BlockDecomp
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (v : Place K L)
variable {n : ℕ}
Lean source · statement
theorem matMulLin_apply (M : Matrix (Fin n) (Fin n) v.adicCompletion)
    (x : Fin n → v.adicCompletion) (i : Fin n) :
    matMulLin v M x i = ∑ j, M i j * x j
def

scalarLin

L3348 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.scalarLin
Documentation

The K-linear map on completion-valued vectors given by multiplication by the scalar in each coordinate.

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.TateTraceCompat_of_isSeparable
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 BlockDecomp
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (v : Place K L)
variable {n : ℕ}
Lean source · statement
def scalarLin (πv : v.adicCompletion) :
    (Fin n → v.adicCompletion) →ₗ[K] (Fin n → v.adicCompletion)
theorem

scalarLin_apply

L3352 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.scalarLin_apply
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.TateTraceCompat_of_isSeparable
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 BlockDecomp
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (v : Place K L)
variable {n : ℕ}
Lean source · statement
theorem scalarLin_apply (πv : v.adicCompletion) (x : Fin n → v.adicCompletion) (i : Fin n) :
    scalarLin v πv x i = πv * x i
theorem

tateCommDual_prodTateProj_eq_blockSum

L3355 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.tateCommDual_prodTateProj_eq_blockSum
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.TateTraceCompat_of_isSeparable
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 BlockDecomp
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (v : Place K L)
variable {n : ℕ}
Lean source · full declaration
theorem tateCommDual_prodTateProj_eq_blockSum
    (M : Matrix (Fin n) (Fin n) v.adicCompletion) (πv : v.adicCompletion) :
    tateCommDual (prodTateProj v (Fin n)) (matMulLin v M) (scalarLin v πv)
      = ∑ i, ∑ j, LinearMap.single K (fun _ => v.adicCompletion) i
          ∘ₗ tateCommDual (tateProj v) (lmulK v (M i j)) (lmulK v πv)
          ∘ₗ LinearMap.proj j := by
  apply LinearMap.ext; intro x; funext i
  have hRHS : ((∑ i', ∑ j, LinearMap.single K (fun _ => v.adicCompletion) i'
          ∘ₗ tateCommDual (tateProj v) (lmulK v (M i' j)) (lmulK v πv)
          ∘ₗ LinearMap.proj j) x) i
      = ∑ j, tateCommDual (tateProj v) (lmulK v (M i j)) (lmulK v πv) (x j) := by
    simp only [LinearMap.sum_apply, LinearMap.comp_apply, LinearMap.proj_apply,
      Finset.sum_apply, LinearMap.single_apply]
    rw [Finset.sum_eq_single i (fun i' _ hi' => ?_) (fun h => absurd (Finset.mem_univ i) h)]
    · simp only [Pi.single_eq_same]
    · exact Finset.sum_eq_zero fun j _ => Pi.single_eq_of_ne' hi' _
  rw [hRHS, tateCommDual_apply]
  simp only [prodTateProj_apply, matMulLin_apply, scalarLin_apply, Pi.sub_apply]
  rw [show tateProj v (∑ j, M i j * tateProj v (x j))
      = ∑ j, tateProj v (M i j * tateProj v (x j)) from map_sum _ _ _,
    Finset.mul_sum, ← Finset.sum_sub_distrib]
  refine Finset.sum_congr rfl fun j _ => ?_
  rw [tateCommDual_apply]; rfl
theorem

finrankTrace_blockSum

L3386 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.finrankTrace_blockSum
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.TateTraceCompat_of_isSeparable
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 BlockTrace
variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
variable {n : ℕ}
Lean source · full declaration
theorem finrankTrace_blockSum (T : Fin n → Fin n → (V →ₗ[K] V))
    [hT : ∀ i j, FiniteDimensional K (LinearMap.range (T i j))] :
    have : ∀ (i j : Fin n), FiniteDimensional K (LinearMap.range
        (LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i j
          ∘ₗ (LinearMap.proj j : (Fin n → V) →ₗ[K] V))) :=
      fun i j => finiteDimensional_range_comp_middle
        (LinearMap.single K (fun _ : Fin n => V) i) (T i j)
        (LinearMap.proj j : (Fin n → V) →ₗ[K] V)
    finrankTrace (∑ i, ∑ j, LinearMap.single K (fun _ : Fin n => V) i
        ∘ₗ T i j ∘ₗ (LinearMap.proj j : (Fin n → V) →ₗ[K] V))
      = ∑ i, finrankTrace (T i i) := by
  have : ∀ (i j : Fin n), FiniteDimensional K (LinearMap.range
      (LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i j
        ∘ₗ (LinearMap.proj j : (Fin n → V) →ₗ[K] V))) :=
    fun i j => finiteDimensional_range_comp_middle
      (LinearMap.single K (fun _ : Fin n => V) i) (T i j)
      (LinearMap.proj j : (Fin n → V) →ₗ[K] V)
  have : ∀ (i : Fin n), FiniteDimensional K (LinearMap.range
      (∑ j, LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i j
        ∘ₗ (LinearMap.proj j : (Fin n → V) →ₗ[K] V))) :=
    fun i => instFinDimRangeSum _ _
  refine (finrankTrace_sum (Finset.univ : Finset (Fin n))
    (fun i => ∑ j : Fin n, LinearMap.single K (fun _ : Fin n => V) i
      ∘ₗ T i j ∘ₗ (LinearMap.proj j : (Fin n → V) →ₗ[K] V))).trans ?_
  refine Finset.sum_congr rfl fun i _ => ?_
  refine (finrankTrace_sum (Finset.univ : Finset (Fin n))
    (fun j => LinearMap.single K (fun _ : Fin n => V) i
      ∘ₗ T i j ∘ₗ (LinearMap.proj j : (Fin n → V) →ₗ[K] V))).trans ?_
  have hassoc : ∀ (j : Fin n), LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i j
      ∘ₗ (LinearMap.proj j : (Fin n → V) →ₗ[K] V)
      = (LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i j)
        ∘ₗ (LinearMap.proj j : (Fin n → V) →ₗ[K] V) := fun j => rfl
  have hswap : ∀ (j : Fin n), (LinearMap.proj j : (Fin n → V) →ₗ[K] V)
      ∘ₗ (LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i j)
      = if j = i then T i i else 0 := fun j => by
    apply LinearMap.ext; intro y
    simp only [LinearMap.comp_apply, LinearMap.proj_apply, LinearMap.single_apply]
    by_cases hji : j = i
    · subst hji; rw [ite_eq_left rfl, Pi.single_eq_same]
    · rw [ite_eq_right hji, Pi.single_eq_of_ne hji, LinearMap.zero_apply]
  rw [Finset.sum_eq_single i (fun j _ hj => ?_) (fun h => absurd (Finset.mem_univ i) h)]
  · have hfi : FiniteDimensional K (LinearMap.range
        ((LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i i)
          ∘ₗ (LinearMap.proj i : (Fin n → V) →ₗ[K] V))) := hassoc i ▸ inferInstance
    have hgi : FiniteDimensional K (LinearMap.range
        ((LinearMap.proj i : (Fin n → V) →ₗ[K] V)
          ∘ₗ (LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i i))) := by
      rw [hswap i, ite_eq_left rfl]; exact hT i i
    calc finrankTrace (LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i i
            ∘ₗ (LinearMap.proj i : (Fin n → V) →ₗ[K] V))
        = finrankTrace ((LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i i)
            ∘ₗ (LinearMap.proj i : (Fin n → V) →ₗ[K] V)) := finrankTrace_congr (hassoc i)
      _ = finrankTrace ((LinearMap.proj i : (Fin n → V) →ₗ[K] V)
            ∘ₗ (LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i i)) :=
          finrankTrace_comp_comm _ _
      _ = finrankTrace (T i i) := finrankTrace_congr (by rw [hswap i, ite_eq_left rfl])
  · have hfj : FiniteDimensional K (LinearMap.range
        ((LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i j)
          ∘ₗ (LinearMap.proj j : (Fin n → V) →ₗ[K] V))) := hassoc j ▸ inferInstance
    have hgj : FiniteDimensional K (LinearMap.range
        ((LinearMap.proj j : (Fin n → V) →ₗ[K] V)
          ∘ₗ (LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i j))) := by
      rw [hswap j, ite_eq_right hj]; exact instFinDimRangeZero
    calc finrankTrace (LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i j
            ∘ₗ (LinearMap.proj j : (Fin n → V) →ₗ[K] V))
        = finrankTrace ((LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i j)
            ∘ₗ (LinearMap.proj j : (Fin n → V) →ₗ[K] V)) := finrankTrace_congr (hassoc j)
      _ = finrankTrace ((LinearMap.proj j : (Fin n → V) →ₗ[K] V)
            ∘ₗ (LinearMap.single K (fun _ : Fin n => V) i ∘ₗ T i j)) :=
          finrankTrace_comp_comm _ _
      _ = finrankTrace (0 : V →ₗ[K] V) := finrankTrace_congr (by rw [hswap j, ite_eq_right hj])
      _ = 0 := finrankTrace_zero
instance

instIsScalarTowerKVhatWhat

L3467 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.instIsScalarTowerKVhatWhat
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.TateTraceCompat_of_isSeparable
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 {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
instance instIsScalarTowerKVhatWhat (w : Place K F) :
    IsScalarTower K (w.restrict E).adicCompletion w.adicCompletion
theorem

kwF4gRRTate_free_adicCompletionIntegers

L3510 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.kwF4gRRTate_free_adicCompletionIntegers
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.TateTraceCompat_of_isSeparable
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 Freeness
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4gRRTate_free_adicCompletionIntegers (w : Place K F) [FiniteDimensional E F]
    [Algebra.IsSeparable (w.restrict E).adicCompletion w.adicCompletion] :
    Module.Free (w.restrict E).adicCompletionIntegers w.adicCompletionIntegers
structure

IntegralBasisData

L3536 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.IntegralBasisData
Documentation

A basis of the completion whose integral coordinate lattice is the completed valuation ring.

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.TateTraceCompat_of_isSeparable
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 IntegralBasisMint
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · full declaration
structure IntegralBasisData (w : Place K F) [FiniteDimensional E F] where
  /-- A basis over the restricted completion, indexed by the extension finrank. -/
  basis : Module.Basis
    (Fin (Module.finrank (w.restrict E).adicCompletion w.adicCompletion))
    (w.restrict E).adicCompletion w.adicCompletion
  /-- Every basis vector is an integral completed element. -/
  basis_mem : ∀ i, basis i ∈ w.adicCompletionIntegers
  /-- A completed element is integral exactly when all its basis coordinates are integral. -/
  mem_integers_iff : ∀ y, y ∈ w.adicCompletionIntegers
    ↔ ∀ i, basis.repr y i ∈ (w.restrict E).adicCompletionIntegers
def

KwF4gRRTateIntegralBasisCompat

L3550 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.KwF4gRRTateIntegralBasisCompat
Documentation

Every place admits a basis identifying its completed valuation ring with integral coordinates over the restricted place.

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.TateTraceCompat_of_isSeparable
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 IntegralBasisMint
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable (K F E) in
Lean source · statement
def KwF4gRRTateIntegralBasisCompat : Prop
def

integralBasisEquivFunK

L3565 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.integralBasisEquivFunK
Documentation

The K-linear coordinate equivalence associated to the chosen integral basis of the completion.

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.TateTraceCompat_of_isSeparable
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 IntegralProdProj
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable (w : Place K F) [FiniteDimensional E F] (D : IntegralBasisData (E := E) w)
Lean source · statement
def integralBasisEquivFunK : w.adicCompletion ≃ₗ[K]
    (Fin (Module.finrank (w.restrict E).adicCompletion w.adicCompletion)
      → (w.restrict E).adicCompletion)
theorem

integralBasisEquivFunK_apply

L3570 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.integralBasisEquivFunK_apply
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.TateTraceCompat_of_isSeparable
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 IntegralProdProj
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable (w : Place K F) [FiniteDimensional E F] (D : IntegralBasisData (E := E) w)
Lean source · statement
theorem integralBasisEquivFunK_apply (y : w.adicCompletion) :
    integralBasisEquivFunK w D y = D.basis.equivFun y
def

integralProdProj

L3574 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.integralProdProj
Documentation

The coordinatewise Tate projector transported to the completion by the chosen integral basis.

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.TateTraceCompat_of_isSeparable
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 IntegralProdProj
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable (w : Place K F) [FiniteDimensional E F] (D : IntegralBasisData (E := E) w)
Lean source · statement
def integralProdProj : w.adicCompletion →ₗ[K] w.adicCompletion
theorem

integralProdProj_idem

L3577 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.integralProdProj_idem
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.TateTraceCompat_of_isSeparable
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 IntegralProdProj
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable (w : Place K F) [FiniteDimensional E F] (D : IntegralBasisData (E := E) w)
Lean source · statement
theorem integralProdProj_idem (y : w.adicCompletion) :
    integralProdProj w D (integralProdProj w D y) = integralProdProj w D y
theorem

range_integralProdProj

L3584 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.range_integralProdProj
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.TateTraceCompat_of_isSeparable
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 IntegralProdProj
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable (w : Place K F) [FiniteDimensional E F] (D : IntegralBasisData (E := E) w)
Lean source · statement
theorem range_integralProdProj :
    LinearMap.range (integralProdProj w D) = adicIntegersKSubmod w
theorem

sameRangeIdemProjectors_integralProdProj

L3615 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.sameRangeIdemProjectors_integralProdProj
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.TateTraceCompat_of_isSeparable
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 IntegralProdProj
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable (w : Place K F) [FiniteDimensional E F] (D : IntegralBasisData (E := E) w)
Lean source · full declaration
theorem sameRangeIdemProjectors_integralProdProj :
    SameRangeIdemProjectors (tateProj w) (integralProdProj w D) where
  idem_pA x := congrFun (congrArg DFunLike.coe (tateProj_idem w)) x
  idem_pA' := integralProdProj_idem w D
  range_eq := (range_tateProj w).trans (range_integralProdProj w D).symm
theorem

integralBasisEquivFunK_conj_lmulK_algebraMap

L3629 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.integralBasisEquivFunK_conj_lmulK_algebraMap
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.TateTraceCompat_of_isSeparable
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 {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem integralBasisEquivFunK_conj_lmulK_algebraMap (w : Place K F) [FiniteDimensional E F]
    (D : IntegralBasisData (E := E) w) (g : F) :
    (integralBasisEquivFunK w D).conj (lmulK w (algebraMap F w.adicCompletion g))
      = matMulLin (w.restrict E)
          (LinearMap.toMatrix D.basis D.basis
            (Algebra.lmul (w.restrict E).adicCompletion w.adicCompletion
              (algebraMap F w.adicCompletion g)))
theorem

integralBasisEquivFunK_conj_lmulK_scalar

L3652 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.integralBasisEquivFunK_conj_lmulK_scalar
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.TateTraceCompat_of_isSeparable
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 {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem integralBasisEquivFunK_conj_lmulK_scalar (w : Place K F) [FiniteDimensional E F]
    (D : IntegralBasisData (E := E) w) (e : E) :
    (integralBasisEquivFunK w D).conj
        (lmulK w (algebraMap F w.adicCompletion (algebraMap E F e)))
      = scalarLin (w.restrict E) (algebraMap E (w.restrict E).adicCompletion e)
theorem

kwF4gRRTate_blockSum_of_integralBasisCompat

L3670 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.kwF4gRRTate_blockSum_of_integralBasisCompat
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.TateTraceCompat_of_isSeparable
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 {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4gRRTate_blockSum_of_integralBasisCompat
    [∀ w : Place K F, w.FiniteResidue] [∀ v : Place K E, v.FiniteResidue]
    (hfinF : KwF4gRRTateCommFinite K F) (hfinE : KwF4gRRTateCommFinite K E)
    (hIBC : KwF4gRRTateIntegralBasisCompat K F E) :
    KwF4gRRTateTraceCompatBlockSum K F E hfinF hfinE
theorem

kwF4gRRTate_traceCompat_of_integralBasisCompat

L3803 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.kwF4gRRTate_traceCompat_of_integralBasisCompat
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.TateTraceCompat_of_isSeparable
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 {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4gRRTate_traceCompat_of_integralBasisCompat
    [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E]
    [∀ w : Place K F, w.FiniteResidue] [∀ v : Place K E, v.FiniteResidue]
    (hfinF : KwF4gRRTateCommFinite K F) (hfinE : KwF4gRRTateCommFinite K E)
    (hIBC : KwF4gRRTateIntegralBasisCompat K F E) :
    KwF4gRRTateTraceCompat K F E hfinF hfinE
instance

instIsLocalizationAlgebraMapSubmonoid

L3850 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.instIsLocalizationAlgebraMapSubmonoid
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable
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 Construct
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable (w : Place K F) [FiniteDimensional E F]
variable [Algebra.IsSeparable (w.restrict E).adicCompletion w.adicCompletion]
variable [Module.IsTorsionFree (w.restrict E).adicCompletionIntegers w.adicCompletion]
Lean source · full declaration
instance instIsLocalizationAlgebraMapSubmonoid :
    have : Algebra.IsAlgebraic (w.restrict E).adicCompletion w.adicCompletion :=
      Algebra.IsAlgebraic.of_finite _ _
    have := TateTraceCompat_of_isSeparable.kw_ffgc_isIntegralClosure_adicCompletionIntegers E w
    IsLocalization (Algebra.algebraMapSubmonoid w.adicCompletionIntegers
      (nonZeroDivisors (w.restrict E).adicCompletionIntegers)) w.adicCompletion := by
  have : Algebra.IsAlgebraic (w.restrict E).adicCompletion w.adicCompletion :=
    Algebra.IsAlgebraic.of_finite _ _
  have := TateTraceCompat_of_isSeparable.kw_ffgc_isIntegralClosure_adicCompletionIntegers E w
  exact IsIntegralClosure.isLocalization (w.restrict E).adicCompletionIntegers
    (w.restrict E).adicCompletion w.adicCompletion w.adicCompletionIntegers
def

integralBasisDataOf

L3864 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.integralBasisDataOf
Documentation

Constructs an integral completion basis by localizing and reindexing a basis of the completed valuation ring.

Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable
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 Construct
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable (w : Place K F) [FiniteDimensional E F]
variable [Algebra.IsSeparable (w.restrict E).adicCompletion w.adicCompletion]
variable [Module.IsTorsionFree (w.restrict E).adicCompletionIntegers w.adicCompletion]
Lean source · statement
def integralBasisDataOf : IntegralBasisData (E := E) w
instance

kwF4R1V384a_instAlgebraFiberCompletion

L3956 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4R1V384a.kwF4R1V384a_instAlgebraFiberCompletion
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.TateTraceCompat_of_isSeparable
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
open _root_.TensorProduct
open AlgebraicCurve.KwBwnmchRFTDCDischarge
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V384a
open _root_.ModularCurve
section FiberAlgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
Lean source · statement
instance kwF4R1V384a_instAlgebraFiberCompletion (v : Place K E) (w' : v.fiber F) :
    Algebra v.adicCompletion w'.1.adicCompletion
instance

kwF4R1V384a_instIsScalarTowerFiberCompletion

L3963 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4R1V384a.kwF4R1V384a_instIsScalarTowerFiberCompletion
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.TateTraceCompat_of_isSeparable
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
open _root_.TensorProduct
open AlgebraicCurve.KwBwnmchRFTDCDischarge
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V384a
open _root_.ModularCurve
section FiberAlgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
Lean source · statement
instance kwF4R1V384a_instIsScalarTowerFiberCompletion (v : Place K E) (w' : v.fiber F) :
    IsScalarTower E v.adicCompletion w'.1.adicCompletion
def

kwF4R1V384a_semilocalComponent

L3983 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4R1V384a.kwF4R1V384a_semilocalComponent
Documentation

The completion-algebra map from the semilocal tensor product to the completion at the chosen place above v.

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.TateTraceCompat_of_isSeparable
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
open _root_.TensorProduct
open AlgebraicCurve.KwBwnmchRFTDCDischarge
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V384a
open _root_.ModularCurve
section SemilocalDiag
variable {K : Type*} (F : Type*) [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
Lean source · statement
def kwF4R1V384a_semilocalComponent (v : Place K E) (w' : v.fiber F) :
    v.adicCompletion ⊗[E] F →ₐ[v.adicCompletion] w'.1.adicCompletion
theorem

kwF4R1V384a_semilocalComponent_tmul

L3990 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4R1V384a.kwF4R1V384a_semilocalComponent_tmul
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.TateTraceCompat_of_isSeparable
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
open _root_.TensorProduct
open AlgebraicCurve.KwBwnmchRFTDCDischarge
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V384a
open _root_.ModularCurve
section SemilocalDiag
variable {K : Type*} (F : Type*) [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
omit [HasPrincipalDivisors K E] in
Lean source · statement
theorem kwF4R1V384a_semilocalComponent_tmul (v : Place K E) (w' : v.fiber F)
    (c : v.adicCompletion) (g : F) :
    kwF4R1V384a_semilocalComponent F v w' (c ⊗ₜ[E] g)
      = algebraMap v.adicCompletion w'.1.adicCompletion c
          * algebraMap F w'.1.adicCompletion g
theorem

kwF4R1V384a_completionLinearCombination_surjective

L4019 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4R1V384a.kwF4R1V384a_completionLinearCombination_surjective
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.TateTraceCompat_of_isSeparable
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
open _root_.TensorProduct
open AlgebraicCurve.KwBwnmchRFTDCDischarge
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V384a
open _root_.ModularCurve
section PerComponentSurjective
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
variable [FiniteDimensional E F]
omit [HasPrincipalDivisors K E] [HasPrincipalDivisors K F] [FiniteDimensional E F] in
Lean source · statement
theorem kwF4R1V384a_completionLinearCombination_surjective
    (w' : Place K F) {ι : Type*} [Fintype ι] (b : Module.Basis ι E F) :
    Function.Surjective (kw_ffgc_completionLinearCombination E w' b)
theorem

kwF4R1V384a_semilocalComponent_surjective

L4032 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4R1V384a.kwF4R1V384a_semilocalComponent_surjective
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.TateTraceCompat_of_isSeparable
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
open _root_.TensorProduct
open AlgebraicCurve.KwBwnmchRFTDCDischarge
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V384a
open _root_.ModularCurve
section PerComponentSurjective
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F] [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
variable [FiniteDimensional E F]
omit [HasPrincipalDivisors K E] in
Lean source · statement
theorem kwF4R1V384a_semilocalComponent_surjective (v : Place K E) (w' : v.fiber F) :
    Function.Surjective (kwF4R1V384a_semilocalComponent F v w')
instance

kwF4R1V384a_instModuleFiberCompletion

L4063 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4R1V384a.kwF4R1V384a_instModuleFiberCompletion
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.TateTraceCompat_of_isSeparable
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
open _root_.TensorProduct
open AlgebraicCurve.KwBwnmchRFTDCDischarge
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V384a
open _root_.ModularCurve
section BijEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
instance kwF4R1V384a_instModuleFiberCompletion
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
    (v : Place K E) (w' : v.fiber F) :
    Module v.adicCompletion w'.1.adicCompletion
theorem

kwF4R1V386a_isSeparable_algebraMap_fiberCompletion

L4114 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4R1V386a.kwF4R1V386a_isSeparable_algebraMap_fiberCompletion
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.TateTraceCompat_of_isSeparable
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
open _root_.TensorProduct
open _root_.IsLocalRing
open scoped AlgebraicCurve.Place _root_.Valued _root_.NNReal _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V386a
open _root_.ModularCurve
open ModularCurve.KwF4R1V384a
section IsSeparableLift
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwF4R1V386a_isSeparable_algebraMap_fiberCompletion
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
    [FiniteDimensional E F] [Algebra.IsSeparable E F]
    (v : Place K E) (w' : v.fiber F) (g : F) :
    IsSeparable v.adicCompletion (algebraMap F w'.1.adicCompletion g)
theorem

kwF4R1V386a_isSeparable_fiberCompletion

L4134 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.kwF4R1V386a_isSeparable_fiberCompletion
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.TateTraceCompat_of_isSeparable
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
open _root_.TensorProduct
open _root_.IsLocalRing
open scoped AlgebraicCurve.Place _root_.Valued _root_.NNReal _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V386a
open _root_.ModularCurve
open ModularCurve.KwF4R1V384a
section IsSeparableLift
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
open TateTraceCompat_of_isSeparable.ModularCurve.KwF4R1V386a in
with_weak_namespace
    _root_.AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable
Lean source · statement
theorem kwF4R1V386a_isSeparable_fiberCompletion
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
    [FiniteDimensional E F] [Algebra.IsSeparable E F]
    (v : Place K E) (w' : v.fiber F) :
    Algebra.IsSeparable v.adicCompletion w'.1.adicCompletion
theorem

kwTateRR3_isSeparable_completion_of_global

L4231 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.kwTateRR3_isSeparable_completion_of_global
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.TateTraceCompat_of_isSeparable
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 IsSeparableLift
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwTateRR3_isSeparable_completion_of_global
    [HasPrincipalDivisors K E] [HasPrincipalDivisors K F]
    [FiniteDimensional E F] [Algebra.IsSeparable E F]
    (w : Place K F) :
    Algebra.IsSeparable (w.restrict E).adicCompletion w.adicCompletion
theorem

kwTateRR3_isTorsionFree_integersCompletion

L4247 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.kwTateRR3_isTorsionFree_integersCompletion
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.TateTraceCompat_of_isSeparable
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 IsTorsionFree
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwTateRR3_isTorsionFree_integersCompletion (w : Place K F) :
    Module.IsTorsionFree (w.restrict E).adicCompletionIntegers w.adicCompletion
theorem

kwTateRR3_integralBasisCompat_of_isSeparable_global

L4260 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.kwTateRR3_integralBasisCompat_of_isSeparable_global
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.TateTraceCompat_of_isSeparable
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 {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwTateRR3_integralBasisCompat_of_isSeparable_global [Algebra.IsSeparable E F] :
    KwF4gRRTateIntegralBasisCompat K F E
theorem

kwTateRR3_traceCompat_of_isSeparable_global

L4267 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateTraceCompat_of_isSeparable.ModularCurve.KwF4gRRTate.kwTateRR3_traceCompat_of_isSeparable_global
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.TateTraceCompat_of_isSeparable
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 {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
Lean source · statement
theorem kwTateRR3_traceCompat_of_isSeparable_global [Algebra.IsSeparable E F]
    [HasCanonicalLocalResidueKStar K F] [HasCanonicalLocalResidueKStar K E]
    [∀ w : Place K F, w.FiniteResidue] [∀ v : Place K E, v.FiniteResidue]
    (hfinF : KwF4gRRTateCommFinite K F) (hfinE : KwF4gRRTateCommFinite K E) :
    KwF4gRRTateTraceCompat K F E hfinF hfinE
theorem

tateTraceCompat_of_isSeparable

L4285 ↗
AlgebraicCurve.tateTraceCompat_of_isSeparable
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.TateTraceCompat_of_isSeparable
Lean source · statement
theorem _root_.AlgebraicCurve.tateTraceCompat_of_isSeparable {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] [Algebra.IsSeparable E F]
        [AlgebraicCurve.HasCanonicalLocalResidueKStar K F]
          [AlgebraicCurve.HasCanonicalLocalResidueKStar K E] [∀ w : AlgebraicCurve.Place K F,
            w.FiniteResidue] [∀ v : AlgebraicCurve.Place K E, v.FiniteResidue] (hfinF :
              ModularCurve.KwF4gRRTate.KwF4gRRTateCommFinite K F) (hfinE :
                ModularCurve.KwF4gRRTate.KwF4gRRTateCommFinite K E) :
                  ModularCurve.KwF4gRRTate.KwF4gRRTateTraceCompat K F E hfinF hfinE

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