NYLL
Module

Mem_span_range_algebraMap_of_constantFieldExtension.lean

Nyll.AlgebraicCurves.FunctionFields.Mem_span_range_algebraMap_of_constantFieldExtension
33 declarations indexed from sourceView source ↗

Module documentation

Mem span range algebra Map of constant Field Extension

Imports6
Imported by3

Declarations

theorem

ord_nonneg_of_mem

L48 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.ord_nonneg_of_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem ord_nonneg_of_mem {f : L} (hf : f ∈ w.toValuationSubring) : 0 ≤ w.ord f
theorem

mem_of_ord_nonneg

L62 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.mem_of_ord_nonneg
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem mem_of_ord_nonneg {f : L} (hf : 0 ≤ w.ord f) : f ∈ w.toValuationSubring
theorem

not_mem_of_ord_neg

L71 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.not_mem_of_ord_neg
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem not_mem_of_ord_neg {f : L} (hf : w.ord f < 0) : f ∉ w.toValuationSubring
theorem

ord_eq_zero_of_mem_of_inv_mem

L75 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.ord_eq_zero_of_mem_of_inv_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem ord_eq_zero_of_mem_of_inv_mem {f : L} (hf : f ∈ w.toValuationSubring)
    (hfi : f⁻¹ ∈ w.toValuationSubring) : w.ord f = 0
theorem

ord_algebraMap

L82 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.ord_algebraMap
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem ord_algebraMap (a : k) : w.ord (algebraMap k L a) = 0
theorem

irreducible_coe_ne_zero

L88 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.irreducible_coe_ne_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem irreducible_coe_ne_zero {π : w.toValuationSubring} (hπ : Irreducible π) : (π : L) ≠ 0
theorem

ord_coe_isUnit

L92 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.ord_coe_isUnit
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem ord_coe_isUnit {X : w.toValuationSubring} (h : IsUnit X) : w.ord (X : L) = 0
theorem

mem_maximalIdeal_of_ord_pos

L96 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.mem_maximalIdeal_of_ord_pos
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem mem_maximalIdeal_of_ord_pos {Y : w.toValuationSubring} (h : 0 < w.ord (Y : L)) :
    Y ∈ IsLocalRing.maximalIdeal w.toValuationSubring
theorem

isUnit_add_of_mem_maximalIdeal

L103 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.isUnit_add_of_mem_maximalIdeal
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem isUnit_add_of_mem_maximalIdeal {X Y : w.toValuationSubring} (hX : IsUnit X)
    (hY : Y ∈ IsLocalRing.maximalIdeal w.toValuationSubring) : IsUnit (X + Y)
theorem

ord_algebraMap_add_eq_zero

L112 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.ord_algebraMap_add_eq_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem ord_algebraMap_add_eq_zero {a : k} (ha : a ≠ 0) {f : L} (hf : 0 < w.ord f) :
    w.ord (algebraMap k L a + f) = 0
theorem

ord_mul_of_ord_eq_zero

L121 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.ord_mul_of_ord_eq_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem ord_mul_of_ord_eq_zero {f g : L} (hf : w.ord f = 0) (hf0 : f ≠ 0) :
    w.ord (f * g) = w.ord g
theorem

exists_sub_algebraMap_mem_maximalIdeal

L127 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.exists_sub_algebraMap_mem_maximalIdeal
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem exists_sub_algebraMap_mem_maximalIdeal [IsAlgClosed k] [IsCurveOver k L]
    (X : w.toValuationSubring) :
    ∃ a : k, X - algebraMap k w.toValuationSubring a ∈
      IsLocalRing.maximalIdeal w.toValuationSubring
theorem

exists_ord_sub_algebraMap_pos

L141 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.exists_ord_sub_algebraMap_pos
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem exists_ord_sub_algebraMap_pos [IsAlgClosed k] [IsCurveOver k L] {f : L}
    (hf : f ∈ w.toValuationSubring) :
    ∃ a : k, f = algebraMap k L a ∨ 0 < w.ord (f - algebraMap k L a)
theorem

aeval_mem

