Number fields, ramification, Frobenius, and the LMFDB invariants

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremDedekind's theorem, with the fixed points counted separately#

The multiset of degrees of the monic irreducible factors of minpoly ℤ θ modulo p is the cycle type of a Frobenius at a prime above p acting on the roots of minpoly ℚ θ, together with one part 1 for each fixed root. This is the form with the cycle type and the fixed points separated; the full cycle type of fullCycleType_galActionHom_restrict_minpoly_eq_map_natDegree_monicFactorsMod packages the two summands.

TauCeti.NumberField.factorizationType_eq_cycleType_isArithFrobAt.{u_1, u_2} {M : Type u_1} [Field M]
  [NumberField M] {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_2} [Field K] [NumberField K]
  {θ : NumberField.RingOfIntegers K}
  (hsq : Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))
  [Fact (Polynomial.map (algebraMap ℚ M) (minpoly ℚ ↑θ)).Splits]
  (Q : Ideal (NumberField.RingOfIntegers M)) [Q.IsPrime] [Q.LiesOver (Ideal.span {↑p})]
  {σ : Gal(M/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) :
  Multiset.map Polynomial.natDegree (RingOfIntegers.monicFactorsMod θ p).val =
    ((Polynomial.Gal.galActionHom (minpoly ℚ ↑θ) M)
          ((Polynomial.Gal.restrict (minpoly ℚ ↑θ) M) σ)).cycleType +
      Multiset.replicate
        (Nat.card
          ↑(Function.fixedPoints
              ⇑((Polynomial.Gal.galActionHom (minpoly ℚ ↑θ) M)
                  ((Polynomial.Gal.restrict (minpoly ℚ ↑θ) M) σ))))
        1
Lean

Formalized in Tau Ceti as TauCeti.NumberField.factorizationType_eq_cycleType_isArithFrobAt.

Other forms

Dedekind's theorem. Formalized in Tau Ceti as TauCeti.NumberField.fullCycleType_galActionHom_restrict_eq_factorDegrees.

TauCeti.NumberField.fullCycleType_galActionHom_restrict_eq_factorDegrees.{u_1} {M : Type u_1}
  [Field M] [NumberField M] {f : Polynomial ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hf : f.Monic)
  (hsq : Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) f))
  [Fact (Polynomial.map (algebraMap ℚ M) (Polynomial.map (Int.castRingHom ℚ) f)).Splits]
  (Q : Ideal (NumberField.RingOfIntegers M)) [Q.IsPrime] [Q.LiesOver (Ideal.span {↑p})]
  {σ : Gal(M/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) :
  ((Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) M)
        ((Polynomial.Gal.restrict (Polynomial.map (Int.castRingHom ℚ) f) M) σ)).fullCycleType =
    f.factorDegrees p

Dedekind's theorem for a generator. Formalized in Tau Ceti as TauCeti.NumberField.fullCycleType_galActionHom_restrict_minpoly_eq_map_natDegree_monicFactorsMod.

