Ramification half of Stichtenoth 1.4.11

This file proves deg (X_K)_∞ ≤ [K : k(X)] via the fundamental identity of ramification index and inertia degree.

@[instance_reducible]

noncomputable def FunctionField.Chart.instDecidableEqPlaceARam (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] : DecidableEq (PlaceA k K)

Decidable equality on coordinate places for ramification proofs.

Equations

• FunctionField.Chart.instDecidableEqPlaceARam k K = Classical.decEq (FunctionField.Chart.PlaceA k K)

@[instance_reducible]

noncomputable def FunctionField.Chart.instDecidableEqRatFuncRam (k : Type u_1) [Field k] : DecidableEq (RatFunc k)

The classical decidable equality on k(X) used by the coordinate places.

Equations

• FunctionField.Chart.instDecidableEqRatFuncRam k = Classical.decEq (RatFunc k)

noncomputable def FunctionField.Chart.tRatFunc (k : Type u_1) [Field k] : RatFunc k

The uniformizer t = X⁻¹ in k(X).

Equations

• FunctionField.Chart.tRatFunc k = 1 / RatFunc.X

noncomputable def FunctionField.Chart.tA (k : Type u_1) [Field k] : ↥(inftyValuationSubring k)

t as an element of the valuation subring at infinity.

Equations

• FunctionField.Chart.tA k = ⟨FunctionField.Chart.tRatFunc k, ⋯⟩

@[simp]

theorem FunctionField.Chart.tRatFunc_coe (k : Type u_1) [Field k] : ↑(tA k) = tRatFunc k

theorem FunctionField.Chart.maximalIdeal_infty_eq_span_t (k : Type u_1) [Field k] : IsLocalRing.maximalIdeal ↥(inftyValuationSubring k) = Ideal.span {tA k}

noncomputable def FunctionField.Chart.ramIdxInfty (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] (P : Ideal ↥(infiniteIntegers k K)) : ℕ

Ramification index of the infinite place above k(X).

Equations

• FunctionField.Chart.ramIdxInfty k K P = (IsLocalRing.maximalIdeal ↥(FunctionField.Chart.inftyValuationSubring k)).ramificationIdx' P

noncomputable def FunctionField.Chart.tK (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] : K

Its image t_K in the function field.

Equations

• FunctionField.Chart.tK k K = (algebraMap (RatFunc k) K) (FunctionField.Chart.tRatFunc k)

theorem FunctionField.Chart.map_maximalIdeal_infty (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] : Ideal.map (algebraMap ↥(inftyValuationSubring k) ↥(infiniteIntegers k K)) (IsLocalRing.maximalIdeal ↥(inftyValuationSubring k)) = Ideal.span {(algebraMap ↥(inftyValuationSubring k) ↥(infiniteIntegers k K)) (tA k)}

theorem FunctionField.Chart.XK_mul_tK (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] : XK k K * tK k K = 1

theorem FunctionField.Chart.XK_mem_ringOfIntegers (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : ∃ (a : ↥(ringOfIntegers k K)), ↑a = XK k K

theorem FunctionField.Chart.ringOfIntegers_coe_ne_zero (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] {a : ↥(ringOfIntegers k K)} (ha : a ≠ 0) : ↑a ≠ 0

theorem FunctionField.Chart.principalDivisorA_nonneg_at_finite_of_mem_ringOfIntegers (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {a : ↥(ringOfIntegers k K)} (ha : a ≠ 0) (w : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : 0 ≤ ((principalDivisorA k K) (Additive.ofMul (Units.mk0 ↑a ⋯))) (Sum.inl w)

theorem FunctionField.Chart.polarDivisor_XK_zero_at_finite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : (polarDivisor k K (XK k K)) (Sum.inl w) = 0

theorem FunctionField.Chart.tK_ne_zero (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] : tK k K ≠ 0

theorem FunctionField.Chart.principalDivisorA_tK_at_infinite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : ((principalDivisorA k K) (Additive.ofMul (Units.mk0 (tK k K) ⋯))) (Sum.inr v) = ↑(ramIdxInfty k K v.asIdeal)

theorem FunctionField.Chart.principalDivisorA_XK_at_infinite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : ((principalDivisorA k K) (Additive.ofMul (Units.mk0 (XK k K) ⋯))) (Sum.inr v) = -↑(ramIdxInfty k K v.asIdeal)

theorem FunctionField.Chart.ramificationIdx_pos_over_infty (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : 0 < ramIdxInfty k K v.asIdeal

theorem FunctionField.Chart.polarDivisor_XK_at_infinite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : (polarDivisor k K (XK k K)) (Sum.inr v) = ↑(ramIdxInfty k K v.asIdeal)

noncomputable def FunctionField.Chart.inftyIdealOfPlace (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (v : PlaceA k K) : Ideal ↥(infiniteIntegers k K)

The height-one ideal above ∞ corresponding to an infinite place.

Equations

• FunctionField.Chart.inftyIdealOfPlace k K (Sum.inr w) = w.asIdeal
• FunctionField.Chart.inftyIdealOfPlace k K (Sum.inl val) = ⊥

theorem FunctionField.Chart.deg_polarDivisor_XK_eq_primesOverFinset_sum (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : deg k K (polarDivisor k K (XK k K)) = ∑ P ∈ IsDedekindDomain.primesOverFinset (IsLocalRing.maximalIdeal ↥(inftyValuationSubring k)) ↥(infiniteIntegers k K), ↑(ramIdxInfty k K P) * ↑((IsLocalRing.maximalIdeal ↥(inftyValuationSubring k)).inertiaDeg' P)

theorem FunctionField.Chart.deg_polarX_le_finrank (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : deg k K (polarDivisor k K (XK k K)) ≤ ↑(Module.finrank (RatFunc k) K)

Stichtenoth 1.4.11 ramification half for the chart variable: deg (X_K)_∞ ≤ [K : k(X)].