Frobenius elements

In algebraic number theory, if L/K is a finite Galois extension of number fields, with rings of integers 𝓞L/𝓞K, and if q is prime ideal of 𝓞L lying over a prime ideal p of 𝓞K, then there exists a Frobenius element Frob p in Gal(L/K) with the property that Frob p x ≡ x ^ #(𝓞K/p) (mod q) for all x ∈ 𝓞L.

Following RingTheory/Invariant.lean, we develop the theory in the setting that there is a finite group G acting on a ring S, and R is the fixed subring of S.

Main results

Let S/R be an extension of rings, Q be a prime of S, and P := R ∩ Q with finite residue field of cardinality q.

• AlgHom.IsArithFrobAt: We say that a φ : S →ₐ[R] S is an (arithmetic) Frobenius at Q if φ x ≡ x ^ q (mod Q) for all x : S.
• AlgHom.IsArithFrobAt.apply_of_pow_eq_one: Suppose S is a domain and φ is a Frobenius at Q, then φ ζ = ζ ^ q for any m-th root of unity ζ with q ∤ m.
• AlgHom.IsArithFrobAt.eq_of_isUnramifiedAt: Suppose S is noetherian, Q contains all zero-divisors, and the extension is unramified at Q. Then the Frobenius is unique (if exists).

Let G be a finite group acting on a ring S, and R is the fixed subring of S.

• IsArithFrobAt: We say that a σ : G is an (arithmetic) Frobenius at Q if σ • x ≡ x ^ q (mod Q) for all x : S.
• IsArithFrobAt.mul_inv_mem_inertia: Two Frobenius elements at Q differ by an element in the inertia subgroup of Q.
• IsArithFrobAt.conj: If σ is a Frobenius at Q, then τστ⁻¹ is a Frobenius at σ • Q.
• IsArithFrobAt.exists_of_isInvariant: Frobenius element exists.

theorem IsArithFrobAt.exists_of_isInvariant_of_profinite (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (G : Type u_3) [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (Q : Ideal S) [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G] [Algebra.IsInvariant R S G] [ContinuousSMulDiscrete G S] [Q.IsMaximal] [Finite (R ⧸ Ideal.under R Q)] : ∃ (σ : G), IsArithFrobAt R σ Q

Let G be a finite group acting on S, and R be the fixed subring. If Q is a prime of S with finite residue field, then there exists a Frobenius element σ : G at Q.

theorem IsArithFrobAt.exists_primesOver_isConj_of_profinite {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (G : Type u_3) [Group G] [MulSemiringAction G S] [SMulCommClass G R S] [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G] [Algebra.IsInvariant R S G] [ContinuousSMulDiscrete G S] (P : Ideal R) [Finite (R ⧸ P)] [P.IsPrime] : ∃ (σ : ↑(P.primesOver S) → G), (∀ (Q : ↑(P.primesOver S)), IsArithFrobAt R (σ Q) ↑Q) ∧ ∀ (Q₁ Q₂ : ↑(P.primesOver S)), IsConj (σ Q₁) (σ Q₂)

noncomputable def arithFrobAt' (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (G : Type u_3) [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (Q : Ideal S) [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G] [Algebra.IsInvariant R S G] [ContinuousSMulDiscrete G S] [Q.IsPrime] [Finite (R ⧸ Ideal.under R Q)] : G

Let G be a finite group acting on S, R be the fixed subring, and Q be a prime of S with finite residue field. This is an arbitrary choice of a Frobenius over Q. It is chosen so that the Frobenius elements of Q₁ and Q₂ are conjugate if they lie over the same prime.

Equations

• arithFrobAt' R G Q = ⋯.choose ⟨Q, ⋯⟩

theorem IsArithFrobAt.arithFrobAt' (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (G : Type u_3) [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (Q : Ideal S) [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G] [Algebra.IsInvariant R S G] [ContinuousSMulDiscrete G S] [Q.IsPrime] [Finite (R ⧸ Ideal.under R Q)] : IsArithFrobAt R (arithFrobAt' R G Q) Q

theorem isConj_arithFrobAt' (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (G : Type u_3) [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (Q : Ideal S) [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G] [IsTopologicalGroup G] [Algebra.IsInvariant R S G] [ContinuousSMulDiscrete G S] [Q.IsPrime] [Finite (R ⧸ Ideal.under R Q)] (Q' : Ideal S) [Q'.IsPrime] [Finite (R ⧸ Ideal.under R Q')] (H : Ideal.under R Q = Ideal.under R Q') : IsConj (arithFrobAt' R G Q) (arithFrobAt' R G Q')