NYLL
Module

TateAgreement.lean

Nyll.AlgebraicCurves.Differentials.Residues.TateAgreement
180 declarations indexed from sourceView source ↗

Module documentation

Agreement between the local Tate residue constructions.

Imports15
Imported by3

Declarations

theorem

maximalIdeal_le

L47 ↗
IsLocalRing.maximalIdeal_le
Source context 4 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
section
open scoped 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
theorem

ord_nonneg_of_mem

L537 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L554 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg
Source context 20 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L564 ↗
AlgebraicCurve.Place.mem_iff_ord_nonneg
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

isClosed_setOf_valued_le

L614 ↗
MazurTorsion.isClosed_setOf_valued_le
Source context 14 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open scoped Multiplicative WithZero
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.MonoidWithZeroHom
namespace MazurTorsion
section Henselian
variable {A : Type*} [CommRing A] [IsDedekindDomain A]
  (K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
  (v : IsDedekindDomain.HeightOneSpectrum A)
Lean source · statement
theorem isClosed_setOf_valued_le (γ : ℤᵐ⁰) :
    IsClosed {x : v.adicCompletion K | Valued.v x ≤ γ}
instance

instIsAdicCompleteCompletionIdealAdicCompletionIntegers

L625 ↗
MazurTorsion.instIsAdicCompleteCompletionIdealAdicCompletionIntegers
Source context 14 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open scoped Multiplicative WithZero
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.MonoidWithZeroHom
namespace MazurTorsion
section Henselian
variable {A : Type*} [CommRing A] [IsDedekindDomain A]
  (K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
  (v : IsDedekindDomain.HeightOneSpectrum A)
Lean source · full declaration
instance instIsAdicCompleteCompletionIdealAdicCompletionIntegers :
    IsAdicComplete (v.completionIdeal K) (v.adicCompletionIntegers K) where
  haus' x hx := by
    have hx' : ∀ n : ℕ, Valued.v x.val ≤ WithZero.exp (-(n : ℤ)) := by
      intro n
      have h := hx n
      simp only [Ideal.smul_eq_mul, Ideal.mul_top, SModEq.zero,
        adicCompletion.mem_completionIdeal_pow K v] at h
      exact h
    by_contra hx0
    have hxne : x.val ≠ (0 : v.adicCompletion K) := fun h => hx0 (Subtype.ext h)
    have hvne : Valued.v x.val ≠ 0 :=
      (Valuation.ne_zero_iff (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)).mpr hxne
    obtain ⟨k, hk⟩ := exists_ofAdd_natCast_lt hvne
    exact absurd (hx' k) (not_le.mpr hk)
  prec' f hf := by
    classical
    have hf' : ∀ m n : ℕ, m ≤ n →
        Valued.v ((f m - f n : v.adicCompletionIntegers K)).val ≤ WithZero.exp (-(m : ℤ)) := by
      intro m n hmn
      have h := hf hmn
      simp only [Ideal.smul_eq_mul, Ideal.mul_top, SModEq.sub_mem,
        adicCompletion.mem_completionIdeal_pow K v] at h
      exact h
    have hcoe : ∀ a b : ℕ, ((f a - f b : v.adicCompletionIntegers K)).val
        = (f a).val - (f b).val := fun a b => rfl
    have hcauchy : CauchySeq (fun n => (f n).val : ℕ → v.adicCompletion K) := by
      rw [(Valued.hasBasis_uniformity (v.adicCompletion K) ℤᵐ⁰).cauchySeq_iff]
      rintro γ -
      have hγ0 : (ValueGroup₀.embedding γ.val : ℤᵐ⁰) ≠ 0 := by
        intro h0
        exact γ.ne_zero (ValueGroup₀.embedding_strictMono.injective
          (h0.trans (_root_.map_zero _).symm))
      obtain ⟨k, hk⟩ := exists_ofAdd_natCast_lt hγ0
      refine ⟨k, fun m hm n hn => ?_⟩
      have key : ∀ a b : ℕ, k ≤ a → a ≤ b →
          Valued.v ((f b).val - (f a).val) < ValueGroup₀.embedding γ.val := by
        intro a b hka hab
        have h1 : Valued.v ((f b).val - (f a).val) ≤ WithZero.exp (-(a : ℤ)) := by
          rw [Valuation.map_sub_swap, ← hcoe a b]
          exact hf' a b hab
        have h2 : WithZero.exp (-(a : ℤ)) ≤ WithZero.exp (-(k : ℤ)) := by
          rw [WithZero.exp_le_exp]
          omega
        exact lt_of_le_of_lt (h1.trans h2) hk
      change ((Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰).restrict
        ((f n).val - (f m).val)) < γ.val
      rw [Valuation.restrict_lt_iff_lt_embedding]
      rcases le_total m n with hmn | hnm
      · exact key m n hm hmn
      · rw [Valuation.map_sub_swap]
        exact key n m hn hnm
    obtain ⟨L₀, hL₀⟩ := cauchySeq_tendsto_of_complete hcauchy
    have hbound : ∀ n : ℕ, Valued.v (L₀ - (f n).val) ≤ WithZero.exp (-(n : ℤ)) := by
      intro n
      have hclosed : IsClosed {y : v.adicCompletion K |
          Valued.v (y - (f n).val) ≤ WithZero.exp (-(n : ℤ))} := by
        have hpre : {y : v.adicCompletion K |
            Valued.v (y - (f n).val) ≤ WithZero.exp (-(n : ℤ))}
              = (fun y => y - (f n).val) ⁻¹'
                {z : v.adicCompletion K | Valued.v z ≤ WithZero.exp (-(n : ℤ))} := rfl
        rw [hpre]
        exact (isClosed_setOf_valued_le K v _).preimage (continuous_sub_right ((f n).val))
      have hev : ∀ᶠ m in Filter.atTop, (f m).val ∈ {y : v.adicCompletion K |
          Valued.v (y - (f n).val) ≤ WithZero.exp (-(n : ℤ))} := by
        refine Filter.eventually_atTop.mpr ⟨n, fun m hm => ?_⟩
        have h := hf' n m hm
        rw [hcoe n m] at h
        rw [Set.mem_ofPred_eq, Valuation.map_sub_swap]
        exact h
      exact hclosed.mem_of_tendsto hL₀ hev
    have hL₀mem : L₀ ∈ v.adicCompletionIntegers K := by
      rw [mem_adicCompletionIntegers]
      have h0 : Valued.v (L₀ - (f 0).val) ≤ (1 : ℤᵐ⁰) := by
        have h := hbound 0
        simpa using h
      have h1 : Valued.v ((f 0).val) ≤ (1 : ℤᵐ⁰) := (f 0).2
      have hmax : Valued.v ((L₀ - (f 0).val) + (f 0).val) ≤ (1 : ℤᵐ⁰) :=
        Valuation.map_add_le _ h0 h1
      have hL : (L₀ - (f 0).val) + (f 0).val = L₀ := by ring
      rwa [hL] at hmax
    refine ⟨⟨L₀, hL₀mem⟩, fun n => ?_⟩
    have h : Valued.v ((f n).val - L₀) ≤ WithZero.exp (-(n : ℤ)) := by
      rw [Valuation.map_sub_swap]
      exact hbound n
    simp only [Ideal.smul_eq_mul, Ideal.mul_top, SModEq.sub_mem,
      adicCompletion.mem_completionIdeal_pow K v]
    have hsub : ((f n - (⟨L₀, hL₀mem⟩ : v.adicCompletionIntegers K) :
        v.adicCompletionIntegers K)).val = (f n).val - L₀ := rfl
    rw [hsub]
    exact h
instance

kw_ffgc_isAdicComplete_placeAdicCompletionIntegers

L783 ↗
AlgebraicCurve.Place.kw_ffgc_isAdicComplete_placeAdicCompletionIntegers
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.MonoidWithZeroHom
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Henselian
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (V : Place K F)
open scoped MazurTorsion in
Lean source · statement
instance kw_ffgc_isAdicComplete_placeAdicCompletionIntegers :
    IsAdicComplete (maximalIdeal V.adicCompletionIntegers) V.adicCompletionIntegers
theorem

mp72a103_t2_evalDepth_pow_uniformizer_mul_eq_zero

L910 ↗
Mp72a103T2.mp72a103_t2_evalDepth_pow_uniformizer_mul_eq_zero
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsLocalRing
open _root_.Polynomial
open scoped Polynomial
namespace Mp72a103T2
open _root_.Mp72a103T2
open _root_.Mp72a103T2
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a102T2
section Calculus
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mp72a103_t2_evalDepth_pow_uniformizer_mul_eq_zero (v : Place K F) :
    ∀ (m : ℕ) (z : lg37_completion v),
      AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) m
        (algebraMap v.toValuationSubring (lg37_completion v)
            v.uniformizerSubring ^ m * z) = 0
theorem

kwHgfV352_localResidueCompletion_spec

L980 ↗
AlgebraicCurve.kwHgfV352_localResidueCompletion_spec
Source context 17 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section LocalResidueCompletion
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
variable [HasCanonicalLocalResidueKStar K E]
Lean source · statement
theorem kwHgfV352_localResidueCompletion_spec (v : Place K E) (xh : v.adicCompletion)
    {x : E} (hx : algebraMap E v.adicCompletion x - xh ∈ v.adicCompletionIntegers) :
    kwHgfV352_localResidueCompletion v xh = v.localResidue x
theorem

kwHgfV352_localResidueCompletion_algebraMap

L998 ↗
AlgebraicCurve.kwHgfV352_localResidueCompletion_algebraMap
Source context 17 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section LocalResidueCompletion
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
variable [HasCanonicalLocalResidueKStar K E]
Lean source · statement
theorem kwHgfV352_localResidueCompletion_algebraMap (v : Place K E) (x : E) :
    kwHgfV352_localResidueCompletion v (algebraMap E v.adicCompletion x)
      = v.localResidue x
theorem

kwHgfV352_localResidueCompletion_eq_zero_of_mem_integers

L1004 ↗
AlgebraicCurve.kwHgfV352_localResidueCompletion_eq_zero_of_mem_integers
Source context 17 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section LocalResidueCompletion
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
variable [HasCanonicalLocalResidueKStar K E]
Lean source · statement
theorem kwHgfV352_localResidueCompletion_eq_zero_of_mem_integers (v : Place K E)
    {xh : v.adicCompletion} (hxh : xh ∈ v.adicCompletionIntegers) :
    kwHgfV352_localResidueCompletion v xh = 0
theorem

kwHgfV352_localResidueCompletion_add

L1011 ↗
AlgebraicCurve.kwHgfV352_localResidueCompletion_add
Source context 17 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.IsDedekindDomain
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section LocalResidueCompletion
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
variable [HasCanonicalLocalResidueKStar K E]
Lean source · statement
theorem kwHgfV352_localResidueCompletion_add (v : Place K E)
    (xh yh : v.adicCompletion) :
    kwHgfV352_localResidueCompletion v (xh + yh)
      = kwHgfV352_localResidueCompletion v xh
        + kwHgfV352_localResidueCompletion v yh
theorem

mem_adicIntegersKSubmod_iff

L1101 ↗
ModularCurve.KwF4gRRTate.mem_adicIntegersKSubmod_iff
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1104 ↗
ModularCurve.KwF4gRRTate.tateProj_mem_integers
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1111 ↗
ModularCurve.KwF4gRRTate.tateProj_of_mem
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1119 ↗
ModularCurve.KwF4gRRTate.tateProj_idem
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1124 ↗
ModularCurve.KwF4gRRTate.range_tateProj
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1186 ↗
ModularCurve.KwF4gRRTate.poleWindowKSubmod
Documentation

The space of completion elements with poles bounded by the given uniformizer power.

Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1198 ↗
ModularCurve.KwF4gRRTate.mem_poleWindowKSubmod_iff
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1203 ↗
ModularCurve.KwF4gRRTate.adicIntegersKSubmod_le_poleWindowKSubmod
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1207 ↗
ModularCurve.KwF4gRRTate.kwF4gRRTate_clearPole
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1234 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTatePoleWindowFinite
Documentation

Finite dimensionality of each bounded pole space modulo integral completion elements.

Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1274 ↗
IsDedekindDomain.HeightOneSpectrum.adicCompletion.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
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open scoped WithZero Multiplicative Topology
open _root_.Filter
namespace IsDedekindDomain
open _root_.IsDedekindDomain
namespace HeightOneSpectrum
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsDedekindDomain
variable {A : Type*} (K : Type*) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K]
    [IsDedekindDomain A] (v : HeightOneSpectrum A)
namespace adicCompletion
open _root_.IsDedekindDomain.HeightOneSpectrum.adicCompletion
open _root_.IsDedekindDomain.HeightOneSpectrum.adicCompletion
local notation "vK" => (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)
Lean source · statement
theorem isOpen_setOf_valued_le {γ : ℤᵐ⁰} (hγ : γ ≠ 0) :
    IsOpen {y : v.adicCompletion K | Valued.v y ≤ γ}
theorem

kwF4R1V410a_factorPow_evalₐ

L1328 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_factorPow_evalₐ
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V410a
open _root_.ModularCurve
Lean source · statement
theorem kwF4R1V410a_factorPow_evalₐ {R : Type*} [CommRing R] {I : Ideal R}
    {m n : ℕ} (hle : m ≤ n) (z : AdicCompletion I R) :
    Ideal.Quotient.factorPow I hle (AdicCompletion.evalₐ I n z)
      = AdicCompletion.evalₐ I m z
instance

kwF4R1V410a_subsingletonHeightOneSpectrumDVR

L1338 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_subsingletonHeightOneSpectrumDVR
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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

L1354 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_algebraMap_mem_completionIdeal_pow_iff
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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

L1365 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_exists_sub_mem_completionIdeal_pow
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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

L1407 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_quotientEquiv
Documentation

The equivalence of valuation-ring and completed valuation-ring quotients at the specified depth.

Source context 25 commands

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

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

kwF4R1V410a_quotientEquiv_mk

L1424 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_quotientEquiv_mk
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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_quotientEquiv_mk (n : ℕ) (x : O_w) :
    kwF4R1V410a_quotientEquiv w n (Ideal.Quotient.mk _ x)
      = Ideal.Quotient.mk _ (algebraMap (O_w) (O_W) x)
theorem

kwF4R1V410a_quotientEquiv_factorPow

L1428 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_quotientEquiv_factorPow
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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_quotientEquiv_factorPow {m n : ℕ} (hle : m ≤ n)
    (z : (O_w) ⧸ (𝔪_w) ^ n) :
    Ideal.Quotient.factorPow (𝔪_W) hle (kwF4R1V410a_quotientEquiv w n z)
      = kwF4R1V410a_quotientEquiv w m (Ideal.Quotient.factorPow (𝔪_w) hle z)
def

kwF4R1V410a_forwardFamily

L1438 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_forwardFamily
Documentation

The compatible quotient-level map from the adic completion to completed valuation-ring quotients.

Source context 25 commands

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

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

kwF4R1V410a_forwardFamily_compat

L1443 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_forwardFamily_compat
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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_forwardFamily_compat {m n : ℕ} (hle : m ≤ n) :
    (Ideal.Quotient.factorPow (𝔪_W) hle).comp (kwF4R1V410a_forwardFamily w n)
      = kwF4R1V410a_forwardFamily w m
def

kwF4R1V410a_forward

L1454 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_forward
Documentation

The map from the adic completion to the completed valuation ring induced by its quotient maps.

Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V410a
open _root_.ModularCurve
section Bridge
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
local notation "O_w" => w.toValuationSubring
local notation "𝔪_w" => IsLocalRing.maximalIdeal w.toValuationSubring
local notation "O_W" => w.adicCompletionIntegers
local notation "𝔪_W" => w.heightOneSpectrum.completionIdeal F
Lean source · statement
def kwF4R1V410a_forward : lg37_completion w →+* (O_W)
theorem

kwF4R1V410a_mk_forward

L1459 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_mk_forward
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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_mk_forward (n : ℕ) (z : lg37_completion w) :
    Ideal.Quotient.mk ((𝔪_W)^n) (kwF4R1V410a_forward w z)
      = kwF4R1V410a_quotientEquiv w n (AdicCompletion.evalₐ (𝔪_w) n z)
def

kwF4R1V410a_backwardFamily

L1468 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_backwardFamily
Documentation

The quotient-level inverse maps from the completed valuation ring to valuation-ring quotients.

Source context 25 commands

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

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

kwF4R1V410a_backwardFamily_compat

L1472 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_backwardFamily_compat
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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_backwardFamily_compat {m n : ℕ} (hle : m ≤ n) :
    (Ideal.Quotient.factorPow (𝔪_w) hle).comp (kwF4R1V410a_backwardFamily w n)
      = kwF4R1V410a_backwardFamily w m
def

kwF4R1V410a_backward

L1484 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_backward
Documentation

The inverse completion map induced by the compatible valuation-ring quotient maps.

Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V410a
open _root_.ModularCurve
section Bridge
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
local notation "O_w" => w.toValuationSubring
local notation "𝔪_w" => IsLocalRing.maximalIdeal w.toValuationSubring
local notation "O_W" => w.adicCompletionIntegers
local notation "𝔪_W" => w.heightOneSpectrum.completionIdeal F
Lean source · statement
def kwF4R1V410a_backward : (O_W) →+* lg37_completion w
theorem

kwF4R1V410a_evalₐ_backward

L1488 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_evalₐ_backward
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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_evalₐ_backward (n : ℕ) (y : O_W) :
    AdicCompletion.evalₐ (𝔪_w) n (kwF4R1V410a_backward w y)
      = (kwF4R1V410a_quotientEquiv w n).symm (Ideal.Quotient.mk ((𝔪_W)^n) y)
theorem

kwF4R1V410a_forward_backward

L1494 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_forward_backward
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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_forward_backward :
    (kwF4R1V410a_forward w).comp (kwF4R1V410a_backward w) = RingHom.id _
theorem

kwF4R1V410a_backward_forward

L1503 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_backward_forward
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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_backward_forward :
    (kwF4R1V410a_backward w).comp (kwF4R1V410a_forward w) = RingHom.id _
def

kwF4R1V410a_ringEquiv

L1510 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_ringEquiv
Documentation

The ring equivalence between the adic completion and the completed valuation ring.

Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V410a
open _root_.ModularCurve
section Bridge
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
local notation "O_w" => w.toValuationSubring
local notation "𝔪_w" => IsLocalRing.maximalIdeal w.toValuationSubring
local notation "O_W" => w.adicCompletionIntegers
local notation "𝔪_W" => w.heightOneSpectrum.completionIdeal F
Lean source · statement
def kwF4R1V410a_ringEquiv : lg37_completion w ≃+* (O_W)
theorem

kwF4R1V410a_ringEquiv_apply

L1514 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_ringEquiv_apply
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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_ringEquiv_apply (z : lg37_completion w) :
    kwF4R1V410a_ringEquiv w z = kwF4R1V410a_forward w z
theorem

kwF4R1V410a_ringEquiv_of

L1517 ↗
ModularCurve.KwF4R1V410a.kwF4R1V410a_ringEquiv_of
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.IsLocalRing
open _root_.WithZero
open _root_.ModularCurve.Lg37
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_ringEquiv_of (x : O_w) :
    kwF4R1V410a_ringEquiv w (algebraMap (O_w) (lg37_completion w) x)
      = algebraMap (O_w) (O_W) x
theorem

coe_smul_K

L1565 ↗
ModularCurve.KwF4gRRTate.coe_smul_K
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1571 ↗
ModularCurve.KwF4gRRTate.poleWindowShift
Documentation

The linear map clearing a bounded pole by the specified uniformizer power.

Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1582 ↗
ModularCurve.KwF4gRRTate.poleWindowShift_injective
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1597 ↗
ModularCurve.KwF4gRRTate.poleWindowShift_surjective
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1611 ↗
ModularCurve.KwF4gRRTate.poleWindowShiftEquiv
Documentation

The linear equivalence obtained by clearing a bounded pole.

Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1617 ↗
ModularCurve.KwF4gRRTate.piPowKSubmod
Documentation

The subspace of integral completion elements divisible by the uniformizer power.

Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1626 ↗
ModularCurve.KwF4gRRTate.poleWindowShift_image_integers
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1642 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTateDVRQuotPowKFinite
Documentation

Finite dimensionality of integral completion quotients by uniformizer powers.

Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1647 ↗
ModularCurve.KwF4gRRTate.kwF4gRRTate_poleWindowFinite_of_DVRQuotPowKFinite
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1693 ↗
ModularCurve.KwF4gRRTate.principalPart_mul_zero_of_mem_integers
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1699 ↗
ModularCurve.KwF4gRRTate.tateCommRestrict_single_term
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1748 ↗
ModularCurve.KwF4gRRTate.range_comp_map_left
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1753 ↗
ModularCurve.KwF4gRRTate.finrankTrace_comp_comm
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1803 ↗
ModularCurve.KwF4gRRTate.SameRangeIdemProjectors
Documentation

Two idempotent linear projectors with the same range.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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
  /-- Idempotence of the first projector. -/
  idem_pA : ∀ x, pA (pA x) = pA x
  /-- Idempotence of the second projector. -/
  idem_pA' : ∀ x, pA' (pA' x) = pA' x
  /-- Equality of the two projector ranges. -/
  range_eq : LinearMap.range pA = LinearMap.range pA'
theorem

pA_fixes_range

L1813 ↗
ModularCurve.KwF4gRRTate.pA_fixes_range
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1817 ↗
ModularCurve.KwF4gRRTate.pA'_fixes_range
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1824 ↗
ModularCurve.KwF4gRRTate.delta_zero_on_range
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1829 ↗
ModularCurve.KwF4gRRTate.delta_range_subset
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1842 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTateProjectorIndep
Documentation

Independence of the Tate commutator trace from a projector with the same range.

Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1860 ↗
ModularCurve.KwF4gRRTate.tateCommRestrict_diff
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L1940 ↗
ModularCurve.KwF4gRRTate.finrankTrace_eq_trace_on_superspace
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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) :
    haveI : 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

L1965 ↗
ModularCurve.KwF4gRRTate.finrankTrace_sub_eq
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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 ψ)] :
    haveI : 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

