Separable and inseparable degrees under a surjective base change

In a tower K → E → L of fields whose lower map algebraMap K E is onto, E carries no more information over K than K itself does, so the degree of L is the same whichever of the two it is measured over. This file records that for the separable and inseparable degrees, alongside Module.finrank, for which Mathlib already has the statement.

The hypothesis is surjectivity rather than bijectivity because a map of fields is automatically injective; and it is stated for an arbitrary tower rather than for a specific construction, so that a caller with any surjectively-presented intermediate field can use it.

Main results

• Field.finSepDegree_eq_of_surjective: [L : E]_s = [L : K]_s.
• Field.finInsepDegree_eq_of_surjective: [L : E]_i = [L : K]_i.

theorem Field.finSepDegree_eq_of_surjective {K : Type u_1} {L : Type u_2} [Field K] [Field L] {E : Type u_3} [Field E] [Algebra K L] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (hsurj : Function.Surjective ⇑(algebraMap K E)) : finSepDegree E L = finSepDegree K L

The separable degree is unchanged by a surjective base change. Use this to move a separable degree between an intermediate field and a field presented as mapping onto it.

theorem Field.finInsepDegree_eq_of_surjective {K : Type u_1} {L : Type u_2} [Field K] [Field L] {E : Type u_3} [Field E] [Algebra K L] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (hsurj : Function.Surjective ⇑(algebraMap K E)) : finInsepDegree E L = finInsepDegree K L

The inseparable degree is unchanged by a surjective base change. The inseparable counterpart of Field.finSepDegree_eq_of_surjective, for the same tower.