Module

TranscendenceTower_degree_poleDivisor_eq_finrank.lean

Nyll.AlgebraicCurves.FunctionFields.TranscendenceTower_degree_poleDivisor_eq_finrank

136 declarations indexed from sourceView source ↗

Module documentation

Transcendence Tower degree pole Divisor eq finrank

Imports7

Imported by2

theorem

ord_nonneg_of_mem

L37 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.Place.ord_nonneg_of_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
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

L51 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.Place.mem_of_ord_nonneg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
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

mem_iff_ord_nonneg

L58 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.Place.mem_iff_ord_nonneg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem mem_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f

theorem

degree_eq_sum_support

L73 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.Divisor.degree_eq_sum_support

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Divisor in

Lean source · statement

theorem Divisor.degree_eq_sum_support (D : Divisor K F) :
    Divisor.degree D = ∑ v ∈ D.support, D v * (v.deg : ℤ)

theorem

degree_nonneg_of_nonneg

L79 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.Divisor.degree_nonneg_of_nonneg

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}
open scoped _root_.AlgebraicCurve.Divisor in

Lean source · statement

theorem Divisor.degree_nonneg_of_nonneg [IsCurveOver K F]
    {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) : 0 ≤ Divisor.degree D

theorem

lSpace_eq_bot_of_degree_neg

L83 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.lSpace_eq_bot_of_degree_neg

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}

Lean source · statement

theorem lSpace_eq_bot_of_degree_neg [IsCurveOver K F]
    (hD : Divisor.degree D < 0) : LSpace D = ⊥

theorem

ell_eq_zero_of_degree_neg

L99 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.ell_eq_zero_of_degree_neg

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}

Lean source · statement

theorem ell_eq_zero_of_degree_neg [IsCurveOver K F] (hD : Divisor.degree D < 0) :
    ell D = 0

theorem

mk_mem_maximalIdeal_iff

L125 ↗

AlgebraicCurve.Place.mk_mem_maximalIdeal_iff

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
variable (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mk_mem_maximalIdeal_iff {f : F} (hf : f ∈
  v.toValuationSubring) :
    (⟨f, hf⟩ : v.toValuationSubring) ∈ IsLocalRing.maximalIdeal v.toValuationSubring
      ↔ f = 0 ∨ 0 < v.ord f

theorem

ell_le_ell_sub_single_add_deg

L155 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.ell_le_ell_sub_single_add_deg

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_ell_sub_single_add_deg [IsCurveOver K F] (D : Divisor K F) (P : Place K F) :
    ell D ≤ ell (D - Finsupp.single P 1) + P.deg

theorem

one_le_deg

L247 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.one_le_deg

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem one_le_deg [IsCurveOver K F] (P : Place K F) : 1 ≤ P.deg

theorem

ell_le_degree_add_ellZero

L251 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.ell_le_degree_add_ellZero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_degree_add_ellZero [IsCurveOver K F] {D : Divisor K F}
    (hD : ∀ v, 0 ≤ D v) :
    (ell D : ℤ) ≤ Divisor.degree D + ell (0 : Divisor K F)

theorem

ell_le_degree_add_one_of_effective

L288 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.ell_le_degree_add_one_of_effective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_degree_add_one_of_effective [IsCurveOver K F]
    (hC : ConstantsAreBase K F) {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) :
    (ell D : ℤ) ≤ Divisor.degree D + 1

def

lSpaceShiftEquiv

L297 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.lSpaceShiftEquiv

Documentation

Multiplication by the inverse of g identifies the spaces for divisors differing by its divisor.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def lSpaceShiftEquiv (D : Divisor K F) {g : F} (hg : g ≠ 0)
    {Dg : Divisor K F} (hDg : ∀ v, Dg v = v.ord g) :
    LSpace D ≃ₗ[K] LSpace (D + Dg) where
  toFun h := ⟨(h : F) * g⁻¹, by
    rw [mem_lSpace_iff_ord]
    rcases eq_or_ne (h : F) 0 with hh0 | hh0
    · left; rw [hh0, zero_mul]
    · right; intro v
      rw [Finsupp.add_apply, hDg, v.ord_mul hh0 (inv_ne_zero hg), v.ord_inv]
      have := (mem_lSpace_iff_ord.mp h.2).resolve_left hh0 v
      linarith⟩
  invFun k := ⟨(k : F) * g, by
    rw [mem_lSpace_iff_ord]
    rcases eq_or_ne (k : F) 0 with hk0 | hk0
    · left; rw [hk0, zero_mul]
    · right; intro v
      have := (mem_lSpace_iff_ord.mp k.2).resolve_left hk0 v
      rw [Finsupp.add_apply, hDg] at this
      rw [v.ord_mul hk0 hg]
      linarith⟩
  map_add' h₁ h₂ := by apply Subtype.ext; push_cast; ring
  map_smul' c h := by
    apply Subtype.ext
    simp only [RingHom.id_apply, SetLike.val_smul, Algebra.smul_def]
    ring
  left_inv h := by
    apply Subtype.ext
    change (h : F) * g⁻¹ * g = (h : F)
    rw [mul_assoc, inv_mul_cancel₀ hg, mul_one]
  right_inv k := by
    apply Subtype.ext
    change (k : F) * g * g⁻¹ = (k : F)
    rw [mul_assoc, mul_inv_cancel₀ hg, mul_one]

theorem

ell_le_degree_add_one

L331 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.ell_le_degree_add_one

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_degree_add_one [IsCurveOver K F] (hC : ConstantsAreBase K F)
    {D : Divisor K F} (hD : 0 ≤ Divisor.degree D) :
    (ell D : ℤ) ≤ Divisor.degree D + 1

def

nestedComapMapMkQEquiv

L370 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.Submodule.nestedComapMapMkQEquiv

Documentation

Identify the image of B in the quotient of C by A with the induced quotient of B.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

def nestedComapMapMkQEquiv {A B C : Submodule K X} (_hAB : A ≤ B) (hBC : B ≤ C) :
    ((B.comap C.subtype).map (A.comap C.subtype).mkQ : Submodule K _)
      ≃ₗ[K] B ⧸ A.comap B.subtype

theorem

finrank_quotient_chain

L398 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.Submodule.finrank_quotient_chain

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem finrank_quotient_chain {A B C : Submodule K X} (hAB : A ≤ B) (hBC : B ≤ C)
    [hCB : Module.Finite K (C ⧸ B.comap C.subtype)]
    [hBA : Module.Finite K (B ⧸ A.comap B.subtype)] :
    Module.Finite K (C ⧸ A.comap C.subtype) ∧
      finrank K (C ⧸ A.comap C.subtype)
        = finrank K (C ⧸ B.comap C.subtype) + finrank K (B ⧸ A.comap B.subtype)

theorem

finrank_quotient_chain'

L417 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.Submodule.finrank_quotient_chain'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem finrank_quotient_chain' {A B C : Submodule K X} (hAB : A ≤ B) (hBC : B ≤ C)
    [hCA : Module.Finite K (C ⧸ A.comap C.subtype)] :
    Module.Finite K (C ⧸ B.comap C.subtype) ∧
      finrank K (C ⧸ B.comap C.subtype)
        = finrank K (C ⧸ A.comap C.subtype) - finrank K (B ⧸ A.comap B.subtype)

def

adeleBddQuotSingleEquivResidueField

L444 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.adeleBddQuotSingleEquivResidueField

Documentation

The quotient obtained by lowering the bound at one place is linearly equivalent to its residue field.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def adeleBddQuotSingleEquivResidueField (D : Divisor K F) (P : Place K F) :
    (adeleBdd D ⧸ (adeleBdd (D - Finsupp.single P 1)).comap (adeleBdd D).subtype)
      ≃ₗ[K] P.ResidueField

theorem

finrank_adeleBdd_quotient_single

L555 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.finrank_adeleBdd_quotient_single

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBdd_quotient_single [IsCurveOver K F] (D : Divisor K F) (P : Place K F) :
    Module.Finite K
        (adeleBdd D ⧸ (adeleBdd (D - Finsupp.single P 1)).comap (adeleBdd D).subtype) ∧
      finrank K
          (adeleBdd D ⧸ (adeleBdd (D - Finsupp.single P 1)).comap (adeleBdd D).subtype)
        = P.deg

theorem

finrank_adeleBdd_quotient

L565 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.finrank_adeleBdd_quotient

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBdd_quotient [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    Module.Finite K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype) ∧
      (finrank K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype) : ℤ)
        = Divisor.degree D₂ - Divisor.degree D₁

