Module

RationalFunctionField_trace_localResidue_finitePlace_div_pow_eq_zero.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_trace_localResidue_finitePlace_div_pow_eq_zero

124 declarations indexed from sourceView source ↗

Module documentation

Rational Function Field trace local Residue finite Place div pow eq zero

Imports41

Imported by3

instance

instIsCurveOver

L91 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField.instIsCurveOver

Source context 15 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve

Lean source · statement

instance instIsCurveOver (K : Type*) [Field K] : IsCurveOver K (RatFunc K)

instance

instHasPrincipalDivisors

L94 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField.instHasPrincipalDivisors

Source context 15 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve

Lean source · statement

instance instHasPrincipalDivisors (K : Type*) [Field K] : HasPrincipalDivisors K (RatFunc K)

theorem

coeff_minpolyDiv_dim_sub_one

L148 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.FLT.EulerDualBasis.coeff_minpolyDiv_dim_sub_one

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
open _root_.Polynomial
open _root_.Module
open _root_.Algebra
namespace FLT
namespace EulerDualBasis
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
omit [FiniteDimensional K L] [Algebra.IsSeparable K L] in

Lean source · statement

theorem coeff_minpolyDiv_dim_sub_one (pb : PowerBasis K L) :
    (minpolyDiv K pb.gen).coeff (pb.dim - 1) = 1

theorem

traceDual_eq_one_div_of_val_eq

L155 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.FLT.EulerDualBasis.traceDual_eq_one_div_of_val_eq

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
open _root_.Polynomial
open _root_.Module
open _root_.Algebra
namespace FLT
namespace EulerDualBasis
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]

Lean source · statement

theorem traceDual_eq_one_div_of_val_eq (pb : PowerBasis K L) {j : Fin pb.dim}
    (hj : (j : ℕ) = pb.dim - 1) :
    pb.basis.traceDual j = 1 / aeval pb.gen (derivative (minpoly K pb.gen))

theorem

trace_pow_div_aeval_derivative_minpoly_of_lt

L161 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.FLT.EulerDualBasis.trace_pow_div_aeval_derivative_minpoly_of_lt

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
open _root_.Polynomial
open _root_.Module
open _root_.Algebra
namespace FLT
namespace EulerDualBasis
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]

Lean source · statement

theorem trace_pow_div_aeval_derivative_minpoly_of_lt (pb : PowerBasis K L) {k : ℕ}
    (hk : k < pb.dim - 1) :
    Algebra.trace K L
      (pb.gen ^ k / aeval pb.gen (derivative (minpoly K pb.gen))) = 0

theorem

trace_pow_div_aeval_derivative_minpoly_self

L174 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.FLT.EulerDualBasis.trace_pow_div_aeval_derivative_minpoly_self

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
open _root_.Polynomial
open _root_.Module
open _root_.Algebra
namespace FLT
namespace EulerDualBasis
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]

Lean source · statement

theorem trace_pow_div_aeval_derivative_minpoly_self (pb : PowerBasis K L)
    (hd : 0 < pb.dim) :
    Algebra.trace K L
      (pb.gen ^ (pb.dim - 1) / aeval pb.gen (derivative (minpoly K pb.gen))) = 1

theorem

ord_add_eq_left

L202 ↗

AlgebraicCurve.Place.ord_add_eq_left

Source context 25 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.Polynomial
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Ultrametric
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_add_eq_left {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) (h
  : v.ord f < v.ord g) :
    v.ord (f + g) = v.ord f

theorem

ord_finitePlace_ne_zero_iff

L239 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField.ord_finitePlace_ne_zero_iff

Source context 23 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem ord_finitePlace_ne_zero_iff {p : K[X]} (hp : Irreducible p) {q : K[X]} (hq : q ≠ 0) :
    (finitePlace K hp).ord (algebraMap K[X] (RatFunc K) q) ≠ 0 ↔ p ∣ q

theorem

exists_sub_algebraMap_intDegree_neg

L247 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField.exists_sub_algebraMap_intDegree_neg

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
section DegInfty
variable (K) [DecidableEq (RatFunc K)]

Lean source · statement

theorem exists_sub_algebraMap_intDegree_neg {x : RatFunc K}
    (hx : RatFunc.inftyValuation K x ≤ 1) :
    ∃ c : K, x - algebraMap K (RatFunc K) c = 0 ∨
      (x - algebraMap K (RatFunc K) c).intDegree < 0

instance

instFiniteResidueOfHeightOneSpectrum

L316 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField.instFiniteResidueOfHeightOneSpectrum

Source context 23 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

instance instFiniteResidueOfHeightOneSpectrum (w : HeightOneSpectrum K[X]) :
    (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).FiniteResidue

instance

instFiniteResiduePlaceInfty

L323 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField.instFiniteResiduePlaceInfty

Source context 23 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

instance instFiniteResiduePlaceInfty [DecidableEq (RatFunc K)] :
    (placeInfty K).FiniteResidue

instance

instFiniteResidue

L328 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField.instFiniteResidue

Source context 24 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K} in

Lean source · statement

instance instFiniteResidue (v : Place K (RatFunc K)) : v.FiniteResidue

theorem

finitePlace_ne_placeInfty

L367 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.finitePlace_ne_placeInfty

Source context 34 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F] [HasCanonicalDivisor (K := K) (F := F)]
variable [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
variable [HasPrincipalDivisors K F]
section P1PrincipalPartSubrows
open _root_.AlgebraicCurve.RationalFunctionField
variable (K)
variable [DecidableEq (RatFunc K)]
variable [HasCanonicalLocalResidueKStar K (RatFunc K)] [HasCanonicalDivisor (K := K) (F := RatFunc
  K)]
variable [∀ v : Place K (RatFunc K), v.DCoordGenerates] [Nontrivial Ω[(RatFunc K)⁄K]]
variable [HasPrincipalDivisors K (RatFunc K)]
variable {K}
omit [HasCanonicalLocalResidueKStar K (RatFunc K)] [HasCanonicalDivisor (K := K) (F := RatFunc K)]
  [∀ v : Place K (RatFunc K), v.DCoordGenerates] [Nontrivial Ω[(RatFunc K)⁄K]]
  [HasPrincipalDivisors K (RatFunc K)] in

Lean source · statement

theorem finitePlace_ne_placeInfty {p : K[X]} (hp : Irreducible p) :
    finitePlace K hp ≠ placeInfty K

theorem

exists_ord_finitePlace_eq_nsmul

L390 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField.exists_ord_finitePlace_eq_nsmul

Source context 23 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.Polynomial
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem exists_ord_finitePlace_eq_nsmul {p : K[X]} (hp : Irreducible p) {q : K[X]}
    (hq : q ≠ 0) :
    ∃ m : ℕ, (finitePlace K hp).ord (algebraMap K[X] (RatFunc K) q)
      = m * (finitePlace K hp).ord (algebraMap K[X] (RatFunc K) p)

theorem

ord_finitePlace_dvd

L409 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField.ord_finitePlace_dvd

Source context 23 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.Polynomial
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem ord_finitePlace_dvd {p : K[X]} (hp : Irreducible p) {f : RatFunc K} (hf : f ≠ 0) :
    (finitePlace K hp).ord (algebraMap K[X] (RatFunc K) p) ∣ (finitePlace K hp).ord f

theorem

ord_finitePlace_self

L423 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField.ord_finitePlace_self

Source context 23 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.Polynomial
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem ord_finitePlace_self {p : K[X]} (hp : Irreducible p) :
    (finitePlace K hp).ord (algebraMap K[X] (RatFunc K) p) = 1

theorem

ord_placeInfty_X_inv

L456 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ord_placeInfty_X_inv

Source context 23 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem ord_placeInfty_X_inv : (placeInfty K).ord (RatFunc.X : RatFunc K)⁻¹ = 1

abbrev

dX

L480 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.dX

Documentation

The differential of the rational function field coordinate.

Source context 25 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

abbrev dX : Ω[(RatFunc K)⁄K]

theorem

aeval_ratFuncX_eq_algebraMap

L482 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.aeval_ratFuncX_eq_algebraMap

Source context 25 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem aeval_ratFuncX_eq_algebraMap (q : K[X]) :
    aeval (RatFunc.X : RatFunc K) q = algebraMap K[X] (RatFunc K) q

theorem

D_algebraMap_polynomial

L489 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.D_algebraMap_polynomial

Source context 25 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem D_algebraMap_polynomial (q : K[X]) :
    KaehlerDifferential.D K (RatFunc K) (algebraMap K[X] (RatFunc K) q)
      = algebraMap K[X] (RatFunc K) q.derivative • dX K

theorem

denom_sq_smul_D_eq

L495 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.denom_sq_smul_D_eq

Source context 25 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem denom_sq_smul_D_eq (f : RatFunc K) :
    (algebraMap K[X] (RatFunc K) f.denom) ^ 2 • KaehlerDifferential.D K (RatFunc K) f
      = algebraMap K[X] (RatFunc K)
          (f.num.derivative * f.denom - f.num * f.denom.derivative) • dX K

theorem

span_dX_eq_top

L513 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.span_dX_eq_top

Source context 25 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem span_dX_eq_top :
    Submodule.span (RatFunc K) {dX K} = ⊤

theorem

dX_ne_zero

L527 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.dX_ne_zero

Source context 25 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem dX_ne_zero [Nontrivial Ω[(RatFunc K)⁄K]] : dX K ≠ 0

theorem

not_dvd_derivative_of_sq_not_dvd

L535 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.not_dvd_derivative_of_sq_not_dvd

Source context 25 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]

