NYLL
Module

Exists_constantFieldDescent_correspondence.lean

Nyll.AlgebraicCurves.Divisors.Exists_constantFieldDescent_correspondence
12 declarations indexed from sourceView source ↗

Module documentation

Exists constant Field Descent correspondence

Imports9
Imported by1

Declarations

theorem

nonempty_ringHom_complex

L67 ↗
AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence.AlgebraicCurve.DescentCorrespondenceProof.nonempty_ringHom_complex
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DescentCorrespondenceProof
open _root_.AlgebraicCurve
Lean source · statement
theorem nonempty_ringHom_complex (k : Type u) [Field k] [CharZero k] [Countable k] :
    Nonempty (k →+* ℂ)
theorem

isAlgebraic_of_rational_relation

L93 ↗
AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence.AlgebraicCurve.DescentCorrespondenceProof.isAlgebraic_of_rational_relation
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DescentCorrespondenceProof
open _root_.AlgebraicCurve
Lean source · statement
theorem isAlgebraic_of_rational_relation {k Φ : Type*} [Field k] [Field Φ] [Algebra k Φ]
    (x y : Φ) (J : Finset ℕ) (r s : ℕ → k[X])
    (hrel : ∑ j ∈ J, (aeval x (r j) / aeval x (s j)) * y ^ j = 0)
    (hne : ∃ j ∈ J, aeval x (r j) / aeval x (s j) ≠ 0) :
    IsAlgebraic k⟮x⟯ y
theorem

descent_abstract

L122 ↗
AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence.AlgebraicCurve.DescentCorrespondenceProof.descent_abstract
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DescentCorrespondenceProof
open _root_.AlgebraicCurve
Lean source · statement
theorem descent_abstract {k F : Type*} [Field k] [Field F] [Algebra k F]
    {x y : F} (hx : Transcendental k x) (J : Finset ℕ) (r s : ℕ → k[X])
    (hrel : ∑ j ∈ J, (aeval x (r j) / aeval x (s j)) * y ^ j = 0)
    (hne : ∃ j ∈ J, aeval x (r j) / aeval x (s j) ≠ 0) :
    ∃ x₀ y₀ : k⟮x, y⟯, (x₀ : F) = x ∧ (y₀ : F) = y ∧ Transcendental k x₀ ∧
      FiniteDimensional k⟮x₀⟯ k⟮x, y⟯ ∧ k⟮x₀, y₀⟯ = ⊤
theorem

aeval_mem_of_lift

L167 ↗
AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence.AlgebraicCurve.DescentCorrespondenceProof.aeval_mem_of_lift
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DescentCorrespondenceProof
open _root_.AlgebraicCurve
Lean source · statement
theorem aeval_mem_of_lift {K₀ K F : Type*} [Field K₀] [Field K] [Field F] [Algebra K₀ K]
    [Algebra K F] [Algebra K₀ F] [IsScalarTower K₀ K F]
    {M : IntermediateField K₀ F} {x : F} (hx : x ∈ M) {p : K[X]}
    (hp : ∃ p₀ : K₀[X], p₀.map (algebraMap K₀ K) = p) : aeval x p ∈ M
theorem

aeval_mem_of_repr

L178 ↗
AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence.AlgebraicCurve.DescentCorrespondenceProof.aeval_mem_of_repr
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DescentCorrespondenceProof
open _root_.AlgebraicCurve
Lean source · statement
theorem aeval_mem_of_repr {K₀ K F : Type*} [Field K₀] [Field K] [Field F] [Algebra K₀ K]
    [Algebra K F] [Algebra K₀ F] [IsScalarTower K₀ K F]
    {M : IntermediateField K₀ F} {x y : F} (hx : x ∈ M) (hy : y ∈ M)
    (P : K⟮x⟯[X]) (rp sp : ℕ → K[X])
    (hrep : ∀ i, ((P.coeff i : K⟮x⟯) : F) = aeval x (rp i) / aeval x (sp i))
    (hr : ∀ i ∈ P.support, ∃ r₀ : K₀[X], r₀.map (algebraMap K₀ K) = rp i)
    (hs : ∀ i ∈ P.support, ∃ s₀ : K₀[X], s₀.map (algebraMap K₀ K) = sp i) :
    aeval y P ∈ M