theorem

module_finite_adeleBdd_quotient

L626 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.module_finite_adeleBdd_quotient

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem module_finite_adeleBdd_quotient [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    Module.Finite K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype)

theorem

finrank_adeleBdd_quotient_eq

L630 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.finrank_adeleBdd_quotient_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBdd_quotient_eq [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    (finrank K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype) : ℤ)
      = Divisor.degree D₂ - Divisor.degree D₁

def

lSpaceQuotientToAdeleBddQuotient

L636 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.lSpaceQuotientToAdeleBddQuotient

Documentation

The map between divisor-bounded quotients induced by the diagonal embedding into adeles.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def lSpaceQuotientToAdeleBddQuotient {D₁ D₂ : Divisor K F} (_hD : D₁ ≤ D₂) :
    (LSpace D₂ ⧸ (LSpace D₁).comap (LSpace D₂).subtype)
      →ₗ[K] (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype)

theorem

lSpaceQuotientToAdeleBddQuotient_injective

L647 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.lSpaceQuotientToAdeleBddQuotient_injective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpaceQuotientToAdeleBddQuotient_injective {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    Function.Injective (lSpaceQuotientToAdeleBddQuotient hD)

theorem

ell_sub_ell_le_degree_sub_degree

L660 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.ell_sub_ell_le_degree_sub_degree

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_sub_ell_le_degree_sub_degree [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂)
    [FiniteDimensional K (LSpace D₂)] :
    (ell D₂ : ℤ) - (ell D₁ : ℤ) ≤ Divisor.degree D₂ - Divisor.degree D₁

theorem

adeleBdd_inf_sup_globalSub

L679 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.adeleBdd_inf_sup_globalSub

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBdd_inf_sup_globalSub {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    adeleBdd D₂ ⊓ (adeleBdd D₁ ⊔ globalSub K F)
      = adeleBdd D₁ ⊔ adeleBdd D₂ ⊓ globalSub K F

theorem

map_diagonal_lSpace_inf_adeleBdd

L684 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.map_diagonal_lSpace_inf_adeleBdd

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem map_diagonal_lSpace_inf_adeleBdd {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    (LSpace D₂).map (diagonalHom K F) ⊓ adeleBdd D₁ = (LSpace D₁).map (diagonalHom K F)

theorem

gate_finrank_adeleBdd_quotient_single_point

L689 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_finrank_adeleBdd_quotient_single_point

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_finrank_adeleBdd_quotient_single_point [IsCurveOver K F] (P : Place K F) :
    (finrank K (adeleBdd (Finsupp.single P 1 : Divisor K F)
        ⧸ (adeleBdd (0 : Divisor K F)).comap (adeleBdd (Finsupp.single P 1)).subtype) : ℤ)
      = (P.deg : ℤ)

theorem

comap_subtype_sup_of_le_of_le

L713 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.Submodule.comap_subtype_sup_of_le_of_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem comap_subtype_sup_of_le_of_le {S T C : Submodule K X} (hS : S ≤ C) (hT : T ≤ C) :
    S.comap C.subtype ⊔ T.comap C.subtype = (S ⊔ T).comap C.subtype

theorem

finrank_quotient_chain_top

L720 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.Submodule.finrank_quotient_chain_top

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem finrank_quotient_chain_top {M : Type*} [AddCommGroup M] [Module K M]
    {A B : Submodule K M} (hAB : A ≤ B)
    [hMB : Module.Finite K (M ⧸ B)] [hBA : Module.Finite K (B ⧸ A.comap B.subtype)] :
    Module.Finite K (M ⧸ A) ∧
      finrank K (M ⧸ A) = finrank K (M ⧸ B) + finrank K (B ⧸ A.comap B.subtype)

theorem

globalSub_le_adeleSpace

L751 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.globalSub_le_adeleSpace

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem globalSub_le_adeleSpace [HasPrincipalDivisors K F] :
    globalSub K F ≤ adeleSpace K F

theorem

adeleBdd_sup_globalSub_le_adeleSpace

L756 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.adeleBdd_sup_globalSub_le_adeleSpace

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBdd_sup_globalSub_le_adeleSpace [HasPrincipalDivisors K F] (D : Divisor K F) :
    adeleBdd D ⊔ globalSub K F ≤ adeleSpace K F

theorem

adeleBddPrincipal_eq_comap

L760 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.adeleBddPrincipal_eq_comap

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBddPrincipal_eq_comap [HasPrincipalDivisors K F] (D : Divisor K F) :
    adeleBddPrincipal K F D = (adeleBdd D ⊔ globalSub K F).comap (adeleSpace K F).subtype

theorem

adeleBddPrincipal_mono

L764 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.adeleBddPrincipal_mono

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBddPrincipal_mono {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    adeleBddPrincipal K F D₁ ≤ adeleBddPrincipal K F D₂

theorem

finiteDimensional_lSpace

L773 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.finiteDimensional_lSpace

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section FiniteLSpace
variable [IsCurveOver K F] [Nonempty (Place K F)]
omit [Nonempty (Place K F)] in

Lean source · statement

theorem finiteDimensional_lSpace [hL0 : FiniteDimensional K (LSpace (0 : Divisor K F))]
    (D : Divisor K F) : FiniteDimensional K (LSpace D)

theorem

range_lSpaceQuotientToAdeleBddQuotient

L793 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.range_lSpaceQuotientToAdeleBddQuotient

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem range_lSpaceQuotientToAdeleBddQuotient {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    LinearMap.range (lSpaceQuotientToAdeleBddQuotient hD)
      = ((adeleBdd D₁ ⊔ globalSub K F).comap (adeleBdd D₂).subtype).map
          ((adeleBdd D₁).comap (adeleBdd D₂).subtype).mkQ

theorem

finrank_adeleBddSup_quotient

L834 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.finrank_adeleBddSup_quotient

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBddSup_quotient [IsCurveOver K F] [Nonempty (Place K F)]
    {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) [hL : FiniteDimensional K (LSpace D₂)] :
    Module.Finite K (↥(adeleBdd D₂ ⊔ globalSub K F)
        ⧸ (adeleBdd D₁ ⊔ globalSub K F).comap (adeleBdd D₂ ⊔ globalSub K F).subtype) ∧
      (finrank K (↥(adeleBdd D₂ ⊔ globalSub K F)
          ⧸ (adeleBdd D₁ ⊔ globalSub K F).comap (adeleBdd D₂ ⊔ globalSub K F).subtype) : ℤ)
        = (Divisor.degree D₂ - ell D₂) - (Divisor.degree D₁ - ell D₁)

theorem

adeleBddSup_eq_of_degree_sub_ell_eq

L905 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.adeleBddSup_eq_of_degree_sub_ell_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Index
variable [IsCurveOver K F] [Nonempty (Place K F)]

Lean source · statement

theorem adeleBddSup_eq_of_degree_sub_ell_eq {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂)
    [FiniteDimensional K (LSpace D₂)]
    (heq : Divisor.degree D₂ - ell D₂ = Divisor.degree D₁ - ell D₁) :
    adeleBdd D₂ ⊔ globalSub K F = adeleBdd D₁ ⊔ globalSub K F

theorem

eq_of_ge

L933 ↗

AlgebraicCurve.RiemannGenusReachedAt.eq_of_ge

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace RiemannGenusReachedAt
open scoped _root_.AlgebraicCurve.RiemannGenusReachedAt in

Lean source · statement

theorem _root_.AlgebraicCurve.RiemannGenusReachedAt.eq_of_ge [IsCurveOver K F] [Nonempty
  (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    {D : Divisor K F} (hD : D₀ ≤ D) :
    Divisor.degree D - ell D = γ - 1

theorem

adeleSpace_eq_of_genusReached

L948 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.adeleSpace_eq_of_genusReached

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem adeleSpace_eq_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    adeleSpace K F = adeleBdd D₀ ⊔ globalSub K F

theorem

indexOfSpecialty_eq_zero_of_genusReached

L964 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.indexOfSpecialty_eq_zero_of_genusReached

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem indexOfSpecialty_eq_zero_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    indexOfSpecialty D₀ = 0

theorem

indexOfSpecialty_eq_of_genusReached

L975 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.indexOfSpecialty_eq_of_genusReached

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem indexOfSpecialty_eq_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) (D : Divisor K F) :
    Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D) ∧
      (indexOfSpecialty D : ℤ) = (ell D : ℤ) - (Divisor.degree D + 1 - γ)

theorem

gate_indexOfSpecialty_at_witness

L1022 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_indexOfSpecialty_at_witness

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_indexOfSpecialty_at_witness [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    (indexOfSpecialty D₀ : ℤ) = 0

theorem

gate_riemannInequality_of_genusReached

L1031 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_riemannInequality_of_genusReached

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_riemannInequality_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) (D : Divisor K F) :
    Divisor.degree D + 1 - γ ≤ (ell D : ℤ)

theorem

adeleSpaceMul_add

L1054 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.adeleSpaceMul_add

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleSpaceMul_add [HasPrincipalDivisors K F] (f g : F) :
    adeleSpaceMul K F (f + g) = adeleSpaceMul K F f + adeleSpaceMul K F g

theorem

adeleSpaceMul_zero

L1060 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.adeleSpaceMul_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleSpaceMul_zero [HasPrincipalDivisors K F] :
    adeleSpaceMul K F (0 : F) = 0

theorem

weilSmul_add_left

L1066 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.weilSmul_add_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_add_left [HasPrincipalDivisors K F] (f g : F)
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (f + g) φ = weilSmul K F f φ + weilSmul K F g φ

theorem

weilSmul_zero_left

L1072 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.weilSmul_zero_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_zero_left [HasPrincipalDivisors K F]
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (0 : F) φ = 0

theorem

weilSmul_neg_left

L1078 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.weilSmul_neg_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_neg_left [HasPrincipalDivisors K F] (f : F)
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (-f) φ = -weilSmul K F f φ

theorem

weilSmul_sub_left

L1085 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.weilSmul_sub_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_sub_left [HasPrincipalDivisors K F] (f g : F)
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (f - g) φ = weilSmul K F f φ - weilSmul K F g φ

theorem

weilSmul_eq_zero_iff_left

L1090 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.weilSmul_eq_zero_iff_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_eq_zero_iff_left [HasPrincipalDivisors K F]
    {f : F} {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ≠ 0) :
    weilSmul K F f φ = 0 ↔ f = 0

theorem

weilSmul_left_injective

L1097 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.weilSmul_left_injective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem weilSmul_left_injective [HasPrincipalDivisors K F]
    {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ≠ 0) :
    Function.Injective (fun f : F => weilSmul K F f φ) := by
  intro f g hfg
  have hsub : weilSmul K F (f - g) φ = 0 := by
    rw [weilSmul_sub_left, sub_eq_zero]; exact hfg
  exact sub_eq_zero.mp ((weilSmul_eq_zero_iff_left hφ).mp hsub)

def

doubleResiduePairing

L1107 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.doubleResiduePairing

Documentation

The sum of the two residue pairings on the product of their spaces of sections.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

def doubleResiduePairing [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W) :
    LSpace (W - D) × LSpace (W - D) →ₗ[K] omegaSpace D

theorem

doubleResiduePairing_apply_coe

L1113 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.doubleResiduePairing_apply_coe

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem doubleResiduePairing_apply_coe [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W) (g h : LSpace (W - D)) :
    (doubleResiduePairing K F W D hφ hμ (g, h) : Module.Dual K (adeleSpace K F))
      = weilSmul K F (g : F) φ + weilSmul K F (h : F) μ

theorem

doubleResiduePairing_injective

L1121 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.doubleResiduePairing_injective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem doubleResiduePairing_injective [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W)
    (hφ0 : φ ≠ 0) (hindep : ∀ f : F, μ ≠ weilSmul K F f φ) :
    Function.Injective (doubleResiduePairing K F W D hφ hμ)

theorem

two_mul_ell_le_indexOfSpecialty

L1148 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.two_mul_ell_le_indexOfSpecialty

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem two_mul_ell_le_indexOfSpecialty [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W)
    (hφ0 : φ ≠ 0) (hindep : ∀ f : F, μ ≠ weilSmul K F f φ)
    [Module.Finite K (omegaSpace (K := K) (F := F) D)]
    [Module.Finite K (LSpace (K := K) (F := F) (W - D))] :
    2 * ell (W - D) ≤ indexOfSpecialty D

theorem

omegaSpace_finite_of_genusReached

L1181 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.omegaSpace_finite_of_genusReached

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Finiteness
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]

Lean source · statement

theorem omegaSpace_finite_of_genusReached
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) (D : Divisor K F) :
    Module.Finite K (omegaSpace (K := K) (F := F) D)

theorem

exists_weilSmul_eq_of_genusReached

L1195 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.exists_weilSmul_eq_of_genusReached

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ParametricRankOne
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]

Lean source · statement

theorem exists_weilSmul_eq_of_genusReached
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    {φ μ : Module.Dual K (adeleSpace K F)} {W : Divisor K F}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W) (hφ0 : φ ≠ 0) :
    ∃ f : F, μ = weilSmul K F f φ

theorem

weilDifferentialRankOne_of_genusReached

L1231 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.weilDifferentialRankOne_of_genusReached

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ParametricRankOne
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]