Lean source · statement

theorem not_dvd_derivative_of_sq_not_dvd {p : K[X]} (hp : Irreducible p) (hsep : p.Separable)
    {q : K[X]} (hpq : p ∣ q) (hpq2 : ¬ p ^ 2 ∣ q) : ¬ p ∣ q.derivative

theorem

not_dvd_derivative_of_ord_eq_one

L549 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.not_dvd_derivative_of_ord_eq_one

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}

Lean source · statement

theorem not_dvd_derivative_of_ord_eq_one {w : HeightOneSpectrum K[X]} {p : K[X]}
    (hp : Irreducible p) (hwp : w.asIdeal = Ideal.span {p}) (hsep : p.Separable)
    {q : K[X]} (hq : q ≠ 0)
    (hord : (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).ord
      (algebraMap K[X] (RatFunc K) q) = 1) :
    ¬ p ∣ q.derivative

theorem

surjective_algebraMap_residueField_placeInfty

L604 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.surjective_algebraMap_residueField_placeInfty

Source context 25 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section SurjectivePlaceInfty
variable (K) [DecidableEq (RatFunc K)]

Lean source · statement

theorem surjective_algebraMap_residueField_placeInfty :
    Function.Surjective (algebraMap K (placeInfty K).ResidueField)

theorem

natDegree_numDenomWronskian_lt

L634 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.natDegree_numDenomWronskian_lt

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section WronskianBound
variable {K : Type*} [Field K]

Lean source · statement

theorem natDegree_numDenomWronskian_lt {n d : K[X]} (hn : n ≠ 0) (hd : d ≠ 0)
    (hW : n.derivative * d - n * d.derivative ≠ 0) :
    (n.derivative * d - n * d.derivative).natDegree < n.natDegree + d.natDegree

def

ratFuncDXCoeff

L653 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ratFuncDXCoeff

Documentation

The rational function derivative given by the quotient rule.

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section DXCoeff
variable (K : Type*) [Field K]

Lean source · statement

def ratFuncDXCoeff (f : RatFunc K) : RatFunc K

theorem

ratFuncDXCoeff_def

L657 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ratFuncDXCoeff_def

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section DXCoeff
variable (K : Type*) [Field K]

Lean source · statement

theorem ratFuncDXCoeff_def (f : RatFunc K) :
    ratFuncDXCoeff K f
      = algebraMap K[X] (RatFunc K) (f.num.derivative * f.denom - f.num * f.denom.derivative)
        / (algebraMap K[X] (RatFunc K) f.denom) ^ 2

theorem

D_eq_ratFuncDXCoeff_smul_dX

L662 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.D_eq_ratFuncDXCoeff_smul_dX

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section DXCoeff
variable (K : Type*) [Field K]

Lean source · statement

theorem D_eq_ratFuncDXCoeff_smul_dX (f : RatFunc K) :
    KaehlerDifferential.D K (RatFunc K) f = ratFuncDXCoeff K f • dX K

theorem

wronskian_ne_zero_of_ratFuncDXCoeff_ne_zero

L669 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.wronskian_ne_zero_of_ratFuncDXCoeff_ne_zero

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section DXCoeff
variable (K : Type*) [Field K]

Lean source · statement

theorem wronskian_ne_zero_of_ratFuncDXCoeff_ne_zero {f : RatFunc K}
    (h : ratFuncDXCoeff K f ≠ 0) :
    f.num.derivative * f.denom - f.num * f.denom.derivative ≠ 0

theorem

ord_algebraMap_denom_eq_zero_of_ord_eq_one

L680 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ord_algebraMap_denom_eq_zero_of_ord_eq_one

Source context 28 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section FinitePlaces
variable {K : Type*} [Field K]
variable {w : HeightOneSpectrum K[X]}
local notation "v" => Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w

Lean source · statement

theorem ord_algebraMap_denom_eq_zero_of_ord_eq_one {p : K[X]}
    (hp : Irreducible p) (hwp : w.asIdeal = Ideal.span {p}) {f : RatFunc K}
    (hf : f ≠ 0) (hord : (v).ord f = 1) :
    (v).ord (algebraMap K[X] (RatFunc K) f.denom) = 0

theorem

ord_algebraMap_num_eq_one_of_ord_eq_one

L708 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ord_algebraMap_num_eq_one_of_ord_eq_one

Source context 28 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section FinitePlaces
variable {K : Type*} [Field K]
variable {w : HeightOneSpectrum K[X]}
local notation "v" => Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w

Lean source · statement

theorem ord_algebraMap_num_eq_one_of_ord_eq_one {p : K[X]}
    (hp : Irreducible p) (hwp : w.asIdeal = Ideal.span {p}) {f : RatFunc K}
    (hf : f ≠ 0) (hord : (v).ord f = 1) :
    (v).ord (algebraMap K[X] (RatFunc K) f.num) = 1

theorem

not_dvd_wronskian_of_ord_eq_one

L721 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.not_dvd_wronskian_of_ord_eq_one

Source context 28 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section FinitePlaces
variable {K : Type*} [Field K]
variable {w : HeightOneSpectrum K[X]}
local notation "v" => Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w

Lean source · statement

theorem not_dvd_wronskian_of_ord_eq_one {p : K[X]}
    (hp : Irreducible p) (hwp : w.asIdeal = Ideal.span {p}) (hsep : p.Separable)
    {f : RatFunc K} (hf : f ≠ 0) (hord : (v).ord f = 1) :
    ¬ p ∣ (f.num.derivative * f.denom - f.num * f.denom.derivative)

theorem

ratFuncDXCoeff_ne_zero_and_ord_eq_zero_of_ord_eq_one

