Module

Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.lean

Nyll.AlgebraicCurves.Divisors.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite

50 declarations indexed from sourceView source ↗

Module documentation

Divisor exists torsion descent of constant Field Extension of finite

Imports23

Imported by1

Nyll.AlgebraicCurves.Divisors.All

def

divOf

L78 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.divOf

Documentation

A principal divisor of a nonzero function, with the zero divisor assigned to zero.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open Classical in

Lean source · statement

def divOf [HasPrincipalDivisors K F] (f : F) : Divisor K F

theorem

divOf_apply

L81 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.divOf_apply

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem divOf_apply [HasPrincipalDivisors K F] {f : F} (hf : f ≠ 0) (v : Place K F) :
    divOf f v = v.ord f

theorem

divOf_zero

L86 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.divOf_zero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem divOf_zero [HasPrincipalDivisors K F] : divOf (K := K) (0 : F) = 0

theorem

degree_divOf

L89 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.degree_divOf

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem degree_divOf [HasPrincipalDivisors K F] (f : F) :
    Divisor.degree (divOf (K := K) f) = 0

theorem

divOf_mem_principal

L96 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.divOf_mem_principal

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem divOf_mem_principal [HasPrincipalDivisors K F] {f : F} (hf : f ≠ 0) :
    divOf (K := K) f ∈ Divisor.principal

theorem

isPrincipal_iff_eq_divOf

L100 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.isPrincipal_iff_eq_divOf

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem isPrincipal_iff_eq_divOf [HasPrincipalDivisors K F] {D : Divisor K F} :
    D.IsPrincipal ↔ ∃ f : F, f ≠ 0 ∧ D = divOf f

theorem

mem_principal_iff_eq_divOf

L108 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.mem_principal_iff_eq_divOf

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_principal_iff_eq_divOf [HasPrincipalDivisors K F] {D : Divisor K F} :
    D ∈ Divisor.principal ↔ ∃ f : F, f ≠ 0 ∧ D = divOf f

theorem

divOf_mul

L112 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.divOf_mul

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem divOf_mul [HasPrincipalDivisors K F] {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) :
    divOf (K := K) (f * g) = divOf f + divOf g

theorem

divOf_inv

L118 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.divOf_inv

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem divOf_inv [HasPrincipalDivisors K F] (f : F) :
    divOf (K := K) f⁻¹ = -divOf f

theorem

divOf_pow

L125 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.divOf_pow

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem divOf_pow [HasPrincipalDivisors K F] (f : F) (n : ℕ) :
    divOf (K := K) (f ^ n) = (n : ℤ) • divOf f

theorem

divOf_smul_const

L144 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.divOf_smul_const

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem divOf_smul_const [HasPrincipalDivisors K F] {c : K} (hc : c ≠ 0) (f : F) :
    divOf (K := K) (c • f) = divOf f

theorem

divOf_algebraMap

L151 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.divOf_algebraMap

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem divOf_algebraMap [HasPrincipalDivisors K F] (c : K) :
    divOf (K := K) (algebraMap K F c) = 0

theorem

ord_smul_eq

L159 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.ord_smul_eq

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ord_smul_eq (g : SemilinearAut K F) (w : Place K F) (f : F) :
    w.ord (g • f) = (g⁻¹ • w).ord f

theorem

smul_divOf

L164 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.smul_divOf

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem smul_divOf [HasPrincipalDivisors K F] (g : SemilinearAut K F) (f : F) :
    g • divOf (K := K) f = divOf (g • f)

theorem

pow_smul_eq_self

L174 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.pow_smul_eq_self

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem pow_smul_eq_self {α : Type*} [MulAction (SemilinearAut K F) α] {g : SemilinearAut K F}
    {a : α} (h : g • a = a) (k : ℕ) : g ^ k • a = a

theorem

smul_zsmul_divisor

