The geometric degree of an extension of function fields

Let F' / k' be a finite extension of an algebraic function field F / k, so that k' is the constant field upstairs and k the constant field downstairs. The two degrees [F' : F] and [k' : k] are related through the compositum F · k', formed inside F': the tower F ⊆ F·k' ⊆ F' splits [F' : F] as [F·k' : F] · [F' : F·k'], and the second factor is the geometric degree n(F'/F), the degree of the extension after the constants have been absorbed.

When F and k' are linearly disjoint over k this reads [F' : F] = n(F'/F) · [k' : k]. The hypothesis is carried here in the degree form [F·k' : F] = [k' : k]; that equality is equivalent to linear disjointness when k' / k is finite and k sits in both F and k' compatibly with the two routes into F', and without those provisos it can hold for want of content, both sides being 0. In particular [k' : k] divides [F' : F], which is what turns the cross-multiplied degree identity [k' : k] · deg (Con D) = [F' : F] · deg D for the conorm into deg (Con D) = n(F'/F) · deg D.

Linear disjointness is not automatic; it is what an inseparable constant field extension can destroy. It does hold whenever k' / k is separable and k is the exact constant field of F; that is TauCeti.linearDisjoint_fieldRange_of_isIntegrallyClosedIn, from which the degree equality is derived here. Mathlib's predicate IntermediateField.LinearDisjoint also supplies the degree equality, through TauCeti.finrank_constantCompositum_eq_finrank_of_linearDisjoint.

Main definitions