L748 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ratFuncDXCoeff_ne_zero_and_ord_eq_zero_of_ord_eq_one

Source context 28 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section FinitePlaces
variable {K : Type*} [Field K]
variable {w : HeightOneSpectrum K[X]}
local notation "v" => Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w

Lean source · statement

theorem ratFuncDXCoeff_ne_zero_and_ord_eq_zero_of_ord_eq_one {p : K[X]}
    (hp : Irreducible p) (hwp : w.asIdeal = Ideal.span {p}) (hsep : p.Separable)
    {f : RatFunc K} (hf : f ≠ 0) (hord : (v).ord f = 1) :
    ratFuncDXCoeff K f ≠ 0 ∧ (v).ord (ratFuncDXCoeff K f) = 0

theorem

ord_placeInfty_ratFuncDXCoeff_ge

L777 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ord_placeInfty_ratFuncDXCoeff_ge

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section PlaceInftySide
variable {K : Type*} [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem ord_placeInfty_ratFuncDXCoeff_ge {g : RatFunc K} (hg : g ≠ 0)
    (hW : g.num.derivative * g.denom - g.num * g.denom.derivative ≠ 0) :
    (placeInfty K).ord g + 1 ≤ (placeInfty K).ord (ratFuncDXCoeff K g)

theorem

exists_dXCoeff_ord_ge_two_of_ord_placeInfty_eq_zero

L803 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.exists_dXCoeff_ord_ge_two_of_ord_placeInfty_eq_zero

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section PlaceInftySide
variable {K : Type*} [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem exists_dXCoeff_ord_ge_two_of_ord_placeInfty_eq_zero {g : RatFunc K}
    (hg : g ≠ 0) (hord : (placeInfty K).ord g = 0) :
    ∃ e : RatFunc K, (e = 0 ∨ 2 ≤ (placeInfty K).ord e) ∧
      KaehlerDifferential.D K (RatFunc K) g = e • dX K

theorem

exists_unit_dXCoeff_of_ord_placeInfty_eq_neg_one

L835 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.exists_unit_dXCoeff_of_ord_placeInfty_eq_neg_one

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section PlaceInftySide
variable {K : Type*} [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem exists_unit_dXCoeff_of_ord_placeInfty_eq_neg_one {h : RatFunc K}
    (hh : h ≠ 0) (hord : (placeInfty K).ord h = -1) :
    ∃ b : RatFunc K, b ≠ 0 ∧ (placeInfty K).ord b = 0 ∧
      KaehlerDifferential.D K (RatFunc K) h = b • dX K

theorem

exists_dXCoeff_ord_two_of_ord_placeInfty_eq_one

L878 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.exists_dXCoeff_ord_two_of_ord_placeInfty_eq_one

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section PlaceInftySide
variable {K : Type*} [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem exists_dXCoeff_ord_two_of_ord_placeInfty_eq_one {f : RatFunc K}
    (hf : f ≠ 0) (hord : (placeInfty K).ord f = 1) :
    ∃ e : RatFunc K, e ≠ 0 ∧ (placeInfty K).ord e = 2 ∧
      KaehlerDifferential.D K (RatFunc K) f = e • dX K

def

finitePlaceResidueFieldAlgEquivAdjoinRoot

L917 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.finitePlaceResidueFieldAlgEquivAdjoinRoot

Documentation

Present the residue field of a finite place by adjoining a root of its polynomial.

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
section AlgEquiv
variable {p : K[X]} (hpirr : Irreducible p)

Lean source · statement

def finitePlaceResidueFieldAlgEquivAdjoinRoot :
    AdjoinRoot p ≃ₐ[K] (finitePlace K hpirr).ResidueField

theorem

finitePlaceResidueFieldAlgEquivAdjoinRoot_mk

L921 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.finitePlaceResidueFieldAlgEquivAdjoinRoot_mk

Source context 27 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
section AlgEquiv
variable {p : K[X]} (hpirr : Irreducible p)
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem finitePlaceResidueFieldAlgEquivAdjoinRoot_mk (q : K[X]) :
    finitePlaceResidueFieldAlgEquivAdjoinRoot K hpirr (AdjoinRoot.mk p q)
      = IsLocalRing.residue _ ⟨algebraMap K[X] (RatFunc K) q,
          algebraMap_mem_ofHeightOneSpectrum K _ q⟩

theorem

trace_finitePlace_residueField_eq_trace_adjoinRoot

L931 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.trace_finitePlace_residueField_eq_trace_adjoinRoot

Source context 27 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]
section TraceTransport
variable {p : K[X]} (hpirr : Irreducible p)
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem trace_finitePlace_residueField_eq_trace_adjoinRoot
    (y : (finitePlace K hpirr).ResidueField) :
    Algebra.trace K (finitePlace K hpirr).ResidueField y
      = Algebra.trace K (AdjoinRoot p)
          ((finitePlaceResidueFieldAlgEquivAdjoinRoot K hpirr).symm y)

theorem

ratFuncDXCoeff_eq_of_D_eq_smul_dX

L961 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ratFuncDXCoeff_eq_of_D_eq_smul_dX

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section DXCoeffIntegrality
variable {K : Type*} [Field K]

Lean source · statement

theorem ratFuncDXCoeff_eq_of_D_eq_smul_dX {f e : RatFunc K}
    (h : KaehlerDifferential.D K (RatFunc K) f = e • dX K) : ratFuncDXCoeff K f = e

theorem

ratFuncDXCoeff_zero

L969 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ratFuncDXCoeff_zero

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section DXCoeffIntegrality
variable {K : Type*} [Field K]

Lean source · statement

theorem ratFuncDXCoeff_zero : ratFuncDXCoeff K (0 : RatFunc K) = 0

theorem

ord_algebraMap_denom_eq_zero_of_ord_nonneg

L975 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ord_algebraMap_denom_eq_zero_of_ord_nonneg

Source context 29 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section DXCoeffIntegrality
variable {K : Type*} [Field K]
section FinitePlaces
variable {w : HeightOneSpectrum K[X]}
local notation "vw" => Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w

Lean source · statement

theorem ord_algebraMap_denom_eq_zero_of_ord_nonneg {p : K[X]}
    (hp : Irreducible p) (hwp : w.asIdeal = Ideal.span {p}) {f : RatFunc K}
    (hf : f ≠ 0) (hord : 0 ≤ (vw).ord f) :
    (vw).ord (algebraMap K[X] (RatFunc K) f.denom) = 0

theorem

ratFuncDXCoeff_eq_zero_or_ord_nonneg_of_ord_nonneg

L1003 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ratFuncDXCoeff_eq_zero_or_ord_nonneg_of_ord_nonneg

Source context 29 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section DXCoeffIntegrality
variable {K : Type*} [Field K]
section FinitePlaces
variable {w : HeightOneSpectrum K[X]}
local notation "vw" => Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w

Lean source · statement

theorem ratFuncDXCoeff_eq_zero_or_ord_nonneg_of_ord_nonneg {p : K[X]}
    (hp : Irreducible p) (hwp : w.asIdeal = Ideal.span {p}) {g : RatFunc K}
    (hg : g ≠ 0) (hord : 0 ≤ (vw).ord g) :
    ratFuncDXCoeff K g = 0 ∨ 0 ≤ (vw).ord (ratFuncDXCoeff K g)

theorem

ratFuncDXCoeff_ne_zero_and_ord_placeInfty_eq_two_of_ord_eq_one

L1037 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ratFuncDXCoeff_ne_zero_and_ord_placeInfty_eq_two_of_ord_eq_one

Source context 28 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section DXCoeffIntegrality
variable {K : Type*} [Field K]
section PlaceInftySide
variable [DecidableEq (RatFunc K)]

Lean source · statement

theorem ratFuncDXCoeff_ne_zero_and_ord_placeInfty_eq_two_of_ord_eq_one
    {f : RatFunc K} (hf : f ≠ 0) (hord : (placeInfty K).ord f = 1) :
    ratFuncDXCoeff K f ≠ 0 ∧ (placeInfty K).ord (ratFuncDXCoeff K f) = 2

theorem

ratFuncDXCoeff_eq_zero_or_two_le_ord_placeInfty_of_ord_nonneg

L1044 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ratFuncDXCoeff_eq_zero_or_two_le_ord_placeInfty_of_ord_nonneg

Source context 28 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section DXCoeffIntegrality
variable {K : Type*} [Field K]
section PlaceInftySide
variable [DecidableEq (RatFunc K)]

Lean source · statement

theorem ratFuncDXCoeff_eq_zero_or_two_le_ord_placeInfty_of_ord_nonneg
    {g : RatFunc K} (hg : g ≠ 0) (hord : 0 ≤ (placeInfty K).ord g) :
    ratFuncDXCoeff K g = 0 ∨ 2 ≤ (placeInfty K).ord (ratFuncDXCoeff K g)

theorem

exists_ne_zero_smul_dX_of_uniformizer

L1078 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.exists_ne_zero_smul_dX_of_uniformizer

Source context 20 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section PerfectDCoord
variable (K : Type*) [Field K] [PerfectField K]

Lean source · statement

theorem exists_ne_zero_smul_dX_of_uniformizer (v : Place K (RatFunc K)) :
    ∃ c : RatFunc K, c ≠ 0 ∧
      KaehlerDifferential.D K (RatFunc K) v.uniformizer = c • dX K

instance

instDCoordGeneratesPerfectField

L1095 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField.instDCoordGeneratesPerfectField

Source context 23 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section PerfectDCoord
variable (K : Type*) [Field K] [PerfectField K]
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField

Lean source · statement

instance (priority := low) instDCoordGeneratesPerfectField (v : Place K (RatFunc K)) :
    v.DCoordGenerates

theorem

ag9b12c_trace_root_pow_div_derivative_of_lt_of_perfectField

L1129 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ag9b12c_trace_root_pow_div_derivative_of_lt_of_perfectField

Source context 28 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [PerfectField K] [DecidableEq (RatFunc K)]
section EulerPerfectField
variable {p : K[X]} [Fact (Irreducible p)]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem ag9b12c_trace_root_pow_div_derivative_of_lt_of_perfectField (hpmon : p.Monic)
    {k : ℕ} (hk : k < p.natDegree - 1) :
    Algebra.trace K (AdjoinRoot p)
      (AdjoinRoot.root p ^ k / aeval (AdjoinRoot.root p) (derivative p)) = 0

theorem

ag9b12c_trace_root_pow_div_derivative_self_of_perfectField

L1142 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ag9b12c_trace_root_pow_div_derivative_self_of_perfectField

Source context 28 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [PerfectField K] [DecidableEq (RatFunc K)]
section EulerPerfectField
variable {p : K[X]} [Fact (Irreducible p)]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem ag9b12c_trace_root_pow_div_derivative_self_of_perfectField (hpmon : p.Monic)
    (hd : 0 < p.natDegree) :
    Algebra.trace K (AdjoinRoot p)
      (AdjoinRoot.root p ^ (p.natDegree - 1) /
        aeval (AdjoinRoot.root p) (derivative p)) = 1

theorem

ag9b12c_aeval_root_eq_sum_range

L1156 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ag9b12c_aeval_root_eq_sum_range

Source context 28 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [PerfectField K] [DecidableEq (RatFunc K)]
section EulerPerfectField
variable {p : K[X]} [Fact (Irreducible p)]
omit [PerfectField K] [DecidableEq (RatFunc K)] in

Lean source · statement

theorem ag9b12c_aeval_root_eq_sum_range {c : K[X]} {d : ℕ} (hd : c.natDegree < d) :
    (aeval (AdjoinRoot.root p) c : AdjoinRoot p)
      = ∑ k ∈ Finset.range d, c.coeff k • AdjoinRoot.root p ^ k

theorem

ag9b12c_trace_adjoinRoot_mk_div_mk_derivative_of_perfectField

L1162 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ag9b12c_trace_adjoinRoot_mk_div_mk_derivative_of_perfectField

Source context 28 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] [PerfectField K] [DecidableEq (RatFunc K)]
section EulerPerfectField
variable {p : K[X]} [Fact (Irreducible p)]
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem ag9b12c_trace_adjoinRoot_mk_div_mk_derivative_of_perfectField (hpmon : p.Monic)
    {c : K[X]} (hdeg : c.degree < p.degree) :
    Algebra.trace K (AdjoinRoot p)
        (AdjoinRoot.mk p c / AdjoinRoot.mk p (derivative p))
      = c.coeff (p.natDegree - 1)

theorem

ag9b13e_ratFuncDXCoeff_uniformizer_ne_zero_and_ord_le_of_perfectField

L1212 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ag9b13e_ratFuncDXCoeff_uniformizer_ne_zero_and_ord_le_of_perfectField

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section LemmaAPerfect
variable {K : Type*} [Field K] [PerfectField K]

Lean source · statement

theorem ag9b13e_ratFuncDXCoeff_uniformizer_ne_zero_and_ord_le_of_perfectField
    (v : Place K (RatFunc K)) {g : RatFunc K} (hg : g ∈ v.toValuationSubring) :
    ratFuncDXCoeff K v.uniformizer ≠ 0 ∧
      (ratFuncDXCoeff K g = 0 ∨
        v.ord (ratFuncDXCoeff K v.uniformizer) ≤ v.ord (ratFuncDXCoeff K g))

theorem

ag9b13e_differentialCoeff_D_eq_ratFuncDXCoeff_div_of_perfectField

L1247 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ag9b13e_differentialCoeff_D_eq_ratFuncDXCoeff_div_of_perfectField

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section LemmaAPerfect
variable {K : Type*} [Field K] [PerfectField K]

Lean source · statement

theorem ag9b13e_differentialCoeff_D_eq_ratFuncDXCoeff_div_of_perfectField
    (v : Place K (RatFunc K)) (f : RatFunc K)
    (hπ : ratFuncDXCoeff K v.uniformizer ≠ 0) :
    v.differentialCoeff (KaehlerDifferential.D K (RatFunc K) f)
      = ratFuncDXCoeff K f / ratFuncDXCoeff K v.uniformizer

theorem

ag9b13e_differentialCoeff_D_mem_of_mem_of_perfectField

L1257 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.ag9b13e_differentialCoeff_D_mem_of_mem_of_perfectField

Source context 26 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
section
section
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
open _root_.Module.IsLocalRing
open _root_.KaehlerDifferential
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped Polynomial FinitePlaceResidueTrace.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
section LemmaAPerfect
variable {K : Type*} [Field K] [PerfectField K]

Lean source · statement

theorem ag9b13e_differentialCoeff_D_mem_of_mem_of_perfectField (v : Place K (RatFunc K))
    {g : RatFunc K} (hg : g ∈ v.toValuationSubring) :
    v.differentialCoeff (KaehlerDifferential.D K (RatFunc K) g) ∈ v.toValuationSubring

theorem

surjective_algebraMap_residueField_of_deg_eq_one

L1283 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.surjective_algebraMap_residueField_of_deg_eq_one

Source context 13 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem surjective_algebraMap_residueField_of_deg_eq_one (K : Type*) [Field K]
    {F : Type*} [Field F] [Algebra K F]
    (v : Place K F) (hdeg : v.deg = 1) :
    Function.Surjective (algebraMap K v.ResidueField)

theorem

ord_neg'

L1304 ↗

AlgebraicCurve.Place.ord_neg'

Source context 16 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_neg' (f : F) : v.ord (-f) = v.ord f

theorem

ord_add_eq_min

L1308 ↗

AlgebraicCurve.Place.ord_add_eq_min

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_add_eq_min {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) (h :
  v.ord f ≠ v.ord g) :
    v.ord (f + g) = min (v.ord f) (v.ord g)

def

substPoly

L1353 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.substPoly

Documentation

Polynomial substitution into the rational function field by the selected polynomial.

Source context 16 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])