L180 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.smul_zsmul_divisor

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem smul_zsmul_divisor (g : SemilinearAut K F) (m : ℤ) (D : Divisor K F) :
    g • (m • D) = m • (g • D)

theorem

mem_lSpace_add_divOf_iff

L184 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.mem_lSpace_add_divOf_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_lSpace_add_divOf_iff [HasPrincipalDivisors K F] {D : Divisor K F} {u : F}
    (hu : u ≠ 0) {y : F} :
    y ∈ LSpace (D + divOf u) ↔ y * u ∈ LSpace D

theorem

smul_mem_lSpace_iff

L203 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.smul_mem_lSpace_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem smul_mem_lSpace_iff (g : SemilinearAut K F) {D : Divisor K F} {y : F} :
    g • y ∈ LSpace (g • D) ↔ y ∈ LSpace D

theorem

divOf_add_mem_lSpace

L212 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.divOf_add_mem_lSpace

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem divOf_add_mem_lSpace [HasPrincipalDivisors K F] {D : Divisor K F} {f : F} (hf0 : f ≠ 0)
    (hf : f ∈ LSpace D) : 0 ≤ D + divOf f

theorem

constantsAreBase_of_isAlgClosed

L219 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.constantsAreBase_of_isAlgClosed

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem constantsAreBase_of_isAlgClosed [IsAlgClosed K] [IsCurveOver K F]
    (j : F) (hj : Transcendental K j)
    [FiniteDimensional (IntermediateField.adjoin K ({j} : Set F)) F] :
    ConstantsAreBase K F

theorem

exists_riemann_inequality

L253 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.exists_riemann_inequality

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_riemann_inequality [IsAlgClosed K] [IsCurveOver K F]
    (j : F) (hj : Transcendental K j)
    [hfd : FiniteDimensional (IntermediateField.adjoin K ({j} : Set F)) F] :
    ∃ γ : ℤ, ∀ D : Divisor K F, Divisor.degree D + 1 - γ ≤ (ell D : ℤ)

theorem

exists_reduced

L267 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.exists_reduced

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_reduced [IsAlgClosed K] [IsCurveOver K F]
    (j : F) (hj : Transcendental K j)
    [FiniteDimensional (IntermediateField.adjoin K ({j} : Set F)) F]
    (c : Divisor K F) (hc : Divisor.degree c = 0) (P : Place K F) :
    ∃ (r : ℕ) (f : F), f ≠ 0 ∧ f ∈ LSpace (c + (r : ℤ) • Finsupp.single P 1) ∧
      ∀ h ∈ LSpace (c + (r : ℤ) • Finsupp.single P 1), ∃ a : K, a • f = h

theorem

smul_reduced_eq

L327 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.smul_reduced_eq

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section General
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem smul_reduced_eq [HasPrincipalDivisors K F] (g : SemilinearAut K F)
    {c : Divisor K F} {r : ℤ} {P : Place K F} {f : F} (hf0 : f ≠ 0)
    (hf : f ∈ LSpace (c + r • Finsupp.single P 1))
    (huniq : ∀ h ∈ LSpace (c + r • Finsupp.single P 1), ∃ a : K, a • f = h)
    (hP : g • P = P) (hc : g • c - c ∈ Divisor.principal) :
    g • (c + r • Finsupp.single P 1 + divOf f) = c + r • Finsupp.single P 1 + divOf f

def

LiesOver

L358 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.LiesOver

Documentation

The condition that a place restricts to the specified place of the original function field.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']

Lean source · statement

