Relative degrees under linearly disjoint base change

If A is finite over k and linearly disjoint from B over k, adjoining A preserves the relative degree of an intermediate extension B/C. This is the field-tower calculation behind the degree comparison for algebraic function fields after extending their constants.

The main result is IntermediateField.relfinrank_sup_sup_eq_relfinrank_of_linearDisjoint. Apply it as A.relfinrank_sup_sup_eq_relfinrank_of_linearDisjoint B C hCB h, where hCB : C ≤ B and h : A.LinearDisjoint B; the finite-dimensionality of A is supplied by an instance. The declarations live in Mathlib's IntermediateField namespace so that this dot notation works.

theorem IntermediateField.extendScalars_sup_right_eq_adjoin {k : Type u} {L : Type v} [Field k] [Field L] [Algebra k L] (A D : IntermediateField k L) : extendScalars ⋯ = adjoin ↥D ↑A

Extending scalars from D to its compositum with A amounts to adjoining A to D.

theorem IntermediateField.relfinrank_sup_right_eq_finrank_of_linearDisjoint {k : Type u} {L : Type v} [Field k] [Field L] [Algebra k L] (A D : IntermediateField k L) [Algebra.IsAlgebraic k ↥A] (hAD : A.LinearDisjoint ↥D) : D.relfinrank (A ⊔ D) = Module.finrank k ↥A

An algebraic extension linearly disjoint from D has the same degree after adjoining D.

theorem IntermediateField.relfinrank_sup_sup_eq_relfinrank_of_linearDisjoint {k : Type u} {L : Type v} [Field k] [Field L] [Algebra k L] (A B C : IntermediateField k L) (hCB : C ≤ B) [FiniteDimensional k ↥A] (h : A.LinearDisjoint ↥B) : (A ⊔ C).relfinrank (A ⊔ B) = C.relfinrank B

Base change by a finite linearly disjoint extension preserves the degree of an intermediate field extension.