Frobenius elements and complete splitting

4 fully proved

Splits Completely

TheoremTrivial decomposition group and the number of primes above#✓fully proved

Let \(B\) be a commutative algebra over a commutative ring \(A\), and let a finite group \(G\) act on \(B\) by \(A\)-algebra automorphisms such that every element of \(B\) fixed by \(G\) is the image of an element of \(A\). Let \(p\) be an ideal of \(A\) and \(P\) a prime of \(B\) lying over \(p\). Then the stabilizer of \(P\) in \(G\) (the decomposition group of \(P\)) is trivial if and only if the number of primes of \(B\) lying over \(p\) equals the order of \(G\).

theorem stabilizer_eq_bot_iff_ncard_primesOver_eq_card :
    MulAction.stabilizer G P = ⊥ ↔ (primesOver p B).ncard = Nat.card G

Used by 1

Used byTrivial Frobenius and the number of primes above, assuming the Frobenius generates

Conditional

TheoremTrivial Frobenius and the number of primes above, assuming the Frobenius generates#✓fully proved

Let \(B\) be a commutative algebra over a commutative ring \(A\), and let a finite group \(G\) act on \(B\) by \(A\)-algebra automorphisms such that every element of \(B\) fixed by \(G\) is the image of an element of \(A\). Let \(p\) be an ideal of \(A\) and \(P\) a prime of \(B\) lying over \(p\) with \(B/P\) finite, and let \(\mathrm{Frob}_P \in G\) be the chosen arithmetic Frobenius element at \(P\), an element \(\sigma \in G\) with \(\sigma(x) \equiv x^q \pmod P\) for all \(x \in B\), where \(q\) is the number of elements of \(A/p\). Suppose every element of the stabilizer of \(P\) in \(G\) equals \(\mathrm{Frob}_P^n\) for some natural number \(n\). Then \(\mathrm{Frob}_P = 1\) if and only if the number of primes of \(B\) lying over \(p\) equals the order of \(G\).

theorem arithFrobAt_eq_one_iff_ncard_primesOver_eq_card_of_generates
    [Finite (B ⧸ P)]
    (hgen : ∀ g ∈ MulAction.stabilizer G P,
      ∃ n : ℕ, g = arithFrobAt A G P ^ n) :
    arithFrobAt A G P = 1 ↔ (Ideal.primesOver p B).ncard = Nat.card G

Uses 1 · Used by 1

Proof usesTrivial decomposition group and the number of primes above

Used byThe Frobenius element is trivial iff the prime splits completely

Unramified

TheoremThe Frobenius element generates the decomposition group at an unramified prime#✓fully proved

Let \(A\) and \(B\) be integral domains with \(B\) a finite flat \(A\)-algebra, and let \(G\) be a finite group acting faithfully on \(B\) by \(A\)-algebra automorphisms such that every element of \(B\) fixed by \(G\) is the image of an element of \(A\). Let \(p\) be a prime of \(A\) and \(P\) a prime of \(B\) lying over \(p\), with \(B/P\) finite and \(B\) unramified over \(A\) at \(P\) (the localization \(B_P\) is formally unramified over \(A\)). Let \(\mathrm{Frob}_P \in G\) be the chosen arithmetic Frobenius element at \(P\), an element \(\sigma \in G\) with \(\sigma(x) \equiv x^q \pmod P\) for all \(x \in B\), where \(q\) is the number of elements of \(A/p\). Then every element of the stabilizer of \(P\) in \(G\) (the decomposition group of \(P\)) equals \(\mathrm{Frob}_P^n\) for some natural number \(n\).

theorem arithFrobAt_generates_stabilizer_of_isUnramifiedAt
    (p : Ideal A) [p.IsPrime] [P.LiesOver p]
    [Finite (B ⧸ P)] [Algebra.IsUnramifiedAt A P] :
    ∀ g ∈ MulAction.stabilizer G P,
      ∃ n : ℕ, g = arithFrobAt A G P ^ n

Used by 1

Used byThe Frobenius element is trivial iff the prime splits completely

TheoremThe Frobenius element is trivial iff the prime splits completely#✓fully proved

Let \(A\) and \(B\) be integral domains with \(B\) a finite flat \(A\)-algebra, and let \(G\) be a finite group acting faithfully on \(B\) by \(A\)-algebra automorphisms such that every element of \(B\) fixed by \(G\) is the image of an element of \(A\). Let \(p\) be a prime of \(A\) and \(P\) a prime of \(B\) lying over \(p\), with \(B/P\) finite and \(B\) unramified over \(A\) at \(P\) (the localization \(B_P\) is formally unramified over \(A\)). Let \(\mathrm{Frob}_P \in G\) be the chosen arithmetic Frobenius element at \(P\), an element \(\sigma \in G\) with \(\sigma(x) \equiv x^q \pmod P\) for all \(x \in B\), where \(q\) is the number of elements of \(A/p\). Then \(\mathrm{Frob}_P = 1\) if and only if the number of primes of \(B\) lying over \(p\) equals the order of \(G\).

theorem arithFrobAt_eq_one_iff_ncard_primesOver_eq_card
    [Finite (B ⧸ P)] [Algebra.IsUnramifiedAt A P] :
    arithFrobAt A G P = 1 ↔ (Ideal.primesOver p B).ncard = Nat.card G

Uses 2

Proof usesTrivial Frobenius and the number of primes above, assuming the Frobenius generates · The Frobenius element generates the decomposition group at an unramified prime

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.