NYLL
Module

Exists_constantFieldExtension_of_finite.lean

Nyll.AlgebraicCurves.FunctionFields.Exists_constantFieldExtension_of_finite
31 declarations indexed from sourceView source ↗

Module documentation

Exists constant Field Extension of finite

Imports10
Imported by2

Declarations

theorem

mem_range_of_forall_mem

L64 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.mem_range_of_forall_mem
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Constants
variable {k F : Type*} [Field k] [Field F] [Algebra k F]
Lean source · statement
theorem mem_range_of_forall_mem (hC : ConstantsAreBase k F) {y : F}
    (hy : ∀ v : Place k F, y ∈ v.toValuationSubring) : y ∈ (algebraMap k F).range
theorem

mem_range_of_isIntegral

L75 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.mem_range_of_isIntegral
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Constants
variable {k F : Type*} [Field k] [Field F] [Algebra k F]
Lean source · statement
theorem mem_range_of_isIntegral (hC : ConstantsAreBase k F) {y : F} (hy : IsIntegral k y) :
    y ∈ (algebraMap k F).range
theorem

minpoly_eq_map

L94 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.minpoly_eq_map
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Minpoly
variable {k F M : Type*} [Field k] [Field F] [Field M] [Algebra k F] [Algebra F M]
  [Algebra k M] [IsScalarTower k F M]
Lean source · statement
theorem minpoly_eq_map (hconst : ∀ y : F, IsIntegral k y → y ∈ (algebraMap k F).range)
    {β : M} (hβ : IsIntegral k β) :
    minpoly F β = (minpoly k β).map (algebraMap k F)
theorem

exists_irreducible_natDegree_eq

L125 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.exists_irreducible_natDegree_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
Lean source · statement
theorem exists_irreducible_natDegree_eq (k : Type u) [Field k] [Finite k] (r : ℕ)
    (hr : 0 < r) : ∃ g : k[X], g.Monic ∧ Irreducible g ∧ g.natDegree = r
theorem

finite_and_separable_of_tower

L137 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.finite_and_separable_of_tower
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Tower
Lean source · statement
theorem finite_and_separable_of_tower {k F F' E : Type*} [Field k] [Field F] [Field F']
    [Field E] [Algebra k F] [Algebra F F'] [Algebra E F'] {t : F}
    (hfd : FiniteDimensional k⟮t⟯ F) (hsep : Algebra.IsSeparable k⟮t⟯ F)
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (ψ : k⟮t⟯ →+* E) (hψ : ∀ x, algebraMap E F' (ψ x) = algebraMap F F' x) :
    FiniteDimensional E F' ∧ Algebra.IsSeparable E F'
theorem

algebraMap_mem_adjoin

