Documentation

TauCeti.FieldTheory.FunctionField.AffineModel.Kummer

Kummer's theorem at an affine model: the places over a place, exactly #

Let F' / k' be a finite extension of an extension of fields F / k, let R be an affine model of F / k and let S be a module-finite affine model of F' / k' over R, as in TauCeti/FieldTheory/FunctionField/AffineModel/Extension.lean. Let y : S and let 𝔭 be a height one prime of R prime to the conductor of R[y] in S β€” Stichtenoth's monogenicity hypothesis π’ͺ'_P = π’ͺ_P[y], in the form that only asks for it after localizing at 𝔭. Then the factorization

Ο† ≑ ∏ᡒ Ξ³α΅’ ^ Ξ΅α΅’ (mod 𝔭), Ο† the minimal polynomial of y over R,

determines the places of F' / k' over the place of 𝔭 completely: they are in bijection with the monic irreducible factors Ξ³α΅’, and the place attached to Ξ³α΅’ has relative degree deg Ξ³α΅’ and ramification index Ξ΅α΅’. This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Corollary 3.3.8 β€” the conclusion that TauCeti/FieldTheory/FunctionField/Place/Extension/Kummer.lean deliberately does not draw: its Theorem 3.3.7 bounds the splitting of a place without the monogenicity hypothesis, and neither computes the ramification indices nor rules out further places over P.

The proof is the affine-model dictionary of TauCeti/FieldTheory/FunctionField/AffineModel/Extension.lean β€” the places over the place of 𝔭 are the primes of S over 𝔭, with e the ramification index and f the residue degree of the centre β€” composed with the Kummer–Dedekind criterion of TauCeti/RingTheory/DedekindDomain/KummerDedekind.lean. Nothing about function fields enters beyond that dictionary; in particular no hypothesis on k, k' or the constant fields is needed.

The polynomial being factored is Stichtenoth's Ο†: R is integrally closed with fraction field F, so minpoly R y maps to minpoly F y under R β†’ F, by Mathlib's minpoly.isIntegrallyClosed_eq_field_fractions. The conductor hypothesis holds at every prime as soon as S = R[y], since then the conductor is the unit ideal by Mathlib's conductor_eq_top_of_adjoin_eq_top.

The places of F' / k' outside the finite chart of S are reached, as always, by running the same statement at a second model, exactly as for the fundamental identity.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.Place.restrictOfPrimeEquivNormalizedFactors (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' : Place k' F' // restrict k F P' = ofPrime k F 𝔭 } ≃ ↑{d : Polynomial (R β§Έ 𝔭.asIdeal) | d ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk 𝔭.asIdeal) (minpoly R y))}

Kummer'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 𝔭.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.Place.restrictOfPrimeEquivNormalizedFactors_symm_apply_coe_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] [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) {Q : Polynomial R} (hQ : Polynomial.map (Ideal.Quotient.mk 𝔭.asIdeal) Q ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk 𝔭.asIdeal) (minpoly R y))) (𝔓 : IsDedekindDomain.HeightOneSpectrum S) (h𝔓 : 𝔓.asIdeal = Ideal.span (↑(Ideal.map (algebraMap R S) 𝔭.asIdeal) βˆͺ {(Polynomial.aeval y) Q})) :
    ↑((restrictOfPrimeEquivNormalizedFactors k F 𝔭 hy hy').symm ⟨Polynomial.map (Ideal.Quotient.mk 𝔭.asIdeal) Q, hQ⟩) = ofPrime k' F' 𝔓

    The place attached to a Kummer factor, explicitly: for Q a lift of a normalized irreducible factor of minpoly R y modulo 𝔭, the place of F' / k' attached to that factor is the place of the prime of S spanned by 𝔭 S together with Q (y).

    source
    theorem TauCeti.Place.valuation_restrictOfPrimeEquivNormalizedFactors_symm_apply_lt_one (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) {Q : Polynomial R} (hQ : Polynomial.map (Ideal.Quotient.mk 𝔭.asIdeal) Q ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk 𝔭.asIdeal) (minpoly R y))) :
    (↑((restrictOfPrimeEquivNormalizedFactors k F 𝔭 hy hy').symm ⟨Polynomial.map (Ideal.Quotient.mk 𝔭.asIdeal) Q, hQ⟩)).valuation ((algebraMap S F') ((Polynomial.aeval y) Q)) < 1

    The place attached to a Kummer factor is the one where that factor vanishes: for Q a lift of a normalized irreducible factor of minpoly R y modulo 𝔭, the place of F' / k' attached to that factor has a zero at Q (y). Since distinct factors give distinct places, this identifies the bijection concretely.

    source
    theorem TauCeti.Place.relativeDegree_restrictOfPrimeEquivNormalizedFactors_symm_apply (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) {d : Polynomial (R β§Έ 𝔭.asIdeal)} (hd : d ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk 𝔭.asIdeal) (minpoly R y))) :
    relativeDegree k F ↑((restrictOfPrimeEquivNormalizedFactors k F 𝔭 hy hy').symm ⟨d, hd⟩) = d.natDegree

    The relative degree of a Kummer factor is its degree (Stichtenoth, Corollary 3.3.8): the place of F' / k' over the place of 𝔭 attached to a normalized irreducible factor d of minpoly R y modulo 𝔭 has relative degree d.natDegree.

    source
    theorem TauCeti.Place.ramificationIdx_restrictOfPrimeEquivNormalizedFactors_symm_apply (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) {d : Polynomial (R β§Έ 𝔭.asIdeal)} (hd : d ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk 𝔭.asIdeal) (minpoly R y))) :
    ramificationIdx F ↑((restrictOfPrimeEquivNormalizedFactors k F 𝔭 hy hy').symm ⟨d, hd⟩) = multiplicity d (Polynomial.map (Ideal.Quotient.mk 𝔭.asIdeal) (minpoly R y))

    The ramification index of a Kummer factor is its multiplicity (Stichtenoth, Corollary 3.3.8): the place of F' / k' over the place of 𝔭 attached to a normalized irreducible factor d of minpoly R y modulo 𝔭 has ramification index the multiplicity of d in minpoly R y modulo 𝔭.