NYLL
Module

Divisor_mapDomain_placeReduction_correspondence.lean

Nyll.AlgebraicCurves.Divisors.Divisor_mapDomain_placeReduction_correspondence
29 declarations indexed from sourceView source ↗

Module documentation

Divisor map Domain place Reduction correspondence

Imports8
Imported by1

Declarations

theorem

mem_of_valuation_lt_one

L65 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.mem_of_valuation_lt_one
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section General
variable {E L : Type*} [Field E] [Field L] [Algebra E L]
Lean source · statement
theorem mem_of_valuation_lt_one (P : Place E L) {y : L}
    (hy : P.toValuationSubring.valuation y < 1) : y ∈ P.toValuationSubring
theorem

eq_zero_of_valuation_algebraMap_lt_one

L69 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.eq_zero_of_valuation_algebraMap_lt_one
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section General
variable {E L : Type*} [Field E] [Field L] [Algebra E L]
Lean source · statement
theorem eq_zero_of_valuation_algebraMap_lt_one (P : Place E L) {c : E}
    (hc : P.toValuationSubring.valuation (algebraMap E L c) < 1) : c = 0
theorem

centre_unique

L79 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.centre_unique
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section General
variable {E L : Type*} [Field E] [Field L] [Algebra E L]
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [Algebra K E] [Algebra F L]
Lean source · statement
theorem centre_unique (P : Place E L) {σ τ : F →ₐ[K] E}
    (hσ : ∀ f : F, P.toValuationSubring.valuation (algebraMap F L f - algebraMap E L (σ f)) < 1)
    (hτ : ∀ f : F, P.toValuationSubring.valuation (algebraMap F L f - algebraMap E L (τ f)) < 1) :
    σ = τ
theorem

algebraMap_mem_of_centred

L91 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.algebraMap_mem_of_centred
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section General
variable {E L : Type*} [Field E] [Field L] [Algebra E L]
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [Algebra K E] [Algebra F L]
Lean source · statement
theorem algebraMap_mem_of_centred (P : Place E L) {σ : F →ₐ[K] E}
    (hσ : ∀ f : F, P.toValuationSubring.valuation (algebraMap F L f - algebraMap E L (σ f)) < 1)
    (f : F) : algebraMap F L f ∈ P.toValuationSubring
theorem

exists_mem_valuation_sub_lt_one_iff_of_centred

L97 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.exists_mem_valuation_sub_lt_one_iff_of_centred
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section General
variable {E L : Type*} [Field E] [Field L] [Algebra E L]
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [Algebra K E] [Algebra F L]
Lean source · statement
theorem exists_mem_valuation_sub_lt_one_iff_of_centred (P : Place E L) {σ : F →ₐ[K] E}
    (hσ : ∀ f : F, P.toValuationSubring.valuation (algebraMap F L f - algebraMap E L (σ f)) < 1)
    (A : ValuationSubring E) (f : F) :
    (∃ a : E, a ∈ A ∧
        P.toValuationSubring.valuation (algebraMap F L f - algebraMap E L a) < 1) ↔ σ f ∈ A
theorem

valuation_lt_one_iff_inv_not_mem

L117 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.valuation_lt_one_iff_inv_not_mem
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Transport
Lean source · statement
theorem valuation_lt_one_iff_inv_not_mem {L : Type*} [Field L] (A : ValuationSubring L) {z : L}
    (hz : z ≠ 0) : A.valuation z < 1 ↔ z⁻¹ ∉ A
theorem

valuation_comap_lt_one_iff

