Affine models of an extension: the fundamental identity

Let F' / k' be a finite extension of the field extension F / k, let R be an affine model of F / k and let S be an affine model of F' / k' that is an R-algebra: a pair of charts of the two curves, compatible with the covering map. This file identifies the extension-theoretic data of a place of F' / k' finite on S with Mathlib's ideal-theoretic data of its centre, and deduces the fundamental identity ∑_{P' ∣ P} e(P' ∣ P) · f(P' ∣ P) = [F' : F] at every place of the finite chart, supplying the inequality of TauCeti/FieldTheory/FunctionField/Place/Extension/Fibre.lean with its converse.

The dictionary is exact at each of the three items. The centre on S of a place of F' / k' lies over the centre on R of the place of F / k it restricts to; the ramification index e(P' ∣ P), defined as the factor by which the order function scales, is Ideal.ramificationIdx, because Mathlib's IsDedekindDomain.HeightOneSpectrum.valuation_liesOver scales the adic valuations by exactly that factor; and the relative degree f(P' ∣ P) = [F'_{P'} : F_P] is Ideal.inertiaDeg, because the residue field of a place finite on a model is the model modulo the centre, compatibly on both levels. Summing over the fibre is then Mathlib's Ideal.sum_ramification_inertia_eq_finrank for the finite extension of Dedekind domains S / R, transported to the fraction fields.

The identity is stated at the place of a height one prime of R; the places outside the finite chart of R are reached by the same statement at a second model, as in Stichtenoth's two-chart device.

Main definitions

• TauCeti.Place.restrictOfPrimeEquivPrimesOver: the places of F' / k' lying over the place of a height one prime 𝔭 of R are exactly the primes of S lying over 𝔭.

Main results

• TauCeti.Place.center_liesOver: the centre on S of a place of F' / k' finite on S lies over the centre on R of its restriction to F.
• TauCeti.Place.ramificationIdx_eq_ramificationIdx_center and TauCeti.Place.relativeDegree_eq_inertiaDeg_center: the two bridge lemmas e(P' ∣ P) = Ideal.ramificationIdx and f(P' ∣ P) = Ideal.inertiaDeg, with TauCeti.Place.ramificationIdx_ofPrime and TauCeti.Place.relativeDegree_ofPrime their forms at the place of a height one prime of S.
• TauCeti.Place.restrict_ofPrime: the place of a prime 𝔓 of S lies over the place of a prime 𝔭 of R as soon as 𝔓 lies over 𝔭.
• TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_finrank: the fundamental identity (Stichtenoth, Theorem 3.1.11) at a place of the finite chart.

References

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

theorem TauCeti.Place.algebraMap_mem_integers_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'] {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'] (P' : Place k' F') (hS : ∀ (s : S), (algebraMap S F') s ∈ P'.integers) (r : R) : (algebraMap R F) r ∈ (restrict k F P').integers

The restriction of a place finite on S is finite on R: an element of R, viewed in F', may equally be read along R → S.

theorem TauCeti.Place.center_liesOver (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'] (P' : Place k' F') (hS : ∀ (s : S), (algebraMap S F') s ∈ P'.integers) [IsFractionRing R F] [IsFractionRing S F'] : (P'.center hS).asIdeal.LiesOver ((restrict k F P').center ⋯).asIdeal

The centre on S of a place of F' / k' finite on S lies over the centre on R of its restriction to F (Stichtenoth, Proposition 3.1.4 at the level of the models): a function of R vanishes at the restriction exactly when its image in S vanishes at the place.

theorem TauCeti.Place.ramificationIdx_eq_ramificationIdx_center (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'] (P' : Place k' F') (hS : ∀ (s : S), (algebraMap S F') s ∈ P'.integers) [IsFractionRing R F] [IsFractionRing S F'] [IsDedekindDomain R] [IsDedekindDomain S] : ramificationIdx F P' = (P'.center hS).asIdeal.ramificationIdx R

The ramification index of a place over its restriction is the ramification index of the centres (Stichtenoth, Definition 3.1.5): both measure how the adic valuation of the centre on S scales the adic valuation of the centre on R. The base field k does not appear in the statement — TauCeti.Place.ramificationIdx does not depend on it — but it is what names the place of F / k that P' lies over.

theorem TauCeti.Place.relativeDegree_eq_inertiaDeg_center (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'] (P' : Place k' F') (hS : ∀ (s : S), (algebraMap S F') s ∈ P'.integers) [IsFractionRing R F] [IsFractionRing S F'] [IsDedekindDomain R] [IsDedekindDomain S] [Algebra k R] [IsScalarTower k R F] [Algebra k' S] [IsScalarTower k' S F'] : relativeDegree k F P' = (P'.center hS).asIdeal.inertiaDeg R

The relative degree of a place over its restriction is the residue degree of the centres (Stichtenoth, Definition 3.1.5): the residue field of a place finite on a model is the model modulo the centre of the place, and the two identifications are compatible with R → S.

theorem TauCeti.Place.algebraMap_mem_integers_of_restrict_eq_ofPrime (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] [IsFractionRing R F] [Algebra k R] [IsScalarTower k R F] (𝔭 : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite R S] {P' : Place k' F'} (h : restrict k F P' = ofPrime k F 𝔭) (s : S) : (algebraMap S F') s ∈ P'.integers

A place of F' / k' lying over the place of a height one prime of R is finite on S: it is finite on R, and S is integral over R.

theorem TauCeti.Place.ramificationIdx_ofPrime (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'] (𝔓 : IsDedekindDomain.HeightOneSpectrum S) : ramificationIdx F (ofPrime k' F' 𝔓) = 𝔓.asIdeal.ramificationIdx R

The ramification index over F of the place of a height one prime 𝔓 of S is the ramification index of 𝔓 over R.

theorem TauCeti.Place.restrict_ofPrime (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) (𝔓 : IsDedekindDomain.HeightOneSpectrum S) [𝔓.asIdeal.LiesOver 𝔭.asIdeal] : restrict k F (ofPrime k' F' 𝔓) = ofPrime k F 𝔭

A place of F' / k' lies over the place of a height one prime of R as soon as the corresponding prime of S lies over it.

theorem TauCeti.Place.relativeDegree_ofPrime (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 S) : relativeDegree k F (ofPrime k' F' 𝔓) = 𝔓.asIdeal.inertiaDeg R

The relative degree over F of the place of a height one prime 𝔓 of S is the residue degree of 𝔓 over R.

noncomputable def TauCeti.Place.restrictOfPrimeEquivPrimesOver (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] : { P' : Place k' F' // restrict k F P' = ofPrime k F 𝔭 } ≃ ↑(𝔭.asIdeal.primesOver S)

The places of F' / k' lying over the place of a height one prime 𝔭 of R are exactly the primes of S lying over 𝔭 (Stichtenoth, Section III.2): a place over the place of 𝔭 is finite on S, and its centre is a prime over 𝔭.

Equations

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

@[simp]

theorem TauCeti.Place.restrictOfPrimeEquivPrimesOver_apply_coe (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] (P' : { P' : Place k' F' // restrict k F P' = ofPrime k F 𝔭 }) : ↑((restrictOfPrimeEquivPrimesOver k F 𝔭) P') = ((↑P').center ⋯).asIdeal

@[simp]

theorem TauCeti.Place.restrictOfPrimeEquivPrimesOver_symm_apply_coe (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] (𝔓 : IsDedekindDomain.HeightOneSpectrum S) (h𝔓 : 𝔓.asIdeal ∈ 𝔭.asIdeal.primesOver S) : ↑((restrictOfPrimeEquivPrimesOver k F 𝔭).symm ⟨𝔓.asIdeal, h𝔓⟩) = ofPrime k' F' 𝔓

theorem TauCeti.Place.sum_ramificationIdx_mul_relativeDegree_eq_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'] {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 (Place k' F')} (hs : ∀ (P' : Place k' F'), P' ∈ s ↔ restrict k F P' = ofPrime k F 𝔭) : ∑ P' ∈ s, ramificationIdx F P' * relativeDegree k F P' = Module.finrank F F'

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.