Galois Groups of Fields

Given an action of a group G on an extension of fields L/K, the predicate IsGaloisGroup G K L states that G acts faithfully on L with fixed field K. In particular, we do not assume that L is an algebraic extension of K.

Implementation notes

We actually define IsGaloisGroup G A B for extensions of rings B/A, with the same definition (faithful action on B with fixed ring A). This definition turns out to axiomatize a common setup in algebraic number theory where a Galois group Gal(L/K) acts on an extension of subrings B/A (e.g., rings of integers). In particular, there are theorems in algebraic number theory that naturally assume [IsGaloisGroup G A B] and whose statements would otherwise require assuming (K L : Type*) [Field K] [Field L] [Algebra K L] [IsGalois K L] (along with predicates relating K and L to the rings A and B) despite K and L not appearing in the conclusion.

Unfortunately, this definition of IsGaloisGroup G A B for extensions of rings B/A is nonstandard and clashes with other notions such as the étale fundamental group. In particular, 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 (see IsGaloisGroup.iff_isFractionRing), rather than B/A being étale for instance.

But in the absence of a more suitable name, the utility of the predicate IsGaloisGroup G A B for extensions of rings B/A seems to outweigh these terminological issues.

instance instIsGaloisGroupRingOfIntegersOfNumberField (K : Type u_1) (L : Type u_2) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (G : Type u_3) [Group G] [MulSemiringAction G L] [IsGaloisGroup G K L] : IsGaloisGroup G (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)

instance instIsGaloisGroupIntRingOfIntegersOfRat (L : Type u_1) [Field L] [NumberField L] (G : Type u_2) [Group G] [MulSemiringAction G L] [IsGaloisGroup G ℚ L] : IsGaloisGroup G ℤ (NumberField.RingOfIntegers L)

