The Fundamental Inequality of Valued Fields

Source: url:https://github.com/linzialessandro/FundamentalInequality Authors: Alessandro Linzi Status: verified Main declarations: Valuation.fundamentalInequality, Valuation.ramificationIndex Tags: valued-fields, number-theory, valuation-theory MSC: 12J20

Ramification Index, Residue Degree, and the Fundamental Inequality

This file defines the ramification index e(w/v) and residue degree f(w/v) for an extension of valued fields (L | K, w | v), and proves the fundamental inequality [L : K] ≥ e(w/v) · f(w/v) for finite extensions.

Main definitions

• Valuation.ramificationIndex : The index [w(L×) : v(K×)].
• Valuation.residueDegree : The degree [Lw : Kv] of the residue field extension.

Main results

• Valuation.valuation_independence : Elements with valuations in distinct cosets and residues that are linearly independent form a linearly independent set over K.
• Valuation.fundamentalInequality : e(w/v) * f(w/v) ≤ [L : K].

References

• [F.-V. Kuhlmann, Valued Fields, Chapter 4, §4.4]

noncomputable def Valuation.residueDegree {K : Type u_1} [Field K] {ΓK : Type u_2} [LinearOrderedCommGroupWithZero ΓK] (vK : Valuation K ΓK) {L : Type u_3} [Field L] {ΓL : Type u_4} [LinearOrderedCommGroupWithZero ΓL] (vL : Valuation L ΓL) [Algebra K L] [vK.HasExtension vL] : ℕ

The residue degree f(w/v) of a valued field extension.

Equations

• vK.residueDegree vL = Module.finrank (IsLocalRing.ResidueField ↥vK.valuationSubring) (IsLocalRing.ResidueField ↥vL.valuationSubring)

noncomputable def Valuation.ramificationIndex (K : Type u_1) [Field K] {L : Type u_2} [Field L] {ΓL : Type u_3} [LinearOrderedCommGroupWithZero ΓL] (vL : Valuation L ΓL) [Algebra K L] : ℕ

The ramification index e(w/v) of a valued field extension. It depends only on the base field K, the valuation w = vL, and the algebra structure K → L.

Equations

• Valuation.ramificationIndex K vL = (MonoidWithZeroHom.ofClass (Valuation.comap (algebraMap K L) vL)).valueGroup.relIndex (MonoidWithZeroHom.ofClass vL).valueGroup

theorem Valuation.sum_eq_zero_implies_val_eq {L : Type u_3} [Field L] {ΓL : Type u_4} [LinearOrderedCommGroupWithZero ΓL] (vL : Valuation L ΓL) {I : Type u_5} [Fintype I] [Nonempty I] (f : I → L) (h_sum : ∑ i : I, f i = 0) (h_nz : ∀ (i : I), f i ≠ 0) : ∃ (i : I) (j : I), i ≠ j ∧ vL (f i) = vL (f j)

If a finite sum is zero, and all elements are non-zero, then at least two elements must have the same valuation.

theorem Valuation.linearIndependent_of_val_distinct_coset {K : Type u_1} [Field K] {L : Type u_3} [Field L] {ΓL : Type u_4} [LinearOrderedCommGroupWithZero ΓL] (vL : Valuation L ΓL) [Algebra K L] {I : Type u_5} [Nonempty I] (z : I → L) (hz_nz : ∀ (i : I), z i ≠ 0) (hz_dist : ∀ (i j : I), i ≠ j → ∀ (c d : K), c ≠ 0 → d ≠ 0 → vL ((algebraMap K L) c * z i) ≠ vL ((algebraMap K L) d * z j)) : LinearIndependent K z

Elements with valuations in strictly distinct cosets modulo v(K×) are linearly independent over K.