TauCeti.NumberField.fullCycleType_galActionHom_restrict_minpoly_eq_map_natDegree_monicFactorsMod.{u_1,
    u_2}
  {M : Type u_1} [Field M] [NumberField M] {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_2} [Field K]
  [NumberField K] {θ : NumberField.RingOfIntegers K}
  (hsq : Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))
  [Fact (Polynomial.map (algebraMap ℚ M) (minpoly ℚ ↑θ)).Splits]
  (Q : Ideal (NumberField.RingOfIntegers M)) [Q.IsPrime] [Q.LiesOver (Ideal.span {↑p})]
  {σ : Gal(M/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) :
  ((Polynomial.Gal.galActionHom (minpoly ℚ ↑θ) M)
        ((Polynomial.Gal.restrict (minpoly ℚ ↑θ) M) σ)).fullCycleType =
    Multiset.map Polynomial.natDegree (RingOfIntegers.monicFactorsMod θ p).val
Sources
LeanTauCeti.NumberField.factorizationType_eq_cycleType_isArithFrobAt · TauCeti.NumberField.fullCycleType_galActionHom_restrict_eq_factorDegrees · TauCeti.NumberField.fullCycleType_galActionHom_restrict_minpoly_eq_map_natDegree_monicFactorsMod
Used by 1
Used byThe polynomial form of Dedekind's theorem

DefinitionThe semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w#

completing L at the finitely many places above a finite place v of K decomposes the scalar extension of L to K_v into the product of those completions.

TauCeti.semilocalEquiv.{u_1, u_2} {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L]
  [NumberField L] [Algebra K L]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
  TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
      L ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v]
    (w : { w // w.asIdeal.LiesOver v.asIdeal }) →
      IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w
Lean

Formalized in Tau Ceti as TauCeti.semilocalEquiv.

Sources
LeanTauCeti.semilocalEquiv
Used by 19
Used byFinite global reciprocity · Hilbert reciprocity · The global class formation · The global invariant · The global invariant is injective · The idelic consequence of Furtwängler's theorem · The Kummer case of global existence (Milne VII, Lemma 9.3) · The norm index theorem · Base change of adeles in a tower K ⊆ L ⊆ M · Hilbert sign prescription (O'Meara 71:19a) · The kernel of the idele Hilbert character · Hilbert's formula for a number-field different exponent · Global existence (Milne VII, Theorem 9.5) · Shapiro's lemma for the normalized order · The cyclic Hasse norm theorem · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality · Hermite's theorem: finitely many extensions of bounded degree are unramified outside a finite set

TheoremHilbert's formula for a number-field different exponent#

For a finite Galois extension L/K, the multiplicity of a prime w in the global different is the sum of the orders of the nonnegative-index lower ramification groups, minus one in each degree.

IsDedekindDomain.HeightOneSpectrum.multiplicity_differentIdeal_eq_finsum_card_ramificationGroup_sub_one.{u_1,
    u_2}
  {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L]
  (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) [IsGalois K L] :
  multiplicity w.asIdeal
      (differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) =
    ∑ᶠ (i : ℕ), (Nat.card ↥(Ideal.ramificationGroup Gal(L/K) w.asIdeal i) - 1)
Lean

Formalized in Tau Ceti as IsDedekindDomain.HeightOneSpectrum.multiplicity_differentIdeal_eq_finsum_card_ramificationGroup_sub_one.

Sources
LeanIsDedekindDomain.HeightOneSpectrum.multiplicity_differentIdeal_eq_finsum_card_ramificationGroup_sub_one
Uses 3 · Used by 2
Proof usesHilbert's formula, truncated · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · TauCeti.algebraicExtensionNormedField
Used byThe relative discriminant coefficient of a fixed field from double cosets · Hilbert's different formula, checked in ℚ(i)

TheoremThe relative discriminant coefficient of a fixed field from double cosets#

Sum the group-theoretic contributions over H \ Gal(L/K) / D(Q), using any choice of representatives. The formula holds at ramified primes as well as unramified ones, including wild ramification.

TauCeti.NumberField.multiplicity_relDiscr_fixedField_eq_sum.{u_1, u_2} (K : Type u_1) (L : Type u_2)
  [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))
  (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L))
  [w.asIdeal.LiesOver v.asIdeal] (H : Subgroup Gal(L/K))
  (r : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer Gal(L/K) w.asIdeal) → Gal(L/K))
  (hr :
    ∀ (q : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer Gal(L/K) w.asIdeal)),
      DoubleCoset.mk H (MulAction.stabilizer Gal(L/K) w.asIdeal) (r q) = q) :
  multiplicity v.asIdeal
      (TauCeti.relDiscr (NumberField.RingOfIntegers K)
        (NumberField.RingOfIntegers ↥(IntermediateField.fixedField H))) =
    ∑ᶠ (q : DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer Gal(L/K) w.asIdeal)),
      H.relIndex (MulAut.conj (r q) • MulAction.stabilizer Gal(L/K) w.asIdeal) /
          H.relIndex (MulAut.conj (r q) • Ideal.inertia Gal(L/K) w.asIdeal) *
        ((∑ᶠ (i : ℕ),
            (Nat.card ↥(Ideal.ramificationGroup Gal(L/K) w.asIdeal i) -
              Nat.card ↥(MulAut.conj (r q) • Ideal.ramificationGroup Gal(L/K) w.asIdeal i ⊓ H))) /
          Nat.card ↥(MulAut.conj (r q) • Ideal.inertia Gal(L/K) w.asIdeal ⊓ H))
