feat(Algebra): expand Subalgebra.restrictScalars API

Author: matthewjasper

Mathlib/Algebra/Algebra/Subalgebra/Tower.lean

@@ -116,6 +116,58 @@ This is a special case of `AlgHom.restrictScalars` that can be helpful in elabor
 def ofRestrictScalars (U : Subalgebra S A) (f : U →ₐ[S] B) : U.restrictScalars R →ₐ[R] B :=
   f.restrictScalars R
 
+instance restrictScalars.SMul {U : Subalgebra S A} : SMul S (U.restrictScalars R)  where
+  smul s := fun ⟨u, hu⟩ ↦
+    ⟨s • u, by simp only [mem_restrictScalars] at hu ⊢; apply smul_mem _ hu⟩
+
+instance restrictScalars.origAlgebra {U : Subalgebra S A} : Algebra S (U.restrictScalars R) where
+  algebraMap := {
+    toFun s :=
+      let ⟨u, hu⟩ := algebraMap S U s
+      ⟨u, by rwa [mem_restrictScalars]⟩
+    map_zero' := by ext; simp
+    map_one' := by ext; simp
+    map_add' x y := by ext; simp
+    map_mul' x y := by ext; simp
+  }
+  commutes' s x := by
+    ext
+    exact Algebra.commutes s x.val
+  smul_def' s x := by
+    ext
+    exact Algebra.smul_def s x.val
+
+@[simp, norm_cast]
+lemma restrictScalars.coe_smul {U : Subalgebra S A} (s : S) (u : U.restrictScalars R) :
+    (↑(s • u) : A) = s • (u : A) := by
+  rfl
+
+@[simp, norm_cast]
+lemma restrictScalars.coe_algebraMap {U : Subalgebra S A} (s : S) :
+    (algebraMap S (U.restrictScalars R) s : A) = algebraMap S A s := by
+  rfl
+
+instance restrictScalars.isScalarTower {U : Subalgebra S A} :
+    IsScalarTower R S (U.restrictScalars R) :=
+  ⟨fun _ _ _ ↦ by ext; simp⟩
+
+instance restrictScalars.isScalarTower' {U : Subalgebra S A} :
+    IsScalarTower S (U.restrictScalars R) A :=
+  ⟨by simp [smul_def]⟩
+
+/-- Turning `p : Subalgebra S A` into an `R`-subalgebra gives the same algebra structure. -/
+def restrictScalarsEquiv (p : Subalgebra S A) : p.restrictScalars R ≃ₐ[S] p :=
+  { RingEquiv.refl p with
+    commutes' := fun _ => rfl }
+
+@[simp]
+theorem restrictScalarsEquiv_apply (p : Subalgebra S A) (a : p.restrictScalars R) :
+    ((restrictScalarsEquiv R p) a : A) = a := rfl
+
+@[simp]
+theorem restrictScalarsEquiv_symm_apply (p : Subalgebra S A) (a : p) :
+    ((restrictScalarsEquiv R p).symm a : A) = a := rfl
+
 end Semiring
 
 section CommSemiring

Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean

@@ -340,13 +340,15 @@ theorem matroid_closure_eq [IsDomain A] {s : Set A} :
     forall_mem_insert]
   exact fun _ ↦ and_iff_left fun x hx ↦ isAlgebraic_algebraMap (⟨x, subset_adjoin hx⟩ : adjoin R B)
 
-set_option backward.isDefEq.respectTransparency false in
 theorem matroid_isFlat_iff [IsDomain A] {s : Set A} :
     (matroid R A).IsFlat s ↔ ∃ S : Subalgebra R A, S = s ∧ ∀ a : A, IsAlgebraic S a → a ∈ s := by
   rw [Matroid.isFlat_iff_closure_eq, matroid_closure_eq]
   set S := algebraicClosure (adjoin R s) A
