English
A field F is a function field over F_q if and only if F is a finite extension of F_q(t).
Русский
Поле F является функциональным полем над F_q тогда и только тогда, когда F является конечным расширением F_q(t).
LaTeX
$$$\\text{FunctionField}(F_q,F) \\iff\\text{FiniteDimensional}_{F_q(t)} F$$$
Lean4
/-- `F` is a function field over `Fq` iff it is a finite extension of `Fq(t)`. -/
theorem functionField_iff (Fqt : Type*) [Field Fqt] [Algebra Fq[X] Fqt] [IsFractionRing Fq[X] Fqt]
[Algebra (RatFunc Fq) F] [Algebra Fqt F] [Algebra Fq[X] F] [IsScalarTower Fq[X] Fqt F]
[IsScalarTower Fq[X] (RatFunc Fq) F] : FunctionField Fq F ↔ FiniteDimensional Fqt F :=
by
let e := IsLocalization.algEquiv Fq[X]⁰ (RatFunc Fq) Fqt
have : ∀ (c) (x : F), e c • x = c • x := by
intro c x
rw [Algebra.smul_def, Algebra.smul_def]
congr
refine congr_fun (f := fun c => algebraMap Fqt F (e c)) ?_ c
refine IsLocalization.ext (nonZeroDivisors Fq[X]) _ _ ?_ ?_ ?_ ?_ ?_ <;> intros <;>
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
constructor <;> intro h
· let b := Module.finBasis (RatFunc Fq) F
exact FiniteDimensional.of_fintype_basis (b.mapCoeffs e this)
· let b := Module.finBasis Fqt F
refine FiniteDimensional.of_fintype_basis (b.mapCoeffs e.symm ?_)
intro c x; convert (this (e.symm c) x).symm; simp only [e.apply_symm_apply]