Lean source · statement

theorem weilDifferentialRankOne_of_genusReached
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    WeilDifferentialRankOne K F

theorem

residuePairing_surjective_of_rankOne_max

L1244 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.residuePairing_surjective_of_rankOne_max

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem residuePairing_surjective_of_rankOne_max [HasPrincipalDivisors K F]
    (hRankOne : WeilDifferentialRankOne K F)
    {W : Divisor K F} {φ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hφ0 : φ ≠ 0)
    (hWmax : ∀ E : Divisor K F, φ ∈ omegaSpace E → E ≤ W) (D : Divisor K F) :
    Function.Surjective (residuePairing K F W D hφ)

theorem

exists_riemannGenusReachedAt_of_bounded

L1289 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.exists_riemannGenusReachedAt_of_bounded

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_riemannGenusReachedAt_of_bounded
    [IsCurveOver K F] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hbdd : RiemannGenusBounded K F) :
    ∃ (γ : ℤ) (D₀ : Divisor K F), RiemannGenusReachedAt γ D₀

theorem

stichtenothGenusExists_of_bounded

L1306 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.stichtenothGenusExists_of_bounded

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem stichtenothGenusExists_of_bounded
    [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hbdd : RiemannGenusBounded K F) :
    StichtenothGenusExists K F

