Galois Groups of Rings

Given an action of a group G on an extension of rings B/A, the predicate IsGaloisGroup G A B states that G acts faithfully on B with fixed ring A. This file develops some of the theory of this predicate without assuming Galois theory for fields.

theorem Subgroup.smul_algebraMap {G : Type u_1} (B : Type u_3) [Group G] [Semiring B] [MulSemiringAction G B] {C : Type u_4} [CommSemiring C] [Algebra C B] {H : Subgroup G} [SMulCommClass (↥H) C B] {g : G} (hg : g ∈ H) (x : C) : g • (algebraMap C B) x = (algebraMap C B) x

theorem IsGaloisGroup.smul_mem_of_normal (G : Type u_1) (B : Type u_3) [Group G] [Semiring B] [MulSemiringAction G B] {C : Type u_4} [CommSemiring C] [Algebra C B] (N : Subgroup G) [hN : N.Normal] [hC : IsGaloisGroup (↥N) C B] (g : G) (x : C) : g • (algebraMap C B) x ∈ Set.range ⇑(algebraMap C B)

@[deprecated Subgroup.smul_algebraMap (since := "2026-05-28")]

theorem smul_eq_self {G : Type u_1} (B : Type u_3) [Group G] [Semiring B] [MulSemiringAction G B] {C : Type u_4} [CommSemiring C] [Algebra C B] {H : Subgroup G} [SMulCommClass (↥H) C B] {g : G} (hg : g ∈ H) (x : C) : g • (algebraMap C B) x = (algebraMap C B) x

Alias of Subgroup.smul_algebraMap.

@[deprecated IsGaloisGroup.smul_mem_of_normal (since := "2026-05-28")]

theorem smul_mem_of_normal (G : Type u_1) (B : Type u_3) [Group G] [Semiring B] [MulSemiringAction G B] {C : Type u_4} [CommSemiring C] [Algebra C B] (N : Subgroup G) [hN : N.Normal] [hC : IsGaloisGroup (↥N) C B] (g : G) (x : C) : g • (algebraMap C B) x ∈ Set.range ⇑(algebraMap C B)

Alias of IsGaloisGroup.smul_mem_of_normal.

instance instIsGaloisGroupSubtypeMemSubringRangeAlgebraMap (G : Type u_1) (A : Type u_2) (B : Type u_3) [Group G] [CommRing A] [CommRing B] [MulSemiringAction G B] [Algebra A B] [IsGaloisGroup G A B] : IsGaloisGroup G (↥(algebraMap A B).range) B

theorem IsGaloisGroup.to_isFractionRing_of_isIntegral (G : Type u_1) (A : Type u_2) (B : Type u_3) (K : Type u_4) (L : Type u_5) [Group G] [CommRing A] [CommRing B] [MulSemiringAction G B] [Algebra A B] [Field K] [Field L] [Algebra K L] [Algebra A K] [Algebra B L] [Algebra A L] [IsFractionRing A K] [IsFractionRing B L] [IsScalarTower A K L] [IsScalarTower A B L] [MulSemiringAction G L] [SMulDistribClass G B L] [Algebra.IsIntegral A B] [hGAB : IsGaloisGroup G A B] : IsGaloisGroup G K L

IsGaloisGroup for rings implies IsGaloisGroup for their fraction fields.

theorem IsGaloisGroup.to_isFractionRing (G : Type u_1) (A : Type u_2) (B : Type u_3) (K : Type u_4) (L : Type u_5) [Group G] [CommRing A] [CommRing B] [MulSemiringAction G B] [Algebra A B] [Field K] [Field L] [Algebra K L] [Algebra A K] [Algebra B L] [Algebra A L] [IsFractionRing A K] [IsFractionRing B L] [IsScalarTower A K L] [IsScalarTower A B L] [MulSemiringAction G L] [SMulDistribClass G B L] [Finite G] [hGAB : IsGaloisGroup G A B] : IsGaloisGroup G K L

IsGaloisGroup for rings implies IsGaloisGroup for their fraction fields.

theorem IsGaloisGroup.of_isFractionRing (G : Type u_1) (A : Type u_2) (B : Type u_3) (K : Type u_4) (L : Type u_5) [Group G] [CommRing A] [CommRing B] [MulSemiringAction G B] [Algebra A B] [Field K] [Field L] [Algebra K L] [Algebra A K] [Algebra B L] [Algebra A L] [IsFractionRing A K] [IsFractionRing B L] [IsScalarTower A K L] [IsScalarTower A B L] [MulSemiringAction G L] [SMulDistribClass G B L] [hGKL : IsGaloisGroup G K L] [IsIntegrallyClosed A] [Algebra.IsIntegral A B] : IsGaloisGroup G A B

If B is an integral extension of an integrally closed domain A, then IsGaloisGroup for their fraction fields implies IsGaloisGroup for these rings.

