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.

def AlgHom.IsArithFrobAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (φ : S →ₐ[R] S) (Q : Ideal S) : Prop

φ : S →ₐ[R] S is an (arithmetic) Frobenius at Q if φ x ≡ x ^ #(R/p) (mod Q) for all x : S (AlgHom.IsArithFrobAt).

theorem AlgHom.IsArithFrobAt.mk_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) (x : S) : (Ideal.Quotient.mk Q) (φ x) = (Ideal.Quotient.mk Q) x ^ Nat.card (R ⧸ Ideal.under R Q)

theorem AlgHom.IsArithFrobAt.finite_quotient {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) : _root_.Finite (R ⧸ Ideal.under R Q)

theorem AlgHom.IsArithFrobAt.card_pos {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) : 0 < Nat.card (R ⧸ Ideal.under R Q)

theorem AlgHom.IsArithFrobAt.le_comap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) : Q ≤ Ideal.comap φ Q

def AlgHom.IsArithFrobAt.restrict {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) : S ⧸ Q →ₐ[R ⧸ Ideal.under R Q] S ⧸ Q

A Frobenius element at Q restricts to the Frobenius map on S ⧸ Q.

theorem AlgHom.IsArithFrobAt.restrict_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) (x : S ⧸ Q) : H.restrict x = x ^ Nat.card (R ⧸ Ideal.under R Q)

theorem AlgHom.IsArithFrobAt.restrict_mk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) (x : S) : H.restrict ((Ideal.Quotient.mk Q) x) = (Ideal.Quotient.mk Q) (φ x)

theorem AlgHom.IsArithFrobAt.restrict_injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) [Q.IsPrime] : Function.Injective ⇑H.restrict

theorem AlgHom.IsArithFrobAt.comap_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) [Q.IsPrime] : Ideal.comap φ Q = Q

theorem AlgHom.IsArithFrobAt.apply_of_pow_eq_one {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) [IsDomain S] {ζ : S} {m : ℕ} (hζ : ζ ^ m = 1) (hk' : ↑m ∉ Q) : φ ζ = ζ ^ Nat.card (R ⧸ Ideal.under R Q)

Suppose S is a domain, and φ : S →ₐ[R] S is a Frobenius at Q : Ideal S. Let ζ be a m-th root of unity with Q ∤ m, then φ sends ζ to ζ ^ q.

noncomputable def AlgHom.IsArithFrobAt.localize {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) [Q.IsPrime] : Localization.AtPrime Q →ₐ[R] Localization.AtPrime Q

A Frobenius element at Q restricts to an automorphism of S_Q.

@[simp]

theorem AlgHom.IsArithFrobAt.localize_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) [Q.IsPrime] (x : S) : H.localize ((algebraMap S (Localization.AtPrime Q)) x) = (algebraMap S (Localization.AtPrime Q)) (φ x)

theorem AlgHom.IsArithFrobAt.isArithFrobAt_localize {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) [Q.IsPrime] : H.localize.IsArithFrobAt (IsLocalRing.maximalIdeal (Localization.AtPrime Q))

theorem AlgHom.IsArithFrobAt.eq_of_isUnramifiedAt {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ ψ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) (H' : ψ.IsArithFrobAt Q) [Q.IsPrime] (hQ : Q.primeCompl ≤ nonZeroDivisors S) [Algebra.IsUnramifiedAt R Q] [IsNoetherianRing S] : φ = ψ

Suppose S is noetherian and Q is a prime of S containing all zero divisors. If S/R is unramified at Q, then the Frobenius φ : S →ₐ[R] S over Q is unique.

@[reducible, inline]

abbrev IsArithFrobAt (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_3} [Monoid M] [MulSemiringAction M S] [SMulCommClass M R S] (σ : M) (Q : Ideal S) : Prop

Suppose S is an R algebra, M is a monoid acting on S whose action is trivial on R σ : M is an (arithmetic) Frobenius at an ideal Q of S if σ • x ≡ x ^ q (mod Q) for all x.

theorem IsArithFrobAt.mul_inv_mem_inertia {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} {σ σ' : G} (H : IsArithFrobAt R σ Q) (H' : IsArithFrobAt R σ' Q) : σ * σ'⁻¹ ∈ (Submodule.toAddSubgroup Q).inertia G

theorem IsArithFrobAt.conj {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} {σ : G} (H : IsArithFrobAt R σ Q) (τ : G) : IsArithFrobAt R (τ * σ * τ⁻¹) (τ • Q)

theorem IsArithFrobAt.exists_of_isInvariant (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) [Finite G] [Algebra.IsInvariant R S G] [Q.IsPrime] [Finite (S ⧸ 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 {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] [Finite G] [Algebra.IsInvariant R S G] (P : Ideal R) (hP : ∃ (Q : ↑(P.primesOver S)), Finite (S ⧸ ↑Q)) : ∃ (σ : ↑(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) [Finite G] [Algebra.IsInvariant R S G] [Q.IsPrime] [Finite (S ⧸ 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.

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) [Finite G] [Algebra.IsInvariant R S G] [Q.IsPrime] [Finite (S ⧸ 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) [Finite G] [Algebra.IsInvariant R S G] [Q.IsPrime] [Finite (S ⧸ Q)] (Q' : Ideal S) [Q'.IsPrime] [Finite (S ⧸ Q')] (H : Ideal.under R Q = Ideal.under R Q') : IsConj (arithFrobAt R G Q) (arithFrobAt R G Q')