NYLL
Module

Place_isRegularAt_and_hasSimplePoleAt_and_hasSimpleResidue_sum_traceAlong_of_separableAlong_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Places.Place_isRegularAt_and_hasSimplePoleAt_and_hasSimpleResidue_sum_traceAlong_of_separableAlong_of_isAlgClosed
9 declarations indexed from sourceView source ↗

Module documentation

Place is Regular At and has Simple Pole At and has Simple Residue sum trace Along of

separable Along of is Alg Closed

Imports7
Imported by1

Declarations

theorem

algebraMap_residueField_bijective

L69 ↗
AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum.AlgebraicCurve.ResTraceAlgClosedProof.algebraMap_residueField_bijective
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
  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.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
noncomputable section
open KaehlerDifferential IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResTraceAlgClosedProof
open _root_.AlgebraicCurve
section Rational
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem algebraMap_residueField_bijective [IsAlgClosed K] [IsCurveOver K F] (v : Place K F) :
    Function.Bijective (algebraMap K v.ResidueField)
theorem

trace_residueField_algebraMap

L75 ↗
AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum.AlgebraicCurve.ResTraceAlgClosedProof.trace_residueField_algebraMap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
  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.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
noncomputable section
open KaehlerDifferential IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResTraceAlgClosedProof
open _root_.AlgebraicCurve
section Rational
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem trace_residueField_algebraMap [IsAlgClosed K] [IsCurveOver K F] (v : Place K F)
    (r : K) : Algebra.trace K v.ResidueField (algebraMap K v.ResidueField r) = r
theorem

trace_residueField_eq_zero_iff

L84 ↗
AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum.AlgebraicCurve.ResTraceAlgClosedProof.trace_residueField_eq_zero_iff
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
  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.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
noncomputable section
open KaehlerDifferential IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResTraceAlgClosedProof
open _root_.AlgebraicCurve
section Rational
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem trace_residueField_eq_zero_iff [IsAlgClosed K] [IsCurveOver K F] (v : Place K F)
    (z : v.ResidueField) : Algebra.trace K v.ResidueField z = 0 ↔ z = 0
theorem

eq_algebraMap_of_trace_eq

L89 ↗
AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum.AlgebraicCurve.ResTraceAlgClosedProof.eq_algebraMap_of_trace_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
  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.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
noncomputable section
open KaehlerDifferential IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResTraceAlgClosedProof
open _root_.AlgebraicCurve
section Rational
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem eq_algebraMap_of_trace_eq [IsAlgClosed K] [IsCurveOver K F] (v : Place K F)
    {z : v.ResidueField} {s : K} (h : Algebra.trace K v.ResidueField z = s) :
    z = algebraMap K v.ResidueField s
theorem

exists_pow_mul_not_mem

L102 ↗
AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum.AlgebraicCurve.ResTraceAlgClosedProof.exists_pow_mul_not_mem
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
  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.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
noncomputable section
open KaehlerDifferential IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResTraceAlgClosedProof
open _root_.AlgebraicCurve
section DVR
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_pow_mul_not_mem (v : Place K F) {T : F} (hT : T ∉ v.toValuationSubring) :
    ∃ k : ℕ, v.uniformizer ^ k * T ∉ v.toValuationSubring ∧
      v.uniformizer ^ (k + 1) * T ∈ v.toValuationSubring
theorem

residue_ne_zero_of_not_mem

L181 ↗
AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum.AlgebraicCurve.ResTraceAlgClosedProof.residue_ne_zero_of_not_mem
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
  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.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
noncomputable section
open KaehlerDifferential IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResTraceAlgClosedProof
open _root_.AlgebraicCurve
section DVR
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem residue_ne_zero_of_not_mem (v : Place K F) {y : F} (hy : y ∉ v.toValuationSubring)
    (hπy : v.uniformizer * y ∈ v.toValuationSubring) :
    residue v.toValuationSubring ⟨v.uniformizer * y, hπy⟩ ≠ 0
theorem

exists_eq_uniformizer_mul_of_not_isUnit