theorem

exists_countable_algebraicallyClosed_constants

L192 ↗
AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence.AlgebraicCurve.DescentCorrespondenceProof.exists_countable_algebraicallyClosed_constants
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DescentCorrespondenceProof
open _root_.AlgebraicCurve
Lean source · statement
theorem exists_countable_algebraicallyClosed_constants
    (K : Type*) [Field K] [IsAlgClosed K] (C : Set K) (hCfin : C.Finite) :
    ∃ (L : Subfield K) (K₀ : IntermediateField L K),
      IsAlgClosed K₀ ∧ Countable K₀ ∧ C ⊆ Set.range (algebraMap K₀ K)
theorem

finiteDimensional_adjoin_map

L216 ↗
AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence.AlgebraicCurve.DescentCorrespondenceProof.finiteDimensional_adjoin_map
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DescentCorrespondenceProof
open _root_.AlgebraicCurve
section Tools
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
Lean source · statement
theorem finiteDimensional_adjoin_map {x : F} (hfin : FiniteDimensional k⟮x⟯ F)
    (ψ : F →ₐ[k] F') (hψfin : FiniteAlong k ψ) : FiniteDimensional k⟮ψ x⟯ F'
def

restrictHom

L240 ↗
AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence.AlgebraicCurve.DescentCorrespondenceProof.restrictHom
Documentation

Restriction of an algebra homomorphism to intermediate fields that it maps into one another.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DescentCorrespondenceProof
open _root_.AlgebraicCurve
section Tools
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
Lean source · full declaration
def restrictHom {k₀ : Type*} [Field k₀] [Algebra k₀ k] [Algebra k₀ F] [Algebra k₀ F']
    [IsScalarTower k₀ k F] [IsScalarTower k₀ k F']
    (σ : F →ₐ[k] F') (M : IntermediateField k₀ F) (N : IntermediateField k₀ F')
    (h : ∀ z ∈ M, σ z ∈ N) : M →ₐ[k₀] N where
  toFun z := ⟨σ (z : F), h z z.2⟩
  map_one' := Subtype.ext (map_one σ)
  map_mul' a b := Subtype.ext (map_mul σ (a : F) (b : F))
  map_zero' := Subtype.ext (map_zero σ)
  map_add' a b := Subtype.ext (map_add σ (a : F) (b : F))
  commutes' c := Subtype.ext (by
    change σ (algebraMap k₀ F c) = algebraMap k₀ F' c
    rw [IsScalarTower.algebraMap_apply k₀ k F, σ.commutes, ← IsScalarTower.algebraMap_apply])
theorem

coe_restrictHom

L253 ↗
AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence.AlgebraicCurve.DescentCorrespondenceProof.coe_restrictHom
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DescentCorrespondenceProof
open _root_.AlgebraicCurve
section Tools
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
Lean source · statement
theorem coe_restrictHom {k₀ : Type*} [Field k₀] [Algebra k₀ k] [Algebra k₀ F]
    [Algebra k₀ F'] [IsScalarTower k₀ k F] [IsScalarTower k₀ k F']
    (σ : F →ₐ[k] F') (M : IntermediateField k₀ F) (N : IntermediateField k₀ F')
    (h : ∀ z ∈ M, σ z ∈ N) (z : M) : ((restrictHom σ M N h z : N) : F') = σ (z : F)
theorem

finiteAlong_of_isIntegral_of_adjoin_eq_top

L258 ↗
AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence.AlgebraicCurve.DescentCorrespondenceProof.finiteAlong_of_isIntegral_of_adjoin_eq_top
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DescentCorrespondenceProof
open _root_.AlgebraicCurve
section Tools
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
Lean source · statement
theorem finiteAlong_of_isIntegral_of_adjoin_eq_top {A B : Type*} [Field A] [Field B]
    [Algebra k A] [Algebra k B] (φ : A →ₐ[k] B)
    (hφ : φ.toRingHom.IsIntegral) (T : Finset B)
    (hT : IntermediateField.adjoin k (T : Set B) = ⊤) : FiniteAlong k φ
theorem

finiteAlong_of_transcendental_image

L278 ↗
AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence.AlgebraicCurve.DescentCorrespondenceProof.finiteAlong_of_transcendental_image
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace DescentCorrespondenceProof
open _root_.AlgebraicCurve
section Tools
variable {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
Lean source · statement
theorem finiteAlong_of_transcendental_image {A B : Type*} [Field A] [Field B]
    [Algebra k A] [Algebra k B] (σ₀ : A →ₐ[k] B)
    (T : Finset B) (hT : IntermediateField.adjoin k (T : Set B) = ⊤)
    (w : B) [FiniteDimensional k⟮w⟯ B]
    (a₀ : A) (ha₀ : Transcendental k (σ₀ a₀)) : FiniteAlong k σ₀
theorem

exists_constantFieldDescent_correspondence

L315 ↗
AlgebraicCurve.exists_constantFieldDescent_correspondence
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Exists_constantFieldDescent_correspondence
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_.Polynomial
open _root_.IntermediateField
open _root_.Cardinal
open _root_.AlgebraicCurve
universe u v w x
open AlgebraicCurve.DescentCorrespondenceProof in
Lean source · statement
theorem _root_.AlgebraicCurve.exists_constantFieldDescent_correspondence
    (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)
    {ι : Type w} [Finite ι] (F' : ι → Type x) [∀ i, Field (F' i)] [∀ i, Algebra K (F' i)]
    (φ ψ : ∀ i, F →ₐ[K] F' i)
    (hfin : ∀ i, FiniteAlong K (ψ i)) :
    ∃ (K₀ : Type u) (F₀ : Type v) (F'₀ : ι → Type x)
      (_ : Field K₀) (_ : Field F₀) (_ : ∀ i, Field (F'₀ i))
      (_ : Algebra K₀ K) (_ : Algebra K₀ ℂ) (_ : IsAlgClosed K₀) (_ : Countable K₀)
      (_ : Algebra K₀ F₀) (_ : Algebra F₀ F) (_ : Algebra K₀ F)
      (_ : IsScalarTower K₀ K F) (_ : IsScalarTower K₀ F₀ F) (_ : IsCurveOver K₀ F₀)
      (_ : ∀ i, Algebra K₀ (F'₀ i)) (_ : ∀ i, Algebra (F'₀ i) (F' i)) (_ : ∀ i, Algebra K₀ (F' i))
      (_ : ∀ i, IsScalarTower K₀ K (F' i)) (_ : ∀ i, IsScalarTower K₀ (F'₀ i) (F' i))
      (_ : ∀ i, IsCurveOver K₀ (F'₀ i))
      (φ₀ ψ₀ : ∀ i, F₀ →ₐ[K₀] F'₀ i),
      (∃ x : F₀, Transcendental K₀ x ∧
        FiniteDimensional (IntermediateField.adjoin K₀ ({x} : Set F₀)) F₀) ∧
      IntermediateField.adjoin K (Set.range (algebraMap F₀ F)) = ⊤ ∧
      (∀ i, ∃ x : F'₀ i, Transcendental K₀ x ∧
        FiniteDimensional (IntermediateField.adjoin K₀ ({x} : Set (F'₀ i))) (F'₀ i)) ∧
      (∀ i, IntermediateField.adjoin K (Set.range (algebraMap (F'₀ i) (F' i))) = ⊤) ∧
      (∀ i (f : F₀), φ i (algebraMap F₀ F f) = algebraMap (F'₀ i) (F' i) (φ₀ i f)) ∧
      (∀ i (f : F₀), ψ i (algebraMap F₀ F f) = algebraMap (F'₀ i) (F' i) (ψ₀ i f)) ∧
      (∀ i, FiniteAlong K₀ (φ₀ i)) ∧ (∀ i, FiniteAlong K₀ (ψ₀ i))

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