The Artin--Schreier genus… to The tame different theorem…

TheoremThe Artin--Schreier genus formula, cross-multiplied for a possible constant-field extension#

The representatives may vary with the place. Pole orders are weighted by residue field degrees, not by the number of poles.

TauCeti.artinSchreier_genus_formula.{u, u', v, v'} {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']
  (hF : TauCeti.IsFunctionField k F) (hF' : TauCeti.IsFunctionField k' F') (p : ℕ)
  [Fact (Nat.Prime p)] [CharP F p] {y : F'} {u : F} (hgen : F⟮y⟯ = ⊤)
  (hy : y ^ p - y = (algebraMap F F') u) (S : Finset (TauCeti.Place k F))
  (m : TauCeti.Place k F → ℕ)
  (hpole : ∀ P ∈ S, ∃ w, P.ord (u - (w ^ p - w)) = -↑(m P) ∧ ¬↑p ∣ P.ord (u - (w ^ p - w)))
  (hreg : ∀ P ∉ S, ∃ w, u - (w ^ p - w) ∈ P.integers) [Algebra.IsSeparable k k']
  (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F')
  (hu : ∀ (w : F), w ^ p - w ≠ u) :
  ↑(Module.finrank k k') * (2 * ↑(TauCeti.genus k' F') - 2) =
    ↑p * (2 * ↑(TauCeti.genus k F) - 2) + (↑p - 1) * ∑ P ∈ S, (↑(m P) + 1) * ↑P.degree

Lean

Formalized in Tau Ceti as TauCeti.artinSchreier_genus_formula.

Sources

• Tau Ceti documentation: TauCeti.artinSchreier_genus_formula
• Source of TauCeti.artinSchreier_genus_formula in TauCeti/FieldTheory/FunctionField/ArtinSchreier/Genus.lean

LeanTauCeti.artinSchreier_genus_formula

Uses 4

Proof usesThe fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · The weak approximation theorem

TheoremCastelnuovo's inequality (Stichtenoth, Theorem 3.11.3)#

Let F / k be a function field with exact constants and a separating element x, and let F₁, F₂ be subfields of F containing k with F = F₁ F₂ and F finite over both. Then g(F) ≤ [F : F₁] g(F₁) + [F : F₂] g(F₂) + ([F : F₁] - 1) ([F : F₂] - 1). The constant field k may be imperfect, and neither subextension is assumed separable.

TauCeti.genus_le_finrank_mul_genus_add_finrank_mul_genus_add.{u_1, u_2, u_3, u_4} {k : Type u_1}
  {F₁ : Type u_2} {F₂ : Type u_3} {F : Type u_4} [Field k] [Field F₁] [Field F₂] [Field F]
  [Algebra k F₁] [Algebra k F₂] [Algebra k F] [Algebra F₁ F] [Algebra F₂ F] [IsScalarTower k F₁ F]
  [IsScalarTower k F₂ F] [FiniteDimensional F₁ F] [FiniteDimensional F₂ F]
  (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F}
  (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F]
  (htop : IntermediateField.adjoin F₁ (Set.range ⇑(algebraMap F₂ F)) = ⊤) :
  TauCeti.genus k F ≤
    Module.finrank F₁ F * TauCeti.genus k F₁ + Module.finrank F₂ F * TauCeti.genus k F₂ +
      (Module.finrank F₁ F - 1) * (Module.finrank F₂ F - 1)

Lean

Formalized in Tau Ceti as TauCeti.genus_le_finrank_mul_genus_add_finrank_mul_genus_add.

Other forms

Castelnuovo's inequality (Stichtenoth, Theorem 3.11.3), from a split place. Formalized in Tau Ceti as TauCeti.genus_le_finrank_mul_genus_add_finrank_mul_genus_add_of_isSplitCompletely.

TauCeti.genus_le_finrank_mul_genus_add_finrank_mul_genus_add_of_isSplitCompletely.{u_1, u_2, u_3,
    u_4}
  {k : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F : Type u_4} [Field k] [Field F₁] [Field F₂]
  [Field F] [Algebra k F₁] [Algebra k F₂] [Algebra k F] [Algebra F₁ F] [Algebra F₂ F]
  [IsScalarTower k F₁ F] [IsScalarTower k F₂ F] [FiniteDimensional F₁ F] [FiniteDimensional F₂ F]
  (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {P₁ : TauCeti.Place k F₁}
  (hsplit : P₁.IsSplitCompletely)
  (hinj :
    Set.InjOn (fun P => TauCeti.Place.restrict k F₂ P) {P | TauCeti.Place.restrict k F₁ P = P₁})
  (hdeg :
    ∀ (P : TauCeti.Place k F),
      TauCeti.Place.restrict k F₁ P = P₁ → (TauCeti.Place.restrict k F₂ P).degree = 1)
  {T : Set (TauCeti.Place k F₂)} (hT : ∀ Q ∈ T, Q.degree = 1)
  (hcard : ↑(TauCeti.genus k F₂) ≤ T.encard)
  (hdisj :
    ∀ (P : TauCeti.Place k F),
      TauCeti.Place.restrict k F₁ P = P₁ → TauCeti.Place.restrict k F₂ P ∉ T) :
  TauCeti.genus k F ≤
    Module.finrank F₁ F * TauCeti.genus k F₁ + Module.finrank F₂ F * TauCeti.genus k F₂ +
      (Module.finrank F₁ F - 1) * (Module.finrank F₂ F - 1)

Castelnuovo's inequality over a perfect constant field (Stichtenoth, Theorem 3.11.3). Formalized in Tau Ceti as TauCeti.genus_le_finrank_mul_genus_add_finrank_mul_genus_add_of_perfectField.

TauCeti.genus_le_finrank_mul_genus_add_finrank_mul_genus_add_of_perfectField.{u_1, u_2, u_3, u_4}
  {k : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {F : Type u_4} [Field k] [Field F₁] [Field F₂]
  [Field F] [Algebra k F₁] [Algebra k F₂] [Algebra k F] [Algebra F₁ F] [Algebra F₂ F]
  [IsScalarTower k F₁ F] [IsScalarTower k F₂ F] [FiniteDimensional F₁ F] [FiniteDimensional F₂ F]
  [PerfectField k] (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F)
  (htop : IntermediateField.adjoin F₁ (Set.range ⇑(algebraMap F₂ F)) = ⊤) :
  TauCeti.genus k F ≤
    Module.finrank F₁ F * TauCeti.genus k F₁ + Module.finrank F₂ F * TauCeti.genus k F₂ +
      (Module.finrank F₁ F - 1) * (Module.finrank F₂ F - 1)

Sources

• Tau Ceti documentation: TauCeti.genus_le_finrank_mul_genus_add_finrank_mul_genus_add
• Source of TauCeti.genus_le_finrank_mul_genus_add_finrank_mul_genus_add in TauCeti/FieldTheory/FunctionField/Consequences/Castelnuovo.lean

LeanTauCeti.genus_le_finrank_mul_genus_add_finrank_mul_genus_add · TauCeti.genus_le_finrank_mul_genus_add_finrank_mul_genus_add_of_isSplitCompletely · TauCeti.genus_le_finrank_mul_genus_add_finrank_mul_genus_add_of_perfectField

Uses 7

Proof usesDedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · Kummer's theorem (Stichtenoth, Corollary 3.3.8) · Riemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · The weak approximation theorem

TheoremClifford's theorem#

Clifford's theorem (Stichtenoth, Theorem 1.6.13), over an arbitrary exact field of constants: a divisor of degree between 0 and 2g - 2 satisfies

2 * ℓ(D) ≤ deg D + 2.

The bound includes the nonspecial and empty-linear-system edge cases.

TauCeti.Divisor.two_mul_dim_le_degree_add_two.{u_1, u_2} {k : Type u_1} {F : Type u_2} [Field k]
  [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F)
  {D : TauCeti.Divisor k F} (hDnonneg : 0 ≤ TauCeti.Divisor.degree D)
  (hDle : TauCeti.Divisor.degree D ≤ 2 * ↑(TauCeti.genus k F) - 2) :
  2 * ↑D.dim ≤ TauCeti.Divisor.degree D + 2

Lean

Formalized in Tau Ceti as TauCeti.Divisor.two_mul_dim_le_degree_add_two.

Sources

• Tau Ceti documentation: TauCeti.Divisor.two_mul_dim_le_degree_add_two
• Source of TauCeti.Divisor.two_mul_dim_le_degree_add_two in TauCeti/FieldTheory/FunctionField/Consequences/Clifford.lean

LeanTauCeti.Divisor.two_mul_dim_le_degree_add_two

Uses 4

Proof usesThe fundamental inequality (Stichtenoth, Theorem 3.1.11) · Riemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · The weak approximation theorem

TheoremDedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a))#

the different exponent of a place is at least one less than its ramification index. It is stated as e(P' ∣ P) ≤ d(P' ∣ P) + 1 so that no truncated subtraction of natural numbers appears.

Unlike the second part of that theorem — equality exactly in the tame case — this half needs no hypothesis beyond separability of F' / F, and in particular none on the residue extension.

TauCeti.Place.ramificationIdx_le_differentExponent_add_one.{u, u', v, v'} (k : Type u)
  {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F]
  [Algebra F F'] [Field k'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
  [IsScalarTower k F F'] [FiniteDimensional F F'] (P' : TauCeti.Place k' F')
  [Algebra.IsSeparable F F'] :
  TauCeti.Place.ramificationIdx F P' ≤ TauCeti.Place.differentExponent k F P' + 1

Lean

Formalized in Tau Ceti as TauCeti.Place.ramificationIdx_le_differentExponent_add_one.

Other forms

Dedekind's different theorem (Stichtenoth, Theorem 3.5.1(a)) at the level of divisors. Formalized in Tau Ceti as TauCeti.Divisor.ramificationIdx_le_coeff_different_add_one.

TauCeti.Divisor.ramificationIdx_le_coeff_different_add_one.{u, u', v, v'} {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'] [FiniteDimensional F F'] [Algebra.IsSeparable F F']
  (hF : TauCeti.IsFunctionField k F) (P' : TauCeti.Place k' F') :
  ↑(TauCeti.Place.ramificationIdx F P') ≤
    TauCeti.AlgebraicGeometry.WeilDivisor.coeff (TauCeti.Divisor.different k' F' hF) P' + 1

Dedekind's different theorem, first part, as an inequality of divisors (Stichtenoth, Theorem 3.5.1(a)). Formalized in Tau Ceti as TauCeti.Divisor.tameDifferent_le_different.

TauCeti.Divisor.tameDifferent_le_different.{u, u', v, v'} {k : Type u} (k' : Type u') {F : Type v}
  (F' : Type v') [Field k] [Field k'] [Field F] [Field F'] [Algebra k F] [Algebra F F']
  [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (hF : TauCeti.IsFunctionField k F) :
  TauCeti.Divisor.tameDifferent k' F' hF ≤ TauCeti.Divisor.different k' F' hF

Dedekind's different theorem, second part (Stichtenoth, Theorem 3.5.1(b)). Formalized in Tau Ceti as TauCeti.Place.ramificationIdx_eq_differentExponent_add_one_iff.

TauCeti.Place.ramificationIdx_eq_differentExponent_add_one_iff.{u, u', v, v'} (k : Type u)
  {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k F]
  [Algebra F F'] [Algebra k k'] [Algebra k' F'] [Algebra k F'] [IsScalarTower k k' F']
  [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F']
  (P' : TauCeti.Place k' F') :
  TauCeti.Place.ramificationIdx F P' = TauCeti.Place.differentExponent k F P' + 1 ↔
    TauCeti.Place.IsTame k F P'

Sources

• Tau Ceti documentation: TauCeti.Place.ramificationIdx_le_differentExponent_add_one
• Source of TauCeti.Place.ramificationIdx_le_differentExponent_add_one in TauCeti/FieldTheory/FunctionField/Different/Basic.lean

LeanTauCeti.Place.ramificationIdx_le_differentExponent_add_one · TauCeti.Divisor.ramificationIdx_le_coeff_different_add_one · TauCeti.Divisor.tameDifferent_le_different · TauCeti.Place.ramificationIdx_eq_differentExponent_add_one_iff

Uses 3 · Used by 16

Proof usesDedekind's different theorem, the tame case, as an exponent · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The weak approximation theorem

Used byPerfect local Tate duality for E[m] · The Hurwitz genus formula for y² = x³ - x over K(x), as a numerical identity · The Wronskian identity of an isogeny · Isogenous curves over a finite field have the same zeta function Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n) · The φ-descent sequence is exact at H¹(G_K, E₁[φ]) · The Hasse bound (Silverman V.1.1) · The m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2) · TauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual · The Riemann–Roch theorem with the sheaf of differentials · Belyi's theorem, existence direction · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · The residue theorem over a perfect field (Stichtenoth, Corollary 4.3.3 and Remark 4.3.7(d)) · The residue theorem (Stichtenoth, Corollary 4.3.3) · Castelnuovo's inequality (Stichtenoth, Theorem 3.11.3) · Hilbert's different formula · The Hurwitz bound (Stichtenoth, Exercise 3.18)

TheoremThe Eisenstein criterion (Stichtenoth, Proposition 3.1.15)#

if F' = F(y) and the minimal polynomial of y over F is Eisenstein at the place of F / k below P', then P' is totally ramified over F. Together with TauCeti.Place.setOf_restrict_eq_eq_singleton_of_isTotallyRamified this says that the place below P' is totally ramified in F' / F: it has exactly one extension, of ramification index [F' : F] and relative degree 1.

TauCeti.Place.isTotallyRamified_of_isEisensteinAt.{u, u', v, v'} (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' : TauCeti.Place k' F'} [Algebra.IsIntegral F F'] [FiniteDimensional F F'] {y : F'}
  (htop : F⟮y⟯ = ⊤) (hφ : (TauCeti.Place.restrict k F P').IsEisensteinAt (minpoly F y)) :
  TauCeti.Place.IsTotallyRamified F P'

Lean

Formalized in Tau Ceti as TauCeti.Place.isTotallyRamified_of_isEisensteinAt.

Sources

• Tau Ceti documentation: TauCeti.Place.isTotallyRamified_of_isEisensteinAt
• Source of TauCeti.Place.isTotallyRamified_of_isEisensteinAt in TauCeti/FieldTheory/FunctionField/Place/Extension/Eisenstein.lean

LeanTauCeti.Place.isTotallyRamified_of_isEisensteinAt

TheoremThe fundamental identity#

The fundamental identity (Stichtenoth, Theorem 3.1.11) at a place of the finite chart of a model: the ramification indices and relative degrees of the places of F' / k' lying over the place of a height one prime 𝔭 of R satisfy ∑ e(P' ∣ P) · f(P' ∣ P) = [F' : F]. Together with TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_le_finrank this settles the fibre over every place that lies on some affine model.

TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank.{u, u', v, v', w, w'} (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'] {R : Type w} [CommRing R] [Algebra R F] (S : Type w') [CommRing S]
  [Algebra S F'] [Algebra R S] [Algebra R F'] [IsScalarTower R S F'] [IsScalarTower R F F']
  [Algebra.IsIntegral F F'] [IsDedekindDomain R] [IsDedekindDomain S] [IsFractionRing R F]
  [IsFractionRing S F'] [Algebra k' S] [IsScalarTower k' S F'] [Algebra k R] [IsScalarTower k R F]
  (𝔭 : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite R S] {s : Finset (TauCeti.Place k' F')}
  (hs :
    ∀ (P' : TauCeti.Place k' F'),
      P' ∈ s ↔ TauCeti.Place.restrict k F P' = TauCeti.Place.ofPrime k F 𝔭) :
  ∑ P' ∈ s, TauCeti.Place.ramificationIdx F P' * TauCeti.Place.relativeDegree k F P' =
    Module.finrank F F'

Lean

Formalized in Tau Ceti as TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank.

Other forms

TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isFunctionField. Formalized in Tau Ceti as TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isFunctionField.

TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isFunctionField.{u, u', v, v'}
  (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'] [FiniteDimensional F F'] [Algebra.IsIntegral k k']
  (hF : TauCeti.IsFunctionField k F) (P : TauCeti.Place k F) {s : Finset (TauCeti.Place k' F')}
  (hs : ∀ (P' : TauCeti.Place k' F'), P' ∈ s ↔ TauCeti.Place.restrict k F P' = P) :
  ∑ P' ∈ s, TauCeti.Place.ramificationIdx F P' * TauCeti.Place.relativeDegree k F P' =
    Module.finrank F F'

The fundamental identity. Formalized in Tau Ceti as TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isSeparable.

TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isSeparable.{u, u', v, v'}
  (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'] [FiniteDimensional F F'] [Algebra.IsIntegral k k']
  [Algebra.IsSeparable F F'] (P : TauCeti.Place k F) {s : Finset (TauCeti.Place k' F')}
  (hs : ∀ (P' : TauCeti.Place k' F'), P' ∈ s ↔ TauCeti.Place.restrict k F P' = P) :
  ∑ P' ∈ s, TauCeti.Place.ramificationIdx F P' * TauCeti.Place.relativeDegree k F P' =
    Module.finrank F F'

Sources

• Tau Ceti documentation: TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank
• Source of TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank in TauCeti/FieldTheory/FunctionField/AffineModel/Extension.lean

LeanTauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank · TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isFunctionField · TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank_of_isSeparable

Uses 2 · Used by 14

Proof usesKrull–Akizuki for Mathlib's integralClosure · TauCeti.Ring.IsJapanese

Used byPerfect local Tate duality for E[m] · The Wronskian identity of an isogeny · Isogenous curves over a finite field have the same zeta function Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n) · The φ-descent sequence is exact at H¹(G_K, E₁[φ]) · The Hasse bound (Silverman V.1.1) · The m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2) · Abhyankar's lemma (Stichtenoth, Theorem 3.9.1) · The genus of a smooth projective plane curve (Fulton, *Algebraic Curves*, Section 8.3) · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · Castelnuovo's inequality (Stichtenoth, Theorem 3.11.3) · Hilbert's different formula · Riemann's inequality (Stichtenoth, Corollary 3.11.4) · The Artin--Schreier genus formula, cross-multiplied for a possible constant-field extension · The Hurwitz bound (Stichtenoth, Exercise 3.18)

TheoremThe fundamental inequality (Stichtenoth, Theorem 3.1.11)#

the ramification indices and relative degrees of finitely many distinct places of F' / k' lying over one place P of F / k satisfy ∑ e(P' ∣ P) · f(P' ∣ P) ≤ [F' : F].

The reverse inequality — the fundamental identity — is not proved here; it is the affine-model reconciliation with Ideal.sum_ramification_inertia.

TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_le_finrank.{u, u', v, v'} (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'] [FiniteDimensional F F'] (P : TauCeti.Place k F)
  (s : Finset (TauCeti.Place k' F')) (hs : ∀ P' ∈ s, TauCeti.Place.restrict k F P' = P) :
  ∑ P' ∈ s, TauCeti.Place.ramificationIdx F P' * TauCeti.Place.relativeDegree k F P' ≤
    Module.finrank F F'

Lean

Formalized in Tau Ceti as TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_le_finrank.

Sources

• Tau Ceti documentation: TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_le_finrank
• Source of TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_le_finrank in TauCeti/FieldTheory/FunctionField/Place/Extension/Fibre.lean

LeanTauCeti.Place.sum_ramificationIdx_mul_relativeDegree_le_finrank

Uses 1 · Used by 23

Proof usesThe weak approximation theorem

Used byPerfect local Tate duality for E[m] · The Hurwitz genus formula for y² = x³ - x over K(x), as a numerical identity · The Wronskian identity of an isogeny · Isogenous curves over a finite field have the same zeta function Z(W/F, T) = exp (∑_{n ≥ 1} #W(𝔽_{qⁿ}) Tⁿ / n) · The φ-descent sequence is exact at H¹(G_K, E₁[φ]) · The Hasse bound (Silverman V.1.1) · The m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2) · TauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual · The Riemann–Roch theorem with the sheaf of differentials · Belyi's theorem, existence direction · Abhyankar's lemma (Stichtenoth, Theorem 3.9.1) · The genus of a smooth projective plane curve (Fulton, *Algebraic Curves*, Section 8.3) · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · The residue theorem over a perfect field (Stichtenoth, Corollary 4.3.3 and Remark 4.3.7(d)) · The residue theorem (Stichtenoth, Corollary 4.3.3) · Castelnuovo's inequality (Stichtenoth, Theorem 3.11.3) · Clifford's theorem · Dedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · Hilbert's different formula · Kummer's theorem (Stichtenoth, Corollary 3.3.8) · Riemann's inequality (Stichtenoth, Corollary 3.11.4) · The Artin--Schreier genus formula, cross-multiplied for a possible constant-field extension · The Hurwitz bound (Stichtenoth, Exercise 3.18)

TheoremThe Galois correspondence for the inertia field#

the automorphisms of F' fixing the inertia field of P pointwise are exactly the inertia group of P.

TauCeti.Place.fixingSubgroup_inertiaField.{u, v, v'} {k : Type u} (F : Type v) {F' : Type v'}
  [Field k] [Field F] [Field F'] [Algebra k F'] [Algebra F F'] (P : TauCeti.Place k F')
  [FiniteDimensional F F'] :
  (TauCeti.Place.inertiaField F P).fixingSubgroup =
    Subgroup.map (ValuationSubring.decompositionSubgroup F P.integers).subtype
      (ValuationSubring.inertiaSubgroup F P.integers)

Lean

Formalized in Tau Ceti as TauCeti.Place.fixingSubgroup_inertiaField.

Other forms

The Galois correspondence for the decomposition field. Formalized in Tau Ceti as TauCeti.Place.fixingSubgroup_decompositionField.

TauCeti.Place.fixingSubgroup_decompositionField.{u, v, v'} {k : Type u} (F : Type v) {F' : Type v'}
  [Field k] [Field F] [Field F'] [Algebra k F'] [Algebra F F'] [FiniteDimensional F F']
  (P : TauCeti.Place k F') :
  (TauCeti.Place.decompositionField F P).fixingSubgroup =
    ValuationSubring.decompositionSubgroup F P.integers

Sources

• Tau Ceti documentation: TauCeti.Place.fixingSubgroup_inertiaField
• Source of TauCeti.Place.fixingSubgroup_inertiaField in TauCeti/FieldTheory/FunctionField/Place/Extension/Inertia.lean

LeanTauCeti.Place.fixingSubgroup_inertiaField · TauCeti.Place.fixingSubgroup_decompositionField

Used by 2

Used byAbhyankar's lemma (Stichtenoth, Theorem 3.9.1) · Hilbert's different formula

TheoremHilbert's different formula#

Hilbert's different formula (Stichtenoth, Theorem 3.8.7), with the sum cut off at an index N from which the ramification groups are trivial: d(P ∣ P ∩ F) = ∑_{i < N} (|G_i(P)| - 1), when the residue extension is separable.

TauCeti.Place.differentExponent_eq_sum_range_card_ramificationGroup_sub_one.{u, v, v'} {k : Type u}
  (F : Type v) {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [IsGalois F F']
  (P : TauCeti.Place k F')
  [Algebra.IsSeparable (TauCeti.Place.restrict k F P).ResidueField P.ResidueField] {N : ℕ}
  (hN : TauCeti.Place.ramificationGroup F P N = ⊥) :
  TauCeti.Place.differentExponent k F P =
    ∑ i ∈ Finset.range N, (Nat.card ↥(TauCeti.Place.ramificationGroup F P i) - 1)

Lean

Formalized in Tau Ceti as TauCeti.Place.differentExponent_eq_sum_range_card_ramificationGroup_sub_one.

Other forms

Hilbert's different formula (Stichtenoth, Theorem 3.8.7). Formalized in Tau Ceti as TauCeti.Place.differentExponent_eq_finsum_card_ramificationGroup_sub_one.

TauCeti.Place.differentExponent_eq_finsum_card_ramificationGroup_sub_one.{u, v, v'} {k : Type u}
  (F : Type v) {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
  [Algebra F F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [IsGalois F F']
  (P : TauCeti.Place k F')
  [Algebra.IsSeparable (TauCeti.Place.restrict k F P).ResidueField P.ResidueField] :
  TauCeti.Place.differentExponent k F P =
    ∑ᶠ (i : ℕ), (Nat.card ↥(TauCeti.Place.ramificationGroup F P i) - 1)

Sources

• Tau Ceti documentation: TauCeti.Place.differentExponent_eq_sum_range_card_ramificationGroup_sub_one
• Source of TauCeti.Place.differentExponent_eq_sum_range_card_ramificationGroup_sub_one in TauCeti/FieldTheory/FunctionField/Different/Hilbert.lean

LeanTauCeti.Place.differentExponent_eq_sum_range_card_ramificationGroup_sub_one · TauCeti.Place.differentExponent_eq_finsum_card_ramificationGroup_sub_one

Uses 7

Proof usesDedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The Galois correspondence for the inertia field · Hilbert's counting identity · The residue action, on residues (Stichtenoth, Theorem 3.8.2) · The weak approximation theorem

TheoremThe Hurwitz bound (Stichtenoth, Exercise 3.18)#

a finite group G of automorphisms of a function field of genus g ≥ 2, every place of which is tame over the fixed field, has order at most 84 (g - 1).

TauCeti.natCard_le_eighty_four_mul_genus_sub_one.{u, v} {k : Type u} {F : Type v} [Field k]
  [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F)
  (G : Subgroup Gal(F/k)) [Finite ↥G] (hgenus : 2 ≤ TauCeti.genus k F)
  (htame :
    ∀ (P : TauCeti.Place k F), TauCeti.Place.IsTame k (↥(IntermediateField.fixedField G)) P) :
  Nat.card ↥G ≤ 84 * (TauCeti.genus k F - 1)

Lean

Formalized in Tau Ceti as TauCeti.natCard_le_eighty_four_mul_genus_sub_one.

Other forms

The Hurwitz bound for a group of order prime to the characteristic (Stichtenoth, Exercise 3.18). Formalized in Tau Ceti as TauCeti.natCard_le_eighty_four_mul_genus_sub_one_of_not_dvd.

TauCeti.natCard_le_eighty_four_mul_genus_sub_one_of_not_dvd.{u, v} {k : Type u} {F : Type v}
  [Field k] [Field F] [Algebra k F] [PerfectField k] (p : ℕ) [CharP k p]
  (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (G : Subgroup Gal(F/k))
  [Finite ↥G] (hgenus : 2 ≤ TauCeti.genus k F) (hp : ¬p ∣ Nat.card ↥G) :
  Nat.card ↥G ≤ 84 * (TauCeti.genus k F - 1)

The Hurwitz bound for the whole automorphism group. Formalized in Tau Ceti as TauCeti.card_algEquiv_le_eighty_four_mul_genus_sub_one_of_charZero.

TauCeti.card_algEquiv_le_eighty_four_mul_genus_sub_one_of_charZero.{u, v} {k : Type u} {F : Type v}
  [Field k] [Field F] [Algebra k F] [CharZero k] [Finite Gal(F/k)]
  (hF : TauCeti.IsFunctionField k F) (hex : IsIntegrallyClosedIn k F)
  (hgenus : 2 ≤ TauCeti.genus k F) : Nat.card Gal(F/k) ≤ 84 * (TauCeti.genus k F - 1)

The Hurwitz bound in characteristic zero (Stichtenoth, Exercise 3.18). Formalized in Tau Ceti as TauCeti.natCard_le_eighty_four_mul_genus_sub_one_of_charZero.

TauCeti.natCard_le_eighty_four_mul_genus_sub_one_of_charZero.{u, v} {k : Type u} {F : Type v}
  [Field k] [Field F] [Algebra k F] [CharZero k] (hF : TauCeti.IsFunctionField k F)
  (hex : IsIntegrallyClosedIn k F) (G : Subgroup Gal(F/k)) [Finite ↥G]
  (hgenus : 2 ≤ TauCeti.genus k F) : Nat.card ↥G ≤ 84 * (TauCeti.genus k F - 1)

Sources

• Tau Ceti documentation: TauCeti.natCard_le_eighty_four_mul_genus_sub_one
• Source of TauCeti.natCard_le_eighty_four_mul_genus_sub_one in TauCeti/FieldTheory/FunctionField/Automorphism/HurwitzBound.lean

LeanTauCeti.natCard_le_eighty_four_mul_genus_sub_one · TauCeti.natCard_le_eighty_four_mul_genus_sub_one_of_not_dvd · TauCeti.card_algEquiv_le_eighty_four_mul_genus_sub_one_of_charZero · TauCeti.natCard_le_eighty_four_mul_genus_sub_one_of_charZero

Uses 6

Statement usesArtin's theorem

Proof usesDedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) · The weak approximation theorem

DefinitionKummer's theorem (Stichtenoth, Corollary 3.3.8)#

when the height one prime 𝔭 of the model R is prime to the conductor of R[y] in the model S, the places of F' / k' lying over the place of 𝔭 are exactly the normalized irreducible factors of minpoly R y modulo 𝔭.

TauCeti.Place.restrictOfPrimeEquivNormalizedFactors.{u, u', v, v', w, w'} (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'] {R : Type w} [CommRing R] [IsDedekindDomain R] [Algebra R F]
  [IsFractionRing R F] {S : Type w'} [CommRing S] [IsDedekindDomain S] [Algebra S F']
  [IsFractionRing S F'] [Algebra R S] [Algebra R F'] [IsScalarTower R S F'] [IsScalarTower R F F']
  [Algebra.IsIntegral F F'] [Algebra k R] [IsScalarTower k R F] [Algebra k' S]
  [IsScalarTower k' S F'] [Module.Finite R S] (𝔭 : IsDedekindDomain.HeightOneSpectrum R) {y : S}
  (hy : Ideal.comap (algebraMap R S) (conductor R y) ⊔ 𝔭.asIdeal = ⊤) (hy' : IsIntegral R y) :
  { P' // TauCeti.Place.restrict k F P' = TauCeti.Place.ofPrime k F 𝔭 } ≃
    ↑{d |
        d ∈
          UniqueFactorizationMonoid.normalizedFactors
            (Polynomial.map (Ideal.Quotient.mk 𝔭.asIdeal) (minpoly R y))}

Lean

Formalized in Tau Ceti as TauCeti.Place.restrictOfPrimeEquivNormalizedFactors.

Other forms

Kummer's theorem (Stichtenoth, Theorem 3.3.7), packaged. Formalized in Tau Ceti as TauCeti.Place.exists_injective_restrict_eq.

TauCeti.Place.exists_injective_restrict_eq.{u, u', v, v', u_1} {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']
  [FiniteDimensional F F'] [Algebra.IsIntegral k k'] (hF : TauCeti.IsFunctionField k F)
  (P : TauCeti.Place k F) (y : F') {φ : Polynomial ↥P.integers}
  (hmin : Polynomial.map (algebraMap (↥P.integers) F) φ = minpoly F y) {ι : Type u_1}
  {γ : ι → Polynomial P.ResidueField} (hmonic : ∀ (i : ι), (γ i).Monic)
  (hirr : ∀ (i : ι), Irreducible (γ i))
  (hdvd : ∀ (i : ι), γ i ∣ Polynomial.map (IsLocalRing.residue ↥P.integers) φ)
  (hinj : Function.Injective γ) :
  ∃ Q,
    Function.Injective Q ∧
      ∀ (i : ι),
        TauCeti.Place.restrict k F (Q i) = P ∧
          (γ i).natDegree ≤ TauCeti.Place.relativeDegree k F (Q i) ∧
            ∃ g,
              g.Monic ∧
                Polynomial.map (IsLocalRing.residue ↥P.integers) g = γ i ∧
                  (Q i).valuation ((P.integersEval y) g) < 1

Kummer's theorem (Stichtenoth, Theorem 3.3.7), for one irreducible factor. Formalized in Tau Ceti as TauCeti.Place.exists_restrict_eq_of_irreducible_map_residue.

TauCeti.Place.exists_restrict_eq_of_irreducible_map_residue.{u, u', v, v'} {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'] [FiniteDimensional F F'] [Algebra.IsIntegral k k']
  (hF : TauCeti.IsFunctionField k F) (P : TauCeti.Place k F) (y : F') {φ g : Polynomial ↥P.integers}
  (hmin : Polynomial.map (algebraMap (↥P.integers) F) φ = minpoly F y) (hg : g.Monic)
  (hirr : Irreducible (Polynomial.map (IsLocalRing.residue ↥P.integers) g))
  (hdvd :
    Polynomial.map (IsLocalRing.residue ↥P.integers) g ∣
      Polynomial.map (IsLocalRing.residue ↥P.integers) φ) :
  ∃ P',
    TauCeti.Place.restrict k F P' = P ∧
      P'.valuation ((P.integersEval y) g) < 1 ∧
        (Polynomial.map (IsLocalRing.residue ↥P.integers) g).natDegree ≤
          TauCeti.Place.relativeDegree k F P'

Kummer's theorem at a place of separable reduction. Formalized in Tau Ceti as TauCeti.Place.exists_restrict_eq_relativeDegree_eq_and_isSeparable.

TauCeti.Place.exists_restrict_eq_relativeDegree_eq_and_isSeparable.{u, u', v, v'} {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'] [FiniteDimensional F F'] [Algebra.IsIntegral k k']
  (hF : TauCeti.IsFunctionField k F) (P : TauCeti.Place k F) {y : F'} (hy : F⟮y⟯ = ⊤)
  {φ : Polynomial ↥P.integers} (hmin : Polynomial.map (algebraMap (↥P.integers) F) φ = minpoly F y)
  (hsep : (Polynomial.map (IsLocalRing.residue ↥P.integers) φ).Separable)
  {γ : Polynomial P.ResidueField} (hmonic : γ.Monic) (hirr : Irreducible γ)
  (hdvd : γ ∣ Polynomial.map (IsLocalRing.residue ↥P.integers) φ) :
  ∃ P',
    TauCeti.Place.restrict k F P' = P ∧
      TauCeti.Place.relativeDegree k F P' = γ.natDegree ∧
        Algebra.IsSeparable (TauCeti.Place.restrict k F P').ResidueField P'.ResidueField

Kummer's theorem at a rational place of split separable reduction. Formalized in Tau Ceti as TauCeti.Place.exists_finset_card_eq_forall_exists_restrict_eq_valuation_sub_lt_one.

TauCeti.Place.exists_finset_card_eq_forall_exists_restrict_eq_valuation_sub_lt_one.{u, u', v, v'}
  {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'] [FiniteDimensional F F'] [Algebra.IsIntegral k k']
  (hF : TauCeti.IsFunctionField k F) (P : TauCeti.Place k F) (hdeg : P.degree = 1) (y : F')
  {φ : Polynomial ↥P.integers} (hmin : Polynomial.map (algebraMap (↥P.integers) F) φ = minpoly F y)
  (hsep : (Polynomial.map (IsLocalRing.residue ↥P.integers) φ).Separable)
  (hsplit : (Polynomial.map (IsLocalRing.residue ↥P.integers) φ).Splits) :
  ∃ s,
    s.card = φ.natDegree ∧
      ∀ a ∈ s, ∃ P', TauCeti.Place.restrict k F P' = P ∧ P'.valuation (y - (algebraMap k F') a) < 1

Kummer's theorem for a reduction without repeated factors (Stichtenoth, Theorem 3.3.7). Formalized in Tau Ceti as TauCeti.Place.exists_equiv_restrict_eq_of_prod_eq_map_residue.

TauCeti.Place.exists_equiv_restrict_eq_of_prod_eq_map_residue.{u, u', v, v', u_1} {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'] [FiniteDimensional F F'] [Algebra.IsIntegral k k']
  (hF : TauCeti.IsFunctionField k F) (P : TauCeti.Place k F) {y : F'} (hy : F⟮y⟯ = ⊤)
  {φ : Polynomial ↥P.integers} (hmin : Polynomial.map (algebraMap (↥P.integers) F) φ = minpoly F y)
  {ι : Type u_1} [Fintype ι] {γ : ι → Polynomial P.ResidueField} (hmonic : ∀ (i : ι), (γ i).Monic)
  (hirr : ∀ (i : ι), Irreducible (γ i)) (hinj : Function.Injective γ)
  (hprod : ∏ i, γ i = Polynomial.map (IsLocalRing.residue ↥P.integers) φ) :
  ∃ e, ∀ (i : ι), TauCeti.Place.relativeDegree k F ↑(e i) = (γ i).natDegree

Kummer's theorem under monogenicity (Stichtenoth, Corollary 3.3.8). Formalized in Tau Ceti as TauCeti.Place.restrictEquivNormalizedFactors.

TauCeti.Place.restrictEquivNormalizedFactors.{u, u', v, v'} (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'] (P : TauCeti.Place k F) {y : F'} [Algebra k F']
  [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral k k'] [FiniteDimensional F F']
  {φ : Polynomial ↥P.integers} (hmin : Polynomial.map (algebraMap (↥P.integers) F) φ = minpoly F y)
  (hy : (↥P.integers)[y] = integralClosure (↥P.integers) F') :
  { P' // TauCeti.Place.restrict k F P' = P } ≃
    { γ //
      γ ∈
        UniqueFactorizationMonoid.normalizedFactors
          (Polynomial.map (IsLocalRing.residue ↥P.integers) φ) }

Sources

• Tau Ceti documentation: TauCeti.Place.restrictOfPrimeEquivNormalizedFactors
• Source of TauCeti.Place.restrictOfPrimeEquivNormalizedFactors in TauCeti/FieldTheory/FunctionField/AffineModel/Kummer.lean

LeanTauCeti.Place.restrictOfPrimeEquivNormalizedFactors · TauCeti.Place.exists_injective_restrict_eq · TauCeti.Place.exists_restrict_eq_of_irreducible_map_residue · TauCeti.Place.exists_restrict_eq_relativeDegree_eq_and_isSeparable · TauCeti.Place.exists_finset_card_eq_forall_exists_restrict_eq_valuation_sub_lt_one · TauCeti.Place.exists_equiv_restrict_eq_of_prod_eq_map_residue · TauCeti.Place.restrictEquivNormalizedFactors

Uses 4 · Used by 1

Proof usesThe fundamental inequality (Stichtenoth, Theorem 3.1.11) · Krull–Akizuki for Mathlib's integralClosure · Kummer's theorem sees one factor per place · The relative degree bound of Kummer's theorem (Stichtenoth, Theorem 3.3.7)

Used byCastelnuovo's inequality (Stichtenoth, Theorem 3.11.3)

TheoremKummer's theorem sees one factor per place#

a place P' over P at which two monic polynomials with irreducible reductions both vanish reduces them to the same irreducible polynomial, namely the minimal polynomial of the residue of y. This is what makes the places attached to distinct irreducible factors of the reduction of φ distinct (Stichtenoth, Theorem 3.3.7).

TauCeti.Place.map_residue_eq_of_valuation_lt_one.{u, u', v, v'} {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']
  [FiniteDimensional F F'] {P : TauCeti.Place k F} {P' : TauCeti.Place k' F'}
  (hres : TauCeti.Place.restrict k F P' = P) {y : F'} (hy : y ∈ P'.integers)
  {g₁ g₂ : Polynomial ↥P.integers} (hg₁ : g₁.Monic)
  (hirr₁ : Irreducible (Polynomial.map (IsLocalRing.residue ↥P.integers) g₁))
  (hv₁ : P'.valuation ((P.integersEval y) g₁) < 1) (hg₂ : g₂.Monic)
  (hirr₂ : Irreducible (Polynomial.map (IsLocalRing.residue ↥P.integers) g₂))
  (hv₂ : P'.valuation ((P.integersEval y) g₂) < 1) :
  Polynomial.map (IsLocalRing.residue ↥P.integers) g₁ =
    Polynomial.map (IsLocalRing.residue ↥P.integers) g₂

Lean

Formalized in Tau Ceti as TauCeti.Place.map_residue_eq_of_valuation_lt_one.

Sources

• Tau Ceti documentation: TauCeti.Place.map_residue_eq_of_valuation_lt_one
• Source of TauCeti.Place.map_residue_eq_of_valuation_lt_one in TauCeti/FieldTheory/FunctionField/Place/Extension/Kummer.lean

LeanTauCeti.Place.map_residue_eq_of_valuation_lt_one

Used by 1

Used byKummer's theorem (Stichtenoth, Corollary 3.3.8)

TheoremThe relative degree bound of Kummer's theorem (Stichtenoth, Theorem 3.3.7)#

a place P' over P at which a monic g with irreducible reduction γ vanishes has relative degree at least deg γ, because γ is the minimal polynomial of the residue of y at P'.

TauCeti.Place.natDegree_map_residue_le_relativeDegree.{u, u', v, v'} {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']
  [FiniteDimensional F F'] {P : TauCeti.Place k F} {P' : TauCeti.Place k' F'}
  (hres : TauCeti.Place.restrict k F P' = P) {y : F'} (hy : y ∈ P'.integers)
  {g : Polynomial ↥P.integers} (hg : g.Monic)
  (hirr : Irreducible (Polynomial.map (IsLocalRing.residue ↥P.integers) g))
  (hv : P'.valuation ((P.integersEval y) g) < 1) :
  (Polynomial.map (IsLocalRing.residue ↥P.integers) g).natDegree ≤
    TauCeti.Place.relativeDegree k F P'

Lean

Formalized in Tau Ceti as TauCeti.Place.natDegree_map_residue_le_relativeDegree.

Sources

• Tau Ceti documentation: TauCeti.Place.natDegree_map_residue_le_relativeDegree
• Source of TauCeti.Place.natDegree_map_residue_le_relativeDegree in TauCeti/FieldTheory/FunctionField/Place/Extension/Kummer.lean

LeanTauCeti.Place.natDegree_map_residue_le_relativeDegree

Used by 1

Used byKummer's theorem (Stichtenoth, Corollary 3.3.8)

TheoremThe residue action, on residues (Stichtenoth, Theorem 3.8.2)#

the automorphism of F'_P induced by g sends the residue of an element x of 𝒪_P to the residue of g x.

TauCeti.Place.residueAut_residue.{u, v, v'} {k : Type u} (F : Type v) {F' : Type v'} [Field k]
  [Field F] [Field F'] [Algebra k F'] [Algebra F F'] (P : TauCeti.Place k F') [Algebra k F]
  [IsScalarTower k F F'] [Algebra.IsIntegral F F']
  (g : ↥(ValuationSubring.decompositionSubgroup F P.integers)) (x : ↥P.integers) :
  ((TauCeti.Place.residueAut F P) g) ((IsLocalRing.residue ↥P.integers) x) =
    (IsLocalRing.residue ↥P.integers) (g • x)

Lean

Formalized in Tau Ceti as TauCeti.Place.residueAut_residue.

Sources

• Tau Ceti documentation: TauCeti.Place.residueAut_residue
• Source of TauCeti.Place.residueAut_residue in TauCeti/FieldTheory/FunctionField/Place/Extension/Inertia.lean

LeanTauCeti.Place.residueAut_residue

Used by 2

Used byAbhyankar's lemma (Stichtenoth, Theorem 3.9.1) · Hilbert's different formula

TheoremThe residue theorem for k(x) (Stichtenoth, Corollary 4.3.3, for k(x))#

if every pole of z is a rational place, then the residues of z dx over ℙ¹(k) sum to zero, in the form ∑_{a ∈ k} res_{P_a, x - a} (z) = res_{P_∞, x⁻¹} (x² z).

The hypothesis is needed: over ℚ, z = 2x / (x² - 2) is integral at every place P_a, so the left side vanishes, while res_{P_∞, x⁻¹} (x² z) = 2; the missing residue sits at the place of x² - 2, which has degree two.

TauCeti.finsum_residue_adicOfIrreducible_X_sub_C.{u_1} {k : Type u_1} [Field k] {z : RatFunc k}
  (hz : ∀ (P : TauCeti.Place k (RatFunc k)), P.degree ≠ 1 → z ∈ P.integers) :
  ∑ᶠ (a : k), ((TauCeti.Place.adicOfIrreducible ⋯).residue ⋯ ⋯) z =
    ((TauCeti.Place.infty k).residue ⋯ ⋯) (RatFunc.X ^ 2 * z)

Lean

Formalized in Tau Ceti as TauCeti.finsum_residue_adicOfIrreducible_X_sub_C.

Sources

• Tau Ceti documentation: TauCeti.finsum_residue_adicOfIrreducible_X_sub_C
• Source of TauCeti.finsum_residue_adicOfIrreducible_X_sub_C in TauCeti/FieldTheory/FunctionField/Differential/RatFunc/Residue.lean

LeanTauCeti.finsum_residue_adicOfIrreducible_X_sub_C

Uses 4 · Used by 1

Proof usesThe abstract residue theorem (Stichtenoth, (1.45)) · Riemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · The weak approximation theorem

Used byThe residue theorem for k(x) over an algebraically closed field (Stichtenoth, Corollary 4.3.3, for k(x))

TheoremThe residue theorem for k(x) over an algebraically closed field (Stichtenoth, Corollary 4.3.3, for k(x))#

∑_{a ∈ k} res_{P_a, x - a} (z) = res_{P_∞, x⁻¹} (x² z) for every rational function z.

TauCeti.finsum_residue_adicOfIrreducible_X_sub_C_of_isAlgClosed.{u_1} {k : Type u_1} [Field k]
  [IsAlgClosed k] (z : RatFunc k) :
  ∑ᶠ (a : k), ((TauCeti.Place.adicOfIrreducible ⋯).residue ⋯ ⋯) z =
    ((TauCeti.Place.infty k).residue ⋯ ⋯) (RatFunc.X ^ 2 * z)

Lean

Formalized in Tau Ceti as TauCeti.finsum_residue_adicOfIrreducible_X_sub_C_of_isAlgClosed.

Sources

• Tau Ceti documentation: TauCeti.finsum_residue_adicOfIrreducible_X_sub_C_of_isAlgClosed
• Source of TauCeti.finsum_residue_adicOfIrreducible_X_sub_C_of_isAlgClosed in TauCeti/FieldTheory/FunctionField/Differential/RatFunc/Residue.lean

LeanTauCeti.finsum_residue_adicOfIrreducible_X_sub_C_of_isAlgClosed

Uses 1

Proof usesThe residue theorem for k(x) (Stichtenoth, Corollary 4.3.3, for k(x))

TheoremRiemann's inequality (Stichtenoth, Corollary 3.11.4)#

if F / k has exact constants and is generated by two transcendental elements x and y, then g ≤ ([F : k(x)] - 1) ([F : k(y)] - 1).

The powers 1, y, …, y^{m - 1}, m = [F : k(x)], are a basis of F / k(x) in L((m - 1) (y)_∞), so this is the case F₀ = k(x) of TauCeti.genus_le_one_add_finrank_mul_genus_sub_one_add_degree.

TauCeti.genus_le_finrank_sub_one_mul_finrank_sub_one.{u_1, u_3} {k : Type u_1} {F : Type u_3}
  [Field k] [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F)
  (hex : IsIntegrallyClosedIn k F) {x y : F} (hx : Transcendental k x) (hy : Transcendental k y)
  (hxy : k⟮x, y⟯ = ⊤) :
  TauCeti.genus k F ≤ (Module.finrank (↥k⟮x⟯) F - 1) * (Module.finrank (↥k⟮y⟯) F - 1)

Lean

Formalized in Tau Ceti as TauCeti.genus_le_finrank_sub_one_mul_finrank_sub_one.

Sources

• Tau Ceti documentation: TauCeti.genus_le_finrank_sub_one_mul_finrank_sub_one
• Source of TauCeti.genus_le_finrank_sub_one_mul_finrank_sub_one in TauCeti/FieldTheory/FunctionField/Consequences/RiemannInequality.lean

LeanTauCeti.genus_le_finrank_sub_one_mul_finrank_sub_one

Uses 5

Proof usesThe fundamental identity · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · Riemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · The weak approximation theorem

TheoremStichtenoth's transformation formula#

Stichtenoth's transformation formula res_{P,s}(z) = res_{P,t}(z · ds/dt) at a place with separable residue field, for two uniformizers s and t with t separating, the residues taking values in F_P (Proposition 4.2.9).

TauCeti.Place.residueResidueField_eq_residueResidueField_mul_derivativeOfSeparating.{u_1, u_2}
  {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : TauCeti.Place k F) {s t : F}
  (ht : P.ord t = 1) [Algebra.IsSeparable k P.ResidueField] (htr : Transcendental k t)
  [Algebra.IsSeparable (↥k⟮t⟯) F] (hs : P.ord s = 1) (z : F) :
  (P.residueResidueField hs) z =
    (P.residueResidueField ht) (z * (TauCeti.derivativeOfSeparating htr) s)

Lean

Formalized in Tau Ceti as TauCeti.Place.residueResidueField_eq_residueResidueField_mul_derivativeOfSeparating.

Other forms

Stichtenoth's transformation formula res_{P,s}(z) = res_{P,t}(z · ds/dt). Formalized in Tau Ceti as TauCeti.Place.residue_eq_residue_mul.

TauCeti.Place.residue_eq_residue_mul.{u_1, u_2} {k : Type u_1} {F : Type u_2} [Field k] [Field F]
  [Algebra k F] (P : TauCeti.Place k F) {s t : F} (hP : P.degree = 1) (ht : P.ord t = 1)
  (hs : P.ord s = 1) {w : F}
  (hw :
    (P.laurentSeriesExpansion hP ht) w =
      (LaurentSeries.derivative k) ((P.laurentSeriesExpansion hP ht) s))
  (z : F) : (P.residue hP hs) z = (P.residue hP ht) (z * w)

Stichtenoth's transformation formula. Formalized in Tau Ceti as TauCeti.Place.residue_eq_residue_mul_derivativeOfSeparating.

TauCeti.Place.residue_eq_residue_mul_derivativeOfSeparating.{u_1, u_2} {k : Type u_1} {F : Type u_2}
  [Field k] [Field F] [Algebra k F] (P : TauCeti.Place k F) {s t : F} (hP : P.degree = 1)
  (ht : P.ord t = 1) (htr : Transcendental k t) [Algebra.IsSeparable (↥k⟮t⟯) F] (hs : P.ord s = 1)
  (z : F) : (P.residue hP hs) z = (P.residue hP ht) (z * (TauCeti.derivativeOfSeparating htr) s)

Sources

• Tau Ceti documentation: TauCeti.Place.residueResidueField_eq_residueResidueField_mul_derivativeOfSeparating
• Source of TauCeti.Place.residueResidueField_eq_residueResidueField_mul_derivativeOfSeparating in TauCeti/FieldTheory/FunctionField/Place/Expansion/Laurent/Derivative.lean

LeanTauCeti.Place.residueResidueField_eq_residueResidueField_mul_derivativeOfSeparating · TauCeti.Place.residue_eq_residue_mul · TauCeti.Place.residue_eq_residue_mul_derivativeOfSeparating

Used by 4

Used byTauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual · The Riemann–Roch theorem with the sheaf of differentials · The residue theorem over a perfect field (Stichtenoth, Corollary 4.3.3 and Remark 4.3.7(d)) · The residue theorem (Stichtenoth, Corollary 4.3.3)

TheoremStrong approximation (Stichtenoth, Theorem 1.6.5)#

for a set S of places of F / k that is not all of them and a finite subset s ⊆ S, some x : F satisfies ord_P (x - f P) = r P at every P ∈ s and is regular at every place of S outside s.

The orders on s are prescribed exactly, as in weak approximation (TauCeti.Place.exists_forall_mem_ord_sub_eq); what strong approximation adds is the regularity of x at the remaining places of S, at the price of requiring S to be proper.

TauCeti.Place.exists_forall_mem_ord_sub_eq_and_forall_mem_integers.{u_1, u_2} {k : Type u_1}
  {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F)
  (hex : IsIntegrallyClosedIn k F) {S : Set (TauCeti.Place k F)} (hS : S ≠ Set.univ)
  {s : Finset (TauCeti.Place k F)} (hsS : ↑s ⊆ S) (f : TauCeti.Place k F → F)
  (r : TauCeti.Place k F → ℤ) :
  ∃ x, (∀ P ∈ s, P.ord (x - f P) = r P) ∧ ∀ P ∈ S, P ∉ s → x ∈ P.integers

Lean

Formalized in Tau Ceti as TauCeti.Place.exists_forall_mem_ord_sub_eq_and_forall_mem_integers.

Other forms

Strong approximation, in the inequality form (Stichtenoth, Theorem 1.6.5). Formalized in Tau Ceti as TauCeti.Place.exists_forall_mem_valuation_sub_le_and_forall_mem_integers.

TauCeti.Place.exists_forall_mem_valuation_sub_le_and_forall_mem_integers.{u_1, u_2} {k : Type u_1}
  {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : TauCeti.IsFunctionField k F)
  (hex : IsIntegrallyClosedIn k F) {S : Set (TauCeti.Place k F)} (hS : S ≠ Set.univ)
  {s : Finset (TauCeti.Place k F)} (hsS : ↑s ⊆ S) (f : TauCeti.Place k F → F)
  (r : TauCeti.Place k F → ℤ) :
  ∃ x, (∀ P ∈ s, P.valuation (x - f P) ≤ WithZero.exp (-r P)) ∧ ∀ P ∈ S, P ∉ s → x ∈ P.integers

Sources

• Tau Ceti documentation: TauCeti.Place.exists_forall_mem_ord_sub_eq_and_forall_mem_integers
• Source of TauCeti.Place.exists_forall_mem_ord_sub_eq_and_forall_mem_integers in TauCeti/FieldTheory/FunctionField/Consequences/StrongApproximation.lean

LeanTauCeti.Place.exists_forall_mem_ord_sub_eq_and_forall_mem_integers · TauCeti.Place.exists_forall_mem_valuation_sub_le_and_forall_mem_integers

Uses 2

Proof usesRiemann's theorem · The weak approximation theorem

TheoremThe tame different theorem fails at infinity#

the different exponent d is at least the ramification index e, so e ≠ d + 1, unlike at every tame place.

TauCeti.ArtinSchreierMonomial.ramificationIdx_le_differentExponent_of_restrict_eq_infty.{u_1}
  {k : Type u_1} [Field k] {p m : ℕ} [Fact (Nat.Prime p)] [CharP k p] [hm : Fact ¬p ∣ m]
  {P : TauCeti.Place k (TauCeti.ArtinSchreierMonomial.FunctionField k p m)}
  (hP : TauCeti.Place.restrict k (RatFunc k) P = TauCeti.Place.infty k) :
  TauCeti.Place.ramificationIdx (RatFunc k) P ≤ TauCeti.Place.differentExponent k (RatFunc k) P

Lean

Formalized in Tau Ceti as TauCeti.ArtinSchreierMonomial.ramificationIdx_le_differentExponent_of_restrict_eq_infty.

Sources

• Tau Ceti documentation: TauCeti.ArtinSchreierMonomial.ramificationIdx_le_differentExponent_of_restrict_eq_infty
• Source of TauCeti.ArtinSchreierMonomial.ramificationIdx_le_differentExponent_of_restrict_eq_infty in TauCeti/FieldTheory/FunctionField/ArtinSchreier/Monomial.lean

LeanTauCeti.ArtinSchreierMonomial.ramificationIdx_le_differentExponent_of_restrict_eq_infty

Uses 1

Proof usesDedekind's different theorem, the tame case, as an exponent

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.