Finite descent in an algebraic constant extension

An arbitrary extension of constants is the directed union of the extensions obtained by adjoining finitely many constants. When the constant extension is algebraic, each of these intermediate constant fields is finite-dimensional over the original constants. Consequently every element, finite set, or finitely generated intermediate field in the full compositum already occurs over a finite constant subextension.

This is the finite-descent step used to pass results proved for finite constant extensions to an algebraic closure of the constant field. In the function-field setting, it lets finite algebraic data be placed in a finite constant extension before applying degree, genus, and Riemann--Roch comparison theorems.

Main results

• TauCeti.constantCompositum_eq_iSup_adjoin_finset: a constant compositum is the supremum of the composita obtained from finitely generated constant subfields.
• TauCeti.exists_finset_of_mem_constantCompositum: one element of a constant compositum is defined over finitely many constants.
• TauCeti.exists_finiteDimensional_constantSubfield_of_finset_subset_constantCompositum: a finite set in an algebraic constant compositum is defined over one finite constant subextension.
• TauCeti.exists_finiteDimensional_constantSubfield_of_fg_le_constantCompositum: a finitely generated intermediate field in the compositum descends to one finite constant subextension.
• TauCeti.exists_finiteDimensional_constantSubfield_of_finiteDimensional_le_constantCompositum: a finite-dimensional intermediate field descends to one finite constant subextension.

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.6.

theorem TauCeti.constantCompositum_mono {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra F F'] {L M : IntermediateField k k'} (h : L ≤ M) : constantCompositum F (↥L) F' ≤ constantCompositum F (↥M) F'

Enlarging an intermediate field of constants enlarges its compositum with F.

theorem TauCeti.constantCompositum_eq_iSup_adjoin_finset {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra F F'] : constantCompositum F k' F' = ⨆ (S : Finset k'), constantCompositum F (↥(IntermediateField.adjoin k ↑S)) F'

A constant compositum is the directed union of its finitely generated constant subextensions. No algebraicity hypothesis is needed for this lattice identity.

theorem TauCeti.exists_finset_of_mem_constantCompositum {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra F F'] {x : F'} (hx : x ∈ constantCompositum F k' F') : ∃ (S : Finset k'), x ∈ constantCompositum F (↥(IntermediateField.adjoin k ↑S)) F'

An element of a constant compositum uses only finitely many constants. If x belongs to F · k', there is a finite set S ⊆ k' such that x already belongs to F · k(S).

theorem TauCeti.exists_finiteDimensional_constantSubfield_of_mem_constantCompositum {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra F F'] [Algebra.IsAlgebraic k k'] {x : F'} (hx : x ∈ constantCompositum F k' F') : ∃ (L : IntermediateField k k'), FiniteDimensional k ↥L ∧ x ∈ constantCompositum F (↥L) F'

One element in an algebraic constant compositum descends to a finite constant subextension.

theorem TauCeti.exists_finiteDimensional_constantSubfield_of_finset_subset_constantCompositum {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra F F'] [Algebra.IsAlgebraic k k'] (S : Finset F') (hS : ∀ x ∈ S, x ∈ constantCompositum F k' F') : ∃ (L : IntermediateField k k'), FiniteDimensional k ↥L ∧ ∀ x ∈ S, x ∈ constantCompositum F (↥L) F'

A finite set in an algebraic constant compositum descends simultaneously to one finite constant subextension.

theorem TauCeti.exists_finiteDimensional_constantSubfield_of_fg_le_constantCompositum {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra F F'] [Algebra.IsAlgebraic k k'] {E : IntermediateField F F'} (hE : E.FG) (hle : E ≤ constantCompositum F k' F') : ∃ (L : IntermediateField k k'), FiniteDimensional k ↥L ∧ E ≤ constantCompositum F (↥L) F'

A finitely generated field inside an algebraic constant compositum descends to a finite constant subextension. This packages simultaneous finite descent in the form used for finite algebraic data: if E / F is generated by finitely many elements and E ⊆ F · k', then some finite-dimensional L / k satisfies E ⊆ F · L.

theorem TauCeti.exists_finiteDimensional_constantSubfield_of_finiteDimensional_le_constantCompositum {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra F F'] [Algebra.IsAlgebraic k k'] {E : IntermediateField F F'} [FiniteDimensional F ↥E] (hle : E ≤ constantCompositum F k' F') : ∃ (L : IntermediateField k k'), FiniteDimensional k ↥L ∧ E ≤ constantCompositum F (↥L) F'

A finite-dimensional field inside an algebraic constant compositum descends to a finite constant subextension. This is the direct interface for finite algebraic data: if E / F is finite-dimensional and E ⊆ F · k', then some finite-dimensional L / k satisfies E ⊆ F · L.