L2027 ↗
ModularCurve.KwF4gRRTate.piPowKSubmod_eq_restrictScalars
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2036 ↗
ModularCurve.KwF4gRRTate.quotPiPowEquivIdealQuot
Documentation

The linear equivalence identifying divisibility by a uniformizer power with its principal ideal.

Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2044 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTateDVRCotangentKFinite
Documentation

Finite dimensionality of the integral completion quotient by an irreducible element.

Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2049 ↗
ModularCurve.KwF4gRRTate.range_mulLeft_eq_restrictScalars_span
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2058 ↗
ModularCurve.KwF4gRRTate.finiteDimensional_restrictScalarsQuot_pow
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2120 ↗
ModularCurve.KwF4gRRTate.finiteDimensional_idealQuot_pow
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2128 ↗
ModularCurve.KwF4gRRTate.kwF4gRRTate_DVRQuotPowKFinite_of_cotangent
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2171 ↗
ModularCurve.KwF4gRRTate.instIsScalarTower_K_toValuationSubring_adicCompletionIntegers
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2180 ↗
ModularCurve.KwF4gRRTate.span_irreducible_eq_completionIdeal_pow_one
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2188 ↗
ModularCurve.KwF4gRRTate.quotientEquivKAlg
Documentation

The base-field algebra equivalence between valuation-ring and completed valuation-ring quotients.

Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2204 ↗
ModularCurve.KwF4gRRTate.quotSpanIrreducibleEquivResidueField
Documentation