Lean source · statement

def substPoly : K[X] →ₐ[K] RatFunc K

theorem

substPoly_apply

L1356 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.substPoly_apply

Source context 16 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])

Lean source · statement

theorem substPoly_apply (q : K[X]) :
    substPoly K p q = algebraMap K[X] (RatFunc K) (q.comp p)

theorem

substPoly_ne_zero

L1361 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.substPoly_ne_zero

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in

Lean source · statement

theorem substPoly_ne_zero (hp : 0 < p.natDegree) {q : K[X]} (hq : q ≠ 0) : substPoly K p q ≠ 0

def

subst

L1367 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.subst

Documentation

The rational-function substitution induced by a polynomial of positive degree.

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in

Lean source · statement

def subst (hp : 0 < p.natDegree) : RatFunc K →ₐ[K] RatFunc K

theorem

subst_algebraMap

L1372 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.subst_algebraMap

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in

Lean source · statement

theorem subst_algebraMap (hp : 0 < p.natDegree) (q : K[X]) :
    subst K p hp (algebraMap K[X] (RatFunc K) q) = algebraMap K[X] (RatFunc K) (q.comp p)

def

Kx

L1379 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.Kx

Documentation

The rational function field used as the target of the polynomial-substitution tower.

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in

Lean source · statement