Lean

Formalized in Tau Ceti as TauCeti.NumberField.multiplicity_relDiscr_fixedField_eq_sum.

Sources
LeanTauCeti.NumberField.multiplicity_relDiscr_fixedField_eq_sum
Uses 3
Statement usesTauCeti.relDiscr
Proof usesArtin's theorem · Hilbert's formula for a number-field different exponent

TheoremSoundness of unit-candidate elimination#

A unit expanding at a real place generates modulo torsion if every candidate below its absolute value has been eliminated.

TauCeti.NumberField.Units.UnitCandidateEliminationCertificate.sound.{u_1} {K : Type u_1} [Field K]
  [NumberField K] {u : (NumberField.RingOfIntegers K)ˣ} {w : NumberField.InfinitePlace K}
  (h :
    TauCeti.NumberField.Units.UnitCandidateEliminationCertificate K
      (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)))
  (hr : NumberField.Units.rank K = 1) (hp : Nat.Prime (Module.finrank ℚ K)) (hw : w.IsReal)
  (hu : 1 < w ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) :
  Subgroup.closure {u} ⊔ NumberField.Units.torsion K = ⊤
Lean

Formalized in Tau Ceti as TauCeti.NumberField.Units.UnitCandidateEliminationCertificate.sound.

Sources
LeanTauCeti.NumberField.Units.UnitCandidateEliminationCertificate.sound
Used by 1
Used byHadamard's bound at ℚ(√2)

DefinitionThe double coset law over an integrally closed base#

For M / K finite Galois with group G, a subgroup H of G, the integral closures B and C of A in M and in M ^ H, and a prime Q of B above p with decomposition group D, the primes of C above p are indexed by the double cosets H \ G / D.

The class of σ corresponds to the contraction σ Q ∩ C, by Ideal.doubleCosetQuotientEquivPrimesOverOfIsIntegralClosure_mk.

Ideal.doubleCosetQuotientEquivPrimesOverOfIsIntegralClosure.{u_1, u_2, u_3, u_4, u_5} {A : Type u_1}
  {K : Type u_2} {M : Type u_3} {B : Type u_4} [CommRing A] [Field K] [Algebra A K]
  [IsFractionRing A K] [Field M] [Algebra K M] [FiniteDimensional K M] [IsGalois K M] [Algebra A M]
  [IsScalarTower A K M] [CommRing B] [Algebra A B] [Algebra B M] [IsScalarTower A B M]
  [IsIntegralClosure B A M] [MulSemiringAction Gal(M/K) B] [SMulDistribClass Gal(M/K) B M]
  (Q : Ideal B) [Q.IsPrime] (p : Ideal A) [Q.LiesOver p] (H : Subgroup Gal(M/K))
  [Algebra A ↥(IntermediateField.fixedField H)]
  [IsScalarTower A K ↥(IntermediateField.fixedField H)] (C : Type u_5) [CommRing C] [Algebra A C]
  [Algebra C ↥(IntermediateField.fixedField H)]
  [IsScalarTower A C ↥(IntermediateField.fixedField H)]
  [IsIntegralClosure C A ↥(IntermediateField.fixedField H)] [Algebra C B] [Algebra C M]
  [IsScalarTower A C B] [IsScalarTower C (↥(IntermediateField.fixedField H)) M]
  [IsScalarTower C B M] [IsDomain A] [IsIntegrallyClosed A] :
  DoubleCoset.Quotient ↑H ↑(MulAction.stabilizer Gal(M/K) Q) ≃ ↑(p.primesOver C)