The residue-field identification of the integral completion quotient by an irreducible element.

Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2213 ↗
ModularCurve.KwF4gRRTate.kwF4gRRTate_DVRCotangentKFinite
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2253 ↗
ModularCurve.KwF4gRRTate.deltaQuotFactor
Documentation

The difference of the two projectors factored through their common-range quotient.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2261 ↗
ModularCurve.KwF4gRRTate.deltaQuotFactor_apply
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2273 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTatePoleWindowImageFinite
Documentation

Finite dimensionality of the principal-part image of integral completion elements after multiplication.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2286 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTateCommFiniteGen
Documentation

Finite dimensionality of all commutator ranges for a projector sharing the integral range.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2324 ↗
ModularCurve.KwF4gRRTate.kwF4gRRTate_poleWindowFinite
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2335 ↗
ModularCurve.KwF4gRRTate.lmul_adicIntegers_subset_poleWindow
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2353 ↗
ModularCurve.KwF4gRRTate.kwF4gRRTate_poleWindowImageFinite
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2410 ↗
ModularCurve.KwF4gRRTate.ker_pA'_inf_integers
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2420 ↗
ModularCurve.KwF4gRRTate.finiteDimensional_ker_pA'_inf_poleWindow
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2453 ↗
ModularCurve.KwF4gRRTate.finiteDimensional_principalPart_pA'_range
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2478 ↗
ModularCurve.KwF4gRRTate.kwF4gRRTate_commFiniteGen
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2550 ↗
ModularCurve.KwF4gRRTate.finrankTrace_congr
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2556 ↗
ModularCurve.KwF4gRRTate.range_sub_le
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2562 ↗
ModularCurve.KwF4gRRTate.instFinDimRangeSub
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2571 ↗
ModularCurve.KwF4gRRTate.finrankTrace_sub
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2590 ↗
ModularCurve.KwF4gRRTate.range_conj_eq_map
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2595 ↗
ModularCurve.KwF4gRRTate.finrankTrace_conj
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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 φ)] :
    haveI : 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

L2627 ↗
ModularCurve.KwF4gRRTate.alphaMap
Documentation

Multiplication followed by projection to the quotient of the Tate projector range.

Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2631 ↗
ModularCurve.KwF4gRRTate.alphaMap_apply
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2635 ↗
ModularCurve.KwF4gRRTate.mulOnRange
Documentation

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

Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2644 ↗
ModularCurve.KwF4gRRTate.mulOnRange_apply
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2650 ↗
ModularCurve.KwF4gRRTate.finiteDimensional_range_alphaMap
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2682 ↗
ModularCurve.KwF4gRRTate.instFinDimRangeDeltaAlpha
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2689 ↗
ModularCurve.KwF4gRRTate.instFinDimRangeMulDeltaAlpha
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2697 ↗
ModularCurve.KwF4gRRTate.finrankTrace_term_eq
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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

L2738 ↗
ModularCurve.KwF4gRRTate.kwF4gRRTate_projectorIndep
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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
def

KwF4gRRTateCohenTateAgreement

L2844 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTateCohenTateAgreement
Documentation

Agreement between the Cohen projector commutator trace and the completed local residue trace.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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 CohenMint
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
Lean source · statement
def KwF4gRRTateCohenTateAgreement : Prop
theorem

kwF4gRRTate_agreement_of_cohenTateAgreement

L2863 ↗
ModularCurve.KwF4gRRTate.kwF4gRRTate_agreement_of_cohenTateAgreement
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.ModularCurve.KwF4gRRTate
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve
section Reprice
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
variable [∀ u : Place K L, u.FiniteResidue]
Lean source · statement
theorem kwF4gRRTate_agreement_of_cohenTateAgreement
    (hfin : KwF4gRRTateCommFinite K L)
    (hCTA : KwF4gRRTateCohenTateAgreement K L) :
    KwF4gRRTateAgreement K L hfin
structure

TateCohenKernelData

L2917 ↗
ModularCurve.KwF4gRRTate.TateCohenKernelData
Documentation

A Cohen projector and residue-field lift realizing the completed residue commutator.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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 CohenKernelData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
Lean source · full declaration
structure TateCohenKernelData (u : Place K L) [u.FiniteResidue] where
  /-- The Cohen projector onto integral completion elements. -/
  pC : u.adicCompletion →ₗ[K] u.adicCompletion
  /-- Idempotence of the Cohen projector. -/
  pC_idem : ∀ x, pC (pC x) = pC x
  /-- Its range agrees with the Tate projector range. -/
  range_pC : LinearMap.range (tateProj u) = LinearMap.range pC
  /-- The residue-field lift into the Cohen projector range. -/
  liftκ : u.ResidueField →ₗ[K] LinearMap.range pC
  /-- Injectivity of the residue-field lift. -/
  liftκ_inj : Function.Injective liftκ
  /-- The uniformizer commutator takes values in the residue-field lift range. -/
  tateComm_mem_range_liftκ : ∀ (fh : u.adicCompletion) (a : LinearMap.range pC),
    tateCommRestrict pC (lmulK u fh)
      (lmulK u (algebraMap L u.adicCompletion u.uniformizer)) a ∈ LinearMap.range liftκ
  /-- The uniformizer commutator on lifted residues is multiplication by the completed local
  residue. -/
  tateComm_liftκ : ∀ (fh : u.adicCompletion) (c : u.ResidueField),
    tateCommRestrict pC (lmulK u fh)
      (lmulK u (algebraMap L u.adicCompletion u.uniformizer)) (liftκ c)
      = liftκ (kwHgfV352_localResidueCompletion u fh * c)
theorem

sameRangeIdemProjectors_of_kernelData

L2941 ↗
ModularCurve.KwF4gRRTate.sameRangeIdemProjectors_of_kernelData
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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 CohenKernelData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
variable {u : Place K L} [u.FiniteResidue]
Lean source · full declaration
theorem sameRangeIdemProjectors_of_kernelData (D : TateCohenKernelData u) :
    SameRangeIdemProjectors (tateProj u) D.pC where
  idem_pA x := congrFun (congrArg DFunLike.coe (tateProj_idem u)) x
  idem_pA' := D.pC_idem
  range_eq := D.range_pC
theorem

tateCommTrace_of_kernelData