L121 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.valuation_comap_lt_one_iff
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Transport
Lean source · statement
theorem valuation_comap_lt_one_iff {L L' : Type*} [Field L] [Field L'] (A : ValuationSubring L')
    (g : L →+* L') (z : L) :
    (A.comap g).valuation z < 1 ↔ A.valuation (g z) < 1
theorem

valuation_restrictAlong_lt_one_iff

L132 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.valuation_restrictAlong_lt_one_iff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Transport
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem valuation_restrictAlong_lt_one_iff (χ : F →ₐ[K] F') (h : χ.toRingHom.IsIntegral)
    [HasPrincipalDivisors K F'] (W : Place K F') (z : F) :
    (W.restrictAlong χ h).toValuationSubring.valuation z < 1 ↔
      W.toValuationSubring.valuation (χ z) < 1
theorem

mem_restrictAlong_iff

L143 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.mem_restrictAlong_iff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Transport
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem mem_restrictAlong_iff (χ : F →ₐ[K] F') (h : χ.toRingHom.IsIntegral)
    [HasPrincipalDivisors K F'] (W : Place K F') (z : F) :
    z ∈ (W.restrictAlong χ h).toValuationSubring ↔ χ z ∈ W.toValuationSubring
theorem

comap_ne_top_of_transcendental

L153 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.comap_ne_top_of_transcendental
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Transport
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem comap_ne_top_of_transcendental {L E : Type*} [Field L] [Field E] [Algebra K L]
    [Algebra K E] (A : ValuationSubring E)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (σ : L →ₐ[K] E) {x : L} (hx : Transcendental K x) : A.comap σ.toRingHom ≠ ⊤
theorem

exists_mem_valuation_sub_lt_one_iff_of_comap

L178 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.exists_mem_valuation_sub_lt_one_iff_of_comap
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section NotIntegral
variable {K L E LE : Type*} [Field K] [Field L] [Algebra K L] [IsAlgClosed K] [IsCurveOver K L]
  [Field E] [Field LE] [Algebra K E] [Algebra E LE] [Algebra L LE] [Algebra K LE]
  [IsScalarTower K E LE] [IsScalarTower K L LE]
Lean source · statement
theorem exists_mem_valuation_sub_lt_one_iff_of_comap (Q : Place E LE) (q : Place K L)
    (hq : q.toValuationSubring = Q.toValuationSubring.comap (algebraMap L LE))
    (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A) (g : L) :
    (∃ a : E, a ∈ A ∧
        Q.toValuationSubring.valuation (algebraMap L LE g - algebraMap E LE a) < 1) ↔
      algebraMap L LE g ∈ Q.toValuationSubring
theorem

span_eq_top_of_adjoin_eq_top

L210 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.span_eq_top_of_adjoin_eq_top
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
Lean source · statement
theorem span_eq_top_of_adjoin_eq_top {E L M : Type*} [Field E] [Field L] [Field M] [Algebra E L]
    [Algebra L M] [Algebra E M] [IsScalarTower E L M] {ι : Type*} [Finite ι] (b : ι → M)
    (hmul : ∀ i j, b i * b j ∈ Submodule.span L (Set.range b))
    (h1 : (1 : M) ∈ Submodule.span L (Set.range b))
    {T : Set M} (hT : T ⊆ Submodule.span L (Set.range b))
    (hgen : IntermediateField.adjoin E T = ⊤) : Submodule.span L (Set.range b) = ⊤
theorem

finite_extension

L259 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.finite_extension
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Extend
variable {K F E FE F' F'E : Type*} [Field K] [Field F] [Algebra K F] [Field E] [Field FE]
  [Algebra E FE] [Algebra F FE] [Field F'] [Algebra K F'] [Field F'E] [Algebra E F'E]
  [Algebra F' F'E]
Lean source · statement
theorem finite_extension (χ : F →ₐ[K] F') (hfin : FiniteAlong K χ) (χE : FE →ₐ[E] F'E)
    (hχE : ∀ f : F, χE (algebraMap F FE f) = algebraMap F' F'E (χ f))
    (hgen' : IntermediateField.adjoin E (Set.range (algebraMap F' F'E)) = ⊤) :
    ∃ _ : FiniteAlong E χE, finrankAlong E χE ≤ finrankAlong K χ
theorem

essFiniteType_of_fg

L299 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.essFiniteType_of_fg
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Bookkeeping
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem essFiniteType_of_fg
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F) :
    Algebra.EssFiniteType K F
theorem

finiteAlong_of_isIntegral

L310 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.finiteAlong_of_isIntegral
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Bookkeeping
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem finiteAlong_of_isIntegral [Algebra.EssFiniteType K F'] (χ : F →ₐ[K] F')
    (hχ : χ.toRingHom.IsIntegral) : FiniteAlong K χ
theorem

fg_of_finiteAlong

L325 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.fg_of_finiteAlong
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Bookkeeping
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem fg_of_finiteAlong (χ : F →ₐ[K] F') (hfin : FiniteAlong K χ) {x : F}
    (hx : Transcendental K x)
    (hfinx : FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F) :
    Transcendental K (χ x) ∧
      FiniteDimensional (IntermediateField.adjoin K ({χ x} : Set F')) F'
theorem

centred_restrictAlong

L357 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.centred_restrictAlong
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Restrict
variable {E FE F'E : Type*} [Field E] [Field FE] [Algebra E FE] [Field F'E] [Algebra E F'E]
Lean source · statement
theorem centred_restrictAlong {K F F' : Type*} [Field K] [Field F] [Algebra K F] [Field F']
    [Algebra K F'] [Algebra K E] [Algebra F FE] [Algebra F' F'E]
    [HasPrincipalDivisors E F'E] (χ : F →ₐ[K] F') (χE : FE →ₐ[E] F'E)
    (h : χE.toRingHom.IsIntegral)
    (hχE : ∀ f : F, χE (algebraMap F FE f) = algebraMap F' F'E (χ f))
    {W : Place E F'E} {σ : F' →ₐ[K] E}
    (hW : ∀ y : F', W.toValuationSubring.valuation
      (algebraMap F' F'E y - algebraMap E F'E (σ y)) < 1) (f : F) :
    (W.restrictAlong χE h).toValuationSubring.valuation
      (algebraMap F FE f - algebraMap E FE (σ (χ f))) < 1
theorem

inertiaDegAlong_eq_one

L370 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.inertiaDegAlong_eq_one
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Restrict
variable {E FE F'E : Type*} [Field E] [Field FE] [Algebra E FE] [Field F'E] [Algebra E F'E]
Lean source · statement
theorem inertiaDegAlong_eq_one [IsAlgClosed E] [IsCurveOver E FE] [IsCurveOver E F'E]
    (χE : FE →ₐ[E] F'E) (h : χE.toRingHom.IsIntegral) (W : Place E F'E) :
    W.inertiaDegAlong χE h = 1
theorem

reduction_restrictAlong

L381 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.reduction_restrictAlong
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Restrict
variable {E FE F'E : Type*} [Field E] [Field FE] [Algebra E FE] [Field F'E] [Algebra E F'E]
Lean source · statement
theorem reduction_restrictAlong {K F F' : Type*} [Field K] [Field F] [Algebra K F] [Field F']
    [Algebra K F'] [Algebra K E] [Algebra F FE] [Algebra F' F'E]
    [HasPrincipalDivisors E F'E] [HasPrincipalDivisors K F']
    (χ : F →ₐ[K] F') (hχ : χ.toRingHom.IsIntegral) (χE : FE →ₐ[E] F'E)
    (hχE : χE.toRingHom.IsIntegral)
    (hcomm : ∀ f : F, χE (algebraMap F FE f) = algebraMap F' F'E (χ f))
    (A : ValuationSubring E)
    (r : Place E FE → Place K F)
    (hr : ∀ (P : Place E FE) (f : F), f ∈ (r P).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧ P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE a) < 1)
    (r' : Place E F'E → Place K F')
    (hr' : ∀ (Q : Place E F'E) (g : F'), g ∈ (r' Q).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧
        Q.toValuationSubring.valuation (algebraMap F' F'E g - algebraMap E F'E a) < 1)
    (W : Place E F'E) :
    r (W.restrictAlong χE hχE) = (r' W).restrictAlong χ hχ
theorem

sum_single_fiberwise

L404 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.sum_single_fiberwise
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
Lean source · statement
theorem sum_single_fiberwise {ι κ Pl : Type*} [DecidableEq κ] (S : Finset ι) (T : Finset κ)
    (θ : ι → κ) (g : κ → Pl) (a : ι → ℤ) (b : κ → ℤ) (n : ℤ)
    (hθ : ∀ i ∈ S, θ i ∈ T) (hfib : ∀ k ∈ T, ∑ i ∈ S with θ i = k, a i = b k) :
    ∑ i ∈ S, Finsupp.single (g (θ i)) (n * a i) =
      ∑ k ∈ T, (Finsupp.single (g k) (n * b k) : Pl →₀ ℤ)
theorem

exists_reduction

L422 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.exists_reduction
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Reduction
variable {K L E LE : Type*} [Field K] [Field L] [Algebra K L] [IsAlgClosed K] [CharZero K]
  [IsCurveOver K L]
  [Field E] [Field LE] [Algebra K E] [Algebra E LE] [Algebra L LE] [Algebra K LE]
  [IsScalarTower K E LE] [IsScalarTower K L LE] [IsAlgClosed E] [IsCurveOver E LE]
Lean source · statement
theorem exists_reduction
    (hfg : ∃ x : L, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set L)) L)
    (hfgE : ∃ x : LE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set LE)) LE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap L LE)) = ⊤)
    (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1) :
    ∃ r : Place E LE → Place K L, ∀ (Q : Place E LE) (g : L), g ∈ (r Q).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧
        Q.toValuationSubring.valuation (algebraMap L LE g - algebraMap E LE a) < 1
theorem

reduction_eq_comap_of_not_forall_mem

L467 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.reduction_eq_comap_of_not_forall_mem
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Reduction
variable {K L E LE : Type*} [Field K] [Field L] [Algebra K L] [IsAlgClosed K] [CharZero K]
  [IsCurveOver K L]
  [Field E] [Field LE] [Algebra K E] [Algebra E LE] [Algebra L LE] [Algebra K LE]
  [IsScalarTower K E LE] [IsScalarTower K L LE] [IsAlgClosed E] [IsCurveOver E LE]
omit [IsAlgClosed E] [IsCurveOver E LE] in
Lean source · statement
theorem reduction_eq_comap_of_not_forall_mem
    (hfg : ∃ x : L, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set L)) L)
    (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (r : Place E LE → Place K L)
    (hr : ∀ (Q : Place E LE) (g : L), g ∈ (r Q).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧
        Q.toValuationSubring.valuation (algebraMap L LE g - algebraMap E LE a) < 1)
    {Q : Place E LE} (hQ : ¬ ∀ g : L, algebraMap L LE g ∈ Q.toValuationSubring) :
    (r Q).toValuationSubring = Q.toValuationSubring.comap (algebraMap L LE)
theorem

mem_reduction_iff_of_centred

L490 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.mem_reduction_iff_of_centred
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Reduction
variable {K L E LE : Type*} [Field K] [Field L] [Algebra K L] [IsAlgClosed K] [CharZero K]
  [IsCurveOver K L]
  [Field E] [Field LE] [Algebra K E] [Algebra E LE] [Algebra L LE] [Algebra K LE]
  [IsScalarTower K E LE] [IsScalarTower K L LE] [IsAlgClosed E] [IsCurveOver E LE]
omit [IsAlgClosed K] [CharZero K] [IsCurveOver K L] [Algebra K LE] [IsScalarTower K E LE]
  [IsScalarTower K L LE] [IsAlgClosed E] [IsCurveOver E LE] in
Lean source · statement
theorem mem_reduction_iff_of_centred
    (A : ValuationSubring E) (r : Place E LE → Place K L)
    (hr : ∀ (Q : Place E LE) (g : L), g ∈ (r Q).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧
        Q.toValuationSubring.valuation (algebraMap L LE g - algebraMap E LE a) < 1)
    {Q : Place E LE} {σ : L →ₐ[K] E}
    (hσ : ∀ g : L, Q.toValuationSubring.valuation (algebraMap L LE g - algebraMap E LE (σ g)) < 1)
    (g : L) : g ∈ (r Q).toValuationSubring ↔ σ g ∈ A
theorem

fibre_centred

L512 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.fibre_centred
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Fibre
variable {K F E FE F' F'E : Type*} [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [CharZero K]
  [IsCurveOver K F]
  [Field E] [Field FE] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
  [IsScalarTower K E FE] [IsScalarTower K F FE] [IsAlgClosed E] [IsCurveOver E FE]
  [Field F'] [Algebra K F'] [IsCurveOver K F']
  [Field F'E] [Algebra E F'E] [Algebra F' F'E] [Algebra K F'E]
  [IsScalarTower K E F'E] [IsScalarTower K F' F'E] [IsCurveOver E F'E]
Lean source · statement
theorem fibre_centred
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (hfg' : ∃ x : F', Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F')
    (hfgE' : ∃ x : F'E, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set F'E)) F'E)
    (hgen' : IntermediateField.adjoin E (Set.range (algebraMap F' F'E)) = ⊤)
    (χ : F →ₐ[K] F') (hfin : FiniteAlong K χ)
    (χE : FE →ₐ[E] F'E) (hχEi : χE.toRingHom.IsIntegral)
    (hχE : ∀ f : F, χE (algebraMap F FE f) = algebraMap F' F'E (χ f))
    (hFI : FundamentalIdentityAlong E χE hχEi)
    {P : Place E FE} {e : F →ₐ[K] E}
    (hP : ∀ f : F, P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE (e f)) < 1) :
    (∀ W ∈ Place.fiberAlong χE hχEi P, W.ramificationIndexAlong χE = 1) ∧
    (∀ W ∈ Place.fiberAlong χE hχEi P, ∃ σ : F' →ₐ[K] E, σ.comp χ = e ∧
      ∀ y : F', W.toValuationSubring.valuation
        (algebraMap F' F'E y - algebraMap E F'E (σ y)) < 1) ∧
    (∀ (σ : F' →ₐ[K] E) (W : Place E F'E), σ.comp χ = e →
      (∀ y : F', W.toValuationSubring.valuation
        (algebraMap F' F'E y - algebraMap E F'E (σ y)) < 1) →
      W ∈ Place.fiberAlong χE hχEi P) ∧
    {σ : F' →ₐ[K] E | σ.comp χ = e}.Finite
theorem

fibre_identity_of_forall_mem

L639 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.fibre_identity_of_forall_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Fibre
variable {K F E FE F' F'E : Type*} [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [CharZero K]
  [IsCurveOver K F]
  [Field E] [Field FE] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
  [IsScalarTower K E FE] [IsScalarTower K F FE] [IsAlgClosed E] [IsCurveOver E FE]
  [Field F'] [Algebra K F'] [IsCurveOver K F']
  [Field F'E] [Algebra E F'E] [Algebra F' F'E] [Algebra K F'E]
  [IsScalarTower K E F'E] [IsScalarTower K F' F'E] [IsCurveOver E F'E]
Lean source · full declaration
theorem fibre_identity_of_forall_mem
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (hfg' : ∃ x : F', Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F')
    (hfgE' : ∃ x : F'E, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set F'E)) F'E)
    (hgen' : IntermediateField.adjoin E (Set.range (algebraMap F' F'E)) = ⊤)
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfinφ : FiniteAlong K φ)
    (φE : FE →ₐ[E] F'E) (hφE : φE.toRingHom.IsIntegral)
    (hφcomm : ∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f))
    (hFIE : FundamentalIdentityAlong E φE hφE)
    (A : ValuationSubring E)
    (r : Place E FE → Place K F)
    (hr : ∀ (P : Place E FE) (f : F), f ∈ (r P).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧ P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE a) < 1)
    (r' : Place E F'E → Place K F')
    (hr' : ∀ (Q : Place E F'E) (g : F'), g ∈ (r' Q).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧
        Q.toValuationSubring.valuation (algebraMap F' F'E g - algebraMap E F'E a) < 1)
    {P : Place E FE} (hint : ∀ f : F, algebraMap F FE f ∈ P.toValuationSubring)
    {q : Place K F'} (hq : q ∈ Place.fiberAlong φ hφ (r P)) [DecidableEq (Place K F')] :
    ∑ W ∈ (Place.fiberAlong φE hφE P).filter (fun W => r' W = q),
        (W.ramificationIndexAlong φE : ℤ) = q.ramificationIndexAlong φ := by
  obtain ⟨e, hP⟩ := (Place.existsUnique_valuation_sub_lt_one_of_constantFieldExtension
    K F hfg E FE hfgE hgen).2 P hint
  have C1F' := Place.existsUnique_valuation_sub_lt_one_of_constantFieldExtension
    K F' hfg' E F'E hfgE' hgen'
  choose Qc hQc hQu using C1F'.1
  obtain ⟨ha, hb, hc, hSfin⟩ :=
    fibre_centred hfg hfgE hgen hfg' hfgE' hgen' φ hfinφ φE hφE hφcomm hFIE hP
  have hev₀ : ∀ f : F, f ∈ (r P).toValuationSubring ↔ e f ∈ A := fun f =>
    mem_reduction_iff_of_centred A r hr hP f
  have hcount := Place.ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong K F F' hfg φ hφ
    hfinφ E A e (r P) hev₀ q (Place.mem_fiberAlong.mp hq)
  set Sq : Set (F' →ₐ[K] E) := {σ | σ.comp φ = e ∧
    ∀ g : F', g ∈ q.toValuationSubring ↔ σ g ∈ A} with hSq
  have hinj : Function.Injective Qc := fun σ τ h =>
    centre_unique (Qc σ) (hQc σ) (fun y => by rw [h]; exact hQc τ y)
  have himage : (((Place.fiberAlong φE hφE P).filter (fun W => r' W = q) : Finset (Place E F'E)) :
      Set (Place E F'E)) = Qc '' Sq := by
    ext W
    rw [Finset.coe_filter, Set.mem_ofPred_eq, Set.mem_image]
    constructor
    · rintro ⟨hW, hWq⟩
      obtain ⟨σ, hσ, hWσ⟩ := hb W hW
      refine ⟨σ, ⟨hσ, fun g => ?_⟩, (hQu σ W hWσ).symm⟩
      rw [← hWq]
      exact mem_reduction_iff_of_centred A r' hr' hWσ g
    · rintro ⟨σ, ⟨hσ, hσq⟩, rfl⟩
      refine ⟨hc σ _ hσ (hQc σ), Place.ext (SetLike.ext fun g => ?_)⟩
      rw [mem_reduction_iff_of_centred A r' hr' (hQc σ) g, hσq g]
  have hone : ∀ W ∈ (Place.fiberAlong φE hφE P).filter (fun W => r' W = q),
      (W.ramificationIndexAlong φE : ℤ) = 1 := fun W hW => by
    rw [ha W (Finset.mem_filter.mp hW).1, Nat.cast_one]
  rw [Finset.sum_congr rfl hone, Finset.sum_const, nsmul_eq_mul, mul_one, ← hcount,
    ← Set.ncard_coe_finset, himage, Set.ncard_image_of_injective _ hinj]
theorem

ramificationIndexAlong_eq_of_ord_eq

L703 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.ramificationIndexAlong_eq_of_ord_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Fibre
variable {K F E FE F' F'E : Type*} [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [CharZero K]
  [IsCurveOver K F]
  [Field E] [Field FE] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
  [IsScalarTower K E FE] [IsScalarTower K F FE] [IsAlgClosed E] [IsCurveOver E FE]
  [Field F'] [Algebra K F'] [IsCurveOver K F']
  [Field F'E] [Algebra E F'E] [Algebra F' F'E] [Algebra K F'E]
  [IsScalarTower K E F'E] [IsScalarTower K F' F'E] [IsCurveOver E F'E]
omit [CharZero K] [IsAlgClosed K] [IsCurveOver K F] [Algebra K E] [Algebra K FE] [IsScalarTower K E
  FE]
  [IsScalarTower K F FE] [IsAlgClosed E] [IsCurveOver E FE] [IsCurveOver K F'] [Algebra K F'E]
  [IsScalarTower K E F'E] [IsScalarTower K F' F'E] [IsCurveOver E F'E] in
Lean source · statement
theorem ramificationIndexAlong_eq_of_ord_eq [HasPrincipalDivisors K F']
    [HasPrincipalDivisors E F'E]
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (φE : FE →ₐ[E] F'E) (hφE : φE.toRingHom.IsIntegral)
    (hφcomm : ∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f))
    {P : Place E FE} {v₀ : Place K F} (hPord : ∀ f : F, P.ord (algebraMap F FE f) = v₀.ord f)
    {q : Place K F'} (hq : q.restrictAlong φ hφ = v₀)
    {W : Place E F'E} (hWord : ∀ g : F', W.ord (algebraMap F' F'E g) = q.ord g)
    (hWP : W.restrictAlong φE hφE = P) :
    W.ramificationIndexAlong φE = q.ramificationIndexAlong φ
theorem

fibre_identity_of_not_forall_mem

L723 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.fibre_identity_of_not_forall_mem
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Fibre
variable {K F E FE F' F'E : Type*} [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [CharZero K]
  [IsCurveOver K F]
  [Field E] [Field FE] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
  [IsScalarTower K E FE] [IsScalarTower K F FE] [IsAlgClosed E] [IsCurveOver E FE]
  [Field F'] [Algebra K F'] [IsCurveOver K F']
  [Field F'E] [Algebra E F'E] [Algebra F' F'E] [Algebra K F'E]
  [IsScalarTower K E F'E] [IsScalarTower K F' F'E] [IsCurveOver E F'E]
omit [IsAlgClosed E] [IsCurveOver E FE] in
Lean source · full declaration
theorem fibre_identity_of_not_forall_mem
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (hfg' : ∃ x : F', Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F')
    (hfgE' : ∃ x : F'E, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set F'E)) F'E)
    (hgen' : IntermediateField.adjoin E (Set.range (algebraMap F' F'E)) = ⊤)
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (φE : FE →ₐ[E] F'E) (hφE : φE.toRingHom.IsIntegral)
    (hφcomm : ∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f))
    (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (r : Place E FE → Place K F)
    (hr : ∀ (P : Place E FE) (f : F), f ∈ (r P).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧ P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE a) < 1)
    (r' : Place E F'E → Place K F')
    (hr' : ∀ (Q : Place E F'E) (g : F'), g ∈ (r' Q).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧
        Q.toValuationSubring.valuation (algebraMap F' F'E g - algebraMap E F'E a) < 1)
    {P : Place E FE} (hint : ¬ ∀ f : F, algebraMap F FE f ∈ P.toValuationSubring)
    {q : Place K F'} (hq : q ∈ Place.fiberAlong φ hφ (r P)) [DecidableEq (Place K F')] :
    ∑ W ∈ (Place.fiberAlong φE hφE P).filter (fun W => r' W = q),
        (W.ramificationIndexAlong φE : ℤ) = q.ramificationIndexAlong φ := by
  have hrP : (r P).toValuationSubring = P.toValuationSubring.comap (algebraMap F FE) :=
    reduction_eq_comap_of_not_forall_mem hfg A hKA r hr hint
  obtain ⟨P', -, hP'ord, hP'u⟩ :=
    Place.exists_comap_algebraMap_eq_of_constantFieldExtension K F E FE hfg hfgE hgen (r P)
  have hPP' : P = P' := hP'u P hrP.symm
  have hPord : ∀ f : F, P.ord (algebraMap F FE f) = (r P).ord f := fun f => by
    rw [← hP'ord f, hPP']
  obtain ⟨Wq, hWq, hWqord, hWqu⟩ :=
    Place.exists_comap_algebraMap_eq_of_constantFieldExtension K F' E F'E hfg' hfgE' hgen' q
  have hqv : q.restrictAlong φ hφ = r P := Place.mem_fiberAlong.mp hq
  have hWqP : Wq.restrictAlong φE hφE = P := by
    rw [hPP']
    refine hP'u _ (SetLike.ext fun f => ?_)
    rw [ValuationSubring.mem_comap, mem_restrictAlong_iff, hφcomm, ← hqv, mem_restrictAlong_iff,
      ← hWq, ValuationSubring.mem_comap]
  have hrWq : r' Wq = q := by
    refine Place.ext (SetLike.ext fun g => ?_)
    rw [hr', exists_mem_valuation_sub_lt_one_iff_of_comap Wq q hWq.symm A hKA g, ← hWq,
      ValuationSubring.mem_comap]
  obtain ⟨f₀, hf₀⟩ : ∃ f : F, algebraMap F FE f ∉ P.toValuationSubring := by
    push Not at hint
    exact hint
  have huniq : ∀ W ∈ (Place.fiberAlong φE hφE P).filter (fun W => r' W = q), W = Wq := by
    intro W hW
    obtain ⟨hWZ, hWq'⟩ := Finset.mem_filter.mp hW
    have hWP : W.restrictAlong φE hφE = P := Place.mem_fiberAlong.mp hWZ
    have hWint : ¬ ∀ g : F', algebraMap F' F'E g ∈ W.toValuationSubring := fun h => hf₀ (by
      rw [← hWP, mem_restrictAlong_iff, hφcomm]
      exact h (φ f₀))
    have hW' : (r' W).toValuationSubring = W.toValuationSubring.comap (algebraMap F' F'E) :=
      reduction_eq_comap_of_not_forall_mem hfg' A hKA r' hr' hWint
    rw [hWq'] at hW'
    exact hWqu W hW'.symm
  have he : Wq.ramificationIndexAlong φE = q.ramificationIndexAlong φ :=
    ramificationIndexAlong_eq_of_ord_eq φ hφ φE hφE hφcomm hPord hqv hWqord hWqP
  have hmem : Wq ∈ (Place.fiberAlong φE hφE P).filter (fun W => r' W = q) :=
    Finset.mem_filter.mpr ⟨Place.mem_fiberAlong.mpr hWqP, hrWq⟩
  have hsingle : (Place.fiberAlong φE hφE P).filter (fun W => r' W = q) = {Wq} :=
    Finset.eq_singleton_iff_unique_mem.mpr ⟨hmem, huniq⟩
  rw [hsingle, Finset.sum_singleton, he]
theorem

mapDomain_correspondence_single

L790 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence.AlgebraicCurve.PlaceReductionCorrespondence.mapDomain_correspondence_single
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceReductionCorrespondence
open _root_.AlgebraicCurve
section Fibre
variable {K F E FE F' F'E : Type*} [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [CharZero K]
  [IsCurveOver K F]
  [Field E] [Field FE] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
  [IsScalarTower K E FE] [IsScalarTower K F FE] [IsAlgClosed E] [IsCurveOver E FE]
  [Field F'] [Algebra K F'] [IsCurveOver K F']
  [Field F'E] [Algebra E F'E] [Algebra F' F'E] [Algebra K F'E]
  [IsScalarTower K E F'E] [IsScalarTower K F' F'E] [IsCurveOver E F'E]
Lean source · statement
theorem mapDomain_correspondence_single
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (hfg' : ∃ x : F', Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F')
    (hfgE' : ∃ x : F'E, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set F'E)) F'E)
    (hgen' : IntermediateField.adjoin E (Set.range (algebraMap F' F'E)) = ⊤)
    (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (hfinφ : FiniteAlong K φ)
    (φE ψE : FE →ₐ[E] F'E) (hφE : φE.toRingHom.IsIntegral) (hψE : ψE.toRingHom.IsIntegral)
    (hφcomm : ∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f))
    (hψcomm : ∀ f : F, ψE (algebraMap F FE f) = algebraMap F' F'E (ψ f))
    (hFIE : FundamentalIdentityAlong E φE hφE)
    (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (r : Place E FE → Place K F)
    (hr : ∀ (P : Place E FE) (f : F), f ∈ (r P).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧ P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE a) < 1)
    (r' : Place E F'E → Place K F')
    (hr' : ∀ (Q : Place E F'E) (g : F'), g ∈ (r' Q).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧
        Q.toValuationSubring.valuation (algebraMap F' F'E g - algebraMap E F'E a) < 1)
    (P : Place E FE) (n : ℤ) :
    Finsupp.mapDomain r (Divisor.correspondence φE ψE hφE hψE (Finsupp.single P n)) =
      Divisor.correspondence φ ψ hφ hψ (Finsupp.mapDomain r (Finsupp.single P n))
theorem

mapDomain_placeReduction_correspondence

L860 ↗
AlgebraicCurve.Divisor.mapDomain_placeReduction_correspondence
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_correspondence
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  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.RationalFunctionField.placeInfty_toValuationSubring
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
open AlgebraicCurve.PlaceReductionCorrespondence in
Lean source · statement
theorem _root_.AlgebraicCurve.Divisor.mapDomain_placeReduction_correspondence
    (K F : Type*) [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [CharZero K] [IsCurveOver K F]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (F' : Type*) [Field F'] [Algebra K F'] [HasPrincipalDivisors K F']
    (φ ψ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (hfin : FiniteAlong K ψ) (hN : NormFormulaAlong K ψ hfin)
    (E FE : Type*) [Field E] [Field FE] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
    [IsScalarTower K E FE] [IsScalarTower K F FE] [IsAlgClosed E] [IsCurveOver E FE]
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (F'E : Type*) [Field F'E] [Algebra E F'E] [Algebra F' F'E] [Algebra K F'E]
    [IsScalarTower K E F'E] [IsScalarTower K F' F'E] [IsCurveOver E F'E]
    (hfgE' : ∃ x' : F'E, Transcendental E x' ∧
      FiniteDimensional (IntermediateField.adjoin E ({x'} : Set F'E)) F'E)
    (hgen' : IntermediateField.adjoin E (Set.range (algebraMap F' F'E)) = ⊤)
    (φE ψE : FE →ₐ[E] F'E)
    (hφcomm : ∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f))
    (hψcomm : ∀ f : F, ψE (algebraMap F FE f) = algebraMap F' F'E (ψ f))
    (hφE : φE.toRingHom.IsIntegral) (hψE : ψE.toRingHom.IsIntegral)
    (hFIE : FundamentalIdentityAlong E φE hφE)
    (hfinE : FiniteAlong E ψE) (hNE : NormFormulaAlong E ψE hfinE)
    (A : ValuationSubring E) (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (r : Place E FE → Place K F)
    (hr : ∀ (P : Place E FE) (f : F), f ∈ (r P).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧ P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE a) < 1)
    (D : Divisor E FE) :
    Finsupp.mapDomain r (Divisor.correspondence φE ψE hφE hψE D) =
      Divisor.correspondence φ ψ hφ hψ (Finsupp.mapDomain r D)

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