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_4) [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_4} [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [hG : IsGaloisGroup G A B] {H : Type u_5} [Group H] [MulSemiringAction H B] (e : H ≃* G) (he : ∀ (h : H) (x : B), e h • x = h • x) : IsGaloisGroup H A B

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

@[simp]

theorem IsGaloisGroup.top_iff {G : Type u_1} {A : Type u_2} {B : Type u_4} [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] : IsGaloisGroup (↥⊤) A B ↔ IsGaloisGroup G A B

instance IsGaloisGroup.instSubtypeMemSubgroupTop (G : Type u_1) (A : Type u_2) (B : Type u_4) [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [IsGaloisGroup G A B] : IsGaloisGroup (↥⊤) A B

theorem IsGaloisGroup.of_algEquiv (G : Type u_1) (A : Type u_2) (B : Type u_4) [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [hG : IsGaloisGroup G A B] (B' : Type u_5) [Semiring B'] [Algebra A B'] [MulSemiringAction G B'] (e : B ≃ₐ[A] B') (he : ∀ (g : G) (x : B), e (g • x) = g • e x) : IsGaloisGroup G A B'

theorem IsGaloisGroup.of_ringHom_surjective (G : Type u_1) (A : Type u_2) (A' : Type u_3) (B : Type u_4) [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [hG : IsGaloisGroup G A B] [CommSemiring A'] [Algebra A' B] (e : A →+* A') (he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a) (he' : Function.Surjective ⇑e) : IsGaloisGroup G A' B

theorem IsGaloisGroup.of_ringEquiv (G : Type u_1) (A : Type u_2) (A' : Type u_3) (B : Type u_4) [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [hG : IsGaloisGroup G A B] [CommSemiring A'] [Algebra A' B] (e : A ≃+* A') (he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a) : IsGaloisGroup G A' B

noncomputable def IsGaloisGroup.ringEquivFixedPoints (G : Type u_1) (A : Type u_2) (B : Type u_4) [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [hA : IsGaloisGroup G A B] [FaithfulSMul A B] : A ≃+* ↥(FixedPoints.subsemiring B G)

If B/A is Galois with Galois group G, then A is isomorphic to the subring of elements of B fixed by G.

Equations

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

@[simp]

theorem IsGaloisGroup.ringEquivFixedPoints_apply_coe (G : Type u_1) (A : Type u_2) (B : Type u_4) [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [hA : IsGaloisGroup G A B] [FaithfulSMul A B] (x : A) : ↑((ringEquivFixedPoints G A B) x) = (algebraMap A B) x

@[simp]

theorem IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply (G : Type u_1) (A : Type u_2) (B : Type u_4) [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [hA : IsGaloisGroup G A B] [FaithfulSMul A B] (x : ↥(FixedPoints.subsemiring B G)) : (algebraMap A B) ((ringEquivFixedPoints G A B).symm x) = ↑x

noncomputable def IsGaloisGroup.ringEquiv (G : Type u_1) (A : Type u_2) (A' : Type u_3) (B : Type u_4) [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [hA : IsGaloisGroup G A B] [FaithfulSMul A B] [CommSemiring A'] [Algebra A' B] [FaithfulSMul A' B] [hA' : IsGaloisGroup G A' B] : A ≃+* A'

If B/A and B/A' are Galois with the same Galois group, then A ≃+* A'.

Equations

• IsGaloisGroup.ringEquiv G A A' B = (IsGaloisGroup.ringEquivFixedPoints G A B).trans (IsGaloisGroup.ringEquivFixedPoints G A' B).symm

@[simp]

theorem IsGaloisGroup.algebraMap_ringEquiv_apply (G : Type u_1) (A : Type u_2) (A' : Type u_3) (B : Type u_4) [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [hA : IsGaloisGroup G A B] [FaithfulSMul A B] [CommSemiring A'] [Algebra A' B] [FaithfulSMul A' B] [hA' : IsGaloisGroup G A' B] (x : A) : (algebraMap A' B) ((ringEquiv G A A' B) x) = (algebraMap A B) x

@[simp]

theorem IsGaloisGroup.algebraMap_ringEquiv_symm_apply (G : Type u_1) (A : Type u_2) (A' : Type u_3) (B : Type u_4) [Group G] [CommSemiring A] [Semiring B] [Algebra A B] [MulSemiringAction G B] [hA : IsGaloisGroup G A B] [FaithfulSMul A B] [CommSemiring A'] [Algebra A' B] [FaithfulSMul A' B] [hA' : IsGaloisGroup G A' B] (x : A') : (algebraMap A B) ((ringEquiv G A A' B).symm x) = (algebraMap A' B) x