L2955 ↗
ModularCurve.KwF4gRRTate.tateCommTrace_of_kernelData
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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 TraceComputation
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
variable {u : Place K L} [u.FiniteResidue]
Lean source · statement
theorem tateCommTrace_of_kernelData (D : TateCohenKernelData u) (fh : u.adicCompletion)
    [FiniteDimensional K (LinearMap.range
      (tateCommRestrict D.pC (lmulK u fh)
        (lmulK u (algebraMap L u.adicCompletion u.uniformizer))))] :
    tateCommTrace D.pC (lmulK u fh)
        (lmulK u (algebraMap L u.adicCompletion u.uniformizer))
      = Algebra.trace K u.ResidueField (kwHgfV352_localResidueCompletion u fh)
def

KwF4gRRTateCohenKernelDataExists

L3009 ↗
ModularCurve.KwF4gRRTate.KwF4gRRTateCohenKernelDataExists
Documentation

Existence of Cohen kernel data at every place with finite residue field.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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]
variable [HasCanonicalLocalResidueKStar K L]
Lean source · statement
def KwF4gRRTateCohenKernelDataExists : Prop
theorem

kwF4gRRTate_cohenTateAgreement_of_kernelData

L3019 ↗
ModularCurve.KwF4gRRTate.kwF4gRRTate_cohenTateAgreement_of_kernelData
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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 [HasCanonicalLocalResidueKStar K L]
Lean source · statement
theorem kwF4gRRTate_cohenTateAgreement_of_kernelData
    (hD : KwF4gRRTateCohenKernelDataExists K L) :
    KwF4gRRTateCohenTateAgreement K L
theorem

kwF4gRRTate_agreement_of_kernelData

L3027 ↗
ModularCurve.KwF4gRRTate.kwF4gRRTate_agreement_of_kernelData
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
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 [HasCanonicalLocalResidueKStar K L]
Lean source · statement
theorem kwF4gRRTate_agreement_of_kernelData
    [∀ u : Place K L, u.FiniteResidue]
    (hfin : KwF4gRRTateCommFinite K L)
    (hD : KwF4gRRTateCohenKernelDataExists K L) :
    KwF4gRRTateAgreement K L hfin
theorem

kwF4R1V394a_localResidueCompletion_smul

L3073 ↗
ModularCurve.KwF4R1V394a.kwF4R1V394a_localResidueCompletion_smul
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.FunctionField
open _root_.KaehlerDifferential
open ModularCurve.GF24a9RRDx
open _root_.ModularCurve.KwF4R1V391a
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwF4R1V394a
open _root_.ModularCurve
section LinearWrappers
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]
variable [Algebra.IsIntegral E F]
variable [HasCanonicalLocalResidueKStar K E] [HasCanonicalLocalResidueKStar K F]
variable [HasPrincipalDivisors K E] [HasPrincipalDivisors K F] [FiniteDimensional E F]
variable [Nontrivial Ω[E⁄K]]
omit [HasPrincipalDivisors K E] [Nontrivial Ω[E⁄K]] in
Lean source · statement
theorem kwF4R1V394a_localResidueCompletion_smul
    (v : Place K E) (c : K) (xh : v.adicCompletion) :
    kwHgfV352_localResidueCompletion v (c • xh)
      = c • kwHgfV352_localResidueCompletion v xh
def

cohenSectionHat

L3169 ↗
ModularCurve.KwTateRR3.cohenSectionHat
Documentation

The residue-field section transported into the valuation completion.

Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenSectionHat
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · full declaration
def cohenSectionHat (u : Place K L) (S : Lg37CompletionSection u) :
    u.ResidueField →ₐ[K] u.adicCompletion where
  toRingHom :=
    (u.adicCompletionIntegers.subtype).comp
      ((kwF4R1V410a_ringEquiv u).toRingHom.comp S.lift.toRingHom)
  commutes' c := by
    change ((kwF4R1V410a_ringEquiv u (S.lift (algebraMap K u.ResidueField c))
        : u.adicCompletionIntegers) : u.adicCompletion)
      = algebraMap K u.adicCompletion c
    rw [S.lift.commutes c,
      IsScalarTower.algebraMap_apply K u.toValuationSubring (lg37_completion u) c,
      kwF4R1V410a_ringEquiv_of u,
      IsScalarTower.algebraMap_apply K L u.adicCompletion c]
    rfl
theorem

cohenSectionHat_apply

L3184 ↗
ModularCurve.KwTateRR3.cohenSectionHat_apply
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenSectionHat
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem cohenSectionHat_apply (u : Place K L) (S : Lg37CompletionSection u)
    (a : u.ResidueField) :
    cohenSectionHat u S a
      = ((kwF4R1V410a_ringEquiv u (S.lift a) : u.adicCompletionIntegers)
          : u.adicCompletion)
theorem

cohenSectionHat_mem_integers

L3190 ↗
ModularCurve.KwTateRR3.cohenSectionHat_mem_integers
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenSectionHat
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem cohenSectionHat_mem_integers (u : Place K L) (S : Lg37CompletionSection u)
    (a : u.ResidueField) :
    cohenSectionHat u S a ∈ u.adicCompletionIntegers
theorem

cohenSectionHat_mem_adicIntegersKSubmod

L3195 ↗
ModularCurve.KwTateRR3.cohenSectionHat_mem_adicIntegersKSubmod
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenSectionHat
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem cohenSectionHat_mem_adicIntegersKSubmod (u : Place K L)
    (S : Lg37CompletionSection u) (a : u.ResidueField) :
    cohenSectionHat u S a ∈ adicIntegersKSubmod u
theorem

cohenSectionHat_injective

L3200 ↗
ModularCurve.KwTateRR3.cohenSectionHat_injective
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenSectionHat
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem cohenSectionHat_injective (u : Place K L) (S : Lg37CompletionSection u) :
    Function.Injective (cohenSectionHat u S)
def

cohenProjC

L3211 ↗
ModularCurve.KwTateRR3.cohenProjC
Documentation

Projection onto integral completion elements along the chosen complementary subspace.

Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenProjC
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
def cohenProjC (B : Submodule K u.adicCompletion)
    (hcompl : IsCompl (adicIntegersKSubmod u) B) :
    u.adicCompletion →ₗ[K] u.adicCompletion
theorem

cohenProjC_mem_integers

L3216 ↗
ModularCurve.KwTateRR3.cohenProjC_mem_integers
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenProjC
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem cohenProjC_mem_integers (B : Submodule K u.adicCompletion)
    (hcompl : IsCompl (adicIntegersKSubmod u) B) (x : u.adicCompletion) :
    cohenProjC u B hcompl x ∈ u.adicCompletionIntegers
theorem

cohenProjC_of_mem

L3221 ↗
ModularCurve.KwTateRR3.cohenProjC_of_mem
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenProjC
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem cohenProjC_of_mem (B : Submodule K u.adicCompletion)
    (hcompl : IsCompl (adicIntegersKSubmod u) B) {x : u.adicCompletion}
    (hx : x ∈ u.adicCompletionIntegers) :
    cohenProjC u B hcompl x = x
theorem

cohenProjC_of_mem_B

L3227 ↗
ModularCurve.KwTateRR3.cohenProjC_of_mem_B
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenProjC
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem cohenProjC_of_mem_B (B : Submodule K u.adicCompletion)
    (hcompl : IsCompl (adicIntegersKSubmod u) B) {x : u.adicCompletion}
    (hx : x ∈ B) :
    cohenProjC u B hcompl x = 0
theorem

cohenProjC_idem

L3233 ↗
ModularCurve.KwTateRR3.cohenProjC_idem
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenProjC
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem cohenProjC_idem (B : Submodule K u.adicCompletion)
    (hcompl : IsCompl (adicIntegersKSubmod u) B) (x : u.adicCompletion) :
    cohenProjC u B hcompl (cohenProjC u B hcompl x) = cohenProjC u B hcompl x
theorem

range_cohenProjC

L3238 ↗
ModularCurve.KwTateRR3.range_cohenProjC
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenProjC
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem range_cohenProjC (B : Submodule K u.adicCompletion)
    (hcompl : IsCompl (adicIntegersKSubmod u) B) :
    LinearMap.range (cohenProjC u B hcompl) = adicIntegersKSubmod u
theorem

sub_cohenProjC_mem_B

L3244 ↗
ModularCurve.KwTateRR3.sub_cohenProjC_mem_B
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenProjC
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem sub_cohenProjC_mem_B (B : Submodule K u.adicCompletion)
    (hcompl : IsCompl (adicIntegersKSubmod u) B) (x : u.adicCompletion) :
    x - cohenProjC u B hcompl x ∈ B
theorem

cohenTateCommRestrict_single_term

L3262 ↗
ModularCurve.KwTateRR3.cohenTateCommRestrict_single_term
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section SingleTerm
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (B : Submodule K u.adicCompletion) (hcompl : IsCompl (adicIntegersKSubmod u) B)
Lean source · statement
theorem cohenTateCommRestrict_single_term (fh : u.adicCompletion)
    (a : LinearMap.range (cohenProjC u B hcompl)) :
    (tateCommRestrict (cohenProjC u B hcompl) (lmulK u fh)
        (lmulK u (algebraMap L u.adicCompletion u.uniformizer)) a
      : u.adicCompletion)
    = cohenProjC u B hcompl
        (algebraMap L u.adicCompletion u.uniformizer
          * (fh * (a : u.adicCompletion)
              - cohenProjC u B hcompl (fh * (a : u.adicCompletion))))
structure

KwTateRR3CohenLaurentSpec

L3297 ↗
ModularCurve.KwTateRR3.KwTateRR3CohenLaurentSpec
Documentation