theorem Valuation.linearIndependent_of_val_no_cancel {K : Type u_1} [Field K] {L : Type u_3} [Field L] {ΓL : Type u_4} [LinearOrderedCommGroupWithZero ΓL] (vL : Valuation L ΓL) [Algebra K L] {J : Type u_5} [Fintype J] (u : J → L) (hu_nz : ∀ (j : J), u j ≠ 0) (hu_no_cancel : ∀ (d : J → K), (∃ (j : J), d j ≠ 0) → ∃ (j0 : J), vL (∑ j : J, (algebraMap K L) (d j) * u j) = vL ((algebraMap K L) (d j0) * u j0) ∧ ∀ (j : J), vL ((algebraMap K L) (d j) * u j) ≤ vL ((algebraMap K L) (d j0) * u j0)) : LinearIndependent K u

Elements with no-cancellation property are linearly independent over K.

theorem Valuation.valuation_independence {K : Type u_1} [Field K] {L : Type u_3} [Field L] {ΓL : Type u_4} [LinearOrderedCommGroupWithZero ΓL] (vL : Valuation L ΓL) [Algebra K L] {I : Type u_5} {J : Type u_6} [Finite I] [Fintype J] [Nonempty I] (z : I → L) (hz_nz : ∀ (i : I), z i ≠ 0) (hz_dist : ∀ (i j : I), i ≠ j → ∀ (c d : K), c ≠ 0 → d ≠ 0 → vL ((algebraMap K L) c * z i) ≠ vL ((algebraMap K L) d * z j)) (u : J → L) (hu_val_one : ∀ (j : J), vL (u j) = 1) (hu_no_cancel : ∀ (d : J → K), (∃ (j : J), d j ≠ 0) → ∃ (j0 : J), vL (∑ j : J, (algebraMap K L) (d j) * u j) = vL ((algebraMap K L) (d j0) * u j0) ∧ ∀ (j : J), vL ((algebraMap K L) (d j) * u j) ≤ vL ((algebraMap K L) (d j0) * u j0)) : LinearIndependent K fun (ij : I × J) => z ij.1 * u ij.2

Valuation Independence. If elements have valuations in distinct cosets and residues that are linearly independent, then their products are linearly independent over K.

theorem Valuation.exists_max_val_no_cancel {K : Type u_1} [Field K] {ΓK : Type u_2} [LinearOrderedCommGroupWithZero ΓK] (vK : Valuation K ΓK) {L : Type u_3} [Field L] {ΓL : Type u_4} [LinearOrderedCommGroupWithZero ΓL] (vL : Valuation L ΓL) [Algebra K L] [vK.HasExtension vL] {J : Type u_5} [Fintype J] [Nonempty J] (u : J → L) (u_sub : J → ↥vL.valuationSubring) (hu_eq : ∀ (j : J), ↑(u_sub j) = u j) (hu_val_one : ∀ (j : J), vL (u j) = 1) (hu_res_indep : LinearIndependent (IsLocalRing.ResidueField ↥vK.valuationSubring) fun (j : J) => (IsLocalRing.residue ↥vL.valuationSubring) (u_sub j)) (d : J → K) : (∃ (j : J), d j ≠ 0) → ∃ (j0 : J), vL (∑ j : J, (algebraMap K L) (d j) * u j) = vL ((algebraMap K L) (d j0) * u j0) ∧ ∀ (j : J), vL ((algebraMap K L) (d j) * u j) ≤ vL ((algebraMap K L) (d j0) * u j0)

For a family u of elements of valuation one whose residues are linearly independent over the base residue field, no nontrivial K-linear combination cancels: there is an index attaining the maximal valuation, equal to the valuation of the whole sum.

theorem Valuation.fundamentalInequality {K : Type u_1} [Field K] {ΓK : Type u_2} [LinearOrderedCommGroupWithZero ΓK] (vK : Valuation K ΓK) {L : Type u_3} [Field L] {ΓL : Type u_4} [LinearOrderedCommGroupWithZero ΓL] (vL : Valuation L ΓL) [Algebra K L] [vK.HasExtension vL] [FiniteDimensional K L] : ramificationIndex K vL * vK.residueDegree vL ≤ Module.finrank K L

The fundamental inequality for finite extensions of valued fields. [L : K] ≥ e(w/v) · f(w/v)