Frobenius elements.

This file proves a general result in commutative algebra which can be used to define Frobenius elements of Galois groups of local or fields (for example number fields).

KB was alerted to this very general result (which needs no Noetherian or finiteness assumptions on the rings, just on the Galois group) by Joel Riou here https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Uses.20of.20Frobenius.20elements.20in.20mathematics/near/448934112

Mathematical details

The general commutative algebra result

This is Theorem 2 in Chapter V, Section 2, number 2 of Bourbaki Alg Comm. It says the following. Let A → B be commutative rings and let G be a finite group acting on B by ring automorphisms, such that the G-invariants of B are exactly the image of A.

The two claims of the theorem are: (i) If P is a prime ideal of A then G acts transitively on the primes of B above P. (ii) If Q is a prime ideal of B lying over P then the canonica map from the stabilizer of Q in G to the automorphism group of the residue field extension Frac(B/Q) / Frac(A/P) is surjective.

We say "automorphism group" rather than "Galois group" because the extension might not be separable (it is algebraic and normal however, but it can be infinite; however its maximal separable subextension is finite).

This result means that if the inertia group I_Q is trivial and the residue fields are finite, there's a Frobenius element Frob_Q in the stabiliser of Q, and a Frobenius conjugacy class Frob_P in G.

theorem Ideal.IsPrime.finprod_mem_iff_exists_mem {R : Type u_4} {S : Type u_5} [Finite R] [CommSemiring S] (I : Ideal S) [hI : I.IsPrime] (f : R → S) : ∏ᶠ (x : R), f x ∈ I ↔ ∃ (p : R), f p ∈ I

theorem part_a {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] {G : Type u_3} [Group G] [Finite G] [MulSemiringAction G B] (P : Ideal B) (Q : Ideal B) [P.IsPrime] [Q.IsPrime] (hPQ : Ideal.comap (algebraMap A B) P = Ideal.comap (algebraMap A B) Q) (hGalois : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ (a : A), b = ↑a) : ∃ (g : G), Q = g • P

theorem Ideal.Quotient.eq_zero_iff_mem' {A : Type u_1} [CommRing A] (P : Ideal A) (x : A) : (algebraMap A (A ⧸ P)) x = 0 ↔ x ∈ P

noncomputable def instAlgebraPolynomial_fLT {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] : Algebra (Polynomial A) (Polynomial B)

Equations

• instAlgebraPolynomial_fLT = (Polynomial.mapRingHom Algebra.toRingHom).toAlgebra

@[simp]

theorem coe_monomial {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] (n : ℕ) (a : A) : ↑((Polynomial.monomial n) a) = (Polynomial.monomial n) ↑a

noncomputable def M {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] (hGalois : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ (a : A), b = ↑a) (b : B) : Polynomial A

Equations

• M G hGalois b = ⋯.choose

theorem M_spec {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] {G : Type u_3} [Group G] [Finite G] [MulSemiringAction G B] (hGalois : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ (a : A), b = ↑a) (b : B) : ↑(M G hGalois b) = F G b

theorem M_eval_eq_zero {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] {G : Type u_3} [Group G] [Finite G] [MulSemiringAction G B] (hGalois : ∀ (b : B), (∀ (g : G), g • b = b) ↔ ∃ (a : A), b = ↑a) (b : B) : Polynomial.eval₂ (algebraMap (Polynomial A) (Polynomial B)) ↑b ↑(M G hGalois b) = 0

theorem Algebra.isAlgebraic_of_subring_isAlgebraic {R : Type u_6} {k : Type u_7} {K : Type u_8} [CommRing R] [CommRing k] [CommRing K] [Algebra R K] [IsFractionRing R K] [Algebra k K] (h : ∀ (x : R), IsAlgebraic k ↑x) : Algebra.IsAlgebraic k K

theorem part_b1 (L : Type u_4) [Field L] (K : Type u_5) [Field K] [Algebra K L] : Algebra.IsAlgebraic K L

theorem part_b2 (L : Type u_4) [Field L] (K : Type u_5) [Field K] [Algebra K L] : Normal K L

def foo {B : Type u_2} [CommRing B] {G : Type u_3} [Group G] [MulSemiringAction G B] (Q : Ideal B) (g : G) (hg : g • Q = Q) : B ⧸ Q ≃+* B ⧸ Q

Equations

• foo Q g hg = Q.quotientEquiv Q (MulSemiringAction.toRingEquiv G B g) ⋯

def bar {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {G : Type u_3} [Group G] [MulSemiringAction G B] (Q : Ideal B) (P : Ideal A) [Algebra (A ⧸ P) (B ⧸ Q)] (g : G) (hg : g • Q = Q) : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q

Equations

• bar Q P g hg = { toEquiv := (foo Q g hg).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def baz {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {G : Type u_3} [Group G] [MulSemiringAction G B] (Q : Ideal B) (P : Ideal A) [Algebra (A ⧸ P) (B ⧸ Q)] : { x : G // x ∈ MulAction.stabilizer G Q } →* (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q

Equations

• baz Q P = { toFun := fun (gh : { x : G // x ∈ MulAction.stabilizer G Q }) => bar Q P ↑gh ⋯, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def bar2 {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] (Q : Ideal B) [Q.IsPrime] (P : Ideal A) [Algebra (A ⧸ P) (B ⧸ Q)] (L : Type u_4) [Field L] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L] (K : Type u_5) [Field K] [Algebra K L] (e : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) : L ≃ₐ[K] L

Equations

• bar2 Q P L K e = { toEquiv := (IsFractionRing.fieldEquivOfRingEquiv e.toRingEquiv).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def baz2 {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] {G : Type u_3} [Group G] [MulSemiringAction G B] (Q : Ideal B) [Q.IsPrime] (P : Ideal A) [Algebra (A ⧸ P) (B ⧸ Q)] (L : Type u_4) [Field L] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L] (K : Type u_5) [Field K] [Algebra K L] : { x : G // x ∈ MulAction.stabilizer G Q } →* L ≃ₐ[K] L

Equations

• baz2 Q P L K = { toFun := fun (gh : { x : G // x ∈ MulAction.stabilizer G Q }) => bar2 Q P L K ((baz Q P) gh), map_one' := ⋯, map_mul' := ⋯ }

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

@[reducible, inline]

abbrev S {A : Type u_1} [CommRing A] (P : Ideal A) [P.IsPrime] : Submonoid A

Equations

• S P = P.primeCompl

@[reducible, inline]

abbrev SA {A : Type u_1} [CommRing A] (P : Ideal A) [P.IsPrime] : Type u_1

Equations

• SA P = OreLocalization (S P) A

@[reducible, inline]

abbrev SB {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [Algebra A B] (P : Ideal A) [P.IsPrime] : Type (max u_1 u_2)

Equations

• SB P = OreLocalization (S P) B