theorem IsGaloisGroup.iff_isFractionRing (G : Type u_1) (A : Type u_2) (B : Type u_3) (K : Type u_4) (L : Type u_5) [Group G] [CommRing A] [CommRing B] [MulSemiringAction G B] [Algebra A B] [Field K] [Field L] [Algebra K L] [Algebra A K] [Algebra B L] [Algebra A L] [IsFractionRing A K] [IsFractionRing B L] [IsScalarTower A K L] [IsScalarTower A B L] [MulSemiringAction G L] [SMulDistribClass G B L] [Finite G] [IsIntegrallyClosed A] : IsGaloisGroup G A B ↔ Algebra.IsIntegral A B ∧ IsGaloisGroup G K L

If G is finite and A is integrally closed then IsGaloisGroup G A B is equivalent to B/A being integral and the fields of fractions Frac(B)/Frac(A) being Galois with Galois group G.

@[deprecated IsFractionRing.mulSemiringAction (since := "2026-04-20")]

def FractionRing.mulSemiringAction_of_isGaloisGroup (G : Type u_10) (B : Type u_12) (L : Type u_14) [Group G] [CommRing B] [MulSemiringAction G B] [Field L] [Algebra B L] [IsFractionRing B L] : MulSemiringAction G L

Alias of IsFractionRing.mulSemiringAction.

Equations

• FractionRing.mulSemiringAction_of_isGaloisGroup = IsFractionRing.mulSemiringAction

instance IsGaloisGroup.toFractionRing (G : Type u_1) (A : Type u_2) (B : Type u_3) [Group G] [CommRing A] [CommRing B] [MulSemiringAction G B] [Algebra A B] [IsDomain A] [IsDomain B] [Finite G] [IsGaloisGroup G A B] [Algebra (FractionRing A) (FractionRing B)] [IsScalarTower A (FractionRing A) (FractionRing B)] : IsGaloisGroup G (FractionRing A) (FractionRing B)

If G is finite and IsGaloisGroup G A B with A and B domains, then G is also a Galois group for FractionRing B / FractionRing A for the action defined by IsFractionRing.mulSemiringAction.

noncomputable def IsGaloisGroup.mulEquivAlgEquiv (G : Type u_1) [Group G] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] [MulSemiringAction G B] [IsGaloisGroup G A B] [Finite G] : G ≃* B ≃ₐ[A] B

If G is a finite Galois group for B/A, then G is isomorphic to Gal(B/A).

Equations

• IsGaloisGroup.mulEquivAlgEquiv G A B = MulEquiv.ofBijective (MulSemiringAction.toAlgAut G A B) ⋯

@[simp]

theorem IsGaloisGroup.mulEquivAlgEquiv_apply_symm_apply (G : Type u_1) [Group G] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] [MulSemiringAction G B] [IsGaloisGroup G A B] [Finite G] (a : G) (a✝ : B) : ((mulEquivAlgEquiv G A B) a).symm a✝ = a⁻¹ • a✝

@[simp]

theorem IsGaloisGroup.mulEquivAlgEquiv_apply_apply (G : Type u_1) [Group G] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] [MulSemiringAction G B] [IsGaloisGroup G A B] [Finite G] (a : G) (a✝ : B) : ((mulEquivAlgEquiv G A B) a) a✝ = a • a✝

@[simp]

theorem IsGaloisGroup.mulEquivAlgEquiv_symm_apply (G : Type u_1) [Group G] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] [MulSemiringAction G B] [IsGaloisGroup G A B] [Finite G] (b : B ≃ₐ[A] B) : (mulEquivAlgEquiv G A B).symm b = Function.surjInv ⋯ b

