NYLL
Module

TateCommFinite.lean

Nyll.AlgebraicCurves.Differentials.Residues.TateCommFinite
55 declarations indexed from sourceView source ↗

Module documentation

Compatibility of Tate constructions with finite extensions.

Imports38
Imported by3

Declarations

theorem

maximalIdeal_le

L152 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.IsLocalRing.maximalIdeal_le
Source context 5 commands

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

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

ord_nonneg_of_mem

L312 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.AlgebraicCurve.Place.ord_nonneg_of_mem
Source context 17 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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 ord_nonneg_of_mem {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L327 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.AlgebraicCurve.Place.mem_of_ord_nonneg
Source context 17 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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 mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring
theorem

valued_eq_one_of_isUnit

L374 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ValuationSubring.valued_eq_one_of_isUnit
Source context 8 commands

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

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

isUnit_of_valued_eq_one

L385 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ValuationSubring.isUnit_of_valued_eq_one
Source context 8 commands

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

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

isUnit_iff_valued_eq_one

L396 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ValuationSubring.isUnit_iff_valued_eq_one
Source context 8 commands

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

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

mem_adicIntegersKSubmod_iff

L492 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.mem_adicIntegersKSubmod_iff
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L495 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.tateProj_mem_integers
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L502 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.tateProj_of_mem
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

range_tateProj

L510 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.range_tateProj
Source context 19 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L572 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.poleWindowKSubmod
Documentation

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

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L584 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.mem_poleWindowKSubmod_iff
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L589 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.adicIntegersKSubmod_le_poleWindowKSubmod
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L593 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.kwF4gRRTate_clearPole
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

KwF4gRRTateClearPole

L620 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.KwF4gRRTateClearPole
Documentation

Every completed element has a pole cleared by some power of an irreducible completed integer.

Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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 KwF4gRRTateClearPole : Prop
theorem

kwF4gRRTate_clearPole_discharged

L625 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.kwF4gRRTate_clearPole_discharged
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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
theorem kwF4gRRTate_clearPole_discharged : KwF4gRRTateClearPole K L
theorem

lmul_mem_poleWindow

L628 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.lmul_mem_poleWindow
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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
theorem lmul_mem_poleWindow (πh : u.adicCompletionIntegers) (M : ℕ) (fh : u.adicCompletion)
    (hM : (πh : u.adicCompletion) ^ M * fh ∈ u.adicCompletionIntegers)
    {a : u.adicCompletion} (ha : a ∈ u.adicCompletionIntegers) :
    fh * a ∈ poleWindowKSubmod u πh M
def

KwF4gRRTatePoleWindowFinite

L637 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.KwF4gRRTatePoleWindowFinite
Documentation

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

Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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
variable (K L) in
Lean source · statement
def KwF4gRRTatePoleWindowFinite : Prop
theorem

ker_tateProj_inf_integers

L644 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.ker_tateProj_inf_integers
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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
variable (K L) in
Lean source · statement
theorem ker_tateProj_inf_integers :
    LinearMap.ker (tateProj u) ⊓ adicIntegersKSubmod u = ⊥
theorem

finiteDimensional_ker_inf_poleWindow

L652 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.finiteDimensional_ker_inf_poleWindow
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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
variable (K L) in
Lean source · statement
theorem finiteDimensional_ker_inf_poleWindow [u.FiniteResidue]
    (hPW : KwF4gRRTatePoleWindowFinite K L)
    (πh : u.adicCompletionIntegers) (hπh : Irreducible πh) (M : ℕ) :
    FiniteDimensional K
      ((LinearMap.ker (tateProj u) ⊓ poleWindowKSubmod u πh M : Submodule K _))
theorem

finiteDimensional_principalPart_range

L677 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.finiteDimensional_principalPart_range
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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
variable (K L) in
Lean source · statement
theorem finiteDimensional_principalPart_range [u.FiniteResidue]
    (hCP : KwF4gRRTateClearPole K L) (hPW : KwF4gRRTatePoleWindowFinite K L)
    (fh : u.adicCompletion) :
    FiniteDimensional K
      (LinearMap.range
        ((LinearMap.id - tateProj u) ∘ₗ lmulK u fh ∘ₗ (adicIntegersKSubmod u).subtype))
theorem

tateComm_target_le_range

L696 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.tateComm_target_le_range
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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
variable (K L) in
Lean source · statement
theorem tateComm_target_le_range (pA φ ψ : u.adicCompletion →ₗ[K] u.adicCompletion)
    (Rf Rg : Submodule K u.adicCompletion) :
    Submodule.map (pA ∘ₗ ψ) Rf ⊔ Submodule.map (pA ∘ₗ φ) Rg ≤ LinearMap.range pA
theorem

kwF4gRRTate_commFinite_of_clearPole_of_poleWindowFinite

L702 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.kwF4gRRTate_commFinite_of_clearPole_of_poleWindowFinite
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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
variable (K L) in
Lean source · statement
theorem kwF4gRRTate_commFinite_of_clearPole_of_poleWindowFinite
    [∀ u : Place K L, u.FiniteResidue]
    (hCP : KwF4gRRTateClearPole K L) (hPW : KwF4gRRTatePoleWindowFinite K L) :
    KwF4gRRTateCommFinite K L
theorem

kwF4gRRTate_commFinite_of_poleWindowFinite

L736 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.kwF4gRRTate_commFinite_of_poleWindowFinite
Source context 24 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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
variable (K L) in
Lean source · statement
theorem kwF4gRRTate_commFinite_of_poleWindowFinite [∀ u : Place K L, u.FiniteResidue]
    (hPW : KwF4gRRTatePoleWindowFinite K L) :
    KwF4gRRTateCommFinite K L
theorem

isOpen_setOf_valued_le

L775 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.isOpen_setOf_valued_le
Source context 18 commands

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

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

kwF4R1V410a_subsingletonHeightOneSpectrumDVR

L830 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4R1V410a.kwF4R1V410a_subsingletonHeightOneSpectrumDVR
Source context 16 commands

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

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

kwF4R1V410a_algebraMap_mem_completionIdeal_pow_iff

L846 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4R1V410a.kwF4R1V410a_algebraMap_mem_completionIdeal_pow_iff
Source context 22 commands

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

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

kwF4R1V410a_exists_sub_mem_completionIdeal_pow

L857 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4R1V410a.kwF4R1V410a_exists_sub_mem_completionIdeal_pow
Source context 22 commands

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

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

kwF4R1V410a_quotientEquiv

L900 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.kwF4R1V410a_quotientEquiv
Documentation

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

Source context 22 commands

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

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

kwF4R1V410a_quotientEquiv_mk

L921 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.kwF4R1V410a_quotientEquiv_mk
Source context 22 commands

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

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

coe_smul_K

L962 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.coe_smul_K
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L968 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.poleWindowShift
Documentation

Multiplication by πh to the power M sends the pole window to the completed integers.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L979 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.poleWindowShift_injective
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L993 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.poleWindowShift_surjective
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1008 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.poleWindowShiftEquiv
Documentation

Multiplication by an irreducible πh to the power M identifies the pole window with the completed integers.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1014 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.piPowKSubmod
Documentation

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

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1023 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.poleWindowShift_image_integers
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1040 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.KwF4gRRTateDVRQuotPowKFinite
Documentation

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

Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1045 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.kwF4gRRTate_poleWindowFinite_of_DVRQuotPowKFinite
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

kwF4gRRTate_commFinite_of_DVRQuotPowKFinite

L1058 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.kwF4gRRTate_commFinite_of_DVRQuotPowKFinite
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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_commFinite_of_DVRQuotPowKFinite [∀ u : Place K L, u.FiniteResidue]
    (hDVR : KwF4gRRTateDVRQuotPowKFinite K L) :
    KwF4gRRTateCommFinite K L
theorem

piPowKSubmod_eq_restrictScalars

L1100 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.piPowKSubmod_eq_restrictScalars
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1109 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.quotPiPowEquivIdealQuot
Documentation

Identifies the quotient by the K-submodule of multiples of πh to the power M with the corresponding ideal quotient.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1118 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.KwF4gRRTateDVRCotangentKFinite
Documentation

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

Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1123 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.range_mulLeft_eq_restrictScalars_span
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1132 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.finiteDimensional_restrictScalarsQuot_pow
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1194 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.finiteDimensional_idealQuot_pow
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1202 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.kwF4gRRTate_DVRQuotPowKFinite_of_cotangent
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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
theorem

kwF4gRRTate_commFinite_of_cotangent

L1209 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.kwF4gRRTate_commFinite_of_cotangent
Source context 23 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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_commFinite_of_cotangent [∀ u : Place K L, u.FiniteResidue]
    (hCot : KwF4gRRTateDVRCotangentKFinite K L) :
    KwF4gRRTateCommFinite K L
instance

instIsScalarTower_K_toValuationSubring_adicCompletionIntegers

L1251 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.instIsScalarTower_K_toValuationSubring_adicCompletionIntegers
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1260 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.span_irreducible_eq_completionIdeal_pow_one
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1268 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.quotientEquivKAlg
Documentation

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

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1285 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.quotSpanIrreducibleEquivResidueField
Documentation

Identifies the quotient of completed integers by an irreducible element with the residue field over K.

Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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

L1294 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.kwF4gRRTate_DVRCotangentKFinite
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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
theorem

kwF4gRRTate_commFinite

L1299 ↗
AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite.ModularCurve.KwF4gRRTate.kwF4gRRTate_commFinite
Source context 22 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
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_commFinite [∀ u : Place K L, u.FiniteResidue] :
    KwF4gRRTateCommFinite K L
theorem

tateCommFinite

L1313 ↗
AlgebraicCurve.tateCommFinite
Source context 3 commands

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

section ProofImplementation
attribute [-ext] IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
namespace AlgebraicCurves.Differentials.Residues.Proofs.TateCommFinite
Lean source · statement
theorem _root_.AlgebraicCurve.tateCommFinite {K L : Type*} [Field K] [Field L] [Algebra K L]
    [∀ u : AlgebraicCurve.Place K L, u.FiniteResidue] :
    ModularCurve.KwF4gRRTate.KwF4gRRTateCommFinite K L

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