def Kx (_hp : 0 < p.natDegree) : Type _

instance

(anonymous instance)

L1383 ↗

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

instance : Field (Kx K p hp)

instance

(anonymous instance)

L1384 ↗

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

instance : Algebra K (Kx K p hp)

instance

(anonymous instance)

L1385 ↗

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

instance : DecidableEq (Kx K p hp)

def

toKx

L1388 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.toKx

Documentation

The identity equivalence to the target copy of the rational function field.

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

def toKx : RatFunc K ≃ₐ[K] Kx K p hp

instance

algebraKx

L1390 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.algebraKx

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

instance algebraKx : Algebra (RatFunc K) (Kx K p hp)

theorem

algebraMap_Kx_apply

L1393 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.algebraMap_Kx_apply

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem algebraMap_Kx_apply (f : RatFunc K) :
    algebraMap (RatFunc K) (Kx K p hp) f = toKx K p hp (subst K p hp f)

instance

(anonymous instance)

L1396 ↗

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

instance : IsScalarTower K (RatFunc K) (Kx K p hp)

theorem

subst_X

L1404 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.subst_X

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem subst_X : subst K p hp (RatFunc.X : RatFunc K) = algebraMap K[X] (RatFunc K) p

theorem

aeval_ratFuncX

L1407 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.aeval_ratFuncX

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem aeval_ratFuncX (q : K[X]) : aeval (RatFunc.X : RatFunc K) q = algebraMap K[X] (RatFunc K) q

def

gen

L1414 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.gen

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

def gen : Kx K p hp

def

minP

L1418 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.minP

Documentation

The polynomial relation obtained by subtracting the base variable from the substituted polynomial.

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

def minP : (RatFunc K)[X]

theorem

toKx_apply

L1420 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.toKx_apply

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem toKx_apply (f : RatFunc K) : toKx K p hp f = (f : RatFunc K)

theorem

aeval_gen_map

L1422 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.aeval_gen_map

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem aeval_gen_map (q : K[X]) :
    aeval (gen K p hp) (q.map (algebraMap K (RatFunc K))) = toKx K p hp (algebraMap K[X] (RatFunc
      K) q)

theorem

aeval_gen_minP

L1428 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.aeval_gen_minP

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem aeval_gen_minP : aeval (gen K p hp) (minP K p) = 0

theorem

monic_minP

L1431 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.monic_minP

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)
include hp in

Lean source · statement

theorem monic_minP (hmon : p.Monic) : (minP K p).Monic

theorem

isIntegral_gen

L1438 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.isIntegral_gen

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem isIntegral_gen (hmon : p.Monic) : IsIntegral (RatFunc K) (gen K p hp)

theorem

minP_ne_zero

L1443 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.minP_ne_zero

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)
include hp in

Lean source · statement

theorem minP_ne_zero (hmon : p.Monic) : minP K p ≠ 0

theorem

toKx_algebraMap_mem_adjoin

L1445 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.toKx_algebraMap_mem_adjoin

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem toKx_algebraMap_mem_adjoin (q : K[X]) :
    toKx K p hp (algebraMap K[X] (RatFunc K) q) ∈ IntermediateField.adjoin (RatFunc K) {gen K p hp}

theorem

adjoin_gen_eq_top

L1452 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.adjoin_gen_eq_top

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem adjoin_gen_eq_top : IntermediateField.adjoin (RatFunc K) {gen K p hp} = ⊤

theorem

finiteDimensional_Kx

L1461 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.finiteDimensional_Kx

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem finiteDimensional_Kx (hmon : p.Monic) : FiniteDimensional (RatFunc K) (Kx K p hp)

theorem

isIntegral_Kx

L1466 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.isIntegral_Kx

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem isIntegral_Kx (hmon : p.Monic) : Algebra.IsIntegral (RatFunc K) (Kx K p hp)

theorem

derivative_minP

L1470 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.derivative_minP

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem derivative_minP : derivative (minP K p) = (derivative p).map (algebraMap K (RatFunc K))

theorem

transcendental_ratFuncX

L1474 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.transcendental_ratFuncX

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem transcendental_ratFuncX : Transcendental K (RatFunc.X : RatFunc K)

theorem

separable_minP

L1479 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.separable_minP

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)
include hp in

Lean source · statement

theorem separable_minP (hsep : p.Separable) : (minP K p).Separable

theorem

isSeparable_gen

L1510 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.isSeparable_gen

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem isSeparable_gen (hsep : p.Separable) : IsSeparable (RatFunc K) (gen K p hp)

theorem

isSeparable_Kx

L1513 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.isSeparable_Kx

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
noncomputable section
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
variable (K : Type*) [Field K] (p : K[X])
variable {p} in
variable (hp : 0 < p.natDegree)

Lean source · statement

theorem isSeparable_Kx (hmon : p.Monic) (hsep : p.Separable) :
    Algebra.IsSeparable (RatFunc K) (Kx K p hp)

instance

hasPrincipalDivisors_Kx

L1540 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.hasPrincipalDivisors_Kx

Source context 16 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)

Lean source · statement

instance hasPrincipalDivisors_Kx : HasPrincipalDivisors K (Kx K p hp)

theorem

ord_finitePlace_pos_iff_dvd

L1544 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.ord_finitePlace_pos_iff_dvd

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in

Lean source · statement

theorem ord_finitePlace_pos_iff_dvd {q : K[X]} (hirr : Irreducible q) {a : K[X]} (ha : a ≠ 0) :
    0 < (finitePlace K hirr).ord (algebraMap K[X] (RatFunc K) a) ↔ q ∣ a

theorem

ord_finitePlace_eq_zero_iff_not_dvd

L1556 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.ord_finitePlace_eq_zero_iff_not_dvd

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in

