The index of a subgroup of a Galois group

For a tower of fields E ⊆ F ⊆ K in which K is Galois over E with Galois group G and Galois over F with Galois group a subgroup H of G, the index of H in G is the degree [F : E]. This is the counting half of the Galois correspondence, in the IsGaloisGroup form: Mathlib's IsGaloisGroup.card_eq_finrank gives Nat.card H = [K : F] and Nat.card G = [K : E], and the tower law cancels [K : F].

Main results

• IsGaloisGroup.index_eq_finrank: H.index = Module.finrank E F.

Provenance

Built directly on Mathlib's IsGaloisGroup.card_eq_finrank and Module.finrank_mul_finrank.

theorem IsGaloisGroup.index_eq_finrank {G : Type u_1} [Group G] (H : Subgroup G) (E : Type u_2) (F : Type u_3) (K : Type u_4) [Field E] [Field F] [Field K] [Algebra E F] [Algebra F K] [Algebra E K] [IsScalarTower E F K] [FiniteDimensional F K] [MulSemiringAction G K] [IsGaloisGroup G E K] [IsGaloisGroup (↥H) F K] : H.index = Module.finrank E F

The index of a subgroup is the degree of its fixed field. If K is Galois over E with Galois group G and H is a subgroup of G whose fixed field is F, then H.index = [F : E]. This is IsGaloisGroup.card_eq_finrank at the two ends of the tower E ⊆ F ⊆ K, combined with the tower law for degrees.