Extensions of places: the ramification index and the relative degree

Let F' / k' be a field extension lying over F / k, with F' algebraic over F. Restricting the valuation of a place P' of F' / k' to F gives a valuation of F that is trivial on the constants and — because F' is algebraic over F, so that a valuation ring of F' containing F would be all of F' — nontrivial. Normalizing it produces a place P = P'.restrict k F of F / k, the place of F that P' lies over, and the index divided out in the normalization is the ramification index e(P' | P). The residue field of P embeds in the residue field of P', and the degree of that extension is the relative degree f(P' | P).

The constant field may grow along with F: if k' is integral over k then a valuation of F' is trivial on k exactly when it is trivial on k', so the places of F' / k and of F' / k' are literally the same objects. That is TauCeti.Place.constantsEquiv, which lets a place of F' / k' be produced from data that only sees the smaller constant field k.

The main theorem is the bound e(P' | P) · f(P' | P) ≤ [F' : F]: residues of elements of 𝒪_{P'} that are independent over F_P, multiplied by the powers t^j of a prime element for P' with 0 ≤ j < e, are independent over F, because the orders of the resulting blocks are pairwise distinct modulo e.

The file also records the action of the valuation ring 𝒪_P of a place P of F / k on the extension field F', through F. That action is not a global instance — for F' = F it would compete with the action of a valuation subring on its own field — so it, and the scalar tower it sits in, are provided to be reinstalled by consumers with attribute [local instance 10]. For a finite extension, it also records the standard local integral-closure model 𝒪_P ⊆ 𝒪'_P: F' is the fraction field and the localization of 𝒪'_P at (𝒪_P)⁰; for a separable extension, 𝒪'_P is Dedekind and module-finite over 𝒪_P, and separability transports to the canonical fraction fields used by Mathlib's different API.

Main definitions

