Module

Divisor_mapDomain_placeReduction_eq_ord_of_retraction.lean

Nyll.AlgebraicCurves.Divisors.Divisor_mapDomain_placeReduction_eq_ord_of_retraction

24 declarations indexed from sourceView source ↗

Module documentation

Divisor map Domain place Reduction eq ord of retraction

Imports22

Imported by1

Nyll.AlgebraicCurves.Divisors.All

def

polyAlg

L59 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.polyAlg

Documentation

The polynomial algebra structure obtained by evaluating at the chosen function.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatAlg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def polyAlg (x : F) : Algebra K[X] F

theorem

faithful_polyAlg

L62 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.faithful_polyAlg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatAlg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem faithful_polyAlg {x : F} (hx : Transcendental K x) :
    letI := polyAlg (K := K) x
    FaithfulSMul K[X] F := by
  let := polyAlg (K := K) x
  exact (faithfulSMul_iff_algebraMap_injective K[X] F).mpr (transcendental_iff_injective.mp hx)

def

ratAlg

L70 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.ratAlg

Documentation

The rational-function algebra structure supplied by a transcendental function.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatAlg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped RatFunc in

Lean source · statement

def ratAlg {x : F} (hx : Transcendental K x) : Algebra (RatFunc K) F

theorem

ratAlg_tower

L75 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.ratAlg_tower

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatAlg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem ratAlg_tower {x : F} (hx : Transcendental K x) :
    letI := ratAlg (K := K) hx
    IsScalarTower K (RatFunc K) F := by
  let := polyAlg (K := K) x
  have := faithful_polyAlg (K := K) hx
  let := ratAlg (K := K) hx
  have : IsScalarTower K K[X] F := IsScalarTower.of_algebraMap_eq fun k => by
    change _ = (Polynomial.aeval x).toRingHom (algebraMap K K[X] k)
    simp
  infer_instance

theorem

ratAlg_X

L86 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.ratAlg_X

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatAlg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem ratAlg_X {x : F} (hx : Transcendental K x) :
    letI := ratAlg (K := K) hx
    algebraMap (RatFunc K) F RatFunc.X = x := by
  let := polyAlg (K := K) x
  have := faithful_polyAlg (K := K) hx
  let := ratAlg (K := K) hx
  have h1 : algebraMap (RatFunc K) F (algebraMap K[X] (RatFunc K) Polynomial.X) =
      algebraMap K[X] F Polynomial.X :=
    (IsScalarTower.algebraMap_apply K[X] (RatFunc K) F _).symm
  rw [RatFunc.algebraMap_X] at h1
  rw [h1]
  change (Polynomial.aeval x).toRingHom Polynomial.X = x
  simp

theorem

ratAlg_finite

L101 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.ratAlg_finite

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatAlg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open IntermediateField in

Lean source · full declaration

theorem ratAlg_finite {x : F} (hx : Transcendental K x)
    (hfin : FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F) :
    letI := ratAlg (K := K) hx
    FiniteDimensional (RatFunc K) F := by
  let := ratAlg (K := K) hx
  have := ratAlg_tower (K := K) hx
  set ψ : RatFunc K →ₐ[K] F := IsScalarTower.toAlgHom K (RatFunc K) F with hψ
  have hψX : ψ RatFunc.X = x := ratAlg_X hx
  have hrange : ψ.fieldRange = IntermediateField.adjoin K ({x} : Set F) := by
    rw [AlgHom.fieldRange_eq_map, ← RatFunc.adjoin_X, IntermediateField.adjoin_map]
    simp [hψX]
  have : FiniteDimensional ψ.fieldRange F := by rw [hrange]; exact hfin
  have hinj : Function.Injective ψ.toRingHom.rangeRestrictField :=
    RingHom.injective _
  have hsurj : Function.Surjective ψ.toRingHom.rangeRestrictField := by
    rintro ⟨y, hy⟩
    obtain ⟨a, rfl⟩ := (AlgHom.mem_fieldRange).mp hy
    exact ⟨a, rfl⟩
  let e : RatFunc K ≃+* ψ.fieldRange := RingEquiv.ofBijective _ ⟨hinj, hsurj⟩
  refine Module.Finite.of_equiv_equiv e.symm (RingEquiv.refl F) (RingHom.ext fun a => ?_)
  obtain ⟨b, rfl⟩ := e.surjective a
  simp only [RingHom.comp_apply]
  erw [RingEquiv.symm_apply_apply]
  rfl

