A common factorial degree for Galois groups in a field tower

For R ⊆ L ⊆ N, the order of Gal(N/L) is at most [N:R]. Consequently every such intermediate Galois-group order divides the factorial of the top degree. This supplies one auxiliary constant-extension degree that works simultaneously for the rational base and the original compositum in the Frobenius-twist argument.

theorem BGS.HasseWeil.natCard_aut_dvd_finrank_factorial (R : Type u_1) (N : Type u_2) [Field R] [Field N] [Algebra R N] [FiniteDimensional R N] [IsGalois R N] : Nat.card Gal(N/R) ∣ (Module.finrank R N).factorial

The Galois group over the bottom field itself divides the factorial of the extension degree.

theorem BGS.HasseWeil.natCard_aut_le_finrank_of_tower (R : Type u_1) (L : Type u_2) (N : Type u_3) [Field R] [Field L] [Field N] [Algebra R L] [Algebra L N] [Algebra R N] [IsScalarTower R L N] [FiniteDimensional R L] [FiniteDimensional L N] [IsGalois L N] : Nat.card Gal(N/L) ≤ Module.finrank R N

The intermediate Galois group order is bounded by the degree over the bottom field.

theorem BGS.HasseWeil.natCard_aut_dvd_finrank_factorial_of_tower (R : Type u_1) (L : Type u_2) (N : Type u_3) [Field R] [Field L] [Field N] [Algebra R L] [Algebra L N] [Algebra R N] [IsScalarTower R L N] [FiniteDimensional R L] [FiniteDimensional L N] [IsGalois L N] : Nat.card Gal(N/L) ∣ (Module.finrank R N).factorial

A single factorial of the top degree is divisible by the order of every intermediate Galois group in the tower.