Basic divisor API aliases

This file re-exports the coordinate divisor API from FunctionField.Divisor under the names used in downstream modules (degA, placeDegA), and hosts the standing IsFullConstantField hypothesis.

@[reducible, inline]

noncomputable abbrev FunctionField.placeDegA (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (v : Chart.PlaceA k K) : ℕ

Backward-compatible alias for placeDegree.

Equations

• FunctionField.placeDegA k K v = FunctionField.Chart.placeDegree k K v

@[reducible, inline]

noncomputable abbrev FunctionField.degA (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (D : Chart.DivisorA k K) : ℤ

Backward-compatible alias for deg.

Equations

• FunctionField.degA k K D = FunctionField.Chart.deg k K D

class FunctionField.IsFullConstantField (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] : Prop

Every element of K that is algebraic over the base field k is already in k.

This is the standing hypothesis for the Stichtenoth/Serre adelic proof track. It is equivalent to k being relatively algebraically closed in K, i.e. Mathlib's algebraicClosure k K = ⊥; see FunctionField.isFullConstantField_iff_algebraicClosure_eq_bot.

• algebraic_mem (x : K) : IsAlgebraic k x → ∃ (c : k), x = (algebraMap k K) c

  Every element of K that is algebraic over k already lies in the image of k.

theorem FunctionField.IsFullConstantField.mem_range (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] [IsFullConstantField k K] {x : K} (hx : IsAlgebraic k x) : x ∈ Set.range ⇑(algebraMap k K)

theorem FunctionField.isFullConstantField_iff_algebraicClosure_eq_bot (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] : IsFullConstantField k K ↔ algebraicClosure k K = ⊥

IsFullConstantField k K is exactly the statement that k is relatively algebraically closed in K, i.e. it coincides with Mathlib's algebraicClosure k K = ⊥. This identifies the standing hypothesis with the standard field-theoretic notion.

instance FunctionField.ratFuncIsFullConstantField (k : Type u_1) [Field k] : IsFullConstantField k (RatFunc k)