Lean

Formalized in Tau Ceti as Ideal.doubleCosetQuotientEquivPrimesOverOfIsIntegralClosure.

Sources
LeanIdeal.doubleCosetQuotientEquivPrimesOverOfIsIntegralClosure

DefinitionTauCeti.relDiscr#

The relative discriminant ideal of the finite torsion-free extension A → B.

TauCeti.relDiscr.{u_3, u_4} (A : Type u_3) (B : Type u_4) [CommRing A] [IsDedekindDomain A]
  [CommRing B] [IsDedekindDomain B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] :
  Ideal A
Lean

Formalized in Tau Ceti as TauCeti.relDiscr.

Sources
LeanTauCeti.relDiscr
Used by 21
Used byThe global class formation · The global invariant · The global invariant is injective · The Kummer case of global existence (Milne VII, Lemma 9.3) · Infinitely many totally ramified extensions in equal characteristic · IntermediateField.wildExponent · Serre's first mass formula · Serre's mass formula for quadratic extensions in odd residue characteristic · Serre's mass formula for the quadratic extensions of ℚ_2 · TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent_eq_one_iff · The totally ramified quadratic extensions of ℚ_2 · The wild exponent is bounded on σ_K(n) away from equal characteristic p ∣ n · Hilbert sign prescription (O'Meara 71:19a) · The relative discriminant coefficient of a fixed field from double cosets · The cyclic Hasse norm theorem · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality · Dedekind's different theorem, the tame case · The first half of Dedekind's different theorem · Hermite's theorem: finitely many extensions of bounded degree are unramified outside a finite set

DefinitionThe ideal-theoretic Artin map#

The multiplicative extension of artinElementAway along the unique factorization of an invertible fractional ideal, on the group of fractional ideals with multiplicity zero at every prime of S.

TauCeti.NumberFieldArithmetic.artinHomAway.{u_1, u_2} {K : Type u_1} [Field K] [NumberField K]
  {L : Type u_2} [Field L] [NumberField L] [Algebra K L] [IsGalois K L]
  (hab : ∀ (σ τ : Gal(L/K)), Commute σ τ)
  (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)))
  (hur :
    ∀ v ∉ S,
      ∀ (Q : Ideal (NumberField.RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver v.asIdeal],
        Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q) :
  ↥(TauCeti.NumberFieldArithmetic.idealsAway K S) →* Gal(L/K)
Lean

Formalized in Tau Ceti as TauCeti.NumberFieldArithmetic.artinHomAway.

Sources
LeanTauCeti.NumberFieldArithmetic.artinHomAway
Used by 3
Used byThe Chebotarev density theorem · Weighted Chebotarev for abelian extensions · The Kronecker–Weber theorem

TheoremThe polynomial form of Dedekind's theorem#

Let f be a monic integer polynomial and p a prime not dividing the discriminant of f. Then some element of the Galois group of f over ℚ acts on the complex roots of f with full cycle type (cycle lengths counted together with fixed points) equal to the multiset of degrees of the irreducible factors of f modulo p.

The statement allows reducible f: the factor degrees of all the irreducible factors of f are read off from a single Galois automorphism.

TauCeti.NumberField.exists_gal_fullCycleType_eq_factorizationType (f : Polynomial ℤ) (hf : f.Monic)
  (p : ℕ) [Fact (Nat.Prime p)] (hp : ¬↑p ∣ f.discr) :
  ∃ σ,
    ((Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ) σ).fullCycleType =
      f.factorDegrees p
Lean

Formalized in Tau Ceti as TauCeti.NumberField.exists_gal_fullCycleType_eq_factorizationType.

Sources
LeanTauCeti.NumberField.exists_gal_fullCycleType_eq_factorizationType
Uses 1 · Used by 1
Proof usesDedekind's theorem, with the fixed points counted separately
Used byTauCeti.exists_monic_int_polynomial_hasFullSymmetricGaloisGroup

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.