The degree above the range of a field embedding

An F-algebra map f : K →ₐ[F] L of fields is injective, so it identifies K with the intermediate field f.fieldRange. This file records that the two therefore support the same degree: [L : f.fieldRange] = [L : K], whenever L is a K-algebra through f.

Both dimensions are needed in practice. A degree over K is what an abstract extension supplies, while a degree over f.fieldRange is what any argument comparing two subfields of L — a tower, or a relative degree — must work with, since those subfields are intermediate fields of one extension rather than separate types.

The K-algebra structure on L is a hypothesis rather than f.toRingHom.toAlgebra, because the structure the caller already has need only agree with f, and for a fixed pair K, L different embeddings f induce different structures, so none can be registered globally.

Main results

• AlgHom.finrank_fieldRange: [L : f.fieldRange] = [L : K].
• AlgHom.finiteDimensional_of_fieldRange and AlgHom.isSeparable_of_fieldRange: finiteness and separability over the range transfer to the source — the same identification read for a property rather than for a number.
• AlgHom.finSepDegree_fieldRange and AlgHom.finInsepDegree_fieldRange: the same for the separable and inseparable degrees. These are the f.fieldRange cases of the general transports in TauCeti.FieldTheory.SeparableDegree, which is where a caller holding some other surjectively-presented intermediate field should look.

theorem AlgHom.finrank_fieldRange {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (f : K →ₐ[F] L) [Algebra K L] (h : ∀ (z : K), (algebraMap K L) z = f z) : Module.finrank (↥f.fieldRange) L = Module.finrank K L

The degree above the range of a field embedding equals the degree above its source. Stated for an arbitrary K-algebra structure on L whose structure map is f, rather than for f.toRingHom.toAlgebra, so that it applies to a structure the caller already has.

theorem AlgHom.finiteDimensional_of_fieldRange {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (f : K →ₐ[F] L) [Algebra K L] (h : ∀ (z : K), (algebraMap K L) z = f z) [FiniteDimensional (↥f.fieldRange) L] : FiniteDimensional K L

Finiteness above the range of a field embedding transfers to its source. The range restriction f.equivFieldRange is onto, so f.fieldRange is finite over K, and the tower K → f.fieldRange → L carries finiteness the rest of the way.

The counterpart of finrank_fieldRange for the property rather than the number: a caller who knows only that L is finite over the range — which is the form an intermediate field usually arrives in — gets finiteness over K itself, and with it the Algebra.IsAlgebraic side condition the separable and inseparable tower laws take.

theorem AlgHom.finSepDegree_fieldRange {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (f : K →ₐ[F] L) [Algebra K L] (h : ∀ (z : K), (algebraMap K L) z = f z) : Field.finSepDegree (↥f.fieldRange) L = Field.finSepDegree K L

The separable degree above the range of a field embedding equals the one above its source. The f.fieldRange case of Field.finSepDegree_eq_of_surjective.

theorem AlgHom.finInsepDegree_fieldRange {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (f : K →ₐ[F] L) [Algebra K L] (h : ∀ (z : K), (algebraMap K L) z = f z) : Field.finInsepDegree (↥f.fieldRange) L = Field.finInsepDegree K L

The inseparable degree above the range of a field embedding equals the one above its source. The f.fieldRange case of Field.finInsepDegree_eq_of_surjective.

theorem AlgHom.isSeparable_of_fieldRange {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (f : K →ₐ[F] L) [Algebra K L] (h : ∀ (z : K), (algebraMap K L) z = f z) [Algebra.IsSeparable (↥f.fieldRange) L] : Algebra.IsSeparable K L

Separability above the range of a field embedding transfers to its source. The range restriction f.equivFieldRange is an isomorphism K ≃ₐ[F] f.fieldRange over L, and separability only depends on the subfield of L the scalars land in.

The counterpart of AlgHom.finiteDimensional_of_fieldRange for separability: a caller who knows only that L is separable over the range — the form in which an intermediate field usually arrives — gets separability over K itself, which is what the theorems stated for an abstract extension take as an instance.