• TauCeti.Place.constantsEquiv: the places of F' / k are the places of F' / k', for k' integral over k; enlarging the constants by an algebraic extension changes nothing.
• TauCeti.Place.algebraIntegersExtension and TauCeti.Place.isScalarTowerIntegersExtension: the action of the valuation ring of a place of F / k on an extension field F', to be installed with attribute [local instance 10].
• TauCeti.Place.restrict: the place of F / k that a place of F' / k' lies over.
• TauCeti.Place.ramificationIdx: the ramification index e(P' | P).
• TauCeti.Place.relativeDegree: the relative degree f(P' | P) = [F'_{P'} : F_P].

Main results

• TauCeti.Place.ord_algebraMap_restrict: the defining property ord_{P'} = e · ord_P on F.
• TauCeti.Place.restrict_eq_iff_integers_le, TauCeti.Place.restrict_eq_iff_forall_ord_pos and TauCeti.Place.restrict_eq_iff_exists_ord_eq: the three characterizations of P' ∣ P (Stichtenoth, Proposition 3.1.4), by the containment of valuation rings, by the containment of maximal ideals, and by the scaling of the order functions. Together with TauCeti.Place.restrict they say that every place of F' lies over exactly one place of F.
• TauCeti.Place.restrict_eq_iff_isEquiv_comap: P' ∣ P exactly when the restricted valuation is equivalent to that of P.
• TauCeti.Place.linearIndependent_mul_pow_of_linearIndependent_residue: the independence statement carrying the fundamental inequality, together with the three ingredients of its proof — TauCeti.Place.ord_sum_eq_zero_of_isUnit, TauCeti.Place.sum_ne_zero_of_linearIndependent_residue and TauCeti.Place.ramificationIdx_dvd_ord_sum_of_linearIndependent_residue — and the ultrametric estimate TauCeti.Place.sum_ne_zero_of_ord_eq_mul_add_natCast with TauCeti.Place.ord_sum_le_of_ord_eq_mul_add_natCast that combines them.
• TauCeti.Place.ramificationIdx_mul_relativeDegree_le_finrank: e(P' ∣ P) · f(P' ∣ P) ≤ [F' : F], with TauCeti.Place.ramificationIdx_le_finrank and TauCeti.Place.relativeDegree_le_finrank its two halves (Stichtenoth, Corollary 3.1.12).
• TauCeti.Place.linearIndependent_pow_fin_ramificationIdx: the first e(P' ∣ P) powers of a uniformizer at P' are linearly independent over F.
• TauCeti.Place.finiteDimensional_residueField_restrict: the relative degree is finite, so it is not the junk value of Module.finrank; TauCeti.Place.one_le_relativeDegree and TauCeti.Place.ramificationIdx_pos are the matching lower bounds.
• TauCeti.Place.finrank_mul_degree_eq_relativeDegree_mul_degree_restrict: [k' : k] · deg P' = f(P' ∣ P) · deg P, the comparison of the degrees of P' and of the place it lies over.
• TauCeti.Place.isFractionRing_integralClosure, TauCeti.Place.isLocalization_integralClosure, TauCeti.Place.isDedekindDomain_integralClosure, TauCeti.Place.moduleFinite_integralClosure, and TauCeti.Place.isSeparable_fractionRing_integralClosure: the fraction-field, localization, Dedekind, finiteness, and separability properties of the local integral closure 𝒪'_P.
• TauCeti.Place.isIntegral_algebraMap_iff_mem_integers: the local integral closure 𝒪'_P contracts to 𝒪_P.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.1.

@[instance_reducible]

noncomputable def TauCeti.Place.algebraIntegersExtension {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) : Algebra (↥P.integers) F'

The valuation ring of a place of F / k acts on an extension field F', through F.

This is not a global instance: for F' = F it would compete with the action of a valuation subring on its own field. Install it, together with TauCeti.Place.isScalarTowerIntegersExtension, with attribute [local instance 10] in any file that works with the local model of the extension at P — at low priority, so that the case F' = F still resolves to the valuation subring's own action, as the fraction-field instances expect.

Equations

• TauCeti.Place.algebraIntegersExtension F' P = ((algebraMap F F').comp (algebraMap (↥P.integers) F)).toAlgebra

theorem TauCeti.Place.isScalarTowerIntegersExtension {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) : IsScalarTower (↥P.integers) F F'

The action of TauCeti.Place.algebraIntegersExtension on F' factors through F.

theorem TauCeti.Place.algebraMap_integersExtension_injective {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) : Function.Injective ⇑(algebraMap (↥P.integers) F')

@[simp]

theorem TauCeti.Place.isIntegral_algebraMap_iff_mem_integers {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) {x : F} : IsIntegral (↥P.integers) ((algebraMap F F') x) ↔ x ∈ P.integers

𝒪'_P contracts to 𝒪_P: a function of F is integral over 𝒪_P in the extension F' exactly when it is regular at P. So enlarging the field does not enlarge the ring of functions of F integral over 𝒪_P, and 𝒪'_P ∩ F = 𝒪_P.

instance TauCeti.Place.isTorsionFree_integersExtension {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) : Module.IsTorsionFree (↥P.integers) F'

instance TauCeti.Place.isFractionRing_integralClosure {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] : IsFractionRing (↥(integralClosure (↥P.integers) F')) F'

The local model 𝒪'_P — the integral closure of 𝒪_P in F' — has fraction field F'.

theorem TauCeti.Place.isLocalization_integralClosure {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure (↥P.integers) F')) (nonZeroDivisors ↥P.integers)) F'

More precisely, F' is the localization of the local model 𝒪'_P at the nonzero divisors of 𝒪_P.

instance TauCeti.Place.isDedekindDomain_integralClosure {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] [Algebra.IsSeparable F F'] : IsDedekindDomain ↥(integralClosure (↥P.integers) F')

The local model 𝒪'_P is a Dedekind domain.

instance TauCeti.Place.moduleFinite_integralClosure {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] [Algebra.IsSeparable F F'] : Module.Finite ↥P.integers ↥(integralClosure (↥P.integers) F')

The local model 𝒪'_P is module-finite over 𝒪_P.

instance TauCeti.Place.isSeparable_fractionRing_integralClosure {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] [Algebra.IsSeparable F F'] : Algebra.IsSeparable (FractionRing ↥P.integers) (FractionRing ↥(integralClosure (↥P.integers) F'))

Separability of F' / F, transported to the canonical fraction fields used by the integral-closure API.

def TauCeti.Place.constantsEquiv (k : Type u) (k' : Type u') (F' : Type v') [Field k] [Field k'] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [Algebra.IsIntegral k k'] : Place k F' ≃ Place k' F'

Enlarging an algebraic constant field does not change the places: a valuation of F' is trivial on k exactly when it is trivial on k', because every nonzero element of k' is algebraic over k and every nonzero element of k is one of k'. So the places of F' / k and the places of F' / k' are the same, with the same valuations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Place.valuation_constantsEquiv {k : Type u} {k' : Type u'} {F' : Type v'} [Field k] [Field k'] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [Algebra.IsIntegral k k'] (Q : Place k F') : ((constantsEquiv k k' F') Q).valuation = Q.valuation

@[simp]

theorem TauCeti.Place.valuation_constantsEquiv_symm {k : Type u} {k' : Type u'} {F' : Type v'} [Field k] [Field k'] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [Algebra.IsIntegral k k'] (Q : Place k' F') : ((constantsEquiv k k' F').symm Q).valuation = Q.valuation

@[simp]

theorem TauCeti.Place.integers_constantsEquiv {k : Type u} {k' : Type u'} {F' : Type v'} [Field k] [Field k'] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [Algebra.IsIntegral k k'] (Q : Place k F') : ((constantsEquiv k k' F') Q).integers = Q.integers

@[simp]

theorem TauCeti.Place.integers_constantsEquiv_symm {k : Type u} {k' : Type u'} {F' : Type v'} [Field k] [Field k'] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [Algebra.IsIntegral k k'] (Q : Place k' F') : ((constantsEquiv k k' F').symm Q).integers = Q.integers

noncomputable def TauCeti.Place.restrict (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] : Place k F

The place of F / k that a place of F' / k' lies over: the normalization of the restriction of its valuation to F (Stichtenoth, Definition 3.1.2). Every place of F' lies over exactly one place of F; which place is characterized in TauCeti.Place.restrict_eq_iff_integers_le.

Equations

• TauCeti.Place.restrict k F P' = { valuation := (Valuation.comap (algebraMap F F') P'.valuation).normalization, valuation_surjective := ⋯, isTrivialOn := ⋯ }

noncomputable def TauCeti.Place.ramificationIdx {k' : Type u'} (F : Type v) {F' : Type v'} [Field k'] [Field F] [Field F'] [Algebra k' F'] [Algebra F F'] (P' : Place k' F') : ℕ

The ramification index e(P' ∣ P) of a place P' of F' / k' over the place P of F / k it lies over: the factor by which the order function at P' scales the order function at P (Stichtenoth, Definition 3.1.5).

Equations

• TauCeti.Place.ramificationIdx F P' = (Valuation.comap (algebraMap F F') P'.valuation).ordIndex

theorem TauCeti.Place.ramificationIdx_def {k' : Type u'} (F : Type v) {F' : Type v'} [Field k'] [Field F] [Field F'] [Algebra k' F'] [Algebra F F'] (P' : Place k' F') : ramificationIdx F P' = (Valuation.comap (algebraMap F F') P'.valuation).ordIndex

The ramification index is the order index of the restricted valuation.

theorem TauCeti.Place.ramificationIdx_pos {k' : Type u'} (F : Type v) {F' : Type v'} [Field k'] [Field F] [Field F'] [Algebra k' F'] [Algebra F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] : 0 < ramificationIdx F P'

The ramification index of a restricted place is positive.

theorem TauCeti.Place.ord_algebraMap_restrict (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] (f : F) : P'.ord ((algebraMap F F') f) = ↑(ramificationIdx F P') * (restrict k F P').ord f

The defining property of the ramification index (Stichtenoth, Definition 3.1.5): on F the order function at P' is e(P' ∣ P) times the order function at P.

theorem TauCeti.Place.mem_integers_restrict_iff (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] (f : F) : f ∈ (restrict k F P').integers ↔ (algebraMap F F') f ∈ P'.integers

An element of F is integral at the restriction exactly when it is integral at P'.

theorem TauCeti.Place.restrict_eq_iff_integers_le (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] (P : Place k F) : restrict k F P' = P ↔ ∀ f ∈ P.integers, (algebraMap F F') f ∈ P'.integers

P' ∣ P by valuation rings (Stichtenoth, Proposition 3.1.4): the place of F / k that P' lies over is the unique place whose valuation ring is carried into the valuation ring of P'.

theorem TauCeti.Place.restrict_eq_iff_isEquiv_comap (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] (P : Place k F) : restrict k F P' = P ↔ (Valuation.comap (algebraMap F F') P'.valuation).IsEquiv P.valuation

P' ∣ P by valuations: P' lies over P exactly when the restriction of its valuation to F is equivalent to the valuation of P. The restriction need not be normalized, so an equivalence, not an equality, is the right statement.

theorem TauCeti.Place.restrict_eq_iff_forall_ord_pos (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] (P : Place k F) : restrict k F P' = P ↔ ∀ (f : F), 0 < P.ord f → 0 < P'.ord ((algebraMap F F') f)

P' ∣ P by maximal ideals (Stichtenoth, Proposition 3.1.4): it is enough that the functions vanishing at P vanish at P'.

theorem TauCeti.Place.restrict_eq_iff_exists_ord_eq (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] (P : Place k F) : restrict k F P' = P ↔ ∃ (e : ℕ), 0 < e ∧ ∀ (f : F), P'.ord ((algebraMap F F') f) = ↑e * P.ord f

P' ∣ P by the scaling of orders (Stichtenoth, Proposition 3.1.4): the place P' lies over P exactly when the order function at P' is a positive multiple of the order function at P along F, and the multiple is then the ramification index.

theorem TauCeti.Place.ramificationIdx_eq_of_forall_ord_eq (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] {e : ℕ} (h : ∀ (f : F), P'.ord ((algebraMap F F') f) = ↑e * (restrict k F P').ord f) : ramificationIdx F P' = e

The ramification index is the only positive scaling factor between the two order functions.

instance TauCeti.Place.instHasExtensionValuation (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] : (restrict k F P').valuation.HasExtension P'.valuation

The valuation of the restricted place extends along F → F'; hence Mathlib's generic valuation-extension API supplies the valuation-ring algebra map, its locality, and the induced residue-field extension.

@[instance_reducible]

noncomputable instance TauCeti.Place.instAlgebraIntegers (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] : Algebra ↥(restrict k F P').integers ↥P'.integers

The valuation ring of the restriction is carried into the valuation ring of P', so the latter is an algebra over the former.

Equations

• TauCeti.Place.instAlgebraIntegers k F P' = (((algebraMap F F').comp (algebraMap (↥(TauCeti.Place.restrict k F P').integers) F)).codRestrict P'.integers ⋯).toAlgebra

@[simp]

theorem TauCeti.Place.coe_algebraMap_integers (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] (x : ↥(restrict k F P').integers) : ↑((algebraMap ↥(restrict k F P').integers ↥P'.integers) x) = (algebraMap F F') ↑x

instance TauCeti.Place.instIsLocalHomIntegers (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] : IsLocalHom (algebraMap ↥(restrict k F P').integers ↥P'.integers)

The valuation-ring algebra map is local, so it induces the residue-field extension used by relativeDegree.

noncomputable def TauCeti.Place.relativeDegree (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] : ℕ

The relative degree f(P' ∣ P) = [F'_{P'} : F_P] of a place P' of F' / k' over the place P of F / k it lies over (Stichtenoth, Definition 3.1.5).

Equations

• TauCeti.Place.relativeDegree k F P' = Module.finrank (TauCeti.Place.restrict k F P').ResidueField P'.ResidueField

theorem TauCeti.Place.relativeDegree_def (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] : relativeDegree k F P' = Module.finrank (restrict k F P').ResidueField P'.ResidueField

The relative degree is the finrank of the extension of residue fields.

theorem TauCeti.Place.finrank_mul_degree_eq_relativeDegree_mul_degree_restrict (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] : Module.finrank k k' * P'.degree = relativeDegree k F P' * (restrict k F P').degree

The degree of a place and the degree of the place below it (Stichtenoth, Section III.1): the residue field F'_{P'} sits in the two towers k ⊆ k' ⊆ F'_{P'} and k ⊆ F_P ⊆ F'_{P'}, whose successive degrees are [k' : k], deg P' and deg P, f(P' ∣ P). Comparing them gives [k' : k] · deg P' = f(P' ∣ P) · deg P.

The factor [k' : k] is mandatory and the identity is stated cross-multiplied: when the constant field grows, deg P' falls short of f(P' ∣ P) · deg P by exactly that factor.

theorem TauCeti.Place.sum_ne_zero_of_ord_eq_mul_add_natCast {k' : Type u'} {F' : Type v'} [Field k'] [Field F'] [Algebra k' F'] (P' : Place k' F') {e : ℕ} (A : Fin e → F') (hAord : ∀ (j : Fin e), A j ≠ 0 → ∃ (m : ℤ), P'.ord (A j) = ↑e * m + ↑↑j) {j₁ : Fin e} (hj₁ : A j₁ ≠ 0) : ∑ j : Fin e, A j ≠ 0

A sum whose nonzero terms have pairwise distinct orders is nonzero. The hypothesis is the form in which the distinctness is met in the extension theory: the order of A j is congruent to j modulo e, so no two nonzero terms can cancel.

theorem TauCeti.Place.ord_sum_le_of_ord_eq_mul_add_natCast {k' : Type u'} {F' : Type v'} [Field k'] [Field F'] [Algebra k' F'] (P' : Place k' F') {e : ℕ} (A : Fin e → F') (hAord : ∀ (j : Fin e), A j ≠ 0 → ∃ (m : ℤ), P'.ord (A j) = ↑e * m + ↑↑j) {j₁ : Fin e} (hj₁ : A j₁ ≠ 0) : P'.ord (∑ j : Fin e, A j) ≤ P'.ord (A j₁)

The order of a sum whose nonzero terms have pairwise distinct orders is the least of them; in particular it is at most the order of any nonzero term.

theorem TauCeti.Place.ord_sum_eq_zero_of_isUnit (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] {ι : Type u_1} [Fintype ι] (s : ι → ↥P'.integers) (hind : LinearIndependent (restrict k F P').ResidueField fun (i : ι) => (IsLocalRing.residue ↥P'.integers) (s i)) (b : ι → ↥(restrict k F P').integers) {i₀ : ι} (hb₀ : IsUnit (b i₀)) : P'.ord (∑ i : ι, (algebraMap F F') ↑(b i) * ↑(s i)) = 0

A combination of elements of 𝒪_{P'} with independent residues and coefficients in 𝒪_P, one of them a unit, has order zero at P' — that is, it is again a unit there.

theorem TauCeti.Place.sum_ne_zero_of_linearIndependent_residue (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] {ι : Type u_1} [Fintype ι] (s : ι → ↥P'.integers) (hind : LinearIndependent (restrict k F P').ResidueField fun (i : ι) => (IsLocalRing.residue ↥P'.integers) (s i)) (c : ι → F) {i₁ : ι} (hi₁ : c i₁ ≠ 0) : ∑ i : ι, (algebraMap F F') (c i) * ↑(s i) ≠ 0

A nontrivial F-combination of elements of 𝒪_{P'} whose residues are independent over the residue field of the place below is nonzero.

theorem TauCeti.Place.ramificationIdx_dvd_ord_sum_of_linearIndependent_residue (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] {ι : Type u_1} [Fintype ι] (s : ι → ↥P'.integers) (hind : LinearIndependent (restrict k F P').ResidueField fun (i : ι) => (IsLocalRing.residue ↥P'.integers) (s i)) (c : ι → F) : ↑(ramificationIdx F P') ∣ P'.ord (∑ i : ι, (algebraMap F F') (c i) * ↑(s i))

The order at P' of an F-combination of elements of 𝒪_{P'} whose residues are independent over the residue field of the place below is divisible by the ramification index, because such a combination is a scalar in F times a unit at P'.

theorem TauCeti.Place.linearIndependent_mul_pow_of_linearIndependent_residue (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [Algebra.IsIntegral F F'] {ι : Type u_1} (s : ι → ↥P'.integers) (hind : LinearIndependent (restrict k F P').ResidueField fun (i : ι) => (IsLocalRing.residue ↥P'.integers) (s i)) {t : F'} (ht : P'.ord t = 1) : LinearIndependent F fun (p : ι × Fin (ramificationIdx F P')) => ↑(s p.1) * t ^ ↑p.2

The independence statement behind the fundamental inequality (Stichtenoth, Theorem 3.1.11): if the residues at P' of a family of elements of 𝒪_{P'} are independent over the residue field of the place P below, and t is a prime element for P', then the products of those elements with t ^ j for 0 ≤ j < e(P' ∣ P) are independent over F. The reason is that the order at P' of an F-combination of the given elements is a multiple of e(P' ∣ P), so the e(P' ∣ P) blocks have pairwise distinct orders.

theorem TauCeti.Place.linearIndependent_pow_fin_ramificationIdx {k' : Type u'} (F : Type v) {F' : Type v'} [Field k'] [Field F] [Field F'] [Algebra k' F'] [Algebra F F'] (P' : Place k' F') {t : F'} (ht : P'.ord t = 1) : LinearIndependent F fun (j : Fin (ramificationIdx F P')) => t ^ ↑j

The first e(P' | P) powers of a uniformizer at P' are linearly independent over the field below.

theorem TauCeti.Place.ramificationIdx_le_finrank {k' : Type u'} (F : Type v) {F' : Type v'} [Field k'] [Field F] [Field F'] [Algebra k' F'] [Algebra F F'] (P' : Place k' F') [FiniteDimensional F F'] : ramificationIdx F P' ≤ Module.finrank F F'

The ramification index of a place is at most the degree of the field extension.

instance TauCeti.Place.finiteDimensional_residueField_restrict (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [FiniteDimensional F F'] : FiniteDimensional (restrict k F P').ResidueField P'.ResidueField

The residue field of a place is finite over the residue field of the place below it.

theorem TauCeti.Place.one_le_relativeDegree (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [FiniteDimensional F F'] : 1 ≤ relativeDegree k F P'

The relative degree is positive because a residue field extension is nontrivial.

theorem TauCeti.Place.ramificationIdx_mul_relativeDegree_le_finrank (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [FiniteDimensional F F'] : ramificationIdx F P' * relativeDegree k F P' ≤ Module.finrank F F'

The fundamental inequality at a single place (Stichtenoth, Theorem 3.1.11 and Corollary 3.1.12): the ramification index times the relative degree of a place P' of F' / k' over the place of F / k it lies over is at most the degree of the extension.

theorem TauCeti.Place.relativeDegree_le_finrank (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (P' : Place k' F') [FiniteDimensional F F'] : relativeDegree k F P' ≤ Module.finrank F F'

The relative degree of a place is at most the degree of the field extension.

@[simp]

theorem TauCeti.Place.restrict_self {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : restrict k F P = P

A place restricts to itself along the identity extension. Restriction normalizes the valuation pulled back along algebraMap F F, which is the identity, and a place's valuation is already surjective, hence already normalized.

@[simp]

theorem TauCeti.Place.ramificationIdx_self {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : ramificationIdx F P = 1

The identity extension is unramified: e(P ∣ P) = 1.