instance IsGaloisGroup.instSubtypeMemSubgroupSubalgebraSubalgebra (G : Type u_1) [Group G] (H : Subgroup G) (R : Type u_2) (S : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [MulSemiringAction G S] [hGKL : IsGaloisGroup G R S] : IsGaloisGroup (↥H) (↥(FixedPoints.subalgebra R S ↥H)) S

@[implicit_reducible]

noncomputable def IsGaloisGroup.smulOfNormal (G : Type u_1) [Group G] (B : Type u_3) (C : Type u_4) [Semiring C] [MulSemiringAction G C] (N : Subgroup G) [CommSemiring B] [Algebra B C] [N.Normal] [IsGaloisGroup (↥N) B C] : SMul G B

If N is a normal subgroup of G and IsGaloisGroup N B C, then G acts on B. For g : G and x : B, g • x is the unique element of B whose image in C is g • algebraMap B C x, see algebraMap_smulOfNormal.

Equations

• IsGaloisGroup.smulOfNormal G B C N = { smul := fun (g : G) (x : B) => Exists.choose ⋯ }

@[simp]

theorem IsGaloisGroup.algebraMap_smulOfNormal (G : Type u_1) [Group G] (B : Type u_3) (C : Type u_4) [Semiring C] [MulSemiringAction G C] (N : Subgroup G) [CommSemiring B] [Algebra B C] [N.Normal] [IsGaloisGroup (↥N) B C] (g : G) (x : B) : (algebraMap B C) (g • x) = g • (algebraMap B C) x

instance IsGaloisGroup.smulDistribClass_smulOfNormal (G : Type u_1) [Group G] (B : Type u_3) (C : Type u_4) [Semiring C] [MulSemiringAction G C] (N : Subgroup G) [CommSemiring B] [Algebra B C] [N.Normal] [IsGaloisGroup (↥N) B C] : SMulDistribClass G B C

If N is normal and IsGaloisGroup N B C, the action smulOfNormal G B C satisfies SMulDistribClass G B C.

@[implicit_reducible]

noncomputable def IsGaloisGroup.mulSemiringActionOfNormal (G : Type u_1) [Group G] (B : Type u_3) (C : Type u_4) [Semiring C] [MulSemiringAction G C] (N : Subgroup G) [CommSemiring B] [Algebra B C] [FaithfulSMul B C] [IsGaloisGroup (↥N) B C] [N.Normal] : MulSemiringAction G B

If N is a normal subgroup of G and IsGaloisGroup N B C, then G acts on B as a MulSemiringAction, via the action defined in smulOfNormal.

Equations

• IsGaloisGroup.mulSemiringActionOfNormal G B C N = mulSemiringActionOfSmulDistribClass B C G

@[implicit_reducible]

noncomputable def IsGaloisGroup.mulSemiringActionQuotient (G : Type u_1) [Group G] (B : Type u_3) (C : Type u_4) [Semiring C] [MulSemiringAction G C] (N : Subgroup G) [CommSemiring B] [Algebra B C] [FaithfulSMul B C] [IsGaloisGroup (↥N) B C] [N.Normal] : MulSemiringAction (G ⧸ N) B

If N is a normal subgroup of G and IsGaloisGroup N B C, then the quotient group G ⧸ N acts on B by (g : G ⧸ N) • x = g • x.

Equations

• One or more equations did not get rendered due to their size.

theorem IsGaloisGroup.mulSemiringActionQuotient_smul_def (G : Type u_1) [Group G] (B : Type u_3) (C : Type u_4) [Semiring C] [MulSemiringAction G C] (N : Subgroup G) [CommSemiring B] [Algebra B C] [FaithfulSMul B C] [MulSemiringAction G B] [SMulDistribClass G B C] [IsGaloisGroup (↥N) B C] [N.Normal] (g : G) (b : B) : ↑g • b = g • b

instance IsGaloisGroup.isScalarTower_mulSemiringActionQuotient (G : Type u_1) [Group G] (B : Type u_3) (C : Type u_4) [Semiring C] [MulSemiringAction G C] (N : Subgroup G) [CommSemiring B] [Algebra B C] [FaithfulSMul B C] [MulSemiringAction G B] [SMulDistribClass G B C] [IsGaloisGroup (↥N) B C] [N.Normal] : IsScalarTower G (G ⧸ N) B

@[implicit_reducible]

def IsGaloisGroup.smulCommClassQuotient (G : Type u_1) [Group G] (A : Type u_2) (B : Type u_3) (C : Type u_4) [CommSemiring A] [Semiring C] [Algebra A C] [MulSemiringAction G C] (N : Subgroup G) [CommSemiring B] [Algebra B C] [FaithfulSMul B C] [N.Normal] [Algebra A B] [IsScalarTower A B C] [SMulCommClass G A C] [MulSemiringAction G B] [MulAction (G ⧸ N) B] [SMulDistribClass G B C] [IsScalarTower G (G ⧸ N) B] : SMulCommClass (G ⧸ N) A B

If G acts on C commuting with A, then the action of G ⧸ N on B commutes with A.

Equations

• ⋯ = ⋯

@[implicit_reducible]

noncomputable instance IsGaloisGroup.instMulSemiringActionQuotientSubgroupSubtypeMemIntermediateField (G : Type u_1) [Group G] {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (F : IntermediateField K L) (N : Subgroup G) [N.Normal] [IsGaloisGroup (↥N) (↥F) L] : MulSemiringAction (G ⧸ N) ↥F

Equations

• IsGaloisGroup.instMulSemiringActionQuotientSubgroupSubtypeMemIntermediateField G F N = IsGaloisGroup.mulSemiringActionQuotient G (↥F) L N

instance IsGaloisGroup.instSMulCommClassQuotientSubgroupSubtypeMemIntermediateFieldOfSMulDistribClassOfIsScalarTower (G : Type u_1) [Group G] {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (F : IntermediateField K L) (N : Subgroup G) [N.Normal] [IsGaloisGroup (↥N) (↥F) L] [SMulCommClass G K L] [MulSemiringAction G ↥F] [SMulDistribClass G (↥F) L] [IsScalarTower G (G ⧸ N) ↥F] : SMulCommClass (G ⧸ N) K ↥F