-  refine ⟨fun eq ↦ ⟨S.restrictScalars R, eq, fun a (h : IsAlgebraic S _) ↦ ?_⟩, ?_⟩
-  · rw [← eq]; exact h.restrictScalars (adjoin R s)
+  refine ⟨fun eq ↦ ⟨S.restrictScalars R, eq, fun a h ↦ ?_⟩, ?_⟩
+  · rw [← eq, ← coe_restrictScalars R]
+    have : Algebra.IsAlgebraic (adjoin R s) (Subalgebra.restrictScalars R S) :=
+      (Subalgebra.restrictScalarsEquiv R S).symm.isAlgebraic
+    exact h.restrictScalars (adjoin R s)
   rintro ⟨s, rfl, hs⟩
   refine Set.ext fun a ↦ ⟨(hs _ <| adjoin_eq s ▸ ·), fun h ↦ ?_⟩
   exact isAlgebraic_algebraMap (A := A) (by exact (⟨a, subset_adjoin h⟩ : adjoin R s))

Mathlib/RingTheory/Finiteness/Basic.lean

@@ -411,10 +411,10 @@ variable {M : Type*} [AddCommMonoid M] [Module R M]
 variable {A : Type*} [Semiring A] [Module R A] [Module A M] [IsScalarTower R A M]
 variable {S : Submodule A M}
 
-set_option backward.isDefEq.respectTransparency false in
 theorem FG.restrictScalars [Module.Finite R A] (hS : S.FG) : (S.restrictScalars R).FG := by
   rw [← Module.Finite.iff_fg] at *
-  exact Module.Finite.trans A S
+  have : Module.Finite R S := Module.Finite.trans A S
+  exact Module.Finite.equiv ((restrictScalarsEquiv R A M S).restrictScalars R).symm
 
 @[simp]
 theorem FG.restrictScalars_iff [Module.Finite R A] : (S.restrictScalars R).FG ↔ S.FG :=

Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

@@ -14,6 +14,7 @@ public import Mathlib.RingTheory.Polynomial.ScaleRoots
 public import Mathlib.RingTheory.TensorProduct.MvPolynomial
 
 import Mathlib.RingTheory.Polynomial.Subring
+import Mathlib.RingTheory.Finiteness.Subalgebra
 
 /-!
 # # Integral closure as a characteristic predicate
@@ -472,7 +473,6 @@ variable [CommRing R] [CommRing A] [Ring B] [CommRing S] [CommRing T]
 variable [Algebra A B] [Algebra R B] (f : R →+* S) (g : S →+* T)
 variable [Algebra R A] [IsScalarTower R A B]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- If A is an R-algebra all of whose elements are integral over R,
 and x is an element of an A-algebra that is integral over A, then x is integral over R. -/
 theorem isIntegral_trans [Algebra.IsIntegral R A] (x : B) (hx : IsIntegral A x) :
@@ -485,16 +485,9 @@ theorem isIntegral_trans [Algebra.IsIntegral R A] (x : B) (hx : IsIntegral A x)
   have hSx : IsIntegral S x := ⟨p', (p.monic_toSubring _ _).mpr pmonic, by
     rw [IsScalarTower.algebraMap_eq S A B, ← eval₂_map]
     convert hp; apply p.map_toSubring S.toSubring⟩
-  let Sx := Subalgebra.toSubmodule (S[x])
-  let MSx : Module S Sx := SMulMemClass.toModule _ -- the next line times out without this
-  have : Module.Finite S Sx := .of_fg hSx.fg_adjoin_singleton
   refine .of_mem_of_fg ((S[x]).restrictScalars R) ?_ _
     ((Subalgebra.mem_restrictScalars R).mpr <| subset_adjoin rfl)
-  rw [← Module.Finite.iff_fg]
-  letI : SMul S Sx := { MSx with } -- need this even though MSx is there
-  have : IsScalarTower R S Sx :=
-    Submodule.isScalarTower Sx -- Lean looks for `Module A Sx` without this
-  exact Module.Finite.trans S Sx
+  simpa using hSx.fg_adjoin_singleton
 
 variable (A) in
 /-- If A is an R-algebra all of whose elements are integral over R,