theorem

indexOfSpecialty_sub_of_ge

L1314 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.indexOfSpecialty_sub_of_ge

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem indexOfSpecialty_sub_of_ge [IsCurveOver K F] [Nonempty (Place K F)]
    {D₀ D : Divisor K F} (hD : D₀ ≤ D)
    [FiniteDimensional K (LSpace D)]
    [hfin : Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D₀)] :
    Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D) ∧
      (Divisor.degree D - ell D) - (Divisor.degree D₀ - ell D₀)
        = (indexOfSpecialty D₀ : ℤ) - (indexOfSpecialty D : ℤ)

theorem

degreeSub_ell_le_of_indexFinite

L1358 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.degreeSub_ell_le_of_indexFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem degreeSub_ell_le_of_indexFinite [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {D₀ : Divisor K F}
    (hfin : Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D₀))
    (D : Divisor K F) :
    Divisor.degree D - ell D ≤ (Divisor.degree D₀ - ell D₀) + indexOfSpecialty D₀

theorem

riemannGenusBounded_of_indexFinite

L1375 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.riemannGenusBounded_of_indexFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem riemannGenusBounded_of_indexFinite [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hfin : IndexOfSpecialtyFinite K F) :
    RiemannGenusBounded K F

theorem

stichtenothGenusExists_of_indexFinite

L1383 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.stichtenothGenusExists_of_indexFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem stichtenothGenusExists_of_indexFinite
    [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hfin : IndexOfSpecialtyFinite K F) :
    StichtenothGenusExists K F

theorem

indexOfSpecialtyFinite_of_stichtenothGenusExists

L1390 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.indexOfSpecialtyFinite_of_stichtenothGenusExists

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem indexOfSpecialtyFinite_of_stichtenothGenusExists
    [IsCurveOver K F] (hSG : StichtenothGenusExists K F) :
    IndexOfSpecialtyFinite K F

theorem

stichtenothGenusExists_iff_indexFinite

L1404 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.stichtenothGenusExists_iff_indexFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem stichtenothGenusExists_iff_indexFinite
    [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))] :
    StichtenothGenusExists K F ↔ IndexOfSpecialtyFinite K F

theorem

gate_indexOfSpecialty_engine_at_witness

L1411 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_indexOfSpecialty_engine_at_witness

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_indexOfSpecialty_engine_at_witness [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    (indexOfSpecialty D₀ : ℤ) = 0

theorem

gate_stichtenothGenus_le_of_indexFinite

L1417 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_stichtenothGenus_le_of_indexFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_stichtenothGenus_le_of_indexFinite [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {D₀ : Divisor K F}
    (hfin : Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D₀))
    {γ : ℤ} {D₁ : Divisor K F} (h : RiemannGenusReachedAt γ D₁) :
    γ - 1 ≤ (Divisor.degree D₀ - ell D₀) + indexOfSpecialty D₀

theorem

gate_riemannGenusBounded_of_reachedAt

L1426 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_riemannGenusBounded_of_reachedAt

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_riemannGenusBounded_of_reachedAt
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    RiemannGenusBounded K F

theorem

gate_indexOfSpecialtyFinite_at_zero

L1431 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_indexOfSpecialtyFinite_at_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_indexOfSpecialtyFinite_at_zero [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F (0 : Divisor K F))

theorem

mul_mem_lSpace_add

L1452 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.mul_mem_lSpace_add

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mul_mem_lSpace_add {D E : Divisor K F} {f g : F}
    (hf : f ∈ LSpace D) (hg : g ∈ LSpace E) :
    f * g ∈ LSpace (D + E)

theorem

pow_mem_lSpace_nsmul

L1465 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.pow_mem_lSpace_nsmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem pow_mem_lSpace_nsmul {B : Divisor K F} {f : F} (hf : f ∈ LSpace B) (j : ℕ) :
    f ^ j ∈ LSpace (j • B)

theorem

pow_mul_u_mem_lSpace

L1479 ↗

AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace (j : ℕ) (i : Fin
  P.n) :
    P.x ^ j * P.u i ∈ LSpace ((j + P.c) • P.B)

theorem

pow_mul_u_mem_lSpace_of_le

L1487 ↗

AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace_of_le

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)
open _root_.AlgebraicCurve.PoleDivisorPackage

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace_of_le {j m : ℕ} (hjm
  : j + P.c ≤ m) (i : Fin P.n) :
    P.x ^ j * P.u i ∈ LSpace (m • P.B)