theorem

finiteDimensional_adjoin_of_transcendental'

L128 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.finiteDimensional_adjoin_of_transcendental'

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatAlg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open IntermediateField in
open scoped IntermediateField IntermediateField.algebraAdjoinAdjoin in

Lean source · statement

theorem finiteDimensional_adjoin_of_transcendental'
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional K⟮x⟯ F)
    {x : F} (hx : Transcendental K x) : FiniteDimensional K⟮x⟯ F

theorem

transcendental_of_linearIndependent_pow

L154 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.transcendental_of_linearIndependent_pow

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatAlg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem transcendental_of_linearIndependent_pow {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
    {x : A} (h : LinearIndependent R (fun j : ℕ => x ^ j)) : Transcendental R x := by
  rw [transcendental_iff]
  intro p hpx
  let l : ℕ →₀ R := Finsupp.onFinset p.support p.coeff fun n hn => Polynomial.mem_support_iff.mpr hn
  have hl : ∀ n, l n = p.coeff n := fun n => Finsupp.onFinset_apply
  have key : Finsupp.linearCombination R (fun j : ℕ => x ^ j) l = Polynomial.aeval x p := by
    rw [Finsupp.linearCombination_apply,
      Finsupp.sum_of_support_subset l Finsupp.support_onFinset_subset (fun i a => a • x ^ i)
        (fun n _ => zero_smul R _),
      Polynomial.aeval_def, Polynomial.eval₂_eq_sum, Polynomial.sum_def]
    refine Finset.sum_congr rfl fun n _ => ?_
    rw [hl, Algebra.smul_def]
  have := linearIndependent_iff.mp h l (by rw [key, hpx])
  ext n
  rw [← hl n, this, Finsupp.zero_apply, Polynomial.coeff_zero]

theorem

X_not_mem_placeInfty

L177 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.X_not_mem_placeInfty

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatFuncPlaces
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem X_not_mem_placeInfty [DecidableEq (RatFunc k)] :
    (RatFunc.X : RatFunc k) ∉ (placeInfty k).toValuationSubring

theorem

X_mem_placeOfPoint

L184 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.X_mem_placeOfPoint

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatFuncPlaces
variable {k L : Type*} [Field k] [Field L] [Algebra k L]

Lean source · statement

theorem X_mem_placeOfPoint (a : k) :
    (RatFunc.X : RatFunc k) ∈ (placeOfPoint k a).toValuationSubring

theorem

restrict_eq_placeInfty_iff

L191 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.restrict_eq_placeInfty_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatFuncPlaces
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
variable [Algebra (RatFunc k) L] [IsScalarTower k (RatFunc k) L] [Algebra.IsIntegral (RatFunc k) L]

Lean source · statement

theorem restrict_eq_placeInfty_iff [IsAlgClosed k] [DecidableEq (RatFunc k)] (w : Place k L) :
    w.restrict (RatFunc k) = placeInfty k ↔
      algebraMap (RatFunc k) L RatFunc.X ∉ w.toValuationSubring

theorem

valuation_X_sub_lt_one_of_restrict_eq_placeOfPoint

L205 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.valuation_X_sub_lt_one_of_restrict_eq_placeOfPoint

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section RatFuncPlaces
variable {k L : Type*} [Field k] [Field L] [Algebra k L]
variable [Algebra (RatFunc k) L] [IsScalarTower k (RatFunc k) L] [Algebra.IsIntegral (RatFunc k) L]

Lean source · statement

theorem valuation_X_sub_lt_one_of_restrict_eq_placeOfPoint (w : Place k L) (β : k)
    (h : w.restrict (RatFunc k) = placeOfPoint k β) :
    w.toValuationSubring.valuation (algebraMap (RatFunc k) L RatFunc.X - algebraMap k L β) < 1

theorem

valuation_algebraMap_eq_one

L251 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.valuation_algebraMap_eq_one

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section Fibre
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem valuation_algebraMap_eq_one (v : Place K F) {c : K} (hc : c ≠ 0) :
    v.toValuationSubring.valuation (algebraMap K F c) = 1

theorem

not_exists_lt_one_iff

L270 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.not_exists_lt_one_iff

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section FibreE
variable {E FE : Type*} [Field E] [Field FE] [Algebra E FE]
  [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE] [Algebra.IsIntegral (RatFunc E) FE]

Lean source · statement

theorem not_exists_lt_one_iff [IsAlgClosed E] [DecidableEq (RatFunc E)]
    (A : ValuationSubring E) (P : Place E FE) :
    (¬ ∃ a : E, a ∈ A ∧
        P.toValuationSubring.valuation (algebraMap (RatFunc E) FE RatFunc.X - algebraMap E FE a) <
          1) ↔
      (P.restrict (RatFunc E) = placeInfty E ∨
        ∃ β : E, β ∉ A ∧ P.restrict (RatFunc E) = placeOfPoint E β)

def

poleSum

L323 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.poleSum

Documentation

The sum of the divisor coefficients at the poles of the selected function.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section PoleSum
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open Classical in

Lean source · statement

def poleSum (x : F) (D : Divisor K F) : ℤ

theorem

poleSum_eq_sum

L327 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.poleSum_eq_sum

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section PoleSum
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open Classical in

Lean source · full declaration

theorem poleSum_eq_sum (x : F) (D : Divisor K F) :
    poleSum x D = ∑ w ∈ D.support, if x ∉ w.toValuationSubring then D w else 0 := rfl

theorem

poleSum_sub

L330 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.poleSum_sub

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section PoleSum
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem poleSum_sub (x : F) (D D' : Divisor K F) :
    poleSum x (D - D') = poleSum x D - poleSum x D'

theorem

poleSum_mapDomain

L338 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.poleSum_mapDomain

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section PoleSum
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open Classical in

Lean source · full declaration

theorem poleSum_mapDomain {ι : Type*} (x : F) (r : ι → Place K F) (D : ι →₀ ℤ) :
    poleSum x (Finsupp.mapDomain r D) =
      ∑ i ∈ D.support, if x ∉ (r i).toValuationSubring then D i else 0 := by
  classical
  unfold poleSum
  exact Finsupp.sum_mapDomain_index (f := r) (s := D)
    (h := fun w n => if x ∉ w.toValuationSubring then n else 0)
    (fun _ => ite_self 0) (fun _ _ _ => by split_ifs <;> simp only [add_zero])

theorem

sum_support_ite_eq

L347 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.sum_support_ite_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section PoleSum
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem sum_support_ite_eq (D : Divisor K F) (p : Place K F → Prop) [DecidablePred p]
    (U : Finset (Place K F)) (hU : D.support ⊆ U) :
    (∑ w ∈ D.support, if p w then D w else 0) = ∑ w ∈ U, if p w then D w else 0 := by
  refine Finset.sum_subset hU fun w _ hw => ?_
  rw [Finsupp.notMem_support_iff.mp hw]
  simp

theorem

sum_restrict_eq_ord_norm

L361 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.sum_restrict_eq_ord_norm

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section Push
variable {k L : Type*} [Field k] [Field L] [Algebra k L] [IsAlgClosed k] [CharZero k]
  [Algebra (RatFunc k) L] [IsScalarTower k (RatFunc k) L] [FiniteDimensional (RatFunc k) L]

Lean source · full declaration

theorem sum_restrict_eq_ord_norm [DecidableEq (Place k (RatFunc k))] {f : L} (hf : f ≠ 0)
    (D : Divisor k L) (hD : ∀ w, D w = w.ord f) (v : Place k (RatFunc k)) :
    (∑ w ∈ D.support, if w.restrict (RatFunc k) = v then D w else 0) =
      v.ord (Algebra.norm (RatFunc k) f) := by
  have H := Divisor.pushforwardNormFormula_of_finiteDimensional
    (K := k) (F := RatFunc k) (F' := L) f hf D hD v
  rw [Divisor.pushforward_apply] at H
  rw [← H]
  refine Finset.sum_congr rfl fun w _ => ?_
  split_ifs with h
  · rw [Place.inertiaDeg_eq_one_of_isRational w (Place.isRational_of_isAlgClosed w)
      (Place.isRational_of_isAlgClosed _)]
    simp
  · rfl

theorem

algebraMap_polynomial_map

L385 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.algebraMap_polynomial_map

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section Core
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]

Lean source · statement

theorem algebraMap_polynomial_map
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
    (p : K[X]) :
    algebraMap (RatFunc E) FE (algebraMap E[X] (RatFunc E) (p.map (algebraMap K E))) =
      algebraMap F FE (algebraMap (RatFunc K) F (algebraMap K[X] (RatFunc K) p))

theorem

isUnit_iff_inv_mem

L408 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.isUnit_iff_inv_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section Core
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]

Lean source · statement

theorem isUnit_iff_inv_mem {L : Type*} [Field L] (O : ValuationSubring L) (z : O) (hz : (z : L) ≠
  0) :
    IsUnit z ↔ (z : L)⁻¹ ∈ O

theorem

core

L425 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction.DeuringPrincipalDivisorReduction.core

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
namespace DeuringPrincipalDivisorReduction
section Core
variable {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra (RatFunc E) FE] [IsScalarTower E (RatFunc E) FE]
variable [IsAlgClosed K] [CharZero K] [IsAlgClosed E]
    [FiniteDimensional (RatFunc K) F] [FiniteDimensional (RatFunc E) FE]

Lean source · statement

theorem core
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (hX : algebraMap (RatFunc E) FE RatFunc.X = algebraMap F FE (algebraMap (RatFunc K) F
      RatFunc.X))
    (A : ValuationSubring E) (r : Place E FE → Place K F)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (hr : ∀ (P : Place E FE) (f : F), f ∈ (r P).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧
        P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE a) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
    (g : O) (hg : ρ g ≠ 0) (Dg : Divisor E FE) (hDg : ∀ P : Place E FE, Dg P = P.ord (g : FE))
    (Df : Divisor K F) (hDf : ∀ v, Df v = v.ord (ρ g)) :
    poleSum (algebraMap (RatFunc K) F RatFunc.X) (Finsupp.mapDomain r Dg) =
      poleSum (algebraMap (RatFunc K) F RatFunc.X) Df

theorem

mapDomain_placeReduction_eq_ord_of_retraction

L580 ↗

AlgebraicCurve.Divisor.mapDomain_placeReduction_eq_ord_of_retraction

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mapDomain_placeReduction_eq_ord_of_retraction
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
open AlgebraicCurve AlgebraicCurve.RationalFunctionField
open scoped Polynomial
open DeuringPrincipalDivisorReduction in

Lean source · statement

theorem _root_.AlgebraicCurve.Divisor.mapDomain_placeReduction_eq_ord_of_retraction
    (K F E FE : Type*) [Field K] [Field F] [Field E] [Field FE] [Algebra K F] [Algebra E FE]
    [Algebra K E] [Algebra F FE] [Algebra K FE] [IsScalarTower K E FE] [IsScalarTower K F FE]
    [IsAlgClosed K] [CharZero K] [IsAlgClosed E]
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    [IsCurveOver K F] [IsCurveOver E FE]
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (A : ValuationSubring E) (r : Place E FE → Place K F)
    (hKA : ∀ k : K, algebraMap K E k ∈ A)
    (hArat : ∀ a : E, a ∈ A → ∃ k : K, A.valuation (a - algebraMap K E k) < 1)
    (hr : ∀ (P : Place E FE) (f : F), f ∈ (r P).toValuationSubring ↔
      ∃ a : E, a ∈ A ∧
        P.toValuationSubring.valuation (algebraMap F FE f - algebraMap E FE a) < 1)
    (O : ValuationSubring FE) (ρ : O →+* F)
    (hO : ∀ c : E, algebraMap E FE c ∈ O ↔ c ∈ A)
    (hker : RingHom.ker ρ = IsLocalRing.maximalIdeal O)
    (hρ : ∀ f : F, ∃ h : algebraMap F FE f ∈ O, ρ ⟨algebraMap F FE f, h⟩ = f)
    (g : O) (hg : ρ g ≠ 0) (Dg : Divisor E FE) (hDg : ∀ P : Place E FE, Dg P = P.ord (g : FE))
    (v : Place K F) :
    Finsupp.mapDomain r Dg v = v.ord (ρ g)

Module documentation

Divisor map Domain place Reduction eq ord of retraction

Declarations