Invariant Extensions of Rings and 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.

This file proves the existence of Frobenius elements in a more general setting.

Given an extension of rings B/A and an action of G on B, we introduce a predicate Algebra.IsInvariant A B G which states that every fixed point of B lies in the image of A.

Main statements

Let G be a finite group acting on a commutative ring B satisfying Algebra.IsInvariant A B G.

• Algebra.IsInvariant.isIntegral: B/A is an integral extension.
• Algebra.IsInvariant.exists_smul_of_under_eq: G acts transitivity on the prime ideals of B lying above a given prime ideal of A.
• IsFractionRing.stabilizerHom_surjective: if Q is a prime ideal of B lying over a prime ideal P of A, then the stabilizer subgroup of Q surjects onto Aut(Frac(B/Q)/Frac(A/P)).

class Algebra.IsInvariant (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommSemiring A] [Semiring B] [Algebra A B] [Group G] [MulSemiringAction G B] : Prop

An action of a group G on an extension of rings B/A is invariant if every fixed point of B lies in the image of A. The converse statement that every point in the image of A is fixed by G is smul_algebraMap (assuming SMulCommClass A B G).

• isInvariant (b : B) : (∀ (g : G), g • b = b) → ∃ (a : A), (algebraMap A B) a = b

theorem Algebra.isInvariant_iff (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommSemiring A] [Semiring B] [Algebra A B] [Group G] [MulSemiringAction G B] : Algebra.IsInvariant A B G ↔ ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), (algebraMap A B) a = b

noncomputable def MulSemiringAction.charpoly {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) : Polynomial B

Characteristic polynomial of a finite group action on a ring.

Equations

• MulSemiringAction.charpoly G b = ∏ g : G, (Polynomial.X - Polynomial.C (g • b))

theorem MulSemiringAction.charpoly_eq {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) : MulSemiringAction.charpoly G b = ∏ g : G, (Polynomial.X - Polynomial.C (g • b))

theorem MulSemiringAction.charpoly_eq_prod_smul {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) : MulSemiringAction.charpoly G b = ∏ g : G, g • (Polynomial.X - Polynomial.C b)

theorem MulSemiringAction.monic_charpoly {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) : (MulSemiringAction.charpoly G b).Monic

theorem MulSemiringAction.eval_charpoly {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) : Polynomial.eval b (MulSemiringAction.charpoly G b) = 0

theorem MulSemiringAction.smul_charpoly {B : Type u_2} {G : Type u_3} [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) (g : G) : g • MulSemiringAction.charpoly G b = MulSemiringAction.charpoly G b

theorem MulSemiringAction.smul_coeff_charpoly {B : Type u_2} {G : Type u_3} [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) (n : ℕ) (g : G) : g • (MulSemiringAction.charpoly G b).coeff n = (MulSemiringAction.charpoly G b).coeff n

theorem Algebra.IsInvariant.charpoly_mem_lifts (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] [Fintype G] (b : B) : MulSemiringAction.charpoly G b ∈ Polynomial.lifts (algebraMap A B)

theorem Algebra.IsInvariant.isIntegral (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] [Finite G] : Algebra.IsIntegral A B

theorem Algebra.IsInvariant.exists_smul_of_under_eq (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] [Finite G] [SMulCommClass G A B] (P Q : Ideal B) [hP : P.IsPrime] [hQ : Q.IsPrime] (hPQ : Ideal.under A P = Ideal.under A Q) : ∃ (g : G), Q = g • P

G acts transitively on the prime ideals of B above a given prime ideal of A.

noncomputable def IsFractionRing.stabilizerHom {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra (A ⧸ P) K] [Algebra (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] [Algebra K L] [IsScalarTower (A ⧸ P) K L] [IsFractionRing (A ⧸ P) K] [IsFractionRing (B ⧸ Q) L] : ↥(MulAction.stabilizer G Q) →* L ≃ₐ[K] L

If Q lies over P, then the stabilizer of Q acts on Frac(B/Q)/Frac(A/P).

Equations

• IsFractionRing.stabilizerHom G P Q K L = (IsFractionRing.fieldEquivOfAlgEquivHom K L).comp (Ideal.Quotient.stabilizerHom Q P G)

theorem IsFractionRing.stabilizerHom_surjective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B] (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [Q.LiesOver P] (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra (A ⧸ P) K] [Algebra (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] [Algebra K L] [IsScalarTower (A ⧸ P) K L] [Algebra.IsInvariant A B G] [IsFractionRing (A ⧸ P) K] [IsFractionRing (B ⧸ Q) L] : Function.Surjective ⇑(IsFractionRing.stabilizerHom G P Q K L)

The stabilizer subgroup of Q surjects onto Aut(Frac(B/Q)/Frac(A/P)).

theorem Ideal.Quotient.stabilizerHom_surjective {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B] (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [Q.LiesOver P] [Algebra.IsInvariant A B G] : Function.Surjective ⇑(Ideal.Quotient.stabilizerHom Q P G)

The stabilizer subgroup of Q surjects onto Aut((B/Q)/(A/P)).