NYLL
Module

Exists_baseChange_correspondence_of_constantFieldExtension.lean

Nyll.AlgebraicCurves.Divisors.Exists_baseChange_correspondence_of_constantFieldExtension
23 declarations indexed from sourceView source ↗

Module documentation

Exists base Change correspondence of constant Field Extension

Imports11
Imported by1

Declarations

theorem

mem_of_valuation_lt_one

L71 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.mem_of_valuation_lt_one
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

L75 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.eq_zero_of_valuation_algebraMap_lt_one
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

L85 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.centre_unique
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

L97 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.algebraMap_mem_of_centred
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

valuation_lt_one_iff_inv_not_mem

L107 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.valuation_lt_one_iff_inv_not_mem
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

L111 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.valuation_comap_lt_one_iff
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

L122 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.valuation_restrictAlong_lt_one_iff
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

span_eq_top_of_adjoin_eq_top

L135 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.span_eq_top_of_adjoin_eq_top
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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) = ⊤
def

liftMap

L185 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.liftMap
Documentation

The tensor-product homomorphism induced by the specified map of function fields.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
open _root_.AlgebraicCurve
section Lift
variable {K F E M : Type*} [Field K] [Field F] [Algebra K F] [Field E] [Algebra K E]
  [Field M] [Algebra K M] [Algebra E M] [IsScalarTower K E M]
variable (E) in
Lean source · statement
def liftMap (g : F →ₐ[K] M) : E ⊗[K] F →ₐ[E] M
theorem

liftMap_tmul

L188 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.liftMap_tmul
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
open _root_.AlgebraicCurve
section Lift
variable {K F E M : Type*} [Field K] [Field F] [Algebra K F] [Field E] [Algebra K E]
  [Field M] [Algebra K M] [Algebra E M] [IsScalarTower K E M]
variable (E) in
Lean source · statement
theorem liftMap_tmul (g : F →ₐ[K] M) (c : E) (f : F) :
    liftMap E g (c ⊗ₜ f) = algebraMap E M c * g f
theorem

liftMap_injective

L191 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.liftMap_injective
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
open _root_.AlgebraicCurve
section Lift
variable {K F E M : Type*} [Field K] [Field F] [Algebra K F] [Field E] [Algebra K E]
  [Field M] [Algebra K M] [Algebra E M] [IsScalarTower K E M]
variable (E) in
Lean source · full declaration
theorem liftMap_injective (g : F →ₐ[K] M) {ι : Type*} (b : Module.Basis ι K F)
    (hli : LinearIndependent E (fun i => g (b i))) : Function.Injective (liftMap E g) := by
  classical
  let bE := Algebra.TensorProduct.basis E b
  rw [injective_iff_map_eq_zero]
  intro z hz
  have hrepr : Finsupp.linearCombination E bE (bE.repr z) = z := bE.linearCombination_repr z
  have hcomp : ((liftMap E g).toLinearMap : E ⊗[K] F → M) ∘ bE = fun i => g (b i) := by
    funext i
    simp [bE, Algebra.TensorProduct.basis_apply]
  have h0 : Finsupp.linearCombination E (fun i => g (b i)) (bE.repr z) = 0 := by
    rw [← hcomp, ← Finsupp.apply_linearCombination, hrepr]
    exact hz
  have hc : bE.repr z = 0 := linearIndependent_iff.mp hli _ h0
  rw [← hrepr, hc, map_zero]
theorem

exists_extension

L220 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.exists_extension
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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]
section WithTower
variable [Algebra K E] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
  [Algebra K F'E] [IsScalarTower K E F'E] [IsScalarTower K F' F'E]