A Cohen section and Laurent complement with a compatible principal-part residue map.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenLaurentSpec
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
Lean source · full declaration
structure KwTateRR3CohenLaurentSpec (u : Place K L) [u.FiniteResidue] where
  /-- The chosen section from the residue field into the adic completion. -/
  S : Lg37CompletionSection u
  /-- The complementary subspace of Laurent principal parts. -/
  B : Submodule K u.adicCompletion
  /-- The Laurent subspace complements integral completion elements. -/
  hcompl : IsCompl (adicIntegersKSubmod u) B
  /-- The leading residue coefficient on the complementary subspace. -/
  ε : B →ₗ[K] u.ResidueField
  /-- Uniformizer multiplication preserves the complement after removing the lifted residue. -/
  shift_sub_mem : ∀ z : B,
    algebraMap L u.adicCompletion u.uniformizer * (z : u.adicCompletion)
      - cohenSectionHat u S (ε z) ∈ B
  /-- The residue coefficient of a multiplied lifted residue agrees with the completed local
  residue. -/
  ε_principalPart_mul_sectionHat : ∀ (fh : u.adicCompletion) (c : u.ResidueField),
    ε ⟨fh * cohenSectionHat u S c
          - cohenProjC u B hcompl (fh * cohenSectionHat u S c),
        sub_cohenProjC_mem_B u B hcompl _⟩
      = kwHgfV352_localResidueCompletion u fh * c
theorem

cohenProjC_uniformizer_mul_of_mem_B

L3320 ↗
ModularCurve.KwTateRR3.cohenProjC_uniformizer_mul_of_mem_B
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenLaurentSpec
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
variable {u : Place K L} [u.FiniteResidue] (D : KwTateRR3CohenLaurentSpec u)
Lean source · statement
theorem cohenProjC_uniformizer_mul_of_mem_B {x : u.adicCompletion} (hx : x ∈ D.B) :
    cohenProjC u D.B D.hcompl
        (algebraMap L u.adicCompletion u.uniformizer * x)
      = cohenSectionHat u D.S (D.ε ⟨x, hx⟩)
def

cohenLiftκ

L3341 ↗
ModularCurve.KwTateRR3.cohenLiftκ
Documentation

The residue-field lift into the integral range of the Cohen projector.

Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Construct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
variable {u : Place K L} [u.FiniteResidue]
Lean source · full declaration
def cohenLiftκ (D : KwTateRR3CohenLaurentSpec u) :
    u.ResidueField →ₗ[K] LinearMap.range (cohenProjC u D.B D.hcompl) where
  toFun c := ⟨cohenSectionHat u D.S c,
    (range_cohenProjC u D.B D.hcompl).symm ▸
      cohenSectionHat_mem_adicIntegersKSubmod u D.S c⟩
  map_add' a b := Subtype.ext (map_add _ a b)
  map_smul' r a := Subtype.ext ((cohenSectionHat u D.S).toLinearMap.map_smul r a)
theorem

cohenLiftκ_coe

L3349 ↗
ModularCurve.KwTateRR3.cohenLiftκ_coe
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Construct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
variable {u : Place K L} [u.FiniteResidue]
Lean source · statement
theorem cohenLiftκ_coe (D : KwTateRR3CohenLaurentSpec u) (c : u.ResidueField) :
    ((cohenLiftκ D c : LinearMap.range (cohenProjC u D.B D.hcompl)) : u.adicCompletion)
      = cohenSectionHat u D.S c
theorem

cohenLiftκ_injective

L3353 ↗
ModularCurve.KwTateRR3.cohenLiftκ_injective
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Construct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
variable {u : Place K L} [u.FiniteResidue]
Lean source · statement
theorem cohenLiftκ_injective (D : KwTateRR3CohenLaurentSpec u) :
    Function.Injective (cohenLiftκ D)
def

tateCohenKernelData_of_cohenLaurentSpec

L3362 ↗
ModularCurve.KwTateRR3.tateCohenKernelData_of_cohenLaurentSpec
Documentation

The Cohen kernel data supplied by a compatible Laurent specification.

Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Construct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
variable {u : Place K L} [u.FiniteResidue]
Lean source · full declaration
def tateCohenKernelData_of_cohenLaurentSpec (D : KwTateRR3CohenLaurentSpec u) :
    TateCohenKernelData u where
  pC := cohenProjC u D.B D.hcompl
  pC_idem := cohenProjC_idem u D.B D.hcompl
  range_pC := (range_tateProj u).trans (range_cohenProjC u D.B D.hcompl).symm
  liftκ := cohenLiftκ D
  liftκ_inj := cohenLiftκ_injective D
  tateComm_mem_range_liftκ fh a := by
    have hmem := sub_cohenProjC_mem_B u D.B D.hcompl (fh * (a : u.adicCompletion))
    refine ⟨D.ε ⟨_, hmem⟩, ?_⟩
    apply Subtype.ext
    rw [cohenLiftκ_coe, cohenTateCommRestrict_single_term u D.B D.hcompl fh a,
      cohenProjC_uniformizer_mul_of_mem_B D hmem]
  tateComm_liftκ fh c := by
    apply Subtype.ext
    have hmem := sub_cohenProjC_mem_B u D.B D.hcompl (fh * cohenSectionHat u D.S c)
    rw [cohenLiftκ_coe, cohenTateCommRestrict_single_term u D.B D.hcompl fh (cohenLiftκ D c),
      cohenLiftκ_coe, cohenProjC_uniformizer_mul_of_mem_B D hmem]
    congr 1
    exact D.ε_principalPart_mul_sectionHat fh c
def

KwTateRR3CohenLaurentSpecExists

L3391 ↗
ModularCurve.KwTateRR3.KwTateRR3CohenLaurentSpecExists
Documentation

Existence of a compatible Cohen Laurent specification at every place.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Mint
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
Lean source · statement
def KwTateRR3CohenLaurentSpecExists : Prop
theorem

kwTateRR3_cohenKernelDataExists_of_cohenLaurentSpec

L3401 ↗
ModularCurve.KwTateRR3.kwTateRR3_cohenKernelDataExists_of_cohenLaurentSpec
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Headline
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
Lean source · statement
theorem kwTateRR3_cohenKernelDataExists_of_cohenLaurentSpec
    (hD : KwTateRR3CohenLaurentSpecExists K L) :
    KwF4gRRTateCohenKernelDataExists K L
theorem

aCoeff_sub

L3438 ↗
ModularCurve.KwNo6HrouteR.aCoeff_sub
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.Polynomial
open _root_.IsLocalRing
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.KwNo6Section
open _root_.ModularCurve.Mp72a102T3
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwNo6HrouteR
open _root_.ModularCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem aCoeff_sub (v : Place K F) (S : Lg37CompletionSection v) (m : ℕ)
    (x y : lg37_completion v) :
    aCoeff v S m (x - y) = aCoeff v S m x - aCoeff v S m y
theorem

aCoeff_uniformizerHat_pow_mul_eq_zero_of_lt

L3443 ↗
ModularCurve.KwNo6HrouteR.aCoeff_uniformizerHat_pow_mul_eq_zero_of_lt
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.Polynomial
open _root_.IsLocalRing
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.KwNo6Section
open _root_.ModularCurve.Mp72a102T3
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwNo6HrouteR
open _root_.ModularCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem aCoeff_uniformizerHat_pow_mul_eq_zero_of_lt (v : Place K F)
    (S : Lg37CompletionSection v) {k m : ℕ} (hk : k < m)
    (x : lg37_completion v) :
    aCoeff v S k ((algebraMap v.toValuationSubring (lg37_completion v)
      v.uniformizerSubring) ^ m * x) = 0
theorem

taylor_choose_eq_aCoeff

L3459 ↗
ModularCurve.KwNo6HrouteR.taylor_choose_eq_aCoeff
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.Polynomial
open _root_.IsLocalRing
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.KwNo6Section
open _root_.ModularCurve.Mp72a102T3
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwNo6HrouteR
open _root_.ModularCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem taylor_choose_eq_aCoeff (v : Place K F) (S : Lg37CompletionSection v)
    (n : ℕ) (x : lg37_completion v) {k : ℕ} (hk : k < n) :
    Classical.choose (mp72a102_t3_sigma_taylor_expansion v S n x) k = aCoeff v S k x
theorem

exists_approximant

L3530 ↗
ModularCurve.KwNo6HrouteR.exists_approximant
Source context 21 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.Polynomial
open _root_.IsLocalRing
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.KwNo6Section
open _root_.ModularCurve.Mp72a102T3
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwNo6HrouteR
open _root_.ModularCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_approximant (v : Place K F) (S : Lg37CompletionSection v)
    (a : v.ResidueField) (M : ℕ) :
    ∃ ℓ : v.toValuationSubring, IsLocalRing.residue _ ℓ = a
      ∧ ∀ k, 1 ≤ k → k ≤ M →
        aCoeff v S k (algebraMap v.toValuationSubring (lg37_completion v) ℓ) = 0
theorem

kwHgf_v277_aCoeff_section_lift_mul

L3651 ↗
ModularCurve.KwOdaDHDR.kwHgf_v277_aCoeff_section_lift_mul
Source context 68 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open scoped PadicInt AlgebraicGeometry
open _root_.BigOperators
open _root_.CategoryTheory
open _root_.AlgebraicCurve
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.ModularCurve
open _root_.Order
open _root_.Topology
open FLT.HopfSpec GoodReductionJacobian
open Deformation.PDivisible Deformation.ModpDieudonne
open _root_.AlgebraicCurve
open _root_.Module
open _root_.CongruenceSubgroup
open NeronOggShafarevich
open AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine
open _root_.AlgebraicCurve.RationalFunctionField
open scoped TensorProduct
open _root_.IntermediateField
open _root_.AlgebraicCurve.RationalFunctionField
open ModularCurve.KwNo6HrouteV
open ModularCurve.KwNo6HrouteY
open ModularCurve.KwNo6HrouteZ
open ModularCurve.GF24a9RRDx
open ModularCurve.GF24a12CohenSupply
open Ldgr30BankGate
open Modularity.Ldgr27TraceSemilinearSlice
open Ldgr24DefectKernelSlice
open Ldgr23CohenDefectCorrectionSlice
open ModularCurve.Ldgr25PlaceExtensionSlice
open Ldgr25CorrectedChoiceSlice
open Modularity.Ldgr26CorrectedRowsBandSlice
open ModularCurve.GF24a11bRowACurrencyBridge
open ModularCurve.GF24a12CohenSupply
open ModularCurve.Ldgr32RegularLegSlice
open ModularCurve.Ldgr31PerPlaceRowJoinSlice
open ModularCurve.Ldgr29SimplePoleResidueSlice
open ModularCurve.Ldgr25CotraceCompatSlice
open AlgebraicCurve.FiberKaehlerLocalDatum
open ModularCurve.KwNo6HrouteS
open _root_.AlgebraicCurve.Place
open _root_.ModularCurve.KwNo6Pin
open ModularCurve.KwNo6HrouteR
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.Mp72a102T1
open _root_.ModularCurve.KwNo6Section
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open scoped Polynomial
noncomputable section
section
namespace ModularCurve
open _root_.ModularCurve
namespace KwOdaDHDR
open _root_.ModularCurve
attribute [local instance 2000] RatFunc.instAlgebraOfPolynomial
section Generic
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem kwHgf_v277_aCoeff_section_lift_mul (v : Place K F)
    (S : Lg37CompletionSection v) (m : ℕ) (a : v.ResidueField)
    (x : lg37_completion v) :
    aCoeff v S m (S.lift a * x) = a * aCoeff v S m x
