move and gen. Module.Finite.top_left

Author: xgenereux

Mathlib/NumberTheory/FunctionField.lean

@@ -267,12 +267,6 @@ variable {Fq F : Type*} [Field Fq] [Field F] [Algebra (RatFunc Fq) F] [FunctionF
 
 open IntermediateField RatFunc
 
--- TODO: Generalize and move to `Mathlib.RingTheory.Finiteness.Basic`
-variable (R M N) in
-variable [CommSemiring R] [CommSemiring M] [Algebra R M] in
-instance Module.Finite.top_left [Module.Finite R M] : Module.Finite (⊤ : Subsemiring R) M :=
-  .of_equiv_equiv (A₁ := R) (Subsemiring.topEquiv.symm) (.refl M) rfl
-
 instance FiniteDimensional.adjoin_X : FiniteDimensional Fq⟮(X : RatFunc Fq)⟯ F := by
   have : Module.Finite (⊤ : IntermediateField Fq (RatFunc Fq)) (RatFunc Fq) :=
     Module.Finite.top_left (RatFunc Fq) (RatFunc Fq)

Mathlib/RingTheory/Finiteness/Basic.lean

@@ -329,6 +329,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 :=
+  haveI : 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. -/
@@ -356,6 +362,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₂)