feat(FunctionField): a function field is finite over Fq(y) for transcendental y (#37447)

Given `F` a function field over `Fq`, we know by assumption that it is finite over `RatFunc Fq`.
This PR adds the result that it is also finite over `Fq(y)` for any transcendental `y` over `Fq`.

Notes:
1. Instance synthesis is known to be slow with `IntermediateField`, so we guide it in the proof of `finiteDimensional_of_adjoin_transcendental`.
2. While looking for the proof of `Module.Finite.top_left`, it took me a while to find `Module.Finite.of_surjective` as I was looking for equiv lemmas. I've added a comment in the docstring of `Module.Finite.of_equiv_equiv` to ease discovery.
3. Since `LinearMap.id'` requires `σ` to have the same domain and codomain, we explicitly provide a generalized version of it in the proof of `Module.Finite.top_left`.

Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
Co-authored-by: Xavier Genereux <xaviergenereux@hotmail.com>

Author: xgenereux

Mathlib/NumberTheory/FunctionField.lean

@@ -10,6 +10,8 @@ public import Mathlib.RingTheory.DedekindDomain.IntegralClosure
 public import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
 public import Mathlib.Topology.Algebra.Valued.ValuedField
 public import Mathlib.Topology.Algebra.InfiniteSum.Defs
+public import Mathlib.FieldTheory.RatFunc.IntermediateField
+public import Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
 public import Mathlib.FieldTheory.RatFunc.Valuation -- for deprecation to `RatFunc.inftyValuation` and `RatFunc.CompletionAtInfty`
 
 /-!
@@ -196,4 +198,59 @@ alias valuedFtInfty.def := RatFunc.valuedCompletionAtInfty.def
 
 end deprecated
 
+section AdjoinTranscendental
+
+open IntermediateField RatFunc
+
+variable {F K : Type*} [Field F] [Field K] [Algebra F⟮X⟯ K] [FunctionField F K]
+
+instance FiniteDimensional.adjoin_X : FiniteDimensional F⟮(X : F⟮X⟯)⟯ K :=
+  have : Module.Finite (⊤ : IntermediateField F F⟮X⟯) F⟮X⟯ :=
+    .top_left F⟮X⟯ F⟮X⟯
+  RatFunc.adjoin_X (K := F) ▸ Module.Finite.trans F⟮X⟯ _
+
+variable [Algebra F K] [IsScalarTower F F⟮X⟯ K]
+
+theorem FiniteDimensional.adjoin_algebraMap_X :
+    FiniteDimensional F⟮algebraMap _ K (X : F⟮X⟯)⟯ K :=
+  .of_restrictScalars_finite F⟮(X : F⟮X⟯)⟯ _ _
+
+theorem Algebra.IsAlgebraic.adjoin_algebraMap_X :
+    Algebra.IsAlgebraic F⟮algebraMap _ K (X : F⟮X⟯)⟯ K := by
+  exact .tower_top (K := F⟮(X : F⟮X⟯)⟯) _
+
+variable {y : K}
+
+theorem isAlgebraic_X_over_adjoin_transcendental (hy : Transcendental F y) :
+    IsAlgebraic F⟮y⟯ (algebraMap _ K (X : F⟮X⟯)) :=
+  isAlgebraic_adjoin_iff.mpr (.adjoin_singleton transcendental_X hy
+    (isAlgebraic_adjoin_iff.mp (Algebra.IsAlgebraic.isAlgebraic y)))
+
+lemma finiteDimensional_of_adjoin_transcendental (hy : Transcendental F y) :
+    FiniteDimensional F⟮y⟯ K :=
+  -- Local definitions for convenience
+  let x := algebraMap _ K (X : F⟮X⟯)
+  let Fyx := restrictScalars F F⟮y⟯⟮x⟯
+  let Fxy := restrictScalars F F⟮x⟯⟮y⟯
+  -- Recalling instance to speed up search
+  let : Algebra F⟮y⟯ Fyx := F⟮y⟯⟮x⟯.algebra
+  let : Module F⟮y⟯ Fyx := Algebra.toModule
+  let : SMul F⟮y⟯ Fyx := Algebra.toSMul
+  let : Algebra F⟮x⟯ Fxy := F⟮x⟯⟮y⟯.algebra
+  let : Module F⟮x⟯ Fxy := Algebra.toModule
+  let : SMul F⟮x⟯ Fxy := Algebra.toSMul
+  let : FiniteDimensional F⟮y⟯ Fyx :=
+    adjoin.finiteDimensional
+      (isAlgebraic_iff_isIntegral.mp (isAlgebraic_X_over_adjoin_transcendental hy))
+  let : FiniteDimensional Fyx K := by
+    let := FiniteDimensional.adjoin_algebraMap_X (F := F) (K := K)
+    unfold Fyx
+    rw [adjoin_simple_comm]
+    let : IsScalarTower F⟮x⟯ Fxy K := isScalarTower_mid' F⟮x⟯⟮y⟯
+    exact .right F⟮x⟯ Fxy K
+  let : IsScalarTower F⟮y⟯ Fyx K := isScalarTower_mid' F⟮y⟯⟮x⟯
+  .trans F⟮y⟯ Fyx K
+
+end AdjoinTranscendental
+
 end FunctionField

Mathlib/RingTheory/Finiteness/Basic.lean

@@ -340,6 +340,12 @@ instance bot : Module.Finite R (⊥ : Submodule R M) := .of_fg fg_bot
 
 instance top [Module.Finite R M] : Module.Finite R (⊤ : Submodule R M) := .of_fg fg_top
 
+instance top_left [Module.Finite R M] : Module.Finite (⊤ : Subsemiring R) M :=
+  have : RingHomSurjective (Subsemiring.topEquiv (R := R)).symm.toRingHom :=
+    RingHomSurjective.instToRingHomRingEquiv Subsemiring.topEquiv.symm
+  of_surjective (σ := (Subsemiring.topEquiv (R := R)).symm.toRingHom)
+      ⟨⟨id, fun _ _ ↦ rfl⟩, fun _ _ ↦ rfl⟩ Function.surjective_id
+
 variable {M}
 
 /-- The submodule generated by a finite set is `R`-finite. -/
@@ -367,6 +373,7 @@ theorem trans {R : Type*} (A M : Type*) [Semiring R] [Semiring A] [Module R A]
         Finite.image2 _ s.finite_toSet t.finite_toSet,
         by rw [image2_smul, span_smul_of_span_eq_top hs (↑t : Set M), ht, restrictScalars_top]⟩⟩
 
+/-- See also `Module.Finite.of_surjective` and `LinearMap.finite_iff_of_bijective`. -/
 lemma of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [CommSemiring A₁] [CommSemiring B₁]
     [CommSemiring A₂] [Semiring B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂)
     (e₂ : B₁ ≃+* B₂)