L173 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.aeval_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Basic
variable {k L : Type*} [Field k] [Field L] [Algebra k L] (w : Place k L)
Lean source · statement
theorem aeval_mem {t : L} (ht : t ∈ w.toValuationSubring) (p : k[X]) :
    aeval t p ∈ w.toValuationSubring
theorem

linearIndependent_pow_of_transcendental

L185 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.linearIndependent_pow_of_transcendental
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Algebra
Lean source · full declaration
theorem linearIndependent_pow_of_transcendental {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
    {x : A} (hx : Transcendental R x) : LinearIndependent R fun n : ℕ => x ^ n := by
  rw [linearIndependent_iff]
  intro l hl
  have hinj := transcendental_iff_injective.mp hx
  have h0 : aeval x (Polynomial.ofFinsupp (.ofCoeff l)) = 0 := by
    rw [Finsupp.linearCombination_apply] at hl
    rw [aeval_def, eval₂_eq_sum, Polynomial.sum, Polynomial.support_ofFinsupp,
      AddMonoidAlgebra.coeff_ofCoeff]
    rw [Finsupp.sum] at hl
    convert hl using 2 with n hn
    rw [Polynomial.coeff_ofFinsupp, Algebra.smul_def]
  have h1 : (Polynomial.ofFinsupp (.ofCoeff l) : R[X]) = 0 := hinj (by rw [h0, map_zero])
  exact AddMonoidAlgebra.ofCoeff_eq_zero.mp (Polynomial.ofFinsupp_eq_zero.mp h1)
theorem

isIntegral_of_forall_mem_valuationSubring

L200 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.isIntegral_of_forall_mem_valuationSubring
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Algebra
Lean source · statement
theorem isIntegral_of_forall_mem_valuationSubring {R L : Type*} [CommRing R] [Field L]
    [Algebra R L] (w : L)
    (h : ∀ B : ValuationSubring L, (∀ r : R, algebraMap R L r ∈ B) → w ∈ B) :
    IsIntegral R w
theorem

degree_eq_sum

L281 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.degree_eq_sum
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section CFE
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
Lean source · full declaration
theorem degree_eq_sum [IsAlgClosed K] [IsCurveOver K F] (E : Divisor K F) :
    E.degree = E.sum fun _ n => n := by
  simp [Divisor.degree, Finsupp.liftAddHom_apply, IsCurveOver.deg_eq_one_of_isAlgClosed]
theorem

algebraMap_mem_adjoin_simple

L285 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.algebraMap_mem_adjoin_simple
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section CFE
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
Lean source · statement
theorem algebraMap_mem_adjoin_simple {x a : F}
    (ha : a ∈ IntermediateField.adjoin K ({x} : Set F)) :
    algebraMap F F' a ∈ IntermediateField.adjoin K' ({algebraMap F F' x} : Set F')
theorem

mem_range_of_isAlgebraic

L294 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.mem_range_of_isAlgebraic
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section CFE
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
Lean source · statement
theorem mem_range_of_isAlgebraic [IsAlgClosed K'] {t : F'} (ht : IsAlgebraic K' t) :
    t ∈ (algebraMap K' F').range
theorem

transcendental_algebraMap

L300 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.transcendental_algebraMap
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section CFE
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
Lean source · statement
theorem transcendental_algebraMap [IsAlgClosed K] [CharZero K] [IsAlgClosed K']
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    [IsCurveOver K F]
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    {x : F} (hx : Transcendental K x) :
    Transcendental K' (algebraMap F F' x)
theorem

algebraMap_mem_of_new

L324 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.algebraMap_mem_of_new
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section CFE
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
Lean source · statement
theorem algebraMap_mem_of_new [CharZero K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (W : Place K' F')
    (hW : ∀ v : Place K F, W.toValuationSubring.comap (algebraMap F F') ≠ v.toValuationSubring)
    (f : F) : algebraMap F F' f ∈ W.toValuationSubring
theorem

exists_ord_sub_pos

L343 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.exists_ord_sub_pos
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section CFE
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
Lean source · statement
theorem exists_ord_sub_pos [IsAlgClosed K'] [IsCurveOver K' F']
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    {x' : F'} (hx' : Transcendental K' x') (c : K') :
    ∃ v' : Place K' F', 0 < v'.ord (x' - algebraMap K' F' c)
theorem

trace_mem

L372 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.trace_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section CFE
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
Lean source · statement
theorem trace_mem [IsAlgClosed K] [CharZero K'] [IsCurveOver K F]
    {x : F} (hx : Transcendental K x)
    (hfg' : ∃ j : F', Transcendental K' j ∧
      FiniteDimensional (IntermediateField.adjoin K' ({j} : Set F')) F')
    [FiniteDimensional (IntermediateField.adjoin K' ({algebraMap F F' x} : Set F')) F']
    {c : K'} (hc : c ∉ Set.range (algebraMap K K'))
    (v' : Place K' F') (hv' : 0 < v'.ord (algebraMap F F' x - algebraMap K' F' c))
    (w : F')
    (hw : ∀ W : Place K' F',
      (∀ v : Place K F, W.toValuationSubring.comap (algebraMap F F') ≠ v.toValuationSubring) →
        w ∈ W.toValuationSubring) :
    ((Algebra.trace (IntermediateField.adjoin K' ({algebraMap F F' x} : Set F')) F' w :
      IntermediateField.adjoin K' ({algebraMap F F' x} : Set F')) : F') ∈ v'.toValuationSubring
theorem

span_range_eq_adjoin

L457 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.span_range_eq_adjoin
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section PF
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
variable (F F') in
Lean source · statement
theorem span_range_eq_adjoin (R : Type*) [CommSemiring R] [Algebra R F'] :
    Subalgebra.toSubmodule (Algebra.adjoin R (Set.range (algebraMap F F'))) =
      Submodule.span R (Set.range (algebraMap F F'))
theorem

mem_span_of_regular

L465 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.mem_span_of_regular
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section PF
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
variable (F F') in
Lean source · statement
theorem mem_span_of_regular [IsAlgClosed K'] [IsCurveOver K' F']
    (hfg' : ∃ j : F', Transcendental K' j ∧
      FiniteDimensional (IntermediateField.adjoin K' ({j} : Set F')) F')
    {x : F} (hx' : Transcendental K' (algebraMap F F' x))
    {t : F'} (ht : t ∈ IntermediateField.adjoin K' ({algebraMap F F' x} : Set F'))
    (hreg : ∀ c : K', c ∉ Set.range (algebraMap K K') →
      ∀ v' : Place K' F', 0 < v'.ord (algebraMap F F' x - algebraMap K' F' c) → 0 ≤ v'.ord t) :
    t ∈ Submodule.span K' (Set.range (algebraMap F F'))
def

iota

L601 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.iota
Documentation

The map between simple intermediate fields induced by the constant-field extension.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section BaseChange
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
variable (K K' F') in
Lean source · full declaration
def iota (x : F) :
    IntermediateField.adjoin K ({x} : Set F) →+*
      IntermediateField.adjoin K' ({algebraMap F F' x} : Set F') where
  toFun a := ⟨algebraMap F F' a, algebraMap_mem_adjoin_simple a.2⟩
  map_one' := Subtype.ext (by simp)
  map_mul' a b := Subtype.ext (by simp)
  map_zero' := Subtype.ext (by simp)
  map_add' a b := Subtype.ext (by simp)
theorem

coe_iota

L610 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.coe_iota
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section BaseChange
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
variable (K K' F') in
Lean source · statement
theorem coe_iota (x : F) (a : IntermediateField.adjoin K ({x} : Set F)) :
    ((iota K K' F' x a : IntermediateField.adjoin K' ({algebraMap F F' x} : Set F')) : F') =
      algebraMap F F' a
theorem

algebraMap_smul

L614 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.algebraMap_smul
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section BaseChange
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
variable (K K' F') in
Lean source · statement
theorem algebraMap_smul (x : F) (a : IntermediateField.adjoin K ({x} : Set F)) (f : F) :
    algebraMap F F' (a • f) = iota K K' F' x a • algebraMap F F' f
theorem

exists_basis

L619 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.exists_basis
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section BaseChange
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
variable (K K' F') in
Lean source · statement
theorem exists_basis [IsAlgClosed K] [CharZero K] [IsAlgClosed K']
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    [IsCurveOver K F]
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    {x : F} (hx : Transcendental K x)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {n : ℕ} (y : Module.Basis (Fin n) (IntermediateField.adjoin K ({x} : Set F)) F) :
    ∃ y' : Module.Basis (Fin n) (IntermediateField.adjoin K' ({algebraMap F F' x} : Set F')) F',
      ∀ i, y' i = algebraMap F F' (y i)
theorem

trace_algebraMap

L744 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.trace_algebraMap
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section BaseChange
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
variable (K K' F') in
Lean source · statement
theorem trace_algebraMap {x : F} {n : ℕ}
    (y : Module.Basis (Fin n) (IntermediateField.adjoin K ({x} : Set F)) F)
    (y' : Module.Basis (Fin n) (IntermediateField.adjoin K' ({algebraMap F F' x} : Set F')) F')
    (hy : ∀ i, y' i = algebraMap F F' (y i)) (f : F) :
    Algebra.trace (IntermediateField.adjoin K' ({algebraMap F F' x} : Set F')) F'
        (algebraMap F F' f) =
      iota K K' F' x (Algebra.trace (IntermediateField.adjoin K ({x} : Set F)) F f)
theorem

eq_sum_trace_mul

L765 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.eq_sum_trace_mul
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section BaseChange
variable {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F]
  [Algebra K' F'] [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F']
  [IsScalarTower K F F']
variable (K K' F') in
Lean source · statement
theorem eq_sum_trace_mul {x : F} {n : ℕ}
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F]
    (y : Module.Basis (Fin n) (IntermediateField.adjoin K ({x} : Set F)) F)
    (y' : Module.Basis (Fin n) (IntermediateField.adjoin K' ({algebraMap F F' x} : Set F')) F')
    (hy : ∀ i, y' i = algebraMap F F' (y i)) (z : F') :
    z = ∑ i, (Algebra.trace (IntermediateField.adjoin K' ({algebraMap F F' x} : Set F')) F'
        (z * algebraMap F F'
          ((Algebra.traceForm (IntermediateField.adjoin K ({x} : Set F)) F).dualBasis
            (traceForm_nondegenerate _ F) y i)) : F') * algebraMap F F' (y i)
theorem

mem_span_range_algebraMap_of_constantFieldExtension

L804 ↗
AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension.AlgebraicCurve.W7XH.mem_span_range_algebraMap_of_constantFieldExtension
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace W7XH
open _root_.AlgebraicCurve
section Main
Lean source · statement
theorem mem_span_range_algebraMap_of_constantFieldExtension
    (K F K' F' : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [IsAlgClosed K] [CharZero K] [IsAlgClosed K']
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    [IsCurveOver K F] [IsCurveOver K' F']
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    (z : F')
    (hz : ∀ v' : Place K' F',
      (∀ v : Place K F, v'.toValuationSubring.comap (algebraMap F F') ≠ v.toValuationSubring) →
        z ∈ v'.toValuationSubring) :
    z ∈ Submodule.span K' (Set.range (algebraMap F F'))
theorem

mem_span_range_algebraMap_of_constantFieldExtension

L855 ↗
AlgebraicCurve.mem_span_range_algebraMap_of_constantFieldExtension
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_span_range_algebraMap_of_constantFieldExtension
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open _root_.AlgebraicCurve
open _root_.Polynomial
Lean source · statement
theorem _root_.AlgebraicCurve.mem_span_range_algebraMap_of_constantFieldExtension
    (K F K' F' : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [IsAlgClosed K] [CharZero K] [IsAlgClosed K']
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    [IsCurveOver K F] [IsCurveOver K' F']
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    (z : F')
    (hz : ∀ v' : Place K' F',
      (∀ v : Place K F, v'.toValuationSubring.comap (algebraMap F F') ≠ v.toValuationSubring) →
        z ∈ v'.toValuationSubring) :
    z ∈ Submodule.span K' (Set.range (algebraMap F F'))

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