Frobenius elements

TheoremIn an abelian group the Frobenius element depends only on the prime below#✓fully proved

Let \(S\) be a commutative algebra over a commutative ring \(R\), and let a finite commutative group \(G\) act on \(S\) by \(R\)-algebra automorphisms such that every element of \(S\) fixed by \(G\) is the image of an element of \(R\). For a prime \(Q\) of \(S\) with \(S/Q\) finite, let \(\mathrm{Frob}_Q \in G\) be the chosen arithmetic Frobenius element at \(Q\): an element \(\sigma \in G\) with \(\sigma(x) \equiv x^q \pmod Q\) for all \(x \in S\), where \(q\) is the number of elements of \(R\) modulo the preimage of \(Q\) in \(R\), chosen so that the elements chosen at primes with the same preimage in \(R\) are conjugate. If \(Q\) and \(Q'\) are primes of \(S\) with \(S/Q\) and \(S/Q'\) finite that have the same preimage in \(R\), then \(\mathrm{Frob}_Q = \mathrm{Frob}_{Q'}\).

theorem arithFrobAt_eq_of_under_eq [IsMulCommutative G]
    (Q Q' : Ideal S) [Q.IsPrime] [Finite (S ⧸ Q)]
    [Q'.IsPrime] [Finite (S ⧸ Q')]
    (h : Q.under R = Q'.under R) :
    arithFrobAt R G Q = arithFrobAt R G Q'

TheoremRestricting a Frobenius element to an intermediate field#✓fully proved

Let \(K \subseteq L \subseteq M\) be a tower of number fields with \(L/K\) and \(M/K\) Galois, and let \(\mathcal{O}_K\), \(\mathcal{O}_L\) and \(\mathcal{O}_M\) be their rings of integers. Let \(Q_L\) be a prime of \(\mathcal{O}_L\) at which \(\mathcal{O}_L\) is unramified over \(\mathcal{O}_K\), let \(Q_M\) be a prime of \(\mathcal{O}_M\) lying over \(Q_L\) with \(\mathcal{O}_M/Q_M\) finite, and let \(q\) be the number of elements of \(\mathcal{O}_K/\mathfrak{p}\), where \(\mathfrak{p}\) is the prime of \(\mathcal{O}_K\) below \(Q_M\) (equivalently, below \(Q_L\)). If \(\sigma_M \in \mathrm{Gal}(M/K)\) satisfies \(\sigma_M(x) \equiv x^q \pmod{Q_M}\) for all \(x \in \mathcal{O}_M\) and \(\sigma_L \in \mathrm{Gal}(L/K)\) satisfies \(\sigma_L(y) \equiv y^q \pmod{Q_L}\) for all \(y \in \mathcal{O}_L\), then the restriction of \(\sigma_M\) to \(L\) equals \(\sigma_L\).

theorem restrictNormalHom_eq_of_isArithFrobAt
    (Q_L : Ideal (NumberField.RingOfIntegers L)) [Q_L.IsPrime]
    (Q_M : Ideal (NumberField.RingOfIntegers M)) [Q_M.IsPrime] [Q_M.LiesOver Q_L]
    [Finite (NumberField.RingOfIntegers M ⧸ Q_M)]
    [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q_L]
    (σ_M : M ≃ₐ[K] M) (σ_L : L ≃ₐ[K] L)
    (hM : IsArithFrobAt (NumberField.RingOfIntegers K) σ_M Q_M)
    (hL : IsArithFrobAt (NumberField.RingOfIntegers K) σ_L Q_L) :
    AlgEquiv.restrictNormalHom L σ_M = σ_L
Sources
  • ATLAS Proposition 7.13, generalized from the chosen Frobenius elements at chosen primes to arbitrary Frobenius elements at explicit primes.
Used by 1
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.