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 field A). In this generality, the name IsGaloisGroup is a bit of a misnomer, since IsGaloisGroup G A B corresponds to the fields of fractions Frac(B)/Frac(A) being a Galois extension of fields, rather than B/A being étale (for instance).

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.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] [FiniteDimensional K L] [IsGalois K L] : IsGaloisGroup Gal(L/K) K L

If L/K is a finite 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

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

Equations

• IsGaloisGroup.mulEquivAlgEquiv G K L = MulEquiv.ofBijective (MulSemiringAction.toAlgAut G K L) ⋯

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

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

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.

Equations

• IsGaloisGroup.mulEquivCongr G H K L = (IsGaloisGroup.mulEquivAlgEquiv G K L).trans (IsGaloisGroup.mulEquivAlgEquiv H K L).symm

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