def LiesOver (w' : Place K' F') (v : Place K F) : Prop

def

IsGeneric

L362 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.IsGeneric

Documentation

The condition that the place does not lie over any place of the original function field.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']

Lean source · statement

def IsGeneric (K F : Type*) [Field K] [Field F] [Algebra K F] [Algebra F F']
    (w' : Place K' F') : Prop

def

FixesF

L368 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.FixesF

Documentation

The condition that a semilinear automorphism fixes the image of the original function field.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']

Lean source · statement

def FixesF (F : Type*) [Field F] [Algebra F F'] (g : SemilinearAut K' F') : Prop

theorem

one

L375 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.FixesF.one

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
namespace FixesF
variable {g h : SemilinearAut K' F'}

Lean source · statement

theorem one : FixesF F (1 : SemilinearAut K' F')

theorem

mul

L377 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.FixesF.mul

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
namespace FixesF
variable {g h : SemilinearAut K' F'}

Lean source · statement

theorem mul (hg : FixesF F g) (hh : FixesF F h) : FixesF F (g * h)

theorem

inv

L380 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.FixesF.inv

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
namespace FixesF
variable {g h : SemilinearAut K' F'}

Lean source · statement

theorem inv (hg : FixesF F g) : FixesF F g⁻¹

theorem

pow

L383 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.FixesF.pow

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
namespace FixesF
variable {g h : SemilinearAut K' F'}

Lean source · statement

theorem pow (hg : FixesF F g) (k : ℕ) : FixesF F (g ^ k)

theorem

comap_smul

L388 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.FixesF.comap_smul

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
namespace FixesF
variable {g h : SemilinearAut K' F'}

Lean source · statement

theorem comap_smul (hg : FixesF F g) (w' : Place K' F') :
    (g • w').toValuationSubring.comap (algebraMap F F') =
      w'.toValuationSubring.comap (algebraMap F F')

theorem

liesOver_smul_iff

L396 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.FixesF.liesOver_smul_iff

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
namespace FixesF
variable {g h : SemilinearAut K' F'}

Lean source · statement

theorem liesOver_smul_iff (hg : FixesF F g) {w' : Place K' F'} {v : Place K F} :
    LiesOver (g • w') v ↔ LiesOver w' v

theorem

isGeneric_smul_iff

L400 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.FixesF.isGeneric_smul_iff

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
namespace FixesF
variable {g h : SemilinearAut K' F'}

Lean source · statement

theorem isGeneric_smul_iff (hg : FixesF F g) {w' : Place K' F'} :
    IsGeneric K F (g • w') ↔ IsGeneric K F w'

theorem

smul_eq_of_liesOver

L404 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.FixesF.smul_eq_of_liesOver

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
namespace FixesF
variable {g h : SemilinearAut K' F'}

Lean source · statement

theorem smul_eq_of_liesOver (hg : FixesF F g)
    (hU : ∀ (v : Place K F) (w₁ w₂ : Place K' F'), LiesOver w₁ v → LiesOver w₂ v → w₁ = w₂)
    {w' : Place K' F'} {v : Place K F} (hw : LiesOver w' v) : g • w' = w'

theorem

comap_eq_top

L415 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.IsGeneric.comap_eq_top

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
section Tower
variable [Algebra K K'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']

Lean source · statement

theorem IsGeneric.comap_eq_top [CharZero K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {w' : Place K' F'} (hw : IsGeneric K F w') :
    w'.toValuationSubring.comap (algebraMap F F') = ⊤

theorem

algebraMap_mem

L427 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.IsGeneric.algebraMap_mem

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
section Tower
variable [Algebra K K'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']

Lean source · statement

theorem IsGeneric.algebraMap_mem [CharZero K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {w' : Place K' F'} (hw : IsGeneric K F w') (y : F) :
    algebraMap F F' y ∈ w'.toValuationSubring

theorem

ord_algebraMap

L434 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.IsGeneric.ord_algebraMap

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
section Tower
variable [Algebra K K'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']

Lean source · statement

theorem IsGeneric.ord_algebraMap [CharZero K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {w' : Place K' F'} (hw : IsGeneric K F w') (y : F) :
    w'.ord (algebraMap F F' y) = 0

def

InMax

L450 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.InMax

Documentation

The condition that an element is zero or has strictly positive order at the place.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']

Lean source · statement

def InMax (w : Place K' F') (y : F') : Prop

theorem

sub

L452 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.InMax.sub

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']

Lean source · statement

theorem InMax.sub {w : Place K' F'} {a b : F'} (ha : InMax w a) (hb : InMax w b) :
    InMax w (a - b)

theorem

eq_zero_of_algebraMap

L472 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.InMax.eq_zero_of_algebraMap

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']

Lean source · statement

theorem InMax.eq_zero_of_algebraMap {w : Place K' F'} {c : K'} (h : InMax w (algebraMap K' F' c)) :
    c = 0

theorem

smul_iff

L479 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.InMax.smul_iff

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']

Lean source · statement

theorem InMax.smul_iff (g : SemilinearAut K' F') {w : Place K' F'} {y : F'} :
    InMax (g • w) (g • y) ↔ InMax w y

theorem

injective_pow_smul

L483 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.injective_pow_smul

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']

Lean source · full declaration

theorem injective_pow_smul [CharZero K'] (g : SemilinearAut K' F') (w : Place K' F') (y : F')
    (hy : InMax w y) (hg : ∀ k : ℕ, g ^ k • y = y - algebraMap K' F' k) :
    Function.Injective fun k : ℕ => g ^ k • w := by
  intro i j hij
  simp only at hij
  have hi : InMax (g ^ i • w) (y - algebraMap K' F' i) := by
    rw [← hg i]; exact (InMax.smul_iff _).mpr hy
  have hj : InMax (g ^ i • w) (y - algebraMap K' F' j) := by
    rw [hij, ← hg j]; exact (InMax.smul_iff _).mpr hy
  have h := hi.sub hj
  rw [show y - algebraMap K' F' (i : K') - (y - algebraMap K' F' (j : K')) =
      algebraMap K' F' ((j : K') - i) by rw [map_sub]; ring] at h
  have := h.eq_zero_of_algebraMap
  exact_mod_cast (sub_eq_zero.mp this).symm

theorem

exists_inMax_sub

L502 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.IsGeneric.exists_inMax_sub

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
section Tower
variable [Algebra K K'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']

Lean source · statement

theorem IsGeneric.exists_inMax_sub [CharZero K] [IsAlgClosed K'] [IsCurveOver K' F'] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {w' : Place K' F'} (hw : IsGeneric K F w') :
    ∃ t : K', InMax w' (algebraMap F F' x - algebraMap K' F' t)

theorem

not_mem_range

L522 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.IsGeneric.not_mem_range

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']
section Tower
variable [Algebra K K'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']

Lean source · statement

theorem IsGeneric.not_mem_range [CharZero K] (x : F) (hx : Transcendental K x)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {w' : Place K' F'} (hw : IsGeneric K F w') {t : K'}
    (ht : InMax w' (algebraMap F F' x - algebraMap K' F' t)) :
    t ∉ Set.range (algebraMap K K')

theorem

transcendental_of_not_mem_range

L543 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.transcendental_of_not_mem_range

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']

Lean source · statement

theorem transcendental_of_not_mem_range [Algebra K K'] [IsAlgClosed K] {t : K'}
    (ht : t ∉ Set.range (algebraMap K K')) : Transcendental K t

theorem

pow_smul_sub_algebraMap

L550 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.pow_smul_sub_algebraMap

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Extension
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra F F']

Lean source · statement

theorem pow_smul_sub_algebraMap (ρ : SemilinearAut K' F') {X : F'} (hX : ρ • X = X) {t a : K'}
    (ht : SemilinearAut.baseAut ρ t = t + a) (ha : SemilinearAut.baseAut ρ a = a) (m : ℕ) :
    ρ ^ m • (X - algebraMap K' F' t) = X - algebraMap K' F' t - algebraMap K' F' (m * a)

theorem

pow_mul_smul_sub_mem_principal

L567 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.pow_mul_smul_sub_mem_principal

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Pigeonhole
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem pow_mul_smul_sub_mem_principal (g : SemilinearAut K F) (D : Divisor K F) (m : ℕ)
    (h : g ^ m • D - D ∈ Divisor.principal) (q : ℕ) :
    g ^ (m * q) • D - D ∈ Divisor.principal

theorem

pow_factorial_smul_sub_mem_principal

L579 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.pow_factorial_smul_sub_mem_principal

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Pigeonhole
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem pow_factorial_smul_sub_mem_principal (g : SemilinearAut K F) (D : Divisor K F) (n : ℕ)
    [Finite {c : Pic0 K F // n • c = 0}]
    (hdeg : ∀ k : ℕ, Divisor.degree (g ^ k • D - D) = 0)
    (htor : ∀ k : ℕ, n • (g ^ k • D - D) ∈ Divisor.principal) :
    g ^ (Nat.card {c : Pic0 K F // n • c = 0}).factorial • D - D ∈ Divisor.principal

theorem

main

L632 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite.AlgebraicCurve.TorsionDescentFin.main

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace TorsionDescentFin
section Main
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
  [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']

Lean source · statement

theorem main [IsAlgClosed K] [CharZero K] [IsAlgClosed K']
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    [IsCurveOver K F] [IsCurveOver K' F']
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    (n : ℕ) (_hn : n ≠ 0) [Finite {c : Pic0 K' F' // n • c = 0}] (D' : Divisor K' F')
    (hD' : ∃ g' : F', g' ≠ 0 ∧ ∀ v' : Place K' F', (n : ℤ) * D' v' = v'.ord g') :
    ∃ (D : Divisor K F) (h' : F'), h' ≠ 0 ∧
      (∃ g : F, g ≠ 0 ∧ ∀ v : Place K F, (n : ℤ) * D v = v.ord g) ∧
      (∀ (v : Place K F) (v' : Place K' F'),
        v'.toValuationSubring.comap (algebraMap F F') = v.toValuationSubring →
          D' v' = D v + v'.ord h') ∧
      (∀ v' : Place K' F',
        (∀ v : Place K F, v'.toValuationSubring.comap (algebraMap F F') ≠ v.toValuationSubring) →
          D' v' = v'.ord h')

theorem

exists_torsion_descent_of_constantFieldExtension_of_finite

L799 ↗

AlgebraicCurve.Divisor.exists_torsion_descent_of_constantFieldExtension_of_finite

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs
namespace Divisor_exists_torsion_descent_of_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open scoped Pointwise
open _root_.AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Divisor.exists_torsion_descent_of_constantFieldExtension_of_finite
    (K F K' F' : Type*) [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [IsAlgClosed K] [CharZero K] [IsAlgClosed K']
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    [IsCurveOver K F] [IsCurveOver K' F']
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    (n : ℕ) (hn : n ≠ 0) (hfin : Finite {c : Pic0 K' F' // n • c = 0}) (D' : Divisor K' F')
    (hD' : ∃ g' : F', g' ≠ 0 ∧ ∀ v' : Place K' F', (n : ℤ) * D' v' = v'.ord g') :
    ∃ (D : Divisor K F) (h' : F'), h' ≠ 0 ∧
      (∃ g : F, g ≠ 0 ∧ ∀ v : Place K F, (n : ℤ) * D v = v.ord g) ∧
      (∀ (v : Place K F) (v' : Place K' F'),
        v'.toValuationSubring.comap (algebraMap F F') = v.toValuationSubring →
          D' v' = D v + v'.ord h') ∧
      (∀ v' : Place K' F',
        (∀ v : Place K F, v'.toValuationSubring.comap (algebraMap F F') ≠ v.toValuationSubring) →
          D' v' = v'.ord h')

Module documentation

Divisor exists torsion descent of constant Field Extension of finite

Declarations