Lean source · statement

theorem ord_finitePlace_eq_zero_iff_not_dvd {q : K[X]} (hirr : Irreducible q) {a : K[X]} (ha : a ≠
  0) :
    (finitePlace K hirr).ord (algebraMap K[X] (RatFunc K) a) = 0 ↔ ¬ q ∣ a

theorem

not_dvd_comp_of_eval_zero_ne_zero

L1564 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.not_dvd_comp_of_eval_zero_ne_zero

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in

Lean source · statement

theorem not_dvd_comp_of_eval_zero_ne_zero {u : K[X]} (hu : u.eval 0 ≠ 0) (hpu : ¬ IsUnit p) :
    ¬ p ∣ u.comp p

theorem

not_isUnit_p

L1582 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.not_isUnit_p

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in
include hp in

Lean source · statement

theorem not_isUnit_p : ¬ IsUnit p

theorem

ord_finitePlace_subst_algebraMap

L1585 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.ord_finitePlace_subst_algebraMap

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in

Lean source · statement

theorem ord_finitePlace_subst_algebraMap (hirr : Irreducible p) {q : K[X]} (hq : q ≠ 0) :
    (finitePlace K hirr).ord (subst K p hp (algebraMap K[X] (RatFunc K) q))
      = (Polynomial.rootMultiplicity 0 q : ℤ)
        * (finitePlace K hirr).ord (algebraMap K[X] (RatFunc K) p)

theorem

ord_finitePlace_subst

L1613 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.ord_finitePlace_subst

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in

Lean source · statement

theorem ord_finitePlace_subst (hirr : Irreducible p) (f : RatFunc K) :
    (finitePlace K hirr).ord (subst K p hp f)
      = (placeOfPoint K 0).ord f * (finitePlace K hirr).ord (algebraMap K[X] (RatFunc K) p)

theorem

restrict_finitePlace

L1636 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.restrict_finitePlace

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in

Lean source · full declaration

theorem restrict_finitePlace (hirr : Irreducible p) [Algebra.IsIntegral (RatFunc K) (Kx K p hp)] :
    Place.restrict (RatFunc K) (show Place K (Kx K p hp) from finitePlace K hirr) = placeOfPoint K
      0 := by
  refine Place.ext (SetLike.ext fun f => ?_)
  rw [Place.mem_restrict_iff]
  change subst K p hp f ∈ (finitePlace K hirr).toValuationSubring ↔ _
  rcases eq_or_ne f 0 with rfl | hf
  · simp [map_zero, zero_mem]
  have hsf : subst K p hp f ≠ 0 := (map_ne_zero_iff _ (subst K p hp).toRingHom.injective).mpr hf
  have hpos : 0 < (finitePlace K hirr).ord (algebraMap K[X] (RatFunc K) p) := by
    rw [ord_finitePlace_pos_iff_dvd K hirr hirr.ne_zero]
  rw [Place.mem_iff_ord_nonneg _ hsf, Place.mem_iff_ord_nonneg _ hf, ord_finitePlace_subst K p hp
    hirr]
  constructor
  · intro h; by_contra hneg; push Not at hneg
    have : (placeOfPoint K 0).ord f * (finitePlace K hirr).ord (algebraMap K[X] (RatFunc K) p) < 0
      :=
      mul_neg_of_neg_of_pos hneg hpos
    omega
  · intro h; exact mul_nonneg h hpos.le

instance

instFiniteResiduePlaceKx

L1657 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.instFiniteResiduePlaceKx

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in

Lean source · statement

instance instFiniteResiduePlaceKx (w : Place K (Kx K p hp)) :
  w.FiniteResidue

theorem

eq_finitePlace_of_ord_pos

L1664 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.eq_finitePlace_of_ord_pos

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in
variable {p} in

Lean source · statement

theorem eq_finitePlace_of_ord_pos (hirr : Irreducible p)
    {w' : Place K (RatFunc K)} (h : 0 < w'.ord (algebraMap K[X] (RatFunc K) p)) :
    w' = finitePlace K hirr

theorem

finitePlace_mem_fiber

L1687 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.finitePlace_mem_fiber

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in
variable {p} in

Lean source · full declaration

theorem finitePlace_mem_fiber (hirr : Irreducible p) [Algebra.IsIntegral (RatFunc K) (Kx K p hp)] :
    (show Place K (Kx K p hp) from finitePlace K hirr) ∈ (placeOfPoint K 0).fiber (Kx K p hp) :=
  Place.mem_fiber.mpr (restrict_finitePlace K p hp hirr)

theorem

fiber_placeOfPoint_zero

L1691 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.fiber_placeOfPoint_zero

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in
variable {p} in

Lean source · full declaration

