Predicate for Galois Groups

Given an action of a group G on an extension of fields L/K, we introduce a predicate IsGaloisGroup G K L saying 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.

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

G is a Galois group for L/K if the action of G on L is faithful with fixed field K. In particular, we do not assume that L is an algebraic extension of K.

See the implementation notes in this file for the meaning of this definition in the case of rings.

• faithful : FaithfulSMul G B
• commutes : SMulCommClass G A B
• isInvariant : Algebra.IsInvariant A B G

theorem IsGaloisGroup.of_mulEquiv {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [hG : IsGaloisGroup G A B] {H : Type u_4} [Group H] [MulSemiringAction H B] (e : H ≃* G) (he : ∀ (h : H) (x : B), e h • x = h • x) : IsGaloisGroup H A B

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.

noncomputable def FractionRing.mulSemiringAction_of_isGaloisGroup (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] [Module.IsTorsionFree A B] [IsGaloisGroup G A B] : MulSemiringAction G (FractionRing B)

Assume that IsGaloisGroup G A B with A and B domains, then G has a MulSemiringAction on FractionRing B. This cannot be an instance since Lean cannot figure out A.

theorem 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] [Module.IsTorsionFree A B] [Finite G] [IsGaloisGroup G A 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 A / FractionRing B for the action defined by FractionRing.mulSemiringAction_of_isGaloisGroup.

instance instIsGaloisGroupRingOfIntegersOfNumberField (K : Type u_6) (L : Type u_7) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (G : Type u_8) [Group G] [MulSemiringAction G L] [IsGaloisGroup G K L] : IsGaloisGroup G (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)

instance instIsGaloisGroupIntRingOfIntegersOfRat (L : Type u_6) [Field L] [NumberField L] (G : Type u_7) [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

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) (K : Type u_3) (L : Type u_4) [Group G] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [FiniteDimensional K L] [IsGaloisGroup G K L] : Finite G

noncomputable def IsGaloisGroup.mulEquivAlgEquiv (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] [Finite G] : G ≃* Gal(L/K)

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

@[simp]

theorem IsGaloisGroup.mulEquivAlgEquiv_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] [IsGaloisGroup G K L] [Finite G] (b : Gal(L/K)) : (mulEquivAlgEquiv G K L).symm b = Function.surjInv ⋯ b

@[simp]

theorem IsGaloisGroup.mulEquivAlgEquiv_apply_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] [IsGaloisGroup G K L] [Finite G] (a : G) (a✝ : L) : ((mulEquivAlgEquiv G K L) a) a✝ = a • a✝

@[simp]

theorem IsGaloisGroup.mulEquivAlgEquiv_apply_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] [IsGaloisGroup G K L] [Finite G] (a : G) (a✝ : L) : ((mulEquivAlgEquiv G K L) a).symm a✝ = a⁻¹ • a✝

noncomputable def IsGaloisGroup.mulEquivCongr (G : Type u_1) (H : Type u_2) (K : Type u_3) (L : Type u_4) [Group G] [Group H] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [MulSemiringAction H L] [IsGaloisGroup G K L] [Finite G] [IsGaloisGroup H K L] [Finite H] : G ≃* H

If G and H are finite Galois groups for L/K, then G is isomorphic to H.

@[simp]

theorem IsGaloisGroup.mulEquivCongr_apply_smul (G : Type u_1) (H : Type u_2) (K : Type u_3) (L : Type u_4) [Group G] [Group H] [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [MulSemiringAction H L] [IsGaloisGroup G K L] [Finite G] [IsGaloisGroup H K L] [Finite H] (g : G) (x : L) : (mulEquivCongr G H K L) g • x = g • x

@[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] [IsGaloisGroup G K L] [Finite G] (F : IntermediateField K L) : Subgroup.map (↑(mulEquivAlgEquiv G K L)) (fixingSubgroup G ↑F) = F.fixingSubgroup

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

@[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

@[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.

@[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