theorem

kwHgf_v278_aCoeff_eq_zero_of_evalDepth_zero

L3791 ↗
ModularCurve.KwOdaDHDR.kwHgf_v278_aCoeff_eq_zero_of_evalDepth_zero
Source context 68 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open scoped PadicInt AlgebraicGeometry
open _root_.BigOperators
open _root_.CategoryTheory
open _root_.AlgebraicCurve
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.ModularCurve
open _root_.Order
open _root_.Topology
open FLT.HopfSpec GoodReductionJacobian
open Deformation.PDivisible Deformation.ModpDieudonne
open _root_.AlgebraicCurve
open _root_.Module
open _root_.CongruenceSubgroup
open NeronOggShafarevich
open AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine
open _root_.AlgebraicCurve.RationalFunctionField
open scoped TensorProduct
open _root_.IntermediateField
open _root_.AlgebraicCurve.RationalFunctionField
open ModularCurve.KwNo6HrouteV
open ModularCurve.KwNo6HrouteY
open ModularCurve.KwNo6HrouteZ
open ModularCurve.GF24a9RRDx
open ModularCurve.GF24a12CohenSupply
open Ldgr30BankGate
open Modularity.Ldgr27TraceSemilinearSlice
open Ldgr24DefectKernelSlice
open Ldgr23CohenDefectCorrectionSlice
open ModularCurve.Ldgr25PlaceExtensionSlice
open Ldgr25CorrectedChoiceSlice
open Modularity.Ldgr26CorrectedRowsBandSlice
open ModularCurve.GF24a11bRowACurrencyBridge
open ModularCurve.GF24a12CohenSupply
open ModularCurve.Ldgr32RegularLegSlice
open ModularCurve.Ldgr31PerPlaceRowJoinSlice
open ModularCurve.Ldgr29SimplePoleResidueSlice
open ModularCurve.Ldgr25CotraceCompatSlice
open AlgebraicCurve.FiberKaehlerLocalDatum
open ModularCurve.KwNo6HrouteS
open _root_.AlgebraicCurve.Place
open _root_.ModularCurve.KwNo6Pin
open ModularCurve.KwNo6HrouteR
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.Mp72a102T1
open _root_.ModularCurve.KwNo6Section
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open scoped Polynomial
noncomputable section
section
namespace ModularCurve
open _root_.ModularCurve
namespace KwOdaDHDR
open _root_.ModularCurve
attribute [local instance 2000] RatFunc.instAlgebraOfPolynomial
section Generic
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem kwHgf_v278_aCoeff_eq_zero_of_evalDepth_zero (v : Place K F)
    (S : Lg37CompletionSection v) {n : ℕ} (w : lg37_completion v)
    (hw : AdicCompletion.evalₐ (maximalIdeal v.toValuationSubring) n w = 0)
    {k : ℕ} (hk : k < n) :
    aCoeff v S k w = 0
theorem

kwHgf_v278_resStar_approximant_mul

L3815 ↗
ModularCurve.KwOdaDHDR.kwHgf_v278_resStar_approximant_mul
Source context 68 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open scoped PadicInt AlgebraicGeometry
open _root_.BigOperators
open _root_.CategoryTheory
open _root_.AlgebraicCurve
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.ModularCurve
open _root_.Order
open _root_.Topology
open FLT.HopfSpec GoodReductionJacobian
open Deformation.PDivisible Deformation.ModpDieudonne
open _root_.AlgebraicCurve
open _root_.Module
open _root_.CongruenceSubgroup
open NeronOggShafarevich
open AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine
open _root_.AlgebraicCurve.RationalFunctionField
open scoped TensorProduct
open _root_.IntermediateField
open _root_.AlgebraicCurve.RationalFunctionField
open ModularCurve.KwNo6HrouteV
open ModularCurve.KwNo6HrouteY
open ModularCurve.KwNo6HrouteZ
open ModularCurve.GF24a9RRDx
open ModularCurve.GF24a12CohenSupply
open Ldgr30BankGate
open Modularity.Ldgr27TraceSemilinearSlice
open Ldgr24DefectKernelSlice
open Ldgr23CohenDefectCorrectionSlice
open ModularCurve.Ldgr25PlaceExtensionSlice
open Ldgr25CorrectedChoiceSlice
open Modularity.Ldgr26CorrectedRowsBandSlice
open ModularCurve.GF24a11bRowACurrencyBridge
open ModularCurve.GF24a12CohenSupply
open ModularCurve.Ldgr32RegularLegSlice
open ModularCurve.Ldgr31PerPlaceRowJoinSlice
open ModularCurve.Ldgr29SimplePoleResidueSlice
open ModularCurve.Ldgr25CotraceCompatSlice
open AlgebraicCurve.FiberKaehlerLocalDatum
open ModularCurve.KwNo6HrouteS
open _root_.AlgebraicCurve.Place
open _root_.ModularCurve.KwNo6Pin
open ModularCurve.KwNo6HrouteR
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.Mp72a102T1
open _root_.ModularCurve.KwNo6Section
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open scoped Polynomial
noncomputable section
section
namespace ModularCurve
open _root_.ModularCurve
namespace KwOdaDHDR
open _root_.ModularCurve
attribute [local instance 2000] RatFunc.instAlgebraOfPolynomial
section Generic
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem kwHgf_v278_resStar_approximant_mul (v : Place K F)
    (S : Lg37CompletionSection v) (ℓ : v.toValuationSubring) (M : ℕ)
    (hvan : ∀ k, 1 ≤ k → k ≤ M →
      aCoeff v S k (algebraMap v.toValuationSubring (lg37_completion v) ℓ) = 0)
    (g : F) (hg : g ∈ v.poleSubmodule (M + 1)) :
    resStar v S ((ℓ : F) * g) = IsLocalRing.residue _ ℓ * resStar v S g
theorem

approximant_evalₐ_sub_lift_eq_zero

L3945 ↗
ModularCurve.KwTateRR3.approximant_evalₐ_sub_lift_eq_zero
Source context 27 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section ApproximantHev
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem approximant_evalₐ_sub_lift_eq_zero (u : Place K L) (S : Lg37CompletionSection u)
    {ℓ : u.toValuationSubring} {M : ℕ}
    (hvan : ∀ k, 1 ≤ k → k ≤ M →
      aCoeff u S k (algebraMap u.toValuationSubring (lg37_completion u) ℓ) = 0) :
    AdicCompletion.evalₐ (maximalIdeal u.toValuationSubring) (M + 1)
      (algebraMap u.toValuationSubring (lg37_completion u) ℓ
        - S.lift (IsLocalRing.residue _ ℓ)) = 0
theorem

v410a_mem_completionIdeal_pow_of_evalₐ_eq_zero

L3981 ↗
ModularCurve.KwTateRR3.v410a_mem_completionIdeal_pow_of_evalₐ_eq_zero
Source context 27 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section V410aBridge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem v410a_mem_completionIdeal_pow_of_evalₐ_eq_zero (n : ℕ)
    (z : lg37_completion u)
    (hz : AdicCompletion.evalₐ (maximalIdeal u.toValuationSubring) n z = 0) :
    kwF4R1V410a_ringEquiv u z ∈ (u.heightOneSpectrum.completionIdeal L) ^ n
theorem

valued_algebraMap_uniformizer

L3988 ↗
ModularCurve.KwTateRR3.valued_algebraMap_uniformizer
Source context 27 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section V410aBridge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem valued_algebraMap_uniformizer :
    Valued.v (algebraMap L u.adicCompletion u.uniformizer) = WithZero.exp (-1 : ℤ)
theorem

v410a_evalDepth_mul_mem_integers

L4000 ↗
ModularCurve.KwTateRR3.v410a_evalDepth_mul_mem_integers
Source context 27 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section V410aBridge
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem v410a_evalDepth_mul_mem_integers (n : ℕ) (z : lg37_completion u)
    (hz : AdicCompletion.evalₐ (maximalIdeal u.toValuationSubring) n z = 0)
    (fh : u.adicCompletion)
    (hfh : (algebraMap L u.adicCompletion u.uniformizer) ^ n * fh ∈ u.adicCompletionIntegers) :
    ((kwF4R1V410a_ringEquiv u z : u.adicCompletionIntegers) : u.adicCompletion) * fh
      ∈ u.adicCompletionIntegers
theorem

kwTateRR3_localResidueCompletion_sub

L4039 ↗
ModularCurve.KwTateRR3.kwTateRR3_localResidueCompletion_sub
Source context 28 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section EpsSpec
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K]
Lean source · statement
theorem kwTateRR3_localResidueCompletion_sub (u : Place K L) (xh yh : u.adicCompletion) :
    kwHgfV352_localResidueCompletion u (xh - yh)
      = kwHgfV352_localResidueCompletion u xh
        - kwHgfV352_localResidueCompletion u yh
theorem