theorem fiber_placeOfPoint_zero (hirr : Irreducible p)
    [Algebra.IsIntegral (RatFunc K) (Kx K p hp)] :
    (placeOfPoint K 0).fiber (Kx K p hp) = {(show Place K (Kx K p hp) from finitePlace K hirr)} :=
      by
  classical
  ext w'
  rw [Finset.mem_singleton, Place.mem_fiber]
  constructor
  · intro hw'
    have hX : (placeOfPoint K 0).ord (RatFunc.X : RatFunc K) = 1 := by
      classical
      rw [← RatFunc.algebraMap_X, ord_placeOfPoint_algebraMap 0 Polynomial.X_ne_zero]
      have h := (Polynomial.rootMultiplicity_X_sub_C : Polynomial.rootMultiplicity (0 : K) (X - C
        0) = _)
      rw [map_zero, sub_zero, ite_eq_left rfl] at h
      exact_mod_cast h
    have hord : w'.ord (algebraMap (RatFunc K) (Kx K p hp) RatFunc.X)
        = (Place.ramificationIndex (F := RatFunc K) w' : ℤ) * 1 := by
      rw [Place.ord_restrict, hw', hX]
    have hpos : 0 < w'.ord (algebraMap (RatFunc K) (Kx K p hp) RatFunc.X) := by
      rw [hord, mul_one]; exact_mod_cast Place.ramificationIndex_pos (F := RatFunc K) w'
    rw [algebraMap_Kx_apply, subst_X] at hpos
    exact eq_finitePlace_of_ord_pos K hirr hpos
  · rintro rfl
    exact restrict_finitePlace K p hp hirr

theorem

ord_placeInfty_subst_algebraMap

L1717 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.ord_placeInfty_subst_algebraMap

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in
variable {p} in

Lean source · statement

theorem ord_placeInfty_subst_algebraMap [DecidableEq (RatFunc K)] {q : K[X]} (hq : q ≠ 0) :
    (placeInfty K).ord (subst K p hp (algebraMap K[X] (RatFunc K) q))
      = (p.natDegree : ℤ) * (placeInfty K).ord (algebraMap K[X] (RatFunc K) q)

theorem

ord_placeInfty_subst

L1729 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.ord_placeInfty_subst

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in
variable {p} in

Lean source · statement

theorem ord_placeInfty_subst [DecidableEq (RatFunc K)] (f : RatFunc K) :
    (placeInfty K).ord (subst K p hp f) = (p.natDegree : ℤ) * (placeInfty K).ord f

theorem

ord_sum_of_injOn

L1748 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.ord_sum_of_injOn

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in
variable {p} in

Lean source · full declaration

theorem ord_sum_of_injOn {F : Type*} [Field F] [Algebra K F] (v : Place K F) {ι : Type*} (s :
  Finset ι)
    (f : ι → F) (hf : ∀ i ∈ s, f i ≠ 0) (hinj : Set.InjOn (fun i => v.ord (f i)) s) (hs :
      s.Nonempty) :
    (∑ i ∈ s, f i) ≠ 0 ∧ v.ord (∑ i ∈ s, f i) = s.inf' hs (fun i => v.ord (f i)) := by
  classical
  induction s using Finset.induction_on with
  | empty => exact absurd hs (Finset.not_nonempty_empty)
  | @insert a s ha ih =>
    rcases s.eq_empty_or_nonempty with rfl | hsne
    · refine ⟨?_, ?_⟩
      · simpa using hf a (Finset.mem_insert_self a ∅)
      · simp
    have hf' : ∀ i ∈ s, f i ≠ 0 := fun i hi => hf i (Finset.mem_insert_of_mem hi)
    have hinj' : Set.InjOn (fun i => v.ord (f i)) s := hinj.mono (Finset.subset_insert a s)
    obtain ⟨hne, hord⟩ := ih hf' hinj' hsne
    have hfa : f a ≠ 0 := hf a (Finset.mem_insert_self a s)
    obtain ⟨j, hj, hjmin⟩ := Finset.exists_mem_eq_inf' hsne (fun i => v.ord (f i))
    have hdiff : v.ord (f a) ≠ v.ord (∑ i ∈ s, f i) := by
      rw [hord, hjmin]
      intro heq
      have := hinj (Finset.mem_insert_self a s) (Finset.mem_insert_of_mem hj) heq
      exact ha (this ▸ hj)
    rw [Finset.sum_insert ha, Finset.inf'_insert hsne]
    refine ⟨?_, ?_⟩
    · intro h0
      have : ∑ i ∈ s, f i = -f a := eq_neg_of_add_eq_zero_right h0
      rw [this, v.ord_neg'] at hdiff
      exact hdiff rfl
    · rw [v.ord_add_eq_min hfa hne hdiff, hord]

theorem

linearIndependent_pow_gen

L1779 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.linearIndependent_pow_gen

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in
variable {p} in

Lean source · full declaration

theorem linearIndependent_pow_gen :
    LinearIndependent (RatFunc K) (fun i : Fin p.natDegree => gen K p hp ^ (i : ℕ)) := by
  classical
  rw [Fintype.linearIndependent_iff]
  intro g hg
  have hsum : ∑ i : Fin p.natDegree, subst K p hp (g i) * (RatFunc.X : RatFunc K) ^ (i : ℕ) = 0 :=
    by
    have : ∀ i : Fin p.natDegree, g i • gen K p hp ^ (i : ℕ)
        = toKx K p hp (subst K p hp (g i) * (RatFunc.X : RatFunc K) ^ (i : ℕ)) := fun i => by
      rw [Algebra.smul_def, algebraMap_Kx_apply]; rfl
    simp_rw [this] at hg
    rw [← map_sum] at hg
    exact (map_eq_zero_iff _ (toKx K p hp).injective).mp hg
  by_contra hne
  push Not at hne
  obtain ⟨i0, hi0⟩ := hne
  let S : Finset (Fin p.natDegree) := Finset.univ.filter (fun i => g i ≠ 0)
  have hS : S.Nonempty := ⟨i0, by simp [S, hi0]⟩
  have hterm : ∀ i ∈ S, subst K p hp (g i) * (RatFunc.X : RatFunc K) ^ (i : ℕ) ≠ 0 := by
    intro i hi
    have hgi : g i ≠ 0 := (Finset.mem_filter.mp hi).2
    exact mul_ne_zero ((_root_.map_ne_zero (subst K p hp)).mpr hgi)
      (pow_ne_zero _ RatFunc.X_ne_zero)
  have hordt : ∀ i ∈ S, (placeInfty K).ord (subst K p hp (g i) * (RatFunc.X : RatFunc K) ^ (i : ℕ))
      = (p.natDegree : ℤ) * (placeInfty K).ord (g i) - (i : ℕ) := by
    intro i hi
    have hgi : g i ≠ 0 := (Finset.mem_filter.mp hi).2
    rw [(placeInfty K).ord_mul ((_root_.map_ne_zero (subst K p hp)).mpr hgi)
      (pow_ne_zero _ RatFunc.X_ne_zero), ← zpow_natCast, (placeInfty K).ord_zpow,
      ord_placeInfty_subst, ord_placeInfty RatFunc.X_ne_zero, RatFunc.intDegree_X]
    ring
  have hinj : Set.InjOn (fun i => (placeInfty K).ord (subst K p hp (g i) * (RatFunc.X : RatFunc K)
    ^ (i : ℕ))) S := by
    intro i hi j hj heq
    simp only at heq
    rw [hordt i hi, hordt j hj] at heq
    have hd : ((p.natDegree : ℤ)) ∣ ((i : ℕ) : ℤ) - ((j : ℕ) : ℤ) := by
      refine ⟨(placeInfty K).ord (g i) - (placeInfty K).ord (g j), ?_⟩
      linear_combination (-1 : ℤ) * heq
    have hlt : (((i : ℕ) : ℤ) - ((j : ℕ) : ℤ)).natAbs < ((p.natDegree : ℤ)).natAbs := by
      have hi' := i.isLt; have hj' := j.isLt
      omega
    have := Int.eq_zero_of_dvd_of_natAbs_lt_natAbs hd hlt
    exact Fin.ext (by omega)
  have key := (ord_sum_of_injOn K (placeInfty K) S _ hterm hinj hS).1
  apply key
  rw [← hsum]
  refine Finset.sum_filter_of_ne (fun i _ hne => ?_)
  intro hgi
  apply hne
  rw [hgi, map_zero, zero_mul]

theorem

natDegree_le_finrank

L1831 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.natDegree_le_finrank

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in
variable {p} in

Lean source · statement

theorem natDegree_le_finrank (hmon : p.Monic) :
    p.natDegree ≤ Module.finrank (RatFunc K) (Kx K p hp)

theorem

minpoly_gen

L1836 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.minpoly_gen

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)
variable {p} in
variable {p} in
variable {p} in

Lean source · statement

theorem minpoly_gen (hmon : p.Monic) :
    minpoly (RatFunc K) (gen K p hp) = minP K p

def

pbGen

L1871 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.pbGen

Documentation

The power basis of the substitution extension generated by the rational function variable.

Source context 16 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)

Lean source · statement

def pbGen [DecidableEq (RatFunc K)] (hmon : p.Monic) : PowerBasis (RatFunc K) (Kx K p
  hp)

theorem

pbGen_gen

L1876 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.pbGen_gen

Source context 16 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)

Lean source · statement

theorem pbGen_gen [DecidableEq (RatFunc K)] (hmon : p.Monic) : (pbGen K p hp hmon).gen = gen K p hp

theorem

pbGen_dim

L1880 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.pbGen_dim

Source context 16 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)

Lean source · statement

theorem pbGen_dim [DecidableEq (RatFunc K)] (hmon : p.Monic) : (pbGen K p hp hmon).dim =
  p.natDegree

theorem

aeval_gen_derivative_minpoly

L1886 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.aeval_gen_derivative_minpoly

Source context 16 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)

Lean source · statement

theorem aeval_gen_derivative_minpoly (hmon : p.Monic) :
    aeval (gen K p hp) (derivative (minpoly (RatFunc K) (gen K p hp)))
      = toKx K p hp (algebraMap K[X] (RatFunc K) (derivative p))

theorem

toKx_algebraMap_eq_sum

L1891 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.toKx_algebraMap_eq_sum

Source context 16 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)

Lean source · statement

theorem toKx_algebraMap_eq_sum {c : K[X]} (hc : c.natDegree < p.natDegree) :
    toKx K p hp (algebraMap K[X] (RatFunc K) c)
      = ∑ k ∈ Finset.range p.natDegree, algebraMap K (RatFunc K) (c.coeff k) • gen K p hp ^ k