L151 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.algebraMap_mem_adjoin
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Tower
Lean source · statement
theorem algebraMap_mem_adjoin {k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F]
    [Algebra F F'] [Algebra k F'] [IsScalarTower k F F']
    (K' : Type*) [Field K'] [Algebra k K'] [Algebra K' F'] [IsScalarTower k K' F']
    (t : F) (x : k⟮t⟯) :
    algebraMap F F' x ∈ K'⟮algebraMap F F' t⟯
abbrev

gF

L174 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.gF
Documentation

The polynomial mapped to the lifted function field.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
abbrev gF : (ULift.{u} F)[X]
abbrev

Kx

L177 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.Kx
Documentation

The algebra obtained by adjoining a root of the polynomial over the original constants.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
abbrev Kx : Type u
abbrev

Fx

L180 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.Fx
Documentation

The extension obtained by adjoining a root of the mapped polynomial over the function field.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
abbrev Fx : Type (max u v)
theorem

eval₂_root_eq_zero

L182 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.eval₂_root_eq_zero
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
theorem eval₂_root_eq_zero :
    g.eval₂ (algebraMap k (Fx k F g)) (AdjoinRoot.root (gF k F g)) = 0
instance

algebraKxFx

L188 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.algebraKxFx
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
instance algebraKxFx : Algebra (Kx k g) (Fx k F g)
theorem

algebraMap_Kx_eq

L192 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.algebraMap_Kx_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
theorem algebraMap_Kx_eq :
    algebraMap (Kx k g) (Fx k F g) =
      AdjoinRoot.lift (algebraMap k (Fx k F g)) (AdjoinRoot.root (gF k F g))
        (eval₂_root_eq_zero k F g)
instance

isScalarTower_k_Kx_Fx

L197 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.isScalarTower_k_Kx_Fx
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
instance isScalarTower_k_Kx_Fx : IsScalarTower k (Kx k g) (Fx k F g)
theorem

algebraMap_root

L201 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.algebraMap_root
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
theorem algebraMap_root :
    algebraMap (Kx k g) (Fx k F g) (AdjoinRoot.root g) = AdjoinRoot.root (gF k F g)
theorem

algebraMap_F₁_apply

L205 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.algebraMap_F₁_apply
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
theorem algebraMap_F₁_apply (c : ULift.{u} F) :
    algebraMap (ULift.{u} F) (Fx k F g) c = algebraMap F (Fx k F g) c.down
theorem

adjoin_range_eq_top

L210 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.adjoin_range_eq_top
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
theorem adjoin_range_eq_top :
    Algebra.adjoin F (Set.range (algebraMap (Kx k g) (Fx k F g))) = ⊤
theorem

finite_F₁

L226 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.finite_F₁
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
theorem finite_F₁ : Module.Finite F (ULift.{u} F)
theorem

finrank_F₁

L229 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.finrank_F₁
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
Lean source · statement
theorem finrank_F₁ : Module.finrank F (ULift.{u} F) = 1
theorem

gF_ne_zero

L234 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.gF_ne_zero
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
variable {g}
Lean source · statement
theorem gF_ne_zero (hg : g.Monic) : gF k F g ≠ 0
theorem

finiteDimensional_Fx

L236 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.finiteDimensional_Fx
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
variable {g}
Lean source · statement
theorem finiteDimensional_Fx (hg : g.Monic) : FiniteDimensional F (Fx k F g)
theorem

finrank_Fx

L242 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.finrank_Fx
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
variable {g}
Lean source · statement
theorem finrank_Fx (hg : g.Monic) : Module.finrank F (Fx k F g) = g.natDegree
theorem

finrank_Kx

L251 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.finrank_Kx
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
variable {g}
Lean source · statement
theorem finrank_Kx (hg : g.Monic) : Module.finrank k (Kx k g) = g.natDegree
theorem

finite_Kx

L254 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.finite_Kx
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
variable {g}
Lean source · statement
theorem finite_Kx [Finite k] (hg : g.Monic) : Finite (Kx k g)
theorem

hconst_ulift

L258 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.hconst_ulift
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
variable {g}
Lean source · statement
theorem hconst_ulift (hconst : ∀ y : F, IsIntegral k y → y ∈ (algebraMap k F).range)
    (y : ULift.{u} F) (hy : IsIntegral k y) : y ∈ (algebraMap k (ULift.{u} F)).range
theorem

irreducible_gF

L267 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.irreducible_gF
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
variable {g}
Lean source · statement
theorem irreducible_gF (hconst : ∀ y : F, IsIntegral k y → y ∈ (algebraMap k F).range)
    (hg : g.Monic) (hirr : Irreducible g) : Irreducible (gF k F g)
theorem

isSeparable_Fx

L284 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.isSeparable_Fx
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
variable {g}
Lean source · statement
theorem isSeparable_Fx [Fact (Irreducible (gF k F g))] (hg : g.Monic) (hsep : g.Separable) :
    Algebra.IsSeparable F (Fx k F g)
theorem

ord_extendConstants

L310 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.ord_extendConstants
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Construction
variable (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (g : k[X])
variable {g}
Lean source · statement
theorem ord_extendConstants {K K' L : Type*} [Field K] [Field K'] [Field L] [Algebra K K']
    [Algebra K' L] [Algebra K L] [IsScalarTower K K' L] [Algebra.IsIntegral K K']
    (w : Place K L) (f : L) : (Place.extendConstants K' w).ord f = w.ord f
theorem

curve_data

L322 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.curve_data
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Curve
variable (k : Type u) (F : Type v) [Field k] [Finite k] [Field F] [Algebra k F]
  [IsCurveOver k F] [Algebra.EssFiniteType k F] {g : k[X]}
  [Fact (Irreducible g)] [Fact (Irreducible (gF k F g))]
Lean source · statement
theorem curve_data (hg : g.Monic) :
    IsCurveOver k (Fx k F g) ∧ IsCurveOver (Kx k g) (Fx k F g) ∧
      Algebra.EssFiniteType (Kx k g) (Fx k F g)
theorem

isIntegral_of_ord_nonneg

L356 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.isIntegral_of_ord_nonneg
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Curve
variable (k : Type u) (F : Type v) [Field k] [Finite k] [Field F] [Algebra k F]
  [IsCurveOver k F] [Algebra.EssFiniteType k F] {g : k[X]}
  [Fact (Irreducible g)] [Fact (Irreducible (gF k F g))]
omit [IsCurveOver k F] [Algebra.EssFiniteType k F] in
Lean source · statement
theorem isIntegral_of_ord_nonneg (hC : ConstantsAreBase k F) (hg : g.Monic)
    [IsCurveOver k (Fx k F g)] {z : Fx k F g} (hz0 : z ≠ 0)
    (hordk : ∀ w : Place k (Fx k F g), 0 ≤ w.ord z) : IsIntegral k z
theorem

constantsAreBase

L382 ↗
AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite.AlgebraicCurve.ConstFieldExtOfFinite.constantsAreBase
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ConstFieldExtOfFinite
universe u v
section Curve
variable (k : Type u) (F : Type v) [Field k] [Finite k] [Field F] [Algebra k F]
  [IsCurveOver k F] [Algebra.EssFiniteType k F] {g : k[X]}
  [Fact (Irreducible g)] [Fact (Irreducible (gF k F g))]
Lean source · statement
theorem constantsAreBase (hC : ConstantsAreBase k F) (hg : g.Monic) :
    ConstantsAreBase (Kx k g) (Fx k F g)
theorem

exists_constantFieldExtension_of_finite

L459 ↗
AlgebraicCurve.exists_constantFieldExtension_of_finite
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_constantFieldExtension_of_finite
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
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 Polynomial
open scoped IntermediateField
universe u v in
Lean source · statement
theorem _root_.AlgebraicCurve.exists_constantFieldExtension_of_finite
    (k : Type u) (F : Type v) [Field k] [Finite k] [Field F] [Algebra k F]
    [AlgebraicCurve.IsCurveOver k F] [Algebra.EssFiniteType k F]
    (hC : AlgebraicCurve.ConstantsAreBase k F) (r : ℕ) (hr : 0 < r) :
    ∃ (k' : Type u) (F' : Type (max u v)) (_ : Field k') (_ : Finite k') (_ : Field F')
      (_ : Algebra k k') (_ : Algebra k' F') (_ : Algebra k F') (_ : Algebra F F')
      (_ : IsScalarTower k k' F') (_ : IsScalarTower k F F') (_ : FiniteDimensional F F')
      (_ : AlgebraicCurve.IsCurveOver k' F') (_ : Algebra.EssFiniteType k' F'),
      Module.finrank k k' = r ∧
        Algebra.adjoin F (Set.range (algebraMap k' F')) = ⊤ ∧
          AlgebraicCurve.ConstantsAreBase k' F'

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