algebraMap_sub_cohenSectionHat_eq_v410a

L4046 ↗
ModularCurve.KwTateRR3.algebraMap_sub_cohenSectionHat_eq_v410a
Source context 29 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section EpsSpec
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K]
omit [IsCurveOver K L] [PerfectField K] in
Lean source · statement
theorem algebraMap_sub_cohenSectionHat_eq_v410a (u : Place K L)
    (S : Lg37CompletionSection u) (ℓ : u.toValuationSubring) :
    algebraMap L u.adicCompletion (ℓ : L)
        - cohenSectionHat u S (IsLocalRing.residue _ ℓ)
      = ((kwF4R1V410a_ringEquiv u
            (algebraMap u.toValuationSubring (lg37_completion u) ℓ
              - S.lift (IsLocalRing.residue _ ℓ))
          : u.adicCompletionIntegers) : u.adicCompletion)
theorem

localResidueCompletion_mul_cohenSectionHat

L4066 ↗
ModularCurve.KwTateRR3.localResidueCompletion_mul_cohenSectionHat
Source context 28 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section EpsSpec
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K]
Lean source · statement
theorem localResidueCompletion_mul_cohenSectionHat
    (u : Place K L) (S : Lg37CompletionSection u)
    (fh : u.adicCompletion) (c : u.ResidueField) :
    kwHgfV352_localResidueCompletion u (fh * cohenSectionHat u S c)
      = kwHgfV352_localResidueCompletion u fh * c
structure

KwTateRR3CohenLaurentCompl

L4141 ↗
ModularCurve.KwTateRR3.KwTateRR3CohenLaurentCompl
Documentation

A Cohen section and a Laurent complement compatible with the completed local residue.

Source context 28 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section ComplMint
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
Lean source · full declaration
structure KwTateRR3CohenLaurentCompl (u : Place K L) [u.FiniteResidue] where
  /-- The chosen section from the residue field into the adic completion. -/
  S : Lg37CompletionSection u
  /-- The complementary subspace of Laurent principal parts. -/
  B : Submodule K u.adicCompletion
  /-- The Laurent subspace complements integral completion elements. -/
  hcompl : IsCompl (adicIntegersKSubmod u) B
  /-- Uniformizer multiplication preserves the complement after removing the lifted completed
  residue. -/
  shift_sub_mem : ∀ z : B,
    algebraMap L u.adicCompletion u.uniformizer * (z : u.adicCompletion)
      - cohenSectionHat u S (kwHgfV352_localResidueCompletion u (z : u.adicCompletion)) ∈ B
def

KwTateRR3CohenLaurentComplExists

L4156 ↗
ModularCurve.KwTateRR3.KwTateRR3CohenLaurentComplExists
Documentation

Existence of a Cohen section with a compatible Laurent complement at every place.

Source context 29 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section ComplMint
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [HasCanonicalLocalResidueKStar K L]
variable (K L) in
Lean source · statement
def KwTateRR3CohenLaurentComplExists : Prop
def

localResidueCompletionₗ

L4168 ↗
ModularCurve.KwTateRR3.localResidueCompletionₗ
Documentation

The completed local residue regarded as a linear map over the base field.

Source context 29 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Construct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K]
variable {u : Place K L} [u.FiniteResidue]
Lean source · full declaration
def localResidueCompletionₗ (u : Place K L) : u.adicCompletion →ₗ[K] u.ResidueField where
  toFun := kwHgfV352_localResidueCompletion u
  map_add' := kwHgfV352_localResidueCompletion_add u
  map_smul' c x := by
    rw [RingHom.id_apply]; exact kwF4R1V394a_localResidueCompletion_smul u c x
def

cohenLaurentSpec_of_compl

L4175 ↗
ModularCurve.KwTateRR3.cohenLaurentSpec_of_compl
Documentation

The Laurent specification induced by the completed local residue on a compatible complement.

Source context 29 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Construct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K]
variable {u : Place K L} [u.FiniteResidue]
Lean source · full declaration
def cohenLaurentSpec_of_compl (C : KwTateRR3CohenLaurentCompl u) :
    KwTateRR3CohenLaurentSpec u where
  S := C.S
  B := C.B
  hcompl := C.hcompl
  ε := (localResidueCompletionₗ u).comp C.B.subtype
  shift_sub_mem z := C.shift_sub_mem z
  ε_principalPart_mul_sectionHat fh c := by
    change kwHgfV352_localResidueCompletion u
        (fh * cohenSectionHat u C.S c
          - cohenProjC u C.B C.hcompl (fh * cohenSectionHat u C.S c))
      = kwHgfV352_localResidueCompletion u fh * c
    rw [kwTateRR3_localResidueCompletion_sub u,
      kwHgfV352_localResidueCompletion_eq_zero_of_mem_integers u
        (cohenProjC_mem_integers u C.B C.hcompl _),
      sub_zero, localResidueCompletion_mul_cohenSectionHat u C.S fh c]
theorem

kwTateRR3_cohenLaurentSpecExists_of_complExists

L4199 ↗
ModularCurve.KwTateRR3.kwTateRR3_cohenLaurentSpecExists_of_complExists
Source context 28 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Headline
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K]
Lean source · statement
theorem kwTateRR3_cohenLaurentSpecExists_of_complExists
    (hC : KwTateRR3CohenLaurentComplExists K L) :
    KwTateRR3CohenLaurentSpecExists K L
theorem

kwTateRR3_cohenKernelDataExists_of_complExists

L4204 ↗
ModularCurve.KwTateRR3.kwTateRR3_cohenKernelDataExists_of_complExists
Source context 28 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.ModularCurve.Mp72a102T3
open _root_.Mp72a103T2
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Headline
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K]
Lean source · statement
theorem kwTateRR3_cohenKernelDataExists_of_complExists
    (hC : KwTateRR3CohenLaurentComplExists K L) :
    KwF4gRRTateCohenKernelDataExists K L
abbrev

uniformizerHat

L4247 ↗
ModularCurve.KwTateRR3.uniformizerHat
Documentation

The image of the chosen uniformizer in the valuation completion.

Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section UniformizerHat
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
abbrev uniformizerHat : u.adicCompletion
theorem

uniformizerHat_ne_zero

L4249 ↗
ModularCurve.KwTateRR3.uniformizerHat_ne_zero
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section UniformizerHat
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem uniformizerHat_ne_zero : uniformizerHat u ≠ 0
theorem

uniformizerHat_mem_integers

L4253 ↗
ModularCurve.KwTateRR3.uniformizerHat_mem_integers
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section UniformizerHat
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem uniformizerHat_mem_integers : uniformizerHat u ∈ u.adicCompletionIntegers
theorem

irreducible_uniformizerHat

L4256 ↗
ModularCurve.KwTateRR3.irreducible_uniformizerHat
Source context 25 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section UniformizerHat
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
Lean source · statement
theorem irreducible_uniformizerHat :
    Irreducible (⟨uniformizerHat u, uniformizerHat_mem_integers u⟩
      : u.adicCompletionIntegers)
def

cohenΦ

L4272 ↗
ModularCurve.KwTateRR3.cohenΦ
Documentation

The finite Laurent principal part associated to finitely supported residue-field coefficients.

Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenPhi
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · statement
def cohenΦ : (ℕ →₀ u.ResidueField) →ₗ[K] u.adicCompletion
theorem

cohenΦ_apply

L4276 ↗
ModularCurve.KwTateRR3.cohenΦ_apply
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenPhi
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · full declaration
theorem cohenΦ_apply (δ : ℕ →₀ u.ResidueField) :
    cohenΦ u S δ = δ.sum fun j c => (uniformizerHat u)⁻¹ ^ (j + 1) * cohenSectionHat u S c := by
  rw [cohenΦ, Finsupp.coe_lsum]; rfl
theorem

cohenΦ_single

L4280 ↗
ModularCurve.KwTateRR3.cohenΦ_single
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenPhi
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · statement
theorem cohenΦ_single (j : ℕ) (c : u.ResidueField) :
    cohenΦ u S (Finsupp.single j c)
      = (uniformizerHat u)⁻¹ ^ (j + 1) * cohenSectionHat u S c
def

cohenB

L4287 ↗
ModularCurve.KwTateRR3.cohenB
Documentation

The subspace of finite Laurent principal parts supplied by the Cohen section.

Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenPhi
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · statement
def cohenB : Submodule K u.adicCompletion
theorem

monomial_mem_cohenB

L4289 ↗
ModularCurve.KwTateRR3.monomial_mem_cohenB
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section CohenPhi
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · statement
theorem monomial_mem_cohenB (j : ℕ) (c : u.ResidueField) :
    (uniformizerHat u)⁻¹ ^ (j + 1) * cohenSectionHat u S c ∈ cohenB u S
theorem

locResCompl_uniformizerHat_inv

L4300 ↗
ModularCurve.KwTateRR3.locResCompl_uniformizerHat_inv
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section LocResComplMonomial
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K] (u : Place K L)
Lean source · statement
theorem locResCompl_uniformizerHat_inv (S : Lg37CompletionSection u) :
    kwHgfV352_localResidueCompletion u ((uniformizerHat u)⁻¹) = 1
theorem

locResCompl_uniformizerHat_inv_pow_succ

L4310 ↗
ModularCurve.KwTateRR3.locResCompl_uniformizerHat_inv_pow_succ
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section LocResComplMonomial
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K] (u : Place K L)
Lean source · statement
theorem locResCompl_uniformizerHat_inv_pow_succ (S : Lg37CompletionSection u)
    {j : ℕ} (hj : 1 ≤ j) :
    kwHgfV352_localResidueCompletion u ((uniformizerHat u)⁻¹ ^ (j + 1)) = 0
theorem

locResCompl_cohenΦ

L4327 ↗
ModularCurve.KwTateRR3.locResCompl_cohenΦ
Source context 27 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section LocResComplPhi
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · statement
theorem locResCompl_cohenΦ (δ : ℕ →₀ u.ResidueField) :
    kwHgfV352_localResidueCompletion u (cohenΦ u S δ) = δ 0