theorem

trace_mul_inv_derivative

L1897 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.trace_mul_inv_derivative

Source context 16 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K] (p : K[X]) (hp : 0 < p.natDegree)

Lean source · statement

theorem trace_mul_inv_derivative (hmon : p.Monic) (hsep : p.Separable)
    {c : K[X]} (hc : c.natDegree < p.natDegree) :
    Algebra.trace (RatFunc K) (Kx K p hp)
      (toKx K p hp (algebraMap K[X] (RatFunc K) c)
        * (toKx K p hp (algebraMap K[X] (RatFunc K) (derivative p)))⁻¹)
      = algebraMap K (RatFunc K) (c.coeff (p.natDegree - 1))

theorem

kwHgfV352_localResidueCompletion_spec

L1936 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.kwHgfV352_localResidueCompletion_spec

Source context 14 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section LocalResidueCompletionC4
variable {K E : Type*} [Field K] [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]

Lean source · statement

theorem kwHgfV352_localResidueCompletion_spec (v : Place K E) (xh : v.adicCompletion)
    {x : E} (hx : algebraMap E v.adicCompletion x - xh ∈ v.adicCompletionIntegers) :
    kwHgfV352_localResidueCompletion v xh = v.localResidue x

theorem

kwHgfV352_localResidueCompletion_algebraMap

L1953 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.kwHgfV352_localResidueCompletion_algebraMap

Source context 14 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section LocalResidueCompletionC4
variable {K E : Type*} [Field K] [Field E] [Algebra K E] [HasCanonicalLocalResidueKStar K E]

Lean source · statement

theorem kwHgfV352_localResidueCompletion_algebraMap (v : Place K E) (x : E) :
    kwHgfV352_localResidueCompletion v (algebraMap E v.adicCompletion x)
      = v.localResidue x

instance

isCurveOver_Kx

L1978 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.isCurveOver_Kx

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.KaehlerDifferential
variable (K : Type*) [Field K] [PerfectField K] [DecidableEq (RatFunc K)]
  [IsCurveOver K (RatFunc K)]
  [∀ v : Place K (RatFunc K), v.DCoordGenerates] [Nontrivial Ω[(RatFunc K)⁄K]]
  (p : K[X]) (hp : 0 < p.natDegree)

Lean source · statement

instance isCurveOver_Kx : IsCurveOver K (Kx K p hp)

instance

nontrivialKaehler_Kx

L1979 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.nontrivialKaehler_Kx

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.KaehlerDifferential
variable (K : Type*) [Field K] [PerfectField K] [DecidableEq (RatFunc K)]
  [IsCurveOver K (RatFunc K)]
  [∀ v : Place K (RatFunc K), v.DCoordGenerates] [Nontrivial Ω[(RatFunc K)⁄K]]
  (p : K[X]) (hp : 0 < p.natDegree)

Lean source · statement

instance nontrivialKaehler_Kx : Nontrivial Ω[(Kx K p hp)⁄K]

instance

dCoordGenerates_Kx

L1980 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.dCoordGenerates_Kx

Source context 17 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.KaehlerDifferential
variable (K : Type*) [Field K] [PerfectField K] [DecidableEq (RatFunc K)]
  [IsCurveOver K (RatFunc K)]
  [∀ v : Place K (RatFunc K), v.DCoordGenerates] [Nontrivial Ω[(RatFunc K)⁄K]]
  (p : K[X]) (hp : 0 < p.natDegree)

Lean source · statement

instance dCoordGenerates_Kx (w : Place K (Kx K p hp)) : w.DCoordGenerates

theorem

D_ratFuncX_ne_zero

L1985 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.D_ratFuncX_ne_zero

Source context 18 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.KaehlerDifferential
variable (K : Type*) [Field K] [PerfectField K] [DecidableEq (RatFunc K)]
  [IsCurveOver K (RatFunc K)]
  [∀ v : Place K (RatFunc K), v.DCoordGenerates] [Nontrivial Ω[(RatFunc K)⁄K]]
  (p : K[X]) (hp : 0 < p.natDegree)
omit [PerfectField K] [DecidableEq (RatFunc K)] [IsCurveOver K (RatFunc K)] [∀ (v : Place K
  (RatFunc K)), v.DCoordGenerates] in

Lean source · statement

theorem D_ratFuncX_ne_zero : KaehlerDifferential.D K (RatFunc K) (RatFunc.X : RatFunc K) ≠ 0

theorem

trace_localResidue_finitePlace_div_pow_eq_zero

L2006 ↗

AlgebraicCurves.Places.Rational.Proofs.FinitePlaceResidueTrace.AlgebraicCurve.P1Tower.trace_localResidue_finitePlace_div_pow_eq_zero

Source context 19 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace P1Tower
open _root_.Polynomial
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.KaehlerDifferential
variable (K : Type*) [Field K] [PerfectField K] [DecidableEq (RatFunc K)]
  [IsCurveOver K (RatFunc K)]
  [∀ v : Place K (RatFunc K), v.DCoordGenerates] [Nontrivial Ω[(RatFunc K)⁄K]]
  (p : K[X]) (hp : 0 < p.natDegree)
include hp in
omit [DecidableEq (RatFunc K)] in

Lean source · statement

theorem trace_localResidue_finitePlace_div_pow_eq_zero
    (hmon : p.Monic) (hirr : Irreducible p) {c : K[X]} (hc : c.degree < p.degree) {m : ℕ} (hm : 2 ≤
      m) :
    Algebra.trace K (finitePlace K hirr).ResidueField
        ((finitePlace K hirr).localResidue
          (algebraMap K[X] (RatFunc K) c / algebraMap K[X] (RatFunc K) p ^ m
            * (finitePlace K hirr).differentialCoeff
                (KaehlerDifferential.D K (RatFunc K) (RatFunc.X : RatFunc K)))) = 0

theorem

trace_localResidue_finitePlace_div_pow_eq_zero

L2134 ↗

AlgebraicCurve.RationalFunctionField.trace_localResidue_finitePlace_div_pow_eq_zero

Source context 10 commands

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

section ProofImplementation
open Polynomial
open scoped Polynomial
namespace AlgebraicCurves.Places.Rational.Proofs
namespace FinitePlaceResidueTrace
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open scoped FinitePlaceResidueTrace.AlgebraicCurve.RationalFunctionField
open _root_.Polynomial Polynomial in

Lean source · statement

theorem _root_.AlgebraicCurve.RationalFunctionField.trace_localResidue_finitePlace_div_pow_eq_zero
    (K : Type*) [Field K] [PerfectField K]
    [AlgebraicCurve.IsCurveOver K (RatFunc K)]
    [∀ v : AlgebraicCurve.Place K (RatFunc K), v.DCoordGenerates] [Nontrivial Ω[(RatFunc K)⁄K]]
    {p c : K[X]} (hmon : p.Monic) (hp : Irreducible p) (hc : c.degree < p.degree) {m : ℕ} (hm : 2 ≤
      m) :
    Algebra.trace K (AlgebraicCurve.RationalFunctionField.finitePlace K hp).ResidueField
        ((AlgebraicCurve.RationalFunctionField.finitePlace K hp).localResidue
          (algebraMap K[X] (RatFunc K) c / algebraMap K[X] (RatFunc K) p ^ m
            * (AlgebraicCurve.RationalFunctionField.finitePlace K hp).differentialCoeff
                (KaehlerDifferential.D K (RatFunc K) (RatFunc.X : RatFunc K)))) = 0

Module documentation

Rational Function Field trace local Residue finite Place div pow eq zero

Declarations