Composita of finite fields

Suppose two finite extensions S / C and K / C are embedded in a common finite field T and generate T. Their degrees determine the compositum:

[T : C] = lcm([S : C], [K : C]).

The relative form is

[T : S] = [K : C] / gcd([S : C], [K : C]).

Generation is expressed by surjectivity of the canonical tensor-product map. This formulation is designed to apply directly to residue fields after a constant extension.

theorem BGS.HasseWeil.finiteField_finrank_eq_lcm_of_tensorLift_surjective (C : Type u_1) (S : Type u_2) (K : Type u_3) (T : Type u_4) [Field C] [Field S] [Field K] [Field T] [Algebra C S] [Algebra C K] [Algebra C T] [Finite C] [Finite S] [Finite K] [Finite T] (f : S →ₐ[C] T) (g : K →ₐ[C] T) (hfg : ∀ (s : S) (k : K), Commute (f s) (g k)) (hsurj : Function.Surjective ⇑(Algebra.TensorProduct.lift f g hfg)) : Module.finrank C T = (Module.finrank C S).lcm (Module.finrank C K)

A finite field generated by two embedded finite subfields has degree the least common multiple of their degrees over the common finite field.

theorem BGS.HasseWeil.finiteField_finrank_over_left_eq_div_gcd_of_tensorLift_surjective (C : Type u_1) (S : Type u_2) (K : Type u_3) (T : Type u_4) [Field C] [Field S] [Field K] [Field T] [Algebra C S] [Algebra C K] [Algebra C T] [Finite C] [Finite S] [Finite K] [Finite T] [Algebra S T] [IsScalarTower C S T] (g : K →ₐ[C] T) (hsurj : Function.Surjective ⇑(Algebra.TensorProduct.lift (IsScalarTower.toAlgHom C S T) g ⋯)) : Module.finrank S T = Module.finrank C K / (Module.finrank C S).gcd (Module.finrank C K)

Relative-degree form of the finite-field compositum formula.