theorem

ell_nsmul_poleDivisor_ge

L1499 ↗

AlgebraicCurve.PoleDivisorPackage.ell_nsmul_poleDivisor_ge

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.ell_nsmul_poleDivisor_ge [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))] {m : ℕ} (hm : P.c ≤ m) :
    (P.n : ℤ) * (m - P.c + 1) ≤ ell (m • P.B)

theorem

degree_nsmul_sub_ell_le

L1527 ↗

AlgebraicCurve.PoleDivisorPackage.degree_nsmul_sub_ell_le

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.degree_nsmul_sub_ell_le [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))] {m : ℕ} (hm : P.c ≤ m) :
    Divisor.degree (m • P.B) - ell (m • P.B) ≤ (P.n : ℤ) * (P.c - 1)

theorem

ell_nsmul_sub_pos

L1544 ↗

AlgebraicCurve.PoleDivisorPackage.ell_nsmul_sub_pos

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace PoleDivisorPackage
open scoped _root_.AlgebraicCurve.PoleDivisorPackage in

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.ell_nsmul_sub_pos [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) {A : Divisor K F} (hA : 0 ≤ A) {m : ℕ} (hm : P.c ≤ m)
    (hbig : Divisor.degree A < (P.n : ℤ) * (m - P.c + 1)) :
    0 < ell (m • P.B - A)

theorem

degree_sub_ell_le

L1565 ↗

AlgebraicCurve.PoleDivisorPackage.degree_sub_ell_le

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
namespace PoleDivisorPackage
open scoped _root_.AlgebraicCurve.PoleDivisorPackage in

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.degree_sub_ell_le [IsCurveOver K F]
  [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) (D : Divisor K F) :
    Divisor.degree D - ell D ≤ (P.n : ℤ) * (P.c - 1)

theorem

riemannGenusBounded_of_poleDivisorPackage

L1614 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.riemannGenusBounded_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem riemannGenusBounded_of_poleDivisorPackage [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) :
    RiemannGenusBounded K F

theorem

stichtenothGenusExists_of_poleDivisorPackage

L1620 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.stichtenothGenusExists_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem stichtenothGenusExists_of_poleDivisorPackage [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) :
    StichtenothGenusExists K F

theorem

indexOfSpecialtyFinite_of_poleDivisorPackage

L1626 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.indexOfSpecialtyFinite_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem indexOfSpecialtyFinite_of_poleDivisorPackage [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) :
    IndexOfSpecialtyFinite K F

theorem

indexOfSpecialtyFinite_of_hasPoleDivisorPackage