theorem

uniformizerHat_mul_cohenΦ

L4350 ↗
ModularCurve.KwTateRR3.uniformizerHat_mul_cohenΦ
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section ShiftCore
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · full declaration
theorem uniformizerHat_mul_cohenΦ (δ : ℕ →₀ u.ResidueField) :
    uniformizerHat u * cohenΦ u S δ
      = δ.sum fun j c => (uniformizerHat u)⁻¹ ^ j * cohenSectionHat u S c := by
  rw [cohenΦ_apply, Finsupp.mul_sum]
  refine Finsupp.sum_congr fun j _ => ?_
  rw [pow_succ', ← mul_assoc, ← mul_assoc,
    mul_inv_cancel₀ (uniformizerHat_ne_zero u), one_mul]
theorem

uniformizerHat_mul_cohenΦ_sub_mem

L4358 ↗
ModularCurve.KwTateRR3.uniformizerHat_mul_cohenΦ_sub_mem
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section ShiftCore
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · statement
theorem uniformizerHat_mul_cohenΦ_sub_mem (δ : ℕ →₀ u.ResidueField) :
    uniformizerHat u * cohenΦ u S δ - cohenSectionHat u S (δ 0) ∈ cohenB u S
theorem

valued_cohenSectionHat_of_ne_zero

L4380 ↗
ModularCurve.KwTateRR3.valued_cohenSectionHat_of_ne_zero
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Disjoint
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · statement
theorem valued_cohenSectionHat_of_ne_zero {c : u.ResidueField} (hc : c ≠ 0) :
    Valued.v (cohenSectionHat u S c) = 1
theorem

uniformizerHat_pow_mul_cohenΦ_sub_top

L4391 ↗
ModularCurve.KwTateRR3.uniformizerHat_pow_mul_cohenΦ_sub_top
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Disjoint
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · full declaration
theorem uniformizerHat_pow_mul_cohenΦ_sub_top (δ : ℕ →₀ u.ResidueField)
    (hδ : δ.support.Nonempty) :
    let J := δ.support.max' hδ
    (uniformizerHat u) ^ (J + 1) * cohenΦ u S δ - cohenSectionHat u S (δ J)
      = ∑ j ∈ δ.support.erase J,
          (uniformizerHat u) ^ (J - j) * cohenSectionHat u S (δ j) := by
  intro J
  have hJmem : J ∈ δ.support := δ.support.max'_mem hδ
  rw [cohenΦ_apply, Finsupp.mul_sum, Finsupp.sum,
    ← Finset.sum_erase_add _ _ hJmem,
    show (uniformizerHat u) ^ (J + 1) * ((uniformizerHat u)⁻¹ ^ (J + 1)
            * cohenSectionHat u S (δ J))
        = cohenSectionHat u S (δ J) by
      rw [← mul_assoc, ← mul_pow, mul_inv_cancel₀ (uniformizerHat_ne_zero u), one_pow, one_mul],
    add_sub_cancel_right]
  refine Finset.sum_congr rfl fun j hj => ?_
  have hjJ : j < J := lt_of_le_of_ne
    (δ.support.le_max' j (Finset.mem_of_mem_erase hj)) (Finset.ne_of_mem_erase hj)
  rw [← mul_assoc]
  congr 1
  rw [show J + 1 = (J - j) + (j + 1) by omega, pow_add, mul_assoc,
    ← mul_pow, mul_inv_cancel₀ (uniformizerHat_ne_zero u), one_pow, mul_one]
theorem

cohenΦ_mem_integers_iff_zero

L4414 ↗
ModularCurve.KwTateRR3.cohenΦ_mem_integers_iff_zero
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Disjoint
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · statement
theorem cohenΦ_mem_integers_iff_zero (δ : ℕ →₀ u.ResidueField) :
    cohenΦ u S δ ∈ u.adicCompletionIntegers → δ = 0
theorem

disjoint_adicIntegersKSubmod_cohenB

L4456 ↗
ModularCurve.KwTateRR3.disjoint_adicIntegersKSubmod_cohenB
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Disjoint
variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)
variable (S : Lg37CompletionSection u)
Lean source · statement
theorem disjoint_adicIntegersKSubmod_cohenB :
    _root_.Disjoint (adicIntegersKSubmod u) (cohenB u S)
theorem

uniformizerHat_inv_mul_mem_integers_of_valued_le

L4471 ↗
ModularCurve.KwTateRR3.uniformizerHat_inv_mul_mem_integers_of_valued_le
Source context 28 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Codisjoint
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K] (u : Place K L)
variable (S : Lg37CompletionSection u)
omit [IsCurveOver K L] [PerfectField K] in
Lean source · statement
theorem uniformizerHat_inv_mul_mem_integers_of_valued_le
    {y : u.adicCompletion} (hy : Valued.v y ≤ WithZero.exp (-1 : ℤ)) :
    (uniformizerHat u)⁻¹ * y ∈ u.adicCompletionIntegers
theorem

valued_le_of_mem_completionIdeal

L4481 ↗
ModularCurve.KwTateRR3.valued_le_of_mem_completionIdeal
Source context 28 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Codisjoint
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K] (u : Place K L)
variable (S : Lg37CompletionSection u)
omit [IsCurveOver K L] [PerfectField K] in
Lean source · statement
theorem valued_le_of_mem_completionIdeal {y : u.adicCompletionIntegers}
    (hy : y ∈ u.heightOneSpectrum.completionIdeal L) :
    Valued.v (y : u.adicCompletion) ≤ WithZero.exp (-1 : ℤ)
theorem

exists_residue_peel

L4489 ↗
ModularCurve.KwTateRR3.exists_residue_peel
Source context 28 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Codisjoint
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K] (u : Place K L)
variable (S : Lg37CompletionSection u)
omit [IsCurveOver K L] [PerfectField K] in
Lean source · statement
theorem exists_residue_peel (ŷ : u.adicCompletionIntegers) :
    ∃ c : u.ResidueField,
      (uniformizerHat u)⁻¹ * ((ŷ : u.adicCompletion) - cohenSectionHat u S c)
        ∈ u.adicCompletionIntegers
theorem

mem_sup_of_uniformizerHat_pow_mul_mem_integers

L4516 ↗
ModularCurve.KwTateRR3.mem_sup_of_uniformizerHat_pow_mul_mem_integers
Source context 28 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Codisjoint
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K] (u : Place K L)
variable (S : Lg37CompletionSection u)
omit [IsCurveOver K L] [PerfectField K] in
Lean source · statement
theorem mem_sup_of_uniformizerHat_pow_mul_mem_integers (M : ℕ) :
    ∀ x : u.adicCompletion, (uniformizerHat u) ^ M * x ∈ u.adicCompletionIntegers →
      x ∈ adicIntegersKSubmod u ⊔ cohenB u S
theorem

codisjoint_adicIntegersKSubmod_cohenB

L4549 ↗
ModularCurve.KwTateRR3.codisjoint_adicIntegersKSubmod_cohenB
Source context 28 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Codisjoint
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K] (u : Place K L)
variable (S : Lg37CompletionSection u)
omit [IsCurveOver K L] [PerfectField K] in
Lean source · statement
theorem codisjoint_adicIntegersKSubmod_cohenB :
    Codisjoint (adicIntegersKSubmod u) (cohenB u S)
def

cohenLaurentCompl_of_section

L4565 ↗
ModularCurve.KwTateRR3.cohenLaurentCompl_of_section
Documentation

The compatible Laurent complement constructed from the chosen Cohen section.

Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Assembly
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K]
Lean source · full declaration
def cohenLaurentCompl_of_section (u : Place K L) [u.FiniteResidue]
    (S : Lg37CompletionSection u) : KwTateRR3CohenLaurentCompl u where
  S := S
  B := cohenB u S
  hcompl := ⟨disjoint_adicIntegersKSubmod_cohenB u S,
    codisjoint_adicIntegersKSubmod_cohenB u S⟩
  shift_sub_mem z := by
    obtain ⟨δ, hδ⟩ := z.2
    rw [← hδ, locResCompl_cohenΦ u S δ]
    exact uniformizerHat_mul_cohenΦ_sub_mem u S δ
theorem

kwTateRR3_cohenLaurentComplExists

L4583 ↗
ModularCurve.KwTateRR3.kwTateRR3_cohenLaurentComplExists
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Headline
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K]
Lean source · statement
theorem kwTateRR3_cohenLaurentComplExists :
    KwTateRR3CohenLaurentComplExists K L
theorem

kwTateRR3_cohenKernelDataExists

L4590 ↗
ModularCurve.KwTateRR3.kwTateRR3_cohenKernelDataExists
Source context 26 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
section
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve.Place
open _root_.LinearMap
open _root_.Submodule
open _root_.IsLocalRing
open _root_.ModularCurve.KwF4gRRTate
open _root_.ModularCurve.Lg37
open _root_.ModularCurve.KwNo6Pin
open _root_.IsDedekindDomain
open _root_.IsDedekindDomain.HeightOneSpectrum
open _root_.WithZero
noncomputable section
namespace ModularCurve
open _root_.ModularCurve
namespace KwTateRR3
open _root_.ModularCurve
section Headline
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [IsCurveOver K L] [PerfectField K]
Lean source · statement
theorem kwTateRR3_cohenKernelDataExists :
    KwF4gRRTateCohenKernelDataExists K L
theorem

tateAgreement

L4603 ↗
AlgebraicCurve.tateAgreement
Source context 7 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
open ModularCurve.KwF4R1V394a
open ModularCurve.KwF4R1V410a
open ModularCurve.KwNo6HrouteR
section
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateAgreement
Lean source · statement
theorem _root_.AlgebraicCurve.tateAgreement
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [AlgebraicCurve.IsCurveOver K L] [PerfectField K]
    [∀ u : AlgebraicCurve.Place K L, u.FiniteResidue]
    (hfin : ModularCurve.KwF4gRRTate.KwF4gRRTateCommFinite K L) :
    ModularCurve.KwF4gRRTate.KwF4gRRTateAgreement K L hfin

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