chore: gather results about Submodule.restrictScalars into new file (…

…#9765)

This is a straight copy-paste: there are no new lemmas and nothing has been removed or renamed. The only changes are a few lemmas where argument explicitness or ordering has changed (and where it did not seem to make sense to replicate the old argument explicitness or ordering).

Mathlib.lean

@@ -337,6 +337,7 @@ import Mathlib.Algebra.Module.Submodule.LinearMap
 import Mathlib.Algebra.Module.Submodule.Localization
 import Mathlib.Algebra.Module.Submodule.Map
 import Mathlib.Algebra.Module.Submodule.Pointwise
+import Mathlib.Algebra.Module.Submodule.RestrictScalars
 import Mathlib.Algebra.Module.Torsion
 import Mathlib.Algebra.Module.ULift
 import Mathlib.Algebra.Module.Zlattice

Mathlib/Algebra/Algebra/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.CharZero.Lemmas
 import Mathlib.Algebra.Module.ULift
 import Mathlib.LinearAlgebra.Basic
 import Mathlib.RingTheory.Subring.Basic
+import Mathlib.Algebra.Module.Submodule.RestrictScalars
 
 #align_import algebra.algebra.basic from "leanprover-community/mathlib"@"36b8aa61ea7c05727161f96a0532897bd72aedab"
 

Mathlib/Algebra/Module/Submodule/Basic.lean

@@ -382,70 +382,6 @@ theorem vadd_def [VAdd M α] (g : p) (m : α) : g +ᵥ m = (g : M) +ᵥ m :=
 
 end AddAction
 
-section RestrictScalars
-
-variable (S) [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M]
-
-/-- `V.restrict_scalars S` is the `S`-submodule of the `S`-module given by restriction of scalars,
-corresponding to `V`, an `R`-submodule of the original `R`-module.
--/
-def restrictScalars (V : Submodule R M) : Submodule S M where
-  carrier := V
-  zero_mem' := V.zero_mem
-  smul_mem' c _ h := V.smul_of_tower_mem c h
-  add_mem' hx hy := V.add_mem hx hy
-#align submodule.restrict_scalars Submodule.restrictScalars
-
-@[simp]
-theorem coe_restrictScalars (V : Submodule R M) : (V.restrictScalars S : Set M) = V :=
-  rfl
-#align submodule.coe_restrict_scalars Submodule.coe_restrictScalars
-
-@[simp]
-theorem restrictScalars_mem (V : Submodule R M) (m : M) : m ∈ V.restrictScalars S ↔ m ∈ V :=
-  Iff.refl _
-#align submodule.restrict_scalars_mem Submodule.restrictScalars_mem
-
-@[simp]
-theorem restrictScalars_self (V : Submodule R M) : V.restrictScalars R = V :=
-  SetLike.coe_injective rfl
-#align submodule.restrict_scalars_self Submodule.restrictScalars_self
-
-variable (R M)
-
-theorem restrictScalars_injective :
-    Function.Injective (restrictScalars S : Submodule R M → Submodule S M) := fun _ _ h =>
-  ext <| Set.ext_iff.1 (SetLike.ext'_iff.1 h : _)
-#align submodule.restrict_scalars_injective Submodule.restrictScalars_injective
-
-@[simp]
-theorem restrictScalars_inj {V₁ V₂ : Submodule R M} :
-    restrictScalars S V₁ = restrictScalars S V₂ ↔ V₁ = V₂ :=
-  (restrictScalars_injective S _ _).eq_iff
-#align submodule.restrict_scalars_inj Submodule.restrictScalars_inj
-
-/-- Even though `p.restrictScalars S` has type `Submodule S M`, it is still an `R`-module. -/
-instance restrictScalars.origModule (p : Submodule R M) : Module R (p.restrictScalars S) :=
-  (by infer_instance : Module R p)
-#align submodule.restrict_scalars.orig_module Submodule.restrictScalars.origModule
-
-instance restrictScalars.isScalarTower (p : Submodule R M) :
-    IsScalarTower S R (p.restrictScalars S) where
-  smul_assoc r s x := Subtype.ext <| smul_assoc r s (x : M)
-#align submodule.restrict_scalars.is_scalar_tower Submodule.restrictScalars.isScalarTower
-
-/-- `restrictScalars S` is an embedding of the lattice of `R`-submodules into
-the lattice of `S`-submodules. -/
-@[simps]
-def restrictScalarsEmbedding : Submodule R M ↪o Submodule S M where
-  toFun := restrictScalars S
-  inj' := restrictScalars_injective S R M
-  map_rel_iff' := by simp [SetLike.le_def]
-#align submodule.restrict_scalars_embedding Submodule.restrictScalarsEmbedding
-#align submodule.restrict_scalars_embedding_apply Submodule.restrictScalarsEmbedding_apply
-
-end RestrictScalars
-
 end AddCommMonoid
 
 section AddCommGroup

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -67,27 +67,12 @@ theorem bot_toAddSubmonoid : (⊥ : Submodule R M).toAddSubmonoid = ⊥ :=
 lemma bot_toAddSubgroup {R M} [Ring R] [AddCommGroup M] [Module R M] :
     (⊥ : Submodule R M).toAddSubgroup = ⊥ := rfl
 
-section
-
-variable (R)
-
-@[simp]
-theorem restrictScalars_bot : restrictScalars S (⊥ : Submodule R M) = ⊥ :=
-  rfl
-#align submodule.restrict_scalars_bot Submodule.restrictScalars_bot
-
+variable (R) in
 @[simp]
 theorem mem_bot {x : M} : x ∈ (⊥ : Submodule R M) ↔ x = 0 :=
   Set.mem_singleton_iff
 #align submodule.mem_bot Submodule.mem_bot
 
-end
-
-@[simp]
-theorem restrictScalars_eq_bot_iff {p : Submodule R M} : restrictScalars S p = ⊥ ↔ p = ⊥ := by
-  simp [SetLike.ext_iff]
-#align submodule.restrict_scalars_eq_bot_iff Submodule.restrictScalars_eq_bot_iff
-
 instance uniqueBot : Unique (⊥ : Submodule R M) :=
   ⟨inferInstance, fun x ↦ Subtype.ext <| (mem_bot R).1 x.mem⟩
 #align submodule.unique_bot Submodule.uniqueBot
@@ -175,22 +160,6 @@ theorem mem_top {x : M} : x ∈ (⊤ : Submodule R M) :=
   trivial
 #align submodule.mem_top Submodule.mem_top
 
-section
-
-variable (R)
-
-@[simp]
-theorem restrictScalars_top : restrictScalars S (⊤ : Submodule R M) = ⊤ :=
-  rfl
-#align submodule.restrict_scalars_top Submodule.restrictScalars_top
-
-end
-
-@[simp]
-theorem restrictScalars_eq_top_iff {p : Submodule R M} : restrictScalars S p = ⊤ ↔ p = ⊤ := by
-  simp [SetLike.ext_iff]
-#align submodule.restrict_scalars_eq_top_iff Submodule.restrictScalars_eq_top_iff
-
 instance : OrderTop (Submodule R M) where
   top := ⊤
   le_top _ _ _ := trivial

Mathlib/Algebra/Module/Submodule/LinearMap.lean

@@ -105,22 +105,6 @@ instance [AddAction M α] : AddAction p α :=
 
 end AddAction
 
-section RestrictScalars
-
-variable (S) [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M]
-variable (R M)
-
-/-- Turning `p : Submodule R M` into an `S`-submodule gives the same module structure
-as turning it into a type and adding a module structure. -/
-@[simps (config := { simpRhs := true })]
-def restrictScalarsEquiv (p : Submodule R M) : p.restrictScalars S ≃ₗ[R] p :=
-  { AddEquiv.refl p with
-    map_smul' := fun _ _ => rfl }
-#align submodule.restrict_scalars_equiv Submodule.restrictScalarsEquiv
-#align submodule.restrict_scalars_equiv_symm_apply Submodule.restrictScalarsEquiv_symm_apply
-
-end RestrictScalars
-
 end AddCommMonoid
 
 end Submodule

Mathlib/Algebra/Module/Submodule/RestrictScalars.lean

@@ -0,0 +1,119 @@
+/-
+Copyright (c) 2024 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Andrew Yang,
+  Johannes Hölzl, Kevin Buzzard, Yury Kudryashov
+-/
+import Mathlib.Algebra.Module.Submodule.Lattice
+
+/-!
+
+# Restriction of scalars for submodules
+
+If semiring `S` acts on a semiring `R` and `M` is a module over both (compatibly with this action)
+then we can turn an `R`-submodule into an `S`-submodule by forgetting the action of `R`. We call
+this restriction of scalars for submodules.
+
+## Main definitions:
+ * `Submodule.restrictScalars`: regard an `R`-submodule as an `S`-submodule if `S` acts on `R`
+
+-/
+
+namespace Submodule
+
+variable (S : Type*) {R M : Type*} [Semiring R] [AddCommMonoid M] [Semiring S]
+  [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M]
+
+/-- `V.restrict_scalars S` is the `S`-submodule of the `S`-module given by restriction of scalars,
+corresponding to `V`, an `R`-submodule of the original `R`-module.
+-/
+def restrictScalars (V : Submodule R M) : Submodule S M where
+  carrier := V
+  zero_mem' := V.zero_mem
+  smul_mem' c _ h := V.smul_of_tower_mem c h
+  add_mem' hx hy := V.add_mem hx hy
+#align submodule.restrict_scalars Submodule.restrictScalars
+
+@[simp]
+theorem coe_restrictScalars (V : Submodule R M) : (V.restrictScalars S : Set M) = V :=
+  rfl
+#align submodule.coe_restrict_scalars Submodule.coe_restrictScalars
+
+@[simp]
+theorem toAddSubmonoid_restrictScalars (V : Submodule R M) :
+    (V.restrictScalars S).toAddSubmonoid = V.toAddSubmonoid :=
+  rfl
+
+@[simp]
+theorem restrictScalars_mem (V : Submodule R M) (m : M) : m ∈ V.restrictScalars S ↔ m ∈ V :=
+  Iff.refl _
+#align submodule.restrict_scalars_mem Submodule.restrictScalars_mem
+
+@[simp]
+theorem restrictScalars_self (V : Submodule R M) : V.restrictScalars R = V :=
+  SetLike.coe_injective rfl
+#align submodule.restrict_scalars_self Submodule.restrictScalars_self
+
+variable (R M)
+
+theorem restrictScalars_injective :
+    Function.Injective (restrictScalars S : Submodule R M → Submodule S M) := fun _ _ h =>
+  ext <| Set.ext_iff.1 (SetLike.ext'_iff.1 h : _)
+#align submodule.restrict_scalars_injective Submodule.restrictScalars_injective
+
+@[simp]
+theorem restrictScalars_inj {V₁ V₂ : Submodule R M} :
+    restrictScalars S V₁ = restrictScalars S V₂ ↔ V₁ = V₂ :=
+  (restrictScalars_injective S _ _).eq_iff
+#align submodule.restrict_scalars_inj Submodule.restrictScalars_inj
+
+/-- Even though `p.restrictScalars S` has type `Submodule S M`, it is still an `R`-module. -/
+instance restrictScalars.origModule (p : Submodule R M) : Module R (p.restrictScalars S) :=
+  (by infer_instance : Module R p)
+#align submodule.restrict_scalars.orig_module Submodule.restrictScalars.origModule
+
+instance restrictScalars.isScalarTower (p : Submodule R M) :
+    IsScalarTower S R (p.restrictScalars S) where
+  smul_assoc r s x := Subtype.ext <| smul_assoc r s (x : M)
+#align submodule.restrict_scalars.is_scalar_tower Submodule.restrictScalars.isScalarTower
+
+/-- `restrictScalars S` is an embedding of the lattice of `R`-submodules into
+the lattice of `S`-submodules. -/
+@[simps]
+def restrictScalarsEmbedding : Submodule R M ↪o Submodule S M where
+  toFun := restrictScalars S
+  inj' := restrictScalars_injective S R M
+  map_rel_iff' := by simp [SetLike.le_def]
+#align submodule.restrict_scalars_embedding Submodule.restrictScalarsEmbedding
+#align submodule.restrict_scalars_embedding_apply Submodule.restrictScalarsEmbedding_apply
+
+/-- Turning `p : Submodule R M` into an `S`-submodule gives the same module structure
+as turning it into a type and adding a module structure. -/
+@[simps (config := { simpRhs := true })]
+def restrictScalarsEquiv (p : Submodule R M) : p.restrictScalars S ≃ₗ[R] p :=
+  { AddEquiv.refl p with
+    map_smul' := fun _ _ => rfl }
+#align submodule.restrict_scalars_equiv Submodule.restrictScalarsEquiv
+#align submodule.restrict_scalars_equiv_symm_apply Submodule.restrictScalarsEquiv_symm_apply
+
+@[simp]
+theorem restrictScalars_bot : restrictScalars S (⊥ : Submodule R M) = ⊥ :=
+  rfl
+#align submodule.restrict_scalars_bot Submodule.restrictScalars_bot
+
+@[simp]
+theorem restrictScalars_eq_bot_iff {p : Submodule R M} : restrictScalars S p = ⊥ ↔ p = ⊥ := by
+  simp [SetLike.ext_iff]
+#align submodule.restrict_scalars_eq_bot_iff Submodule.restrictScalars_eq_bot_iff
+
+@[simp]
+theorem restrictScalars_top : restrictScalars S (⊤ : Submodule R M) = ⊤ :=
+  rfl
+#align submodule.restrict_scalars_top Submodule.restrictScalars_top
+
+@[simp]
+theorem restrictScalars_eq_top_iff {p : Submodule R M} : restrictScalars S p = ⊤ ↔ p = ⊤ := by
+  simp [SetLike.ext_iff]
+#align submodule.restrict_scalars_eq_top_iff Submodule.restrictScalars_eq_top_iff
+
+end Submodule

Mathlib/LinearAlgebra/Span.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Frédéric Dupuis,
   Heather Macbeth
 -/
+import Mathlib.Algebra.Module.Submodule.RestrictScalars
 import Mathlib.LinearAlgebra.Basic
 import Mathlib.Order.CompactlyGenerated
 import Mathlib.Order.OmegaCompletePartialOrder

Mathlib/RingTheory/Kaehler.lean

@@ -666,7 +666,7 @@ open IsScalarTower (toAlgHom)
 theorem KaehlerDifferential.map_surjective_of_surjective
     (h : Function.Surjective (algebraMap A B)) :
     Function.Surjective (KaehlerDifferential.map R S A B) := by
-  rw [← LinearMap.range_eq_top, _root_.eq_top_iff, ← @Submodule.restrictScalars_top B A,
+  rw [← LinearMap.range_eq_top, _root_.eq_top_iff, ← @Submodule.restrictScalars_top A B,
     ← KaehlerDifferential.span_range_derivation, Submodule.restrictScalars_span _ _ h,
     Submodule.span_le]
   rintro _ ⟨x, rfl⟩