L1633 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.indexOfSpecialtyFinite_of_hasPoleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem indexOfSpecialtyFinite_of_hasPoleDivisorPackage [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (h : HasPoleDivisorPackage K F) :
    IndexOfSpecialtyFinite K F

theorem

stichtenothGenusExists_of_hasPoleDivisorPackage

L1639 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.stichtenothGenusExists_of_hasPoleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem stichtenothGenusExists_of_hasPoleDivisorPackage [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (h : HasPoleDivisorPackage K F) :
    StichtenothGenusExists K F

theorem

gate_stichtenothGenus_le_of_poleDivisorPackage

L1645 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_stichtenothGenus_le_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_stichtenothGenus_le_of_poleDivisorPackage [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F)
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    γ ≤ (P.n : ℤ) * (P.c - 1) + 1

theorem

gate_ell_c_nsmul_ge

L1653 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_ell_c_nsmul_ge

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_ell_c_nsmul_ge [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) :
    (P.n : ℤ) ≤ ell (P.c • P.B)

theorem

gate_x_transcendental_of_poleDivisorPackage

L1661 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_x_transcendental_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · full declaration

theorem gate_x_transcendental_of_poleDivisorPackage (P : PoleDivisorPackage K F) :
    LinearIndependent K (fun j : ℕ => P.x ^ j * P.u ⟨0, P.hn_pos⟩) := by
  refine P.lin_indep.comp (fun j => (j, ⟨0, P.hn_pos⟩)) ?_
  intro a b hab
  exact (Prod.mk.injEq .. ▸ hab).1

theorem

gate_u_linearIndependent_of_poleDivisorPackage

L1667 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_u_linearIndependent_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_u_linearIndependent_of_poleDivisorPackage (P : PoleDivisorPackage K F) :
    LinearIndependent K P.u

instance

instSumRamificationInertia_port

L1684 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.instSumRamificationInertia_port

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg

Lean source · statement

instance instSumRamificationInertia_port {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F']
    [Algebra F F'] [IsScalarTower K F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    [HasPrincipalDivisors K F'] : SumRamificationInertia K F F'

theorem

x_ne_zero

L1715 ↗

AlgebraicCurve.TranscendenceTower.x_ne_zero

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerPrincipalDivisors
variable [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.x_ne_zero : T.x ≠ 0

theorem

xF_ne_zero

L1720 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.TranscendenceTower.xF_ne_zero

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerPrincipalDivisors
variable [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] in

Lean source · statement

theorem xF_ne_zero : T.xF ≠ 0

theorem

poleDivisor_apply

L1724 ↗

AlgebraicCurve.TranscendenceTower.poleDivisor_apply

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerPrincipalDivisors
variable [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.poleDivisor_apply (w : Place K F) :
    T.poleDivisor w = (w.ramificationIndex E : ℤ) * (Finsupp.single T.v 1) (w.restrict E)

theorem

poleDivisor_nonneg

L1730 ↗

AlgebraicCurve.TranscendenceTower.poleDivisor_nonneg

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerPrincipalDivisors
variable [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.poleDivisor_nonneg : 0 ≤ T.poleDivisor

theorem

xF_mem_lSpace_poleDivisor

L1740 ↗

AlgebraicCurve.TranscendenceTower.xF_mem_lSpace_poleDivisor

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerPrincipalDivisors
variable [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.xF_mem_lSpace_poleDivisor : T.xF ∈ LSpace
  T.poleDivisor

theorem

degree_poleDivisor_eq_finrank_port

L1753 ↗

AlgebraicCurve.TranscendenceTower.degree_poleDivisor_eq_finrank_port

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerPrincipalDivisors
variable [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.degree_poleDivisor_eq_finrank_port :
    Divisor.degree T.poleDivisor = (Module.finrank E F : ℤ)

theorem

mem_lSpace_nsmul_poleDivisor_of_regular_outside

L1760 ↗

AlgebraicCurve.TranscendenceTower.mem_lSpace_nsmul_poleDivisor_of_regular_outside

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerPrincipalDivisors
variable [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] in

Lean source · statement

theorem
  _root_.AlgebraicCurve.TranscendenceTower.mem_lSpace_nsmul_poleDivisor_of_regular_outside {f : F}
    (hreg : ∀ w : Place K F, w.restrict E ≠ T.v → 0 ≤ w.ord f)
    {c : ℕ} (hc : ∀ w ∈ T.v.fiber F, -(c : ℤ) ≤ w.ord f) :
    f ∈ LSpace (c • T.poleDivisor)

theorem

exists_forall_mem_lSpace_nsmul_poleDivisor

L1782 ↗

AlgebraicCurve.TranscendenceTower.exists_forall_mem_lSpace_nsmul_poleDivisor

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
namespace TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerPrincipalDivisors
variable [HasPrincipalDivisors K F]
variable (T : TranscendenceTower K E F)
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
open _root_.AlgebraicCurve.TranscendenceTower
omit [FiniteDimensional E F] in

Lean source · statement

theorem
  _root_.AlgebraicCurve.TranscendenceTower.exists_forall_mem_lSpace_nsmul_poleDivisor {n : ℕ} (u :
  Fin n → F)
    (hreg : ∀ i, ∀ w : Place K F, w.restrict E ≠ T.v → 0 ≤ w.ord (u i)) :
    ∃ c : ℕ, ∀ i, u i ∈ LSpace (c • T.poleDivisor)

def

ofRegularOutside

L1818 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.IntegralBasisInLSpace.ofRegularOutside

Documentation

The integral-basis package built from a basis regular away from the tower place.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section IntegralBasisPrincipalDivisors
variable [HasPrincipalDivisors K F]
open scoped _root_.AlgebraicCurve.IntegralBasisInLSpace in

Lean source · full declaration

def IntegralBasisInLSpace.ofRegularOutside (T : TranscendenceTower K E F)
    (u : Fin (Module.finrank E F) → F) (hu_indep : LinearIndependent E u)
    (hreg : ∀ i, ∀ w : Place K F, w.restrict E ≠ T.v → 0 ≤ w.ord (u i)) :
    IntegralBasisInLSpace T where
  c := (T.exists_forall_mem_lSpace_nsmul_poleDivisor u hreg).choose
  u := u
  hu_indep := hu_indep
  hu_mem := (T.exists_forall_mem_lSpace_nsmul_poleDivisor u hreg).choose_spec

theorem

hasIntegralBasisInLSpace_of_regularOutside

L1828 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.hasIntegralBasisInLSpace_of_regularOutside

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section IntegralBasisPrincipalDivisors
variable [HasPrincipalDivisors K F]
omit [FiniteDimensional E F] in

Lean source · statement

theorem hasIntegralBasisInLSpace_of_regularOutside (T : TranscendenceTower K E F)
    (h : HasIntegralBasisRegularOutside K E F T) :
    HasIntegralBasisInLSpace K E F T

theorem

linearIndependent_pow_mul

L1835 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.linearIndependent_pow_mul

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section IntegralBasisPrincipalDivisors
variable [HasPrincipalDivisors K F]
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] in

Lean source · full declaration

theorem linearIndependent_pow_mul {x : E} {n : ℕ} {u : Fin n → F}
    (hx : LinearIndependent K (fun j : ℕ => x ^ j)) (hu : LinearIndependent E u) :
    LinearIndependent K (fun p : ℕ × Fin n => (algebraMap E F x) ^ p.1 * u p.2) := by
  have heq : (fun p : ℕ × Fin n => (algebraMap E F x) ^ p.1 * u p.2)
      = (fun p : ℕ × Fin n => (x ^ p.1) • u p.2) := by
    funext p
    rw [Algebra.smul_def, map_pow]
  rw [heq]
  exact linearIndependent_smul (R := K) (S := E) (A := F) hx hu

def

ofTranscendenceTower

L1847 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.PoleDivisorPackage.ofTranscendenceTower

Documentation

The pole-divisor data obtained from a transcendence tower and its integral basis.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section IntegralBasisPrincipalDivisors
variable [HasPrincipalDivisors K F]
open scoped _root_.AlgebraicCurve.PoleDivisorPackage in

Lean source · full declaration

def PoleDivisorPackage.ofTranscendenceTower (T : TranscendenceTower K E F)
    (IB : IntegralBasisInLSpace T) :
    PoleDivisorPackage K F where
  x := T.xF
  B := T.poleDivisor
  hB_eff := T.poleDivisor_nonneg
  hx_mem := T.xF_mem_lSpace_poleDivisor
  n := Module.finrank E F
  hn_pos := Module.finrank_pos
  degB_eq := T.degree_poleDivisor_eq_finrank_port
  c := IB.c
  u := IB.u
  hu_mem := IB.hu_mem
  lin_indep := linearIndependent_pow_mul T.hx_indep IB.hu_indep

theorem

hasPoleDivisorPackage_of_transcendenceTower

L1862 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.hasPoleDivisorPackage_of_transcendenceTower

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section IntegralBasisPrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem hasPoleDivisorPackage_of_transcendenceTower
    (T : TranscendenceTower K E F) (IB : IntegralBasisInLSpace T) :
    HasPoleDivisorPackage K F

theorem

hasPoleDivisorPackage_of_hasIntegralBasisInLSpace

L1867 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.hasPoleDivisorPackage_of_hasIntegralBasisInLSpace

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section IntegralBasisPrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem hasPoleDivisorPackage_of_hasIntegralBasisInLSpace
    (T : TranscendenceTower K E F) (h : HasIntegralBasisInLSpace K E F T) :
    HasPoleDivisorPackage K F

theorem

hasPoleDivisorPackage_of_hasIntegralBasisRegularOutside

L1872 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.hasPoleDivisorPackage_of_hasIntegralBasisRegularOutside

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section IntegralBasisPrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem hasPoleDivisorPackage_of_hasIntegralBasisRegularOutside
    (T : TranscendenceTower K E F) (h : HasIntegralBasisRegularOutside K E F T) :
    HasPoleDivisorPackage K F

theorem

indexOfSpecialtyFinite_of_transcendenceTower

L1880 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.indexOfSpecialtyFinite_of_transcendenceTower

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]

Lean source · statement

theorem indexOfSpecialtyFinite_of_transcendenceTower [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (T : TranscendenceTower K E F) (IB : IntegralBasisInLSpace T) :
    IndexOfSpecialtyFinite K F

theorem

stichtenothGenusExists_of_transcendenceTower

L1887 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.stichtenothGenusExists_of_transcendenceTower

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]

Lean source · statement

theorem stichtenothGenusExists_of_transcendenceTower [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (T : TranscendenceTower K E F) (IB : IntegralBasisInLSpace T) :
    StichtenothGenusExists K F

theorem

gate_ofTranscendenceTower_n_eq

L1898 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_ofTranscendenceTower_n_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerGatesPrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem gate_ofTranscendenceTower_n_eq (T : TranscendenceTower K E F)
    (IB : IntegralBasisInLSpace T) :
    (PoleDivisorPackage.ofTranscendenceTower T IB).n = Module.finrank E F

theorem

gate_ofTranscendenceTower_B_eq

L1902 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_ofTranscendenceTower_B_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerGatesPrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem gate_ofTranscendenceTower_B_eq (T : TranscendenceTower K E F)
    (IB : IntegralBasisInLSpace T) :
    (PoleDivisorPackage.ofTranscendenceTower T IB).B = T.poleDivisor

theorem

gate_ofTranscendenceTower_x_transcendental

L1906 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_ofTranscendenceTower_x_transcendental

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerGatesPrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · full declaration

theorem gate_ofTranscendenceTower_x_transcendental (T : TranscendenceTower K E F)
    (IB : IntegralBasisInLSpace T) :
    LinearIndependent K
      (fun j : ℕ => T.xF ^ j *
        (PoleDivisorPackage.ofTranscendenceTower T IB).u ⟨0, Module.finrank_pos⟩) :=
  gate_x_transcendental_of_poleDivisorPackage
    (PoleDivisorPackage.ofTranscendenceTower T IB)

theorem

gate_degree_pullback_single_of_deg_eq

L1914 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_degree_pullback_single_of_deg_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]
section TranscendenceTowerGatesPrincipalDivisors
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem gate_degree_pullback_single_of_deg_eq (v : Place K E) (d : ℕ) (hd : v.deg = d) :
    Divisor.degree (Divisor.pullback F (Finsupp.single v (1 : ℤ)))
      = (Module.finrank E F : ℤ) * d

theorem

gate_stichtenothGenus_le_of_transcendenceTower

L1921 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_stichtenothGenus_le_of_transcendenceTower

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F]

Lean source · statement

theorem gate_stichtenothGenus_le_of_transcendenceTower [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (T : TranscendenceTower K E F) (IB : IntegralBasisInLSpace T)
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    γ ≤ (Module.finrank E F : ℤ) * (IB.c - 1) + 1

theorem

mem_of_isIntegral

L1948 ↗

AlgebraicCurve.Place.mem_of_isIntegral

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_of_isIntegral {f : F} (hf : IsIntegral
  w.toValuationSubring f) :
    f ∈ w.toValuationSubring

theorem

ord_nonneg_of_isIntegral

L1956 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.Place.ord_nonneg_of_isIntegral

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem ord_nonneg_of_isIntegral {f : F} (hf : IsIntegral w.toValuationSubring f) :
    0 ≤ w.ord f

theorem

mem_of_isIntegral_of_algebraMap_mem

L1960 ↗

AlgebraicCurve.Place.mem_of_isIntegral_of_algebraMap_mem

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_of_isIntegral_of_algebraMap_mem {A : Type*}
  [CommRing A] [Algebra A F]
    (hA : ∀ a : A, algebraMap A F a ∈ w.toValuationSubring)
    {f : F} (hf : IsIntegral A f) : f ∈ w.toValuationSubring

theorem

ord_nonneg_of_isIntegral_of_algebraMap_mem

L1972 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.Place.ord_nonneg_of_isIntegral_of_algebraMap_mem

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg mem_iff_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem ord_nonneg_of_isIntegral_of_algebraMap_mem {A : Type*} [CommRing A] [Algebra A F]
    (hA : ∀ a : A, algebraMap A F a ∈ w.toValuationSubring)
    {f : F} (hf : IsIntegral A f) : 0 ≤ w.ord f

theorem

mem_of_isIntegral_of_restrict

L1990 ↗

AlgebraicCurve.Place.mem_of_isIntegral_of_restrict

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Bridge
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable {A : Type*} [CommRing A] [Algebra A E] [Algebra A F] [IsScalarTower A E F]
namespace Place
open scoped _root_.AlgebraicCurve.Place in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_of_isIntegral_of_restrict [Algebra.IsIntegral E F]
  (w : Place K F)
    {u : Place K E} (hw : w.restrict E = u)
    (hA : ∀ a : A, algebraMap A E a ∈ u.toValuationSubring)
    {f : F} (hf : IsIntegral A f) : f ∈ w.toValuationSubring

theorem

ord_nonneg_of_isIntegral_of_restrict

L2003 ↗

AlgebraicCurve.Place.ord_nonneg_of_isIntegral_of_restrict

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Bridge
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable {A : Type*} [CommRing A] [Algebra A E] [Algebra A F] [IsScalarTower A E F]
open _root_.AlgebraicCurve
namespace Place
open scoped _root_.AlgebraicCurve.Place in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_isIntegral_of_restrict
  [Algebra.IsIntegral E F] (w : Place K F)
    {u : Place K E} (hw : w.restrict E = u)
    (hA : ∀ a : A, algebraMap A E a ∈ u.toValuationSubring)
    {f : F} (hf : IsIntegral A f) : 0 ≤ w.ord f

theorem

ord_nonneg_of_isIntegral_of_regularOutside

L2017 ↗

AlgebraicCurve.TranscendenceTower.ord_nonneg_of_isIntegral_of_regularOutside

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Bridge
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable {A : Type*} [CommRing A] [Algebra A E] [Algebra A F] [IsScalarTower A E F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace TranscendenceTower
open scoped _root_.AlgebraicCurve.TranscendenceTower in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.ord_nonneg_of_isIntegral_of_regularOutside
    [Algebra.IsIntegral E F] (T : TranscendenceTower K E F) (hA : T.RegularOutside A)
    {f : F} (hf : IsIntegral A f) :
    ∀ w : Place K F, w.restrict E ≠ T.v → 0 ≤ w.ord f

theorem

linearIndependent_reindex_basis

L2034 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.linearIndependent_reindex_basis

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] in

Lean source · full declaration

theorem linearIndependent_reindex_basis {s : Finset F} (b : Basis s E F) :
    LinearIndependent E (fun i : Fin (Module.finrank E F) =>
      b ((Fintype.equivFinOfCardEq (Module.finrank_eq_card_basis b).symm).symm i)) :=
  b.linearIndependent.comp _ (Equiv.injective _)

theorem

hasIntegralBasisRegularOutside_of_isFractionRing

L2040 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.hasIntegralBasisRegularOutside_of_isFractionRing

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem hasIntegralBasisRegularOutside_of_isFractionRing
    {A : Type*} [CommRing A] [IsDomain A] [Algebra A E] [IsFractionRing A E]
    [Algebra A F] [IsScalarTower A E F]
    (T : TranscendenceTower K E F) (hA : T.RegularOutside A) :
    HasIntegralBasisRegularOutside K E F T

theorem

hasIntegralBasisRegularOutside_of_hasRegularFractionSubring

L2052 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.hasIntegralBasisRegularOutside_of_hasRegularFractionSubring

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem hasIntegralBasisRegularOutside_of_hasRegularFractionSubring
    (T : TranscendenceTower K E F) (h : HasRegularFractionSubring K E F T) :
    HasIntegralBasisRegularOutside K E F T

theorem

hasPoleDivisorPackage_of_isFractionRing

L2060 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.hasPoleDivisorPackage_of_isFractionRing

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]

Lean source · statement

theorem hasPoleDivisorPackage_of_isFractionRing
    {A : Type*} [CommRing A] [IsDomain A] [Algebra A E] [IsFractionRing A E]
    [Algebra A F] [IsScalarTower A E F]
    (T : TranscendenceTower K E F) (hA : T.RegularOutside A) :
    HasPoleDivisorPackage K F

theorem

stichtenothGenusExists_of_isFractionRing

L2069 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.stichtenothGenusExists_of_isFractionRing

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem stichtenothGenusExists_of_isFractionRing [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {A : Type*} [CommRing A] [IsDomain A] [Algebra A E] [IsFractionRing A E]
    [Algebra A F] [IsScalarTower A E F]
    (T : TranscendenceTower K E F) (hA : T.RegularOutside A) :
    StichtenothGenusExists K F

theorem

hasPoleDivisorPackage_of_hasRegularFractionSubring

L2078 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.hasPoleDivisorPackage_of_hasRegularFractionSubring

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]

Lean source · statement

theorem hasPoleDivisorPackage_of_hasRegularFractionSubring
    (T : TranscendenceTower K E F) (h : HasRegularFractionSubring K E F T) :
    HasPoleDivisorPackage K F

theorem

stichtenothGenusExists_of_hasRegularFractionSubring

L2085 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.stichtenothGenusExists_of_hasRegularFractionSubring

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem stichtenothGenusExists_of_hasRegularFractionSubring [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (T : TranscendenceTower K E F) (h : HasRegularFractionSubring K E F T) :
    StichtenothGenusExists K F

theorem

adjoin_x_regularOutside

L2095 ↗

AlgebraicCurve.TranscendenceTower.adjoin_x_regularOutside

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
namespace TranscendenceTower
open scoped _root_.AlgebraicCurve.TranscendenceTower in
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.adjoin_x_regularOutside (T :
  TranscendenceTower K E F) :
    ∀ u : Place K E, u ≠ T.v →
      ∀ a ∈ Algebra.adjoin K {T.x}, a ∈ u.toValuationSubring

theorem

hasRegularFractionSubring_of_adjoin_x_isFractionRing

L2114 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.hasRegularFractionSubring_of_adjoin_x_isFractionRing

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve
omit [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F] in

Lean source · statement

theorem hasRegularFractionSubring_of_adjoin_x_isFractionRing
    (T : TranscendenceTower K E F)
    (hfrac : IsFractionRing (Algebra.adjoin K {T.x}) E) :
    HasRegularFractionSubring K E F T

theorem

hasIntegralBasisRegularOutside_of_adjoin_x_isFractionRing

L2121 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.hasIntegralBasisRegularOutside_of_adjoin_x_isFractionRing

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem hasIntegralBasisRegularOutside_of_adjoin_x_isFractionRing
    (T : TranscendenceTower K E F)
    (hfrac : IsFractionRing (Algebra.adjoin K {T.x}) E) :
    HasIntegralBasisRegularOutside K E F T

theorem

stichtenothGenusExists_of_adjoin_x_isFractionRing

L2129 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.stichtenothGenusExists_of_adjoin_x_isFractionRing

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Headline
variable {K E F : Type*} [Field K] [Field E] [Field F]
  [Algebra K E] [Algebra K F] [Algebra E F] [IsScalarTower K E F]
variable [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K F]
open _root_.AlgebraicCurve
omit [HasPrincipalDivisors K F] in

Lean source · statement

theorem stichtenothGenusExists_of_adjoin_x_isFractionRing [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (T : TranscendenceTower K E F)
    (hfrac : IsFractionRing (Algebra.adjoin K {T.x}) E) :
    StichtenothGenusExists K F

theorem

gate_mem_of_isIntegral_recovers_comap

L2143 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_mem_of_isIntegral_recovers_comap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_mem_of_isIntegral_recovers_comap (w : Place K F) (E : Type*) [Field E]
    [Algebra E F] [Algebra.IsIntegral E F]
    (hE : ∀ a : E, algebraMap E F a ∈ w.toValuationSubring) (f : F) :
    f ∈ w.toValuationSubring

theorem

gate_bridge_recovers_hxreg

L2155 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_bridge_recovers_hxreg

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]

Lean source · statement

theorem gate_bridge_recovers_hxreg [Algebra.IsIntegral E F]
    (T : TranscendenceTower K E F) (w : Place K F) (hw : w.restrict E ≠ T.v) :
    0 ≤ w.ord T.xF

theorem

gate_regularOutside_mono

L2161 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_regularOutside_mono

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]

Lean source · statement

theorem gate_regularOutside_mono (T : TranscendenceTower K E F) {A A' : Subalgebra K E}
    (hle : A ≤ A')
    (hA' : ∀ u : Place K E, u ≠ T.v → ∀ a ∈ A', a ∈ u.toValuationSubring) :
    ∀ u : Place K E, u ≠ T.v → ∀ a ∈ A, a ∈ u.toValuationSubring

theorem

gate_bot_regularOutside

L2167 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_bot_regularOutside

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]

Lean source · statement

theorem gate_bot_regularOutside (T : TranscendenceTower K E F) :
    ∀ u : Place K E, u ≠ T.v → ∀ a ∈ (⊥ : Subalgebra K E), a ∈ u.toValuationSubring

theorem

gate_adjoin_x_not_regular_at_v

L2173 ↗

AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole.AlgebraicCurve.gate_adjoin_x_not_regular_at_v

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.ord_nonneg_of_mem Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower K E F]

Lean source · statement

theorem gate_adjoin_x_not_regular_at_v (T : TranscendenceTower K E F) :
    ¬ ∀ a ∈ Algebra.adjoin K {T.x}, a ∈ T.v.toValuationSubring

theorem

degree_poleDivisor_eq_finrank

L2192 ↗

AlgebraicCurve.TranscendenceTower.degree_poleDivisor_eq_finrank

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.TranscendenceTowerDegreePole
open _root_.AlgebraicCurves.FunctionFields.Proofs in
open _root_.AlgebraicCurve hiding
  Place.ord_nonneg_of_mem
  Place.mem_of_ord_nonneg
  Place.mem_iff_ord_nonneg in
open TranscendenceTowerDegreePole.AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.TranscendenceTower.degree_poleDivisor_eq_finrank {K : Type*} {E :
  Type*} {F : Type*} [Field K] [Field E] [Field F] [Algebra K E] [Algebra K F] [Algebra E F]
  [IsScalarTower K E F] [FiniteDimensional E F] [Algebra.IsSeparable E F] [HasPrincipalDivisors K
  F] (T : TranscendenceTower K E F) :
    Divisor.degree T.poleDivisor = (Module.finrank E F : ℤ)

Module documentation

Transcendence Tower degree pole Divisor eq finrank

Declarations