Frobenius elements under trivial inertia

TheoremFrobenius elements coincide when inertia is trivial#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra, let a group \(G\) act on \(S\) by \(R\)-algebra automorphisms, and let \(Q\) be an ideal of \(S\). Write \(P\) for the preimage of \(Q\) in \(R\) and \(q\) for the number of elements of \(R/P\) (with \(q = 0\) when \(R/P\) is infinite). Call \(\sigma \in G\) an arithmetic Frobenius element at \(Q\) if \(\sigma x - x^q \in Q\) for all \(x \in S\), and call the inertia subgroup of \(Q\) the set of \(\tau \in G\) with \(\tau x - x \in Q\) for all \(x \in S\). If \(\sigma, \sigma' \in G\) are arithmetic Frobenius elements at \(Q\) and the inertia subgroup of \(Q\) is trivial, then \(\sigma = \sigma'\).

theorem eq_of_inertia_eq_bot (hσ : IsArithFrobAt R σ Q)
    (hσ' : IsArithFrobAt R σ' Q) (hbot : Q.inertia G = ⊥) : σ = σ'

Used by 1

Used byExistence and uniqueness of the Frobenius element under trivial inertia

TheoremExistence and uniqueness of the Frobenius element under trivial inertia#✓fully proved

Let \(R\) and \(S\) be commutative rings with \(S\) an \(R\)-algebra, and let a finite 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\). Let \(Q\) be a prime ideal of \(S\) with \(S/Q\) finite, write \(P\) for the preimage of \(Q\) in \(R\) and \(q\) for the number of elements of \(R/P\). Call \(\sigma \in G\) an arithmetic Frobenius element at \(Q\) if \(\sigma x - x^q \in Q\) for all \(x \in S\). If the inertia subgroup of \(Q\), the set of \(\tau \in G\) with \(\tau x - x \in Q\) for all \(x \in S\), is trivial, then there is exactly one arithmetic Frobenius element at \(Q\) in \(G\).

theorem existsUnique_of_inertia_eq_bot [Finite G] [Algebra.IsInvariant R S G]
    [Q.IsPrime] [Finite (S ⧸ Q)] (hbot : Q.inertia G = ⊥) :
    ∃! σ : G, IsArithFrobAt R σ Q

Uses 1

Proof usesFrobenius elements coincide when inertia is trivial

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.