NYLL
Module

Place_exists_finite_constantField_form_fiberConstants_eq_singleton.lean

Nyll.AlgebraicCurves.Places.Place_exists_finite_constantField_form_fiberConstants_eq_singleton
19 declarations indexed from sourceView source ↗

Module documentation

Place exists finite constant Field form fiber Constants eq singleton

Imports11
Imported by2

Declarations

theorem

isAlgebraic_of_forall_pow_pow_eq

L64 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.isAlgebraic_of_forall_pow_pow_eq
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
Lean source · statement
theorem isAlgebraic_of_forall_pow_pow_eq (K K' : Type*) [Field K] [Field K'] [Algebra K K']
    (ℓ : ℕ) [Fact ℓ.Prime] (halg : ∀ a : K', ∃ n : ℕ, 0 < n ∧ a ^ ℓ ^ n = a) :
    Algebra.IsAlgebraic K K'
theorem

perfectField_of_forall_pow_pow_eq

L73 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.perfectField_of_forall_pow_pow_eq
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
Lean source · statement
theorem perfectField_of_forall_pow_pow_eq (K' : Type*) [Field K'] (ℓ : ℕ) [Fact ℓ.Prime] [CharP K'
  ℓ]
    (halg : ∀ a : K', ∃ n : ℕ, 0 < n ∧ a ^ ℓ ^ n = a) : PerfectField K'
theorem

mem_iff_zero_or_ord_nonneg

L87 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.mem_iff_zero_or_ord_nonneg
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section PlaceBasics
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mem_iff_zero_or_ord_nonneg (v : Place K F) (f : F) :
    f ∈ v.toValuationSubring ↔ f = 0 ∨ 0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L91 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.mem_of_ord_nonneg
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section PlaceBasics
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mem_of_ord_nonneg (v : Place K F) {f : F} (h : 0 ≤ v.ord f) : f ∈ v.toValuationSubring
theorem

ord_nonneg_of_mem

L94 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.ord_nonneg_of_mem
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section PlaceBasics
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_nonneg_of_mem (v : Place K F) {f : F} (hf : f ≠ 0) (h : f ∈ v.toValuationSubring) :
    0 ≤ v.ord f
theorem

exists_mem_and_not_mem_of_ne

L98 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.exists_mem_and_not_mem_of_ne
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section PlaceBasics
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_mem_and_not_mem_of_ne {w w' : Place K F} (h : w ≠ w') :
    ∃ f : F, f ∈ w.toValuationSubring ∧ f ∉ w'.toValuationSubring
theorem

restrictConstants_eq_iff

L153 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.restrictConstants_eq_iff
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Square
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
Lean source · statement
theorem restrictConstants_eq_iff (w w' : Place K' F') :
    restrictConstants F (K := K) w = restrictConstants F (K := K) w' ↔
      ∀ f : F, algebraMap F F' f ∈ w.toValuationSubring ↔ algebraMap F F' f ∈ w'.toValuationSubring
theorem

constantsAreBase_of_forall

L166 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.constantsAreBase_of_forall
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Square
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
Lean source · statement
theorem constantsAreBase_of_forall (hC' : ConstantsAreBase K' F')
    (h : ∀ a : K', algebraMap K' F' a ∈ Set.range (algebraMap F F') → a ∈ Set.range (algebraMap K
      K')) :
    ConstantsAreBase K F
theorem

mem_range_of_isAlgebraic_of_constantsAreBase

L193 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.mem_range_of_isAlgebraic_of_constantsAreBase
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Square
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F']
Lean source · statement
theorem mem_range_of_isAlgebraic_of_constantsAreBase
    (hC : ConstantsAreBase K F) (y : F) (hy : IsAlgebraic K y) : y ∈ (algebraMap K F).range
abbrev

Klvl

L219 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.Klvl
Documentation

The intermediate constant field generated by the selected finite set over the prime field.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Level
variable (K' : Type u) (F' : Type v) [Field K'] [Field F'] [Algebra K' F']
  (ℓ : ℕ) [Fact ℓ.Prime] [CharP K' ℓ]
attribute [local instance] ZMod.algebra
Lean source · statement
abbrev Klvl (S : Finset K') : IntermediateField (ZMod ℓ) K'
abbrev

Flvl

L224 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.Flvl
Documentation

The intermediate function field generated by the selected finite set over the chosen constants.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Level
variable (K' : Type u) (F' : Type v) [Field K'] [Field F'] [Algebra K' F']
  (ℓ : ℕ) [Fact ℓ.Prime] [CharP K' ℓ]
attribute [local instance] ZMod.algebra
Lean source · statement
abbrev Flvl (S : Finset K') (T : Finset F') : IntermediateField (Klvl K' ℓ S) F'
theorem

finite_Klvl

L228 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.finite_Klvl
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Level
variable (K' : Type u) (F' : Type v) [Field K'] [Field F'] [Algebra K' F']
  (ℓ : ℕ) [Fact ℓ.Prime] [CharP K' ℓ]
attribute [local instance] ZMod.algebra
variable {K' ℓ} in
Lean source · statement
theorem finite_Klvl (halg : ∀ a : K', ∃ n : ℕ, 0 < n ∧ a ^ ℓ ^ n = a) (S : Finset K') :
    Finite (Klvl K' ℓ S)
theorem

range_algebraMap_Klvl

L236 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.range_algebraMap_Klvl
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Level
variable (K' : Type u) (F' : Type v) [Field K'] [Field F'] [Algebra K' F']
  (ℓ : ℕ) [Fact ℓ.Prime] [CharP K' ℓ]
attribute [local instance] ZMod.algebra
variable {K' ℓ} in
Lean source · statement
theorem range_algebraMap_Klvl (S : Finset K') :
    Set.range (algebraMap (Klvl K' ℓ S) F') = algebraMap K' F' '' (Klvl K' ℓ S : Set K')
theorem

coe_Flvl

L245 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.coe_Flvl
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Level
variable (K' : Type u) (F' : Type v) [Field K'] [Field F'] [Algebra K' F']
  (ℓ : ℕ) [Fact ℓ.Prime] [CharP K' ℓ]
attribute [local instance] ZMod.algebra
variable {K' ℓ} in
Lean source · statement
theorem coe_Flvl (S : Finset K') (T : Finset F') :
    ((Flvl K' F' ℓ S T : IntermediateField (Klvl K' ℓ S) F') : Set F')
      = Subfield.closure (algebraMap K' F' '' (Klvl K' ℓ S : Set K') ∪ (T : Set F'))
theorem

coe_Flvl_mono

L252 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.coe_Flvl_mono
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Level
variable (K' : Type u) (F' : Type v) [Field K'] [Field F'] [Algebra K' F']
  (ℓ : ℕ) [Fact ℓ.Prime] [CharP K' ℓ]
attribute [local instance] ZMod.algebra
variable {K' ℓ} in
Lean source · statement
theorem coe_Flvl_mono {S S' : Finset K'} {T T' : Finset F'} (hS : S ⊆ S') (hT : T ⊆ T') :
    ((Flvl K' F' ℓ S T : IntermediateField (Klvl K' ℓ S) F') : Set F')
      ⊆ ((Flvl K' F' ℓ S' T' : IntermediateField (Klvl K' ℓ S') F') : Set F')
theorem

algebraMap_mem_Flvl

L259 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.algebraMap_mem_Flvl
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Level
variable (K' : Type u) (F' : Type v) [Field K'] [Field F'] [Algebra K' F']
  (ℓ : ℕ) [Fact ℓ.Prime] [CharP K' ℓ]
attribute [local instance] ZMod.algebra
variable {K' ℓ} in
Lean source · statement
theorem algebraMap_mem_Flvl {S : Finset K'} (T : Finset F') {a : K'} (ha : a ∈ Klvl K' ℓ S) :
    algebraMap K' F' a ∈ Flvl K' F' ℓ S T
theorem

mem_Flvl_of_mem

L263 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.mem_Flvl_of_mem
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Level
variable (K' : Type u) (F' : Type v) [Field K'] [Field F'] [Algebra K' F']
  (ℓ : ℕ) [Fact ℓ.Prime] [CharP K' ℓ]
attribute [local instance] ZMod.algebra
variable {K' ℓ} in
Lean source · statement
theorem mem_Flvl_of_mem {S : Finset K'} {T : Finset F'} {f : F'} (hf : f ∈ T) :
    f ∈ Flvl K' F' ℓ S T
theorem

level_core

L268 ↗
AlgebraicCurves.Places.Proofs.Place_exists_finite_constantField_form_fiberConstants_eq_singleton.AlgebraicCurve.Place.FiniteConstantFieldFormAux.level_core
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FiniteConstantFieldFormAux
open _root_.AlgebraicCurve.Place hiding ord_nonneg_of_mem mem_of_ord_nonneg
open _root_.AlgebraicCurve
section Level
variable (K' : Type u) (F' : Type v) [Field K'] [Field F'] [Algebra K' F']
  (ℓ : ℕ) [Fact ℓ.Prime] [CharP K' ℓ]
attribute [local instance] ZMod.algebra
variable {K' ℓ} in
Lean source · statement
theorem level_core (halg : ∀ a : K', ∃ n : ℕ, 0 < n ∧ a ^ ℓ ^ n = a)
    {t : F'} (ht : Transcendental K' t) (hfd : FiniteDimensional K'⟮t⟯ F')
    (hsep : Algebra.IsSeparable K'⟮t⟯ F') (S : Finset K') (T : Finset F') (htT : t ∈ T) :
    ∃ x : Flvl K' F' ℓ S T, (x : F') = t ∧ Transcendental (Klvl K' ℓ S) x ∧
      FiniteDimensional (IntermediateField.adjoin (Klvl K' ℓ S) ({x} : Set (Flvl K' F' ℓ S T)))
        (Flvl K' F' ℓ S T) ∧
      Algebra.IsSeparable (IntermediateField.adjoin (Klvl K' ℓ S) ({x} : Set (Flvl K' F' ℓ S T)))
        (Flvl K' F' ℓ S T) ∧
      Algebra.IsAlgebraic (Flvl K' F' ℓ S T) F'
theorem

exists_finite_constantField_form_fiberConstants_eq_singleton

L390 ↗
AlgebraicCurve.Place.exists_finite_constantField_form_fiberConstants_eq_singleton
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_finite_constantField_form_fiberConstants_eq_singleton
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.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 _root_.IntermediateField
universe u v
open AlgebraicCurve.Place.FiniteConstantFieldFormAux in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_finite_constantField_form_fiberConstants_eq_singleton
    (K' : Type u) (F' : Type v) [Field K'] [Field F'] [Algebra K' F']
    (ℓ : ℕ) [Fact ℓ.Prime] [CharP K' ℓ]
    (halg : ∀ a : K', ∃ n : ℕ, 0 < n ∧ a ^ ℓ ^ n = a)
    (hfg : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    [IsCurveOver K' F'] (hC : ConstantsAreBase K' F') (W : Finset (Place K' F')) :
    ∃ (K : Type u) (F : Type v) (_ : Field K) (_ : Finite K) (_ : Field F)
      (_ : Algebra K K') (_ : Algebra K F) (_ : Algebra F F') (_ : Algebra K F')
      (_ : IsScalarTower K K' F') (_ : IsScalarTower K F F') (_ : Algebra.IsIntegral F F')
      (_ : IsCurveOver K F) (_ : Algebra.EssFiniteType K F),
        Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤ ∧
        ConstantsAreBase K F ∧
        ∀ w ∈ W, Place.fiberConstants K' F' (Place.restrictConstants F (K := K) w) = {w} ∧
          (Place.restrictConstants F (K := K) w).deg = w.deg

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