• TauCeti.constantCompositum: the compositum F · k' inside F'.
• TauCeti.geometricDegree: the geometric degree n(F'/F) = [F' : F·k'].

Main results

• TauCeti.finrank_constantCompositum_mul_geometricDegree: the tower law [F·k' : F] · n(F'/F) = [F' : F].
• TauCeti.finrank_eq_geometricDegree_mul_finrank_of_finrank_constantCompositum_eq: [F' : F] = n(F'/F) · [k' : k] when adjoining the constants to F costs [k' : k], and TauCeti.finrank_dvd_finrank_of_finrank_constantCompositum_eq for the divisibility it contains.
• TauCeti.geometricDegree_eq_finrank_of_constantCompositum_eq_bot: the geometric degree is the whole degree as soon as the compositum is trivial, however that is established.
• TauCeti.geometricDegree_eq_finrank: the geometric degree is the whole degree when the constants of F' already lie in F.
• TauCeti.geometricDegree_eq_one_of_constantCompositum_eq_top: the geometric degree is one when F' is the compositum F · k'.
• TauCeti.finrank_constantCompositum_eq_finrank_of_isSeparable: that degree equality holds for a separable constant field extension over an exact constant field.
• TauCeti.linearDisjoint_fieldRange_of_isIntegrallyClosedIn and TauCeti.linearIndependent_algebraMap_comp_of_isIntegrallyClosedIn: the stronger linear-disjointness and persistence-of-linear-independence statements from which that degree equality follows.
• TauCeti.finrank_constantCompositum_eq_finrank_of_linearDisjoint: it also follows from IntermediateField.LinearDisjoint.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section III.6: the degree form [F·k' : F] = [k' : k] extracted from Proposition 3.6.1(b) (whose own statement, the persistence over k' of linear independence over k, is TauCeti.linearIndependent_algebraMap_comp_of_isIntegrallyClosedIn) is TauCeti.finrank_constantCompositum_eq_finrank_of_isSeparable, the geometric degree [F' : F·k'] is the factor appearing in Corollary 3.6.4, and the splitting [F' : F] = n(F'/F) · [k' : k] is the companion of Proposition 3.6.6. Section III.1 (Corollary 3.1.14) is the cross-multiplied conorm identity this feeds, in TauCeti.FieldTheory.FunctionField.Divisor.Conorm.

def TauCeti.constantCompositum (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] : IntermediateField F F'

The compositum F · k' formed inside F': the smallest intermediate field of F' / F containing the image of the commutative semiring k' under algebraMap k' F'.

In the intended application k' is the constant field of the upper function field F' / k' and F / k is the lower function field, so F · k' is F with the constants of F' adjoined.

Equations

• TauCeti.constantCompositum F k' F' = IntermediateField.adjoin F (Set.range ⇑(algebraMap k' F'))

@[simp]

theorem TauCeti.algebraMap_mem_constantCompositum (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] (c : k') : (algebraMap k' F') c ∈ constantCompositum F k' F'

The image of every element of k' lies in the compositum F · k'.

theorem TauCeti.constantCompositum_def (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] : constantCompositum F k' F' = IntermediateField.adjoin F (Set.range ⇑(algebraMap k' F'))

The defining equation of the compositum F · k': it is F with the image of k' in F' adjoined.

@[simp]

theorem TauCeti.constantCompositum_le_iff (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] {K : IntermediateField F F'} : constantCompositum F k' F' ≤ K ↔ ∀ (c : k'), (algebraMap k' F') c ∈ K

The universal property of the compositum F · k': it is the least intermediate field of F' / F containing the image of k'.

noncomputable def TauCeti.geometricDegree (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] : ℕ

The geometric degree n(F'/F): the degree [F' : F·k'] of F' over the compositum F · k', that is, what remains of F' / F once the image of k' has been adjoined to F.

In the intended application F' / k' is a finite extension of the function field F / k with constant field k' upstairs, and n(F'/F) is the degree of the extension after the constants have been absorbed. Under linear disjointness of F and k' over k it is the quotient [F' : F] / [k' : k]; see TauCeti.finrank_eq_geometricDegree_mul_finrank_of_finrank_constantCompositum_eq. It is the factor [F' : F·k'] by which the conorm multiplies degrees in Stichtenoth's Corollary 3.6.4.

Equations

• TauCeti.geometricDegree F k' F' = Module.finrank (↥(TauCeti.constantCompositum F k' F')) F'

theorem TauCeti.geometricDegree_def (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] : geometricDegree F k' F' = Module.finrank (↥(constantCompositum F k' F')) F'

The defining equation of the geometric degree: n(F'/F) is the degree of F' over the compositum F · k'.

theorem TauCeti.finrank_constantCompositum_mul_geometricDegree (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] : Module.finrank F ↥(constantCompositum F k' F') * geometricDegree F k' F' = Module.finrank F F'

The tower law for the compositum: [F·k' : F] · n(F'/F) = [F' : F].

theorem TauCeti.geometricDegree_pos (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] [FiniteDimensional F F'] : 0 < geometricDegree F k' F'

The geometric degree of a finite extension is positive.

theorem TauCeti.geometricDegree_eq_finrank_of_constantCompositum_eq_bot (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] (h : constantCompositum F k' F' = ⊥) : geometricDegree F k' F' = Module.finrank F F'

The geometric degree is the whole degree as soon as the compositum is trivial, that is, when adjoining the image of k' to F adds nothing. geometricDegree_eq_finrank is the special case where k' maps to F' through F.

@[simp]

theorem TauCeti.geometricDegree_eq_one_of_constantCompositum_eq_top (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] (h : constantCompositum F k' F' = ⊤) : geometricDegree F k' F' = 1

The geometric degree is one when F' is the compositum F · k': nothing is left after the image of k' has been adjoined. This is the case of a constant field extension: combined with the conorm degree formula TauCeti.Divisor.degree_conorm, it is the ingredient that makes the conorm along a constant field extension preserve degrees.

When k' maps to F' through F

@[simp]

theorem TauCeti.constantCompositum_eq_bot (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] [Algebra k' F] [IsScalarTower k' F F'] : constantCompositum F k' F' = ⊥

The compositum is F itself when k' maps to F' through F, as when the constants of F' already lie in F: there is nothing to adjoin.

@[simp]

theorem TauCeti.geometricDegree_eq_finrank (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [CommSemiring k'] [Algebra k' F'] [Algebra F F'] [Algebra k' F] [IsScalarTower k' F F'] : geometricDegree F k' F' = Module.finrank F F'

The geometric degree is the whole degree when k' maps to F' through F, as when the constants of F' already lie in F: n(F'/F) = [F' : F].

Generators of the compositum

theorem TauCeti.constantCompositum_eq_adjoin_of_adjoin_eq_top {k : Type u} (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [Field k] [Field k'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (S : Set k') (hS : IntermediateField.adjoin k S = ⊤) : constantCompositum F k' F' = IntermediateField.adjoin F (⇑(algebraMap k' F') '' S)

If a set generates k' over k, its image generates the compositum over F.

The degree of F' / F when [F·k' : F] is known

theorem TauCeti.finrank_eq_geometricDegree_mul_finrank_of_finrank_constantCompositum_eq {k : Type u} (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [Semiring k] [CommSemiring k'] [Module k k'] [Algebra k' F'] [Algebra F F'] (h : Module.finrank F ↥(constantCompositum F k' F') = Module.finrank k k') : Module.finrank F F' = geometricDegree F k' F' * Module.finrank k k'

The degree of F' / F in terms of the geometric degree: for any k-module structure on k', if [F·k' : F] equals Module.finrank k k', then [F' : F] = n(F'/F) · Module.finrank k k'.

When k' / k is a field extension compatible with k ⊆ F inside F', the hypothesis h is the degree form [F·k' : F] = [k' : k] of the linear-disjointness condition on F and k' over k. It is then supplied by TauCeti.finrank_constantCompositum_eq_finrank_of_linearDisjoint from IntermediateField.LinearDisjoint, and by TauCeti.finrank_constantCompositum_eq_finrank_of_isSeparable for a separable constant field extension over an exact constant field; it can fail for an inseparable k' / k.

This is the companion of Stichtenoth's Proposition 3.6.6, which splits [F' : F] the same way.

theorem TauCeti.finrank_dvd_finrank_of_finrank_constantCompositum_eq {k : Type u} (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [Semiring k] [CommSemiring k'] [Module k k'] [Algebra k' F'] [Algebra F F'] (h : Module.finrank F ↥(constantCompositum F k' F') = Module.finrank k k') : Module.finrank k k' ∣ Module.finrank F F'

Module.finrank k k' divides [F' : F] when it equals [F·k' : F], with the geometric degree as quotient. For a constant field extension k' / k compatible with k ⊆ F, the hypothesis is the degree form of linear disjointness (see TauCeti.finrank_eq_geometricDegree_mul_finrank_of_finrank_constantCompositum_eq), and the conclusion says [k' : k] divides [F' : F].

Linear disjointness from the constant field

theorem TauCeti.finrank_constantCompositum_eq_finrank_of_linearDisjoint {k : Type u} (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [Field k] [Field k'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsAlgebraic k k'] (H : (IsScalarTower.toAlgHom k k' F').fieldRange.LinearDisjoint F) : Module.finrank F ↥(constantCompositum F k' F') = Module.finrank k k'

Mathlib's linear disjointness implies the degree hypothesis: if the constants of F' and the lower function field F are linearly disjoint over k in the sense of IntermediateField.LinearDisjoint, and k' / k is algebraic, then adjoining the constants to F costs exactly [k' : k].

This is the bridge from Mathlib's predicate to the degree form [F·k' : F] = [k' : k] in which the hypothesis is carried by TauCeti.finrank_eq_geometricDegree_mul_finrank_of_finrank_constantCompositum_eq, TauCeti.finrank_dvd_finrank_of_finrank_constantCompositum_eq and TauCeti.Divisor.degree_conorm.

theorem TauCeti.finrank_constantCompositum_eq_finrank_of_isSeparable {k : Type u} (F : Type v) (k' : Type u') (F' : Type v') [Field F] [Field F'] [Field k] [Field k'] [Algebra k k'] [Algebra k F] [Algebra k F'] [Algebra k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] (hex : IsIntegrallyClosedIn k F) [Algebra.IsSeparable k k'] : Module.finrank F ↥(constantCompositum F k' F') = Module.finrank k k'

Adjoining a separable constant field extension to the lower function field preserves finrank, provided the constant field downstairs is exact: [F·k' : F] = [k' : k], which for finite k' / k is the degree form of linear disjointness of F and k' over k.

This is the degree consequence of Stichtenoth's Proposition 3.6.1(b); that proposition's own statement — the persistence over k' of linear independence over k — is TauCeti.linearIndependent_algebraMap_comp_of_isIntegrallyClosedIn.

The statement is over the full compatible tower: k embeds in F and in k', and the two routes k → F → F' and k → k' → F' agree.