L197 ↗
AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum.AlgebraicCurve.ResTraceAlgClosedProof.exists_eq_uniformizer_mul_of_not_isUnit
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
  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.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
noncomputable section
open KaehlerDifferential IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResTraceAlgClosedProof
open _root_.AlgebraicCurve
section DVR
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_eq_uniformizer_mul_of_not_isUnit (w : Place K F) {a : F}
    (ha : a ∈ w.toValuationSubring) (hu : ¬ IsUnit (⟨a, ha⟩ : w.toValuationSubring)) :
    ∃ b ∈ w.toValuationSubring, a = w.uniformizer * b
theorem

main

L215 ↗
AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum.AlgebraicCurve.ResTraceAlgClosedProof.main
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
  instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
  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.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
noncomputable section
open KaehlerDifferential IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResTraceAlgClosedProof
open _root_.AlgebraicCurve
section Main
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem main [IsAlgClosed K]
    {x : F} (htr : Transcendental K x)
    (hfd : FiniteDimensional ↥(IntermediateField.adjoin K ({x} : Set F)) F)
    {x' : F'} (htr' : Transcendental K x')
    (hfd' : FiniteDimensional ↥(IntermediateField.adjoin K ({x'} : Set F')) F')
    [HasPrincipalDivisors K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hsep : SeparableAlong K φ)
    (v : Place K F) (η : Ω[F'⁄K]) :
    ((∀ w ∈ Place.fiberAlong φ hφ v, w.IsRegularAt η) →
        v.IsRegularAt (Differential.traceAlong φ η)) ∧
    ((∀ w ∈ Place.fiberAlong φ hφ v, w.HasSimplePoleAt η) →
        v.HasSimplePoleAt (Differential.traceAlong φ η)) ∧
    (∀ r : Place K F' → K,
      (∀ w ∈ Place.fiberAlong φ hφ v, w.HasSimpleResidue η (r w)) →
        v.HasSimpleResidue (Differential.traceAlong φ η)
          (∑ w ∈ Place.fiberAlong φ hφ v, r w))
theorem

isRegularAt_and_hasSimplePoleAt_and_hasSimpleResidue_sum_traceAlong_of_separableAlong_of_isAlgClosed

L430 ↗
AlgebraicCurve.Place.isRegularAt_and_hasSimplePoleAt_and_hasSimpleResidue_sum_traceAlong_of_separableAlong_of_isAlgClosed
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurve.Place
open _root_.AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum
  _root_.AlgebraicCurves.Places.Proofs.SimpleResidueTraceSum.AlgebraicCurve in
Lean source · statement
theorem
isRegularAt_and_hasSimplePoleAt_and_hasSimpleResidue_sum_traceAlong_of_separableAlong_of_isAlgClosed
    {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [IsAlgClosed K]
    {x : F} (htr : Transcendental K x) (hfd : FiniteDimensional ↥(IntermediateField.adjoin K ({x} :
      Set F)) F)
    {x' : F'} (htr' : Transcendental K x') (hfd' : FiniteDimensional ↥(IntermediateField.adjoin K
      ({x'} : Set F')) F')
    [AlgebraicCurve.HasPrincipalDivisors K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hsep : AlgebraicCurve.SeparableAlong K φ)
    (v : AlgebraicCurve.Place K F) (η : Ω[F'⁄K]) :
    ((∀ w ∈ AlgebraicCurve.Place.fiberAlong φ hφ v, w.IsRegularAt η) →
        v.IsRegularAt (AlgebraicCurve.Differential.traceAlong φ η)) ∧
    ((∀ w ∈ AlgebraicCurve.Place.fiberAlong φ hφ v, w.HasSimplePoleAt η) →
        v.HasSimplePoleAt (AlgebraicCurve.Differential.traceAlong φ η)) ∧
    (∀ r : AlgebraicCurve.Place K F' → K,
      (∀ w ∈ AlgebraicCurve.Place.fiberAlong φ hφ v, w.HasSimpleResidue η (r w)) →
        v.HasSimpleResidue (AlgebraicCurve.Differential.traceAlong φ η)
          (∑ w ∈ AlgebraicCurve.Place.fiberAlong φ hφ v, r w))

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