theorem IsGaloisGroup.fixedPoints_eq_bot (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [IsGaloisGroup G K L] : FixedPoints.intermediateField G = ⊥

theorem IsGaloisGroup.isGalois (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [Finite G] [IsGaloisGroup G K L] : IsGalois K L

If G is a finite Galois group for L/K, then L/K is a Galois extension.

instance IsGaloisGroup.of_isGalois (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] [IsGalois K L] : IsGaloisGroup Gal(L/K) K L

If L/K is a Galois extension, then Gal(L/K) is a Galois group for L/K.

theorem IsGaloisGroup.card_eq_finrank (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [IsGaloisGroup G K L] : Nat.card G = Module.finrank K L

The cardinality of a Galois group equals the degree of the field extension.

See IsGaloisGroup.card_eq_finrank' for a ring-theoretic generalization assuming finiteness.

theorem IsGaloisGroup.finiteDimensional (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [Finite G] [IsGaloisGroup G K L] : FiniteDimensional K L

theorem IsGaloisGroup.finite (G : Type u_1) [Group G] (R : Type u_5) (B : Type u_6) [CommRing R] [CommRing B] [Algebra R B] [Module.Finite R B] [IsDomain B] [MulSemiringAction G B] [IsGaloisGroup G R B] : Finite G

theorem IsGaloisGroup.card_eq_finrank' (G : Type u_1) [Group G] (A : Type u_5) (B : Type u_6) [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] [MulSemiringAction G B] [IsGaloisGroup G A B] [Finite G] : Nat.card G = Module.finrank A B

The cardinality of a Galois group of B/A equals the rank of B as an A-module.

See IsGaloisGroup.card_eq_finrank, a field-theoretic version that does not assume finiteness.

@[simp]

theorem IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [Finite G] [IsGaloisGroup G K L] (F : IntermediateField K L) : Subgroup.map (↑(mulEquivAlgEquiv G K L)) (fixingSubgroup G ↑F) = F.fixingSubgroup

noncomputable def IsGaloisGroup.mulEquivCongr (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] [MulSemiringAction G B] [MulSemiringAction G' B] [IsGaloisGroup G A B] [IsGaloisGroup G' A B] [Finite G] [Finite G'] : G ≃* G'

If G and G' are finite Galois groups for B/A, then G is isomorphic to G'.

Equations

• IsGaloisGroup.mulEquivCongr G G' A B = (IsGaloisGroup.mulEquivAlgEquiv G A B).trans (IsGaloisGroup.mulEquivAlgEquiv G' A B).symm

@[simp]

theorem IsGaloisGroup.mulEquivCongr_apply_smul (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] [MulSemiringAction G B] [MulSemiringAction G' B] [IsGaloisGroup G A B] [IsGaloisGroup G' A B] [Finite G] [Finite G'] (g : G) (x : B) : (mulEquivCongr G G' A B) g • x = g • x

@[simp]

theorem IsGaloisGroup.mulEquivCongr_symm_apply_smul (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] [MulSemiringAction G B] [MulSemiringAction G' B] [IsGaloisGroup G A B] [IsGaloisGroup G' A B] [Finite G] [Finite G'] (g : G') (x : B) : (mulEquivCongr G G' A B).symm g • x = g • x

@[deprecated IsGaloisGroup.mulEquivCongr (since := "2026-06-19")]

def IsGaloisGroup.mulEquivCongr' (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] [MulSemiringAction G B] [MulSemiringAction G' B] [IsGaloisGroup G A B] [IsGaloisGroup G' A B] [Finite G] [Finite G'] : G ≃* G'

Alias of IsGaloisGroup.mulEquivCongr.

---

If G and G' are finite Galois groups for B/A, then G is isomorphic to G'.

Equations

• IsGaloisGroup.mulEquivCongr' = IsGaloisGroup.mulEquivCongr

@[deprecated IsGaloisGroup.mulEquivCongr_apply_smul (since := "2026-06-19")]

theorem IsGaloisGroup.mulEquivCongr'_apply_smul (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] [MulSemiringAction G B] [MulSemiringAction G' B] [IsGaloisGroup G A B] [IsGaloisGroup G' A B] [Finite G] [Finite G'] (g : G) (x : B) : (mulEquivCongr G G' A B) g • x = g • x

Alias of IsGaloisGroup.mulEquivCongr_apply_smul.

theorem IsGaloisGroup.mulEquivCongr_mapSubgroup_fixingSubgroup (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) [CommRing A] [CommRing B] [IsDomain B] [Algebra A B] [FaithfulSMul A B] [MulSemiringAction G B] [MulSemiringAction G' B] [IsGaloisGroup G A B] [IsGaloisGroup G' A B] [Finite G] [Finite G'] (S : Set B) : Subgroup.map (↑(mulEquivCongr G G' A B)) (fixingSubgroup G S) = fixingSubgroup G' S

instance IsGaloisGroup.subgroup (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H : Subgroup G) [hGKL : IsGaloisGroup G K L] : IsGaloisGroup (↥H) (↥(FixedPoints.intermediateField ↥H)) L

theorem IsGaloisGroup.fixedPoints_of_isGaloisGroup (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H : Subgroup G) (F : IntermediateField K L) [hGKL : IsGaloisGroup G K L] [hHFL : IsGaloisGroup (↥H) (↥F) L] : FixedPoints.intermediateField ↥H = F

theorem IsGaloisGroup.of_fixedPoints_eq (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H : Subgroup G) (F : IntermediateField K L) [hGKL : IsGaloisGroup G K L] (hF : FixedPoints.intermediateField ↥H = F) : IsGaloisGroup (↥H) (↥F) L

theorem IsGaloisGroup.subgroup_iff {G : Type u_1} {K : Type u_3} {L : Type u_4} [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] {H : Subgroup G} {F : IntermediateField K L} [hGKL : IsGaloisGroup G K L] : IsGaloisGroup (↥H) (↥F) L ↔ FixedPoints.intermediateField ↥H = F

@[simp]

theorem IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H : Subgroup G) [IsGaloisGroup G K L] : Module.finrank (↥(FixedPoints.intermediateField ↥H)) L = Nat.card ↥H

theorem IsGaloisGroup.of_mulEquiv_algEquiv {G : Type u_1} {K : Type u_3} {L : Type u_4} [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [IsGalois K L] (e : G ≃* Gal(L/K)) (he : ∀ (g : G) (x : L), (e g) x = g • x) : IsGaloisGroup G K L

instance IsGaloisGroup.fixedPoints (G : Type u_1) (L : Type u_4) [Group G] [Field L] [MulSemiringAction G L] [Finite G] [FaithfulSMul G L] : IsGaloisGroup G (↥(FixedPoints.subfield G L)) L

instance IsGaloisGroup.intermediateField (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (F : IntermediateField K L) [Finite G] [hGKL : IsGaloisGroup G K L] : IsGaloisGroup (↥(fixingSubgroup G ↑F)) (↥F) L

theorem IsGaloisGroup.of_isScalarTower (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [Finite G] [IsGaloisGroup G K L] (E : Type u_5) [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] : IsGaloisGroup (↥(fixingSubgroup G (Set.range ⇑(algebraMap E L)))) E L

If G is a Galois group on L/K and L/E/K is a tower of field extensions, then the fixing subgroup of the image of E in L is a Galois group on L/E.

@[simp]

theorem IsGaloisGroup.card_fixingSubgroup_eq_finrank (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (F : IntermediateField K L) [Finite G] [IsGaloisGroup G K L] : Nat.card ↥(fixingSubgroup G ↑F) = Module.finrank (↥F) L

theorem IsGaloisGroup.fixingSubgroup_le_of_le (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (F F' : IntermediateField K L) (h : F ≤ F') : fixingSubgroup G ↑F' ≤ fixingSubgroup G ↑F

@[simp]

theorem IsGaloisGroup.fixingSubgroup_bot (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [SMulCommClass G K L] : fixingSubgroup G ↑⊥ = ⊤

@[simp]

theorem IsGaloisGroup.fixedPoints_bot (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [SMulCommClass G K L] : FixedPoints.intermediateField ↥⊥ = ⊤

theorem IsGaloisGroup.le_fixedPoints_iff_le_fixingSubgroup (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H : Subgroup G) (F : IntermediateField K L) [SMulCommClass G K L] : F ≤ FixedPoints.intermediateField ↥H ↔ H ≤ fixingSubgroup G ↑F

theorem IsGaloisGroup.fixedPoints_le_of_le (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H H' : Subgroup G) [SMulCommClass G K L] (h : H ≤ H') : FixedPoints.intermediateField ↥H' ≤ FixedPoints.intermediateField ↥H

theorem IsGaloisGroup.fixingSubgroup_top (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] : fixingSubgroup G ↑⊤ = ⊥

@[simp]

theorem IsGaloisGroup.fixedPoints_top (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] : FixedPoints.intermediateField ↥⊤ = ⊥

noncomputable def IsGaloisGroup.intermediateFieldEquivSubgroup (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] [Finite G] : IntermediateField K L ≃o (Subgroup G)ᵒᵈ

The Galois correspondence from intermediate fields to subgroups.

Equations

• IsGaloisGroup.intermediateFieldEquivSubgroup G K L = IsGalois.intermediateFieldEquivSubgroup.trans (IsGaloisGroup.mulEquivAlgEquiv G K L).comapSubgroup.dual

@[simp]

theorem IsGaloisGroup.intermediateFieldEquivSubgroup_apply (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] [Finite G] {F : IntermediateField K L} : (intermediateFieldEquivSubgroup G K L) F = OrderDual.toDual (fixingSubgroup G ↑F)

theorem IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] [Finite G] {F : IntermediateField K L} : OrderDual.ofDual ((intermediateFieldEquivSubgroup G K L) F) = fixingSubgroup G ↑F

@[simp]

theorem IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] [Finite G] {H : (Subgroup G)ᵒᵈ} : (intermediateFieldEquivSubgroup G K L).symm H = FixedPoints.intermediateField ↥(OrderDual.ofDual H)

theorem IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] [Finite G] {H : Subgroup G} : (intermediateFieldEquivSubgroup G K L).symm (OrderDual.toDual H) = FixedPoints.intermediateField ↥H

@[simp]

theorem IsGaloisGroup.fixingSubgroup_fixedPoints (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H : Subgroup G) [hGKL : IsGaloisGroup G K L] [Finite G] : fixingSubgroup G ↑(FixedPoints.intermediateField ↥H) = H

@[simp]

theorem IsGaloisGroup.fixedPoints_fixingSubgroup (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (F : IntermediateField K L) [hGKL : IsGaloisGroup G K L] [Finite G] : FixedPoints.intermediateField ↥(fixingSubgroup G ↑F) = F

theorem IsGaloisGroup.fixedPoints_eq_range_algebraMap (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H : Subgroup G) [hGKL : IsGaloisGroup G K L] (B : Type u_5) [CommSemiring B] [Algebra B L] [IsGaloisGroup (↥H) B L] : ↑(FixedPoints.intermediateField ↥H) = Set.range ⇑(algebraMap B L)

If G acts as a Galois group on L/K and the subgroup H acts as a Galois group on L/B, then the fixed points of H equals the range of algebraMap B L.

theorem IsGaloisGroup.fixingSubgroup_range_algebraMap' (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H : Subgroup G) [hGKL : IsGaloisGroup G K L] [Finite G] (B : Type u_5) [CommSemiring B] [Algebra B L] [IsGaloisGroup (↥H) B L] : fixingSubgroup G (Set.range ⇑(algebraMap B L)) = H

If G acts as a Galois group on L/K and the subgroup H acts as a Galois group on L/B, then the fixing subgroup of algebraMap B L inside G equals H. See fixingSubgroup_range_algebraMap for a more general version.

theorem IsGaloisGroup.fixingSubgroup_range_algebraMap (G : Type u_1) [Group G] [Finite G] (A : Type u_5) (B : Type u_6) (C : Type u_7) (H : Subgroup G) [CommRing A] [CommRing B] [CommRing C] [IsDomain C] [Algebra A C] [FaithfulSMul A C] [MulSemiringAction G C] [hGAC : IsGaloisGroup G A C] [Algebra B C] [FaithfulSMul B C] [hH : IsGaloisGroup (↥H) B C] : fixingSubgroup G (Set.range ⇑(algebraMap B C)) = H

If G acts on a domain C with IsGaloisGroup G A C, and a subgroup H acts on C with IsGaloisGroup H B C, then the fixing subgroup of algebraMap B C equals H.

theorem IsGaloisGroup.normal_of_isGalois (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H : Subgroup G) [hGKL : IsGaloisGroup G K L] (E : Type u_5) [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] [Finite G] [IsGaloisGroup (↥H) E L] [IsGalois K E] : H.Normal

If G is a finite Galois group for L/K, H is a Galois group for L/E, and E/K is Galois, then H is a normal subgroup of G.

theorem IsGaloisGroup.quotient (G : Type u_1) [Group G] (A : Type u_5) (B : Type u_6) (C : Type u_7) [CommRing A] [CommRing B] [CommRing C] [IsDomain C] [Algebra A B] [Algebra A C] [Algebra B C] [FaithfulSMul A B] [FaithfulSMul B C] [IsScalarTower A B C] [Finite G] (N : Subgroup G) [N.Normal] [MulSemiringAction G C] [hG : IsGaloisGroup G A C] [MulSemiringAction G B] [MulSemiringAction (G ⧸ N) B] [SMulCommClass (G ⧸ N) A B] [SMulDistribClass G B C] [IsScalarTower G (G ⧸ N) B] [IsGaloisGroup (↥N) B C] : IsGaloisGroup (G ⧸ N) A B

If G is a Galois group for C/A, and the normal subgroup N ≤ G is a Galois group for C/B, then the quotient G ⧸ N is a Galois group for B/A.

noncomputable def IsGaloisGroup.quotientMulEquiv (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7) [CommRing A] [CommRing B] [CommRing C] [IsDomain C] [Algebra A B] [Algebra A C] [Algebra B C] [FaithfulSMul A B] [FaithfulSMul B C] [IsScalarTower A B C] [Finite G] [Finite G'] (N : Subgroup G) [N.Normal] [MulSemiringAction G C] [IsGaloisGroup G A C] [IsGaloisGroup (↥N) B C] [MulSemiringAction G' B] [IsGaloisGroup G' A B] : G ⧸ N ≃* G'

If G is a Galois group for C/A, the normal subgroup N ≤ G is a Galois group for C/B, and G' is a Galois group for B/A, then G ⧸ N ≃* G'.

Equations

• IsGaloisGroup.quotientMulEquiv G G' A B C N = IsGaloisGroup.mulEquivCongr (G ⧸ N) G' A B

@[simp]

theorem IsGaloisGroup.algebraMap_quotientMulEquiv_smul (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7) [CommRing A] [CommRing B] [CommRing C] [IsDomain C] [Algebra A B] [Algebra A C] [Algebra B C] [FaithfulSMul A B] [FaithfulSMul B C] [IsScalarTower A B C] [Finite G] [Finite G'] (N : Subgroup G) [N.Normal] [MulSemiringAction G C] [IsGaloisGroup G A C] [IsGaloisGroup (↥N) B C] [MulSemiringAction G' B] [IsGaloisGroup G' A B] (g : G) (x : B) : (algebraMap B C) ((quotientMulEquiv G G' A B C N) ↑g • x) = g • (algebraMap B C) x

noncomputable def IsGaloisGroup.restrictHom (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7) [CommRing A] [CommRing B] [CommRing C] [IsDomain C] [Algebra A B] [Algebra A C] [Algebra B C] [FaithfulSMul A B] [FaithfulSMul B C] [IsScalarTower A B C] [Finite G] [Finite G'] [MulSemiringAction G C] [IsGaloisGroup G A C] [MulSemiringAction G' B] [IsGaloisGroup G' A B] : G →* G'

The restriction homomorphism from the Galois group of C/A to the Galois group of B/A where C/B/A is a tower of domains with C/A and B/A Galois.

Equations

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

@[simp]

theorem IsGaloisGroup.algebraMap_restrictHom_smul (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7) [CommRing A] [CommRing B] [CommRing C] [IsDomain C] [Algebra A B] [Algebra A C] [Algebra B C] [FaithfulSMul A B] [FaithfulSMul B C] [IsScalarTower A B C] [Finite G] [Finite G'] [MulSemiringAction G C] [IsGaloisGroup G A C] [MulSemiringAction G' B] [IsGaloisGroup G' A B] (g : G) (x : B) : (algebraMap B C) ((restrictHom G G' A B C) g • x) = g • (algebraMap B C) x

theorem IsGaloisGroup.restrictHom_surjective (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7) [CommRing A] [CommRing B] [CommRing C] [IsDomain C] [Algebra A B] [Algebra A C] [Algebra B C] [FaithfulSMul A B] [FaithfulSMul B C] [IsScalarTower A B C] [Finite G] [Finite G'] [MulSemiringAction G C] [IsGaloisGroup G A C] [MulSemiringAction G' B] [IsGaloisGroup G' A B] : Function.Surjective ⇑(restrictHom G G' A B C)

theorem IsGaloisGroup.restrictHom_smul_under (G : Type u_1) (G' : Type u_2) [Group G] [Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7) [CommRing A] [CommRing B] [CommRing C] [IsDomain C] [Algebra A B] [Algebra A C] [Algebra B C] [FaithfulSMul A B] [FaithfulSMul B C] [IsScalarTower A B C] [Finite G] [Finite G'] [MulSemiringAction G C] [IsGaloisGroup G A C] [MulSemiringAction G' B] [IsGaloisGroup G' A B] (g : G) (I : Ideal C) : (restrictHom G G' A B C) g • Ideal.under B I = Ideal.under B (g • I)

instance IsGaloisGroup.instQuotientSubgroupSubtypeMemIntermediateFieldOfFinite (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (F : IntermediateField K L) (N : Subgroup G) [N.Normal] [IsGaloisGroup (↥N) (↥F) L] [Finite G] [IsGaloisGroup G K L] : IsGaloisGroup (G ⧸ N) K ↥F

If G is a finite Galois group for L/K and N is a normal subgroup of G that is a Galois group for L/F, then the quotient group G ⧸ N is a Galois group for F/K.

theorem IsGaloisGroup.map_quotientMk' (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H : Subgroup G) (F : IntermediateField K L) (N : Subgroup G) [N.Normal] [IsGaloisGroup (↥N) (↥F) L] (E : IntermediateField K L) [hE : IsGaloisGroup (↥H) (↥E) L] [Finite G] [IsGaloisGroup G K L] (h : E ≤ F) : IsGaloisGroup ↥(Subgroup.map (QuotientGroup.mk' N) H) ↥E ↥F

If G is a finite Galois group for L/K, N is a normal subgroup that is a Galois group for L/F, and H is a subgroup that is a Galois group for L/E with E ≤ F, then the image of H under the canonical quotient map G → G ⧸ N is a Galois group for F/E.

@[deprecated IsGaloisGroup.map_quotientMk' (since := "2026-04-21")]

theorem IsGaloisGroup.quotientMap (G : Type u_1) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] (H : Subgroup G) (F : IntermediateField K L) (N : Subgroup G) [N.Normal] [IsGaloisGroup (↥N) (↥F) L] (E : IntermediateField K L) [hE : IsGaloisGroup (↥H) (↥E) L] [Finite G] [IsGaloisGroup G K L] (h : E ≤ F) : IsGaloisGroup ↥(Subgroup.map (QuotientGroup.mk' N) H) ↥E ↥F

Alias of IsGaloisGroup.map_quotientMk'.

---

If G is a finite Galois group for L/K, N is a normal subgroup that is a Galois group for L/F, and H is a subgroup that is a Galois group for L/E with E ≤ F, then the image of H under the canonical quotient map G → G ⧸ N is a Galois group for F/E.