Invariant Extensions of Rings

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.

The main application is in algebraic number theory, where G := Gal(L/K) is the galois group of some finite galois extension of number fields, and A := 𝓞K and B := 𝓞L are their ring of integers. This main result in this file implies the existence of Frobenius elements in this setting. See Mathlib/RingTheory/Frobenius.lean.

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.

If Q is a prime ideal of B lying over a prime ideal P of A, then

• IsFractionRing.stabilizerHom_surjective: The stabilizer subgroup of Q surjects onto Aut(Frac(B/Q)/Frac(A/P)).
• Ideal.Quotient.stabilizerHom_surjective: The stabilizer subgroup of Q surjects onto Aut((B/Q)/(A/P)).
• Ideal.Quotient.exists_algEquiv_fixedPoint_quotient_under: If k is a domain containing B/Q, then any A/P-algebra automorphism of k restricts to an automorphism of B/Q.

noncomputable def IsIntegralClosure.MulSemiringAction (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic K L] : _root_.MulSemiringAction (L ≃ₐ[K] L) B

In the AKLB setup, the Galois group of L/K acts on B.

theorem Algebra.isInvariant_of_isGalois (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsIntegrallyClosed A] [IsIntegralClosure B A L] [FiniteDimensional K L] [h : IsGalois K L] : IsInvariant A B (L ≃ₐ[K] L)

In the AKLB setup, every fixed point of B lies in the image of A.

theorem Algebra.isInvariant_of_isGalois' (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Field K] [Field L] [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsIntegrallyClosed A] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsGalois K L] : IsInvariant A B (B ≃ₐ[A] B)

A variant of Algebra.isInvariant_of_isGalois, replacing Gal(L/K) by Aut(B/A).

instance instMulSemiringActionQuotientSubgroupSubtypeMemSubringSubring {B : Type u_2} [CommRing B] {G : Type u_3} [Group G] [MulSemiringAction G B] (H : Subgroup G) [H.Normal] : MulSemiringAction (G ⧸ H) ↥(FixedPoints.subring B ↥H)

instance instMulSemiringActionQuotientSubgroupSubtypeMemSubalgebraSubalgebra {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] (H : Subgroup G) [H.Normal] : MulSemiringAction (G ⧸ H) ↥(FixedPoints.subalgebra A B ↥H)

instance instSMulCommClassQuotientSubgroupSubtypeMemSubalgebraSubalgebra {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] (H : Subgroup G) [H.Normal] : SMulCommClass (G ⧸ H) A ↥(FixedPoints.subalgebra A B ↥H)

instance instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient {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] (H : Subgroup G) [H.Normal] [Algebra.IsInvariant A B G] : Algebra.IsInvariant A (↥(FixedPoints.subalgebra A B ↥H)) (G ⧸ H)

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.

theorem MulSemiringAction.charpoly_eq {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) : 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) : 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) : (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 (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 • charpoly G b = 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 • (charpoly G b).coeff n = (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] [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] [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] [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.

theorem Algebra.IsInvariant.orbit_eq_primesOver (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [IsInvariant A B G] [Finite G] [SMulCommClass G A B] (P : Ideal A) (Q : Ideal B) [hP : Q.LiesOver P] [hQ : Q.IsPrime] : MulAction.orbit G Q = P.primesOver B

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).

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 ⇑(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 ⇑(stabilizerHom Q P G)

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

theorem Ideal.Quotient.exists_algHom_fixedPoint_quotient_under {A : Type u_1} {B : Type u_2} {k : Type u_3} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_4) [Finite G] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] [CommRing k] [Algebra (A ⧸ P) k] [Algebra (B ⧸ Q) k] [IsScalarTower (A ⧸ P) (B ⧸ Q) k] [IsDomain k] [FaithfulSMul (B ⧸ Q) k] (σ : k →ₐ[A ⧸ P] k) : ∃ (τ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q), ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ x) = σ ((algebraMap (B ⧸ Q) k) x)

For any domain k containing B ⧸ Q, any endomorphism of k can be restricted to an endomorphism of B ⧸ Q.

This is basically the fact that L/K normal implies κ(Q)/κ(P) normal in the galois setting.

theorem Ideal.Quotient.exists_algEquiv_fixedPoint_quotient_under {A : Type u_1} {B : Type u_2} {k : Type u_3} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_4) [Finite G] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] [CommRing k] [Algebra (A ⧸ P) k] [Algebra (B ⧸ Q) k] [IsScalarTower (A ⧸ P) (B ⧸ Q) k] [IsDomain k] [FaithfulSMul (B ⧸ Q) k] (σ : k ≃ₐ[A ⧸ P] k) : ∃ (τ : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q), ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ x) = σ ((algebraMap (B ⧸ Q) k) x)

For any domain k containing B ⧸ Q, any endomorphism of k can be restricted to an endomorphism of B ⧸ Q.