Lean source · statement
theorem exists_extension [IsAlgClosed K] [CharZero K]
    (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') :
    ∃ χE : FE →ₐ[E] F'E, ∀ f : F, χE (algebraMap F FE f) = algebraMap F' F'E (χ f)
theorem

isIntegral_extension

L272 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.isIntegral_extension
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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 isIntegral_extension (χ : F →ₐ[K] F') (hχ : χ.toRingHom.IsIntegral) (χ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)) = ⊤) :
    χE.toRingHom.IsIntegral
theorem

finite_extension

L304 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.finite_extension
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

L344 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.essFiniteType_of_fg
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

L355 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.finiteAlong_of_isIntegral
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

L370 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.fg_of_finiteAlong
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

L402 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.centred_restrictAlong
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

L415 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.inertiaDegAlong_eq_one
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

exists_of_correspondence_single_ne_zero

L426 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.exists_of_correspondence_single_ne_zero
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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 exists_of_correspondence_single_ne_zero [HasPrincipalDivisors E F'E]
    (φE ψE : FE →ₐ[E] F'E) (hφ : φE.toRingHom.IsIntegral) (hψ : ψE.toRingHom.IsIntegral)
    {P Q : Place E FE}
    (hQ : Divisor.correspondence φE ψE hφ hψ (Finsupp.single P 1) Q ≠ 0) :
    ∃ W ∈ Place.fiberAlong φE hφ P, W.restrictAlong ψE hψ = Q
theorem

fibre_centred

L453 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.fibre_centred
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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

correspondence_single_apply_centred

L580 ↗
AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension.AlgebraicCurve.BaseChangeCorrespondence.correspondence_single_apply_centred
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace BaseChangeCorrespondence
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 correspondence_single_apply_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 ψE : FE →ₐ[E] F'E) (hφEi : φE.toRingHom.IsIntegral) (hψEi : ψE.toRingHom.IsIntegral)
    (hφE : ∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f))
    (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)
    {Q : Place E FE} {e' : F →ₐ[K] E}
    (hQ : ∀ f : F, Q.toValuationSubring.valuation
      (algebraMap F FE f - algebraMap E FE (e' f)) < 1) :
    Divisor.correspondence φE ψE hφEi hψEi (Finsupp.single P 1) Q =
      (∑ᶠ σ ∈ {σ : F' →ₐ[K] E | σ.comp φ = e},
        Finsupp.single (σ.comp ψ) (1 : ℤ) : (F →ₐ[K] E) →₀ ℤ) e'
theorem

exists_baseChange_correspondence_of_constantFieldExtension

L647 ↗
AlgebraicCurve.exists_baseChange_correspondence_of_constantFieldExtension
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_baseChange_correspondence_of_constantFieldExtension
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
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
open _root_.AlgebraicCurve
open scoped TensorProduct
universe u v w x
open AlgebraicCurve.BaseChangeCorrespondence in
Lean source · statement
theorem _root_.AlgebraicCurve.exists_baseChange_correspondence_of_constantFieldExtension
    (K : Type u) (F : Type v) [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 w) [Field F'] [Algebra K F'] [HasPrincipalDivisors K F']
    (φ ψ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (hFI : FundamentalIdentityAlong K φ hφ)
    (hfin : FiniteAlong K ψ) (hN : NormFormulaAlong K ψ hfin)
    (E : Type x) (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 (max w x)) (_ : 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)
      (φE ψE : FE →ₐ[E] F'E) (hφE : φE.toRingHom.IsIntegral) (hψE : ψE.toRingHom.IsIntegral)
      (_ : FundamentalIdentityAlong E φE hφE) (hfinE : FiniteAlong E ψE)
      (_ : NormFormulaAlong E ψE hfinE),
      (∃ x' : F'E, Transcendental E x' ∧
        FiniteDimensional (IntermediateField.adjoin E ({x'} : Set F'E)) F'E) ∧
      IntermediateField.adjoin E (Set.range (algebraMap F' F'E)) = ⊤ ∧
      (∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f)) ∧
      (∀ f : F, ψE (algebraMap F FE f) = algebraMap F' F'E (ψ f)) ∧
      (∀ (P : Place E FE) (e : F →ₐ[K] E),
        (∀ f : F, P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE (e f)) < 1) →
        ∀ (Q : Place E FE) (e' : F →ₐ[K] E),
        (∀ f : F, Q.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE (e' f)) < 1) →
          Divisor.correspondence φE ψE hφE hψE (Finsupp.single P 1) Q =
            (∑ᶠ σ ∈ {σ : F' →ₐ[K] E | σ.comp φ = e},
              Finsupp.single (σ.comp ψ) (1 : ℤ) : (F →ₐ[K] E) →₀ ℤ) e') ∧
      (∀ (P : Place E FE) (e : F →ₐ[K] E),
        (∀ f : F, P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE (e f)) < 1) →
        ∀ Q : Place E FE, Divisor.correspondence φE ψE hφE hψE (Finsupp.single P 1) Q ≠ 0 →
          ∃ e' : F →ₐ[K] E, ∀ f : F,
            Q.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE (e' f)) < 1) ∧
      (∀ P : Place E FE, (∃ f : F, algebraMap F FE f ∉ P.toValuationSubring) →
        ∀ Q : Place E FE, Divisor.correspondence φE ψE hφE hψE (Finsupp.single P 1) Q ≠ 0 →
          ∃ f : F, algebraMap F FE f ∉ Q.toValuationSubring)

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