chore: redistribute some of the results in LinearAlgebra.Basic (#7801)

This reduces the file from ~2600 lines to ~1600 lines.



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Mathlib.lean

@@ -315,6 +315,7 @@ import Mathlib.Algebra.Module.Projective
 import Mathlib.Algebra.Module.Submodule.Basic
 import Mathlib.Algebra.Module.Submodule.Bilinear
 import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Algebra.Module.Submodule.LinearMap
 import Mathlib.Algebra.Module.Submodule.Map
 import Mathlib.Algebra.Module.Submodule.Pointwise
 import Mathlib.Algebra.Module.Torsion

Mathlib/Algebra/Algebra/Basic.lean

@@ -3,14 +3,8 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
-import Mathlib.Data.Rat.Order
-import Mathlib.Algebra.Module.Basic
-import Mathlib.Algebra.Module.ULift
-import Mathlib.Algebra.NeZero
-import Mathlib.Algebra.PUnitInstances
-import Mathlib.Algebra.Ring.Aut
-import Mathlib.Algebra.Ring.ULift
 import Mathlib.Algebra.CharZero.Lemmas
+import Mathlib.Algebra.Module.ULift
 import Mathlib.LinearAlgebra.Basic
 import Mathlib.RingTheory.Subring.Basic
 

Mathlib/Algebra/Algebra/Hom.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import Mathlib.Algebra.Algebra.Basic
+import Mathlib.Algebra.BigOperators.Finsupp
 
 #align_import algebra.algebra.hom from "leanprover-community/mathlib"@"e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b"
 

Mathlib/Algebra/BigOperators/Pi.lean

@@ -68,6 +68,13 @@ theorem prod_mk_prod {α β γ : Type*} [CommMonoid α] [CommMonoid β] (s : Fin
 #align prod_mk_prod prod_mk_prod
 #align prod_mk_sum prod_mk_sum
 
+/-- decomposing `x : ι → R` as a sum along the canonical basis -/
+theorem pi_eq_sum_univ {ι : Type*} [Fintype ι] [DecidableEq ι] {R : Type*} [Semiring R]
+    (x : ι → R) : x = ∑ i, (x i) • fun j => if i = j then (1 : R) else 0 := by
+  ext
+  simp
+#align pi_eq_sum_univ pi_eq_sum_univ
+
 section MulSingle
 
 variable {I : Type*} [DecidableEq I] {Z : I → Type*}

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert A. Spencer, Markus Himmel
 -/
 import Mathlib.Algebra.Category.GroupCat.Preadditive
-import Mathlib.CategoryTheory.Linear.Basic
-import Mathlib.CategoryTheory.Elementwise
-import Mathlib.LinearAlgebra.Basic
 import Mathlib.CategoryTheory.Conj
+import Mathlib.CategoryTheory.Linear.Basic
 import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
 
 #align_import algebra.category.Module.basic from "leanprover-community/mathlib"@"829895f162a1f29d0133f4b3538f4cd1fb5bffd3"

Mathlib/Algebra/Category/ModuleCat/Products.lean

@@ -3,8 +3,9 @@ Copyright (c) 2022 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.LinearAlgebra.Pi
 import Mathlib.Algebra.Category.ModuleCat.Basic
+import Mathlib.LinearAlgebra.Pi
+import Mathlib.Tactic.CategoryTheory.Elementwise
 
 #align_import algebra.category.Module.products from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
 

Mathlib/Algebra/Lie/Basic.lean

@@ -3,7 +3,6 @@ Copyright (c) 2019 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import Mathlib.Algebra.Module.Equiv
 import Mathlib.Data.Bracket
 import Mathlib.LinearAlgebra.Basic
 

Mathlib/Algebra/Module/Equiv.lean

@@ -893,3 +893,29 @@ theorem toIntLinearEquiv_trans (e₂ : M₂ ≃+ M₃) :
 end AddCommGroup
 
 end AddEquiv
+
+namespace LinearMap
+
+variable (R S M)
+variable [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M]
+
+/-- The equivalence between R-linear maps from `R` to `M`, and points of `M` itself.
+This says that the forgetful functor from `R`-modules to types is representable, by `R`.
+
+This is an `S`-linear equivalence, under the assumption that `S` acts on `M` commuting with `R`.
+When `R` is commutative, we can take this to be the usual action with `S = R`.
+Otherwise, `S = ℕ` shows that the equivalence is additive.
+See note [bundled maps over different rings].
+-/
+@[simps]
+def ringLmapEquivSelf [Module S M] [SMulCommClass R S M] : (R →ₗ[R] M) ≃ₗ[S] M :=
+  { applyₗ' S (1 : R) with
+    toFun := fun f => f 1
+    invFun := smulRight (1 : R →ₗ[R] R)
+    left_inv := fun f => by
+      ext
+      simp only [coe_smulRight, one_apply, smul_eq_mul, ← map_smul f, mul_one]
+    right_inv := fun x => by simp }
+#align linear_map.ring_lmap_equiv_self LinearMap.ringLmapEquivSelf
+
+end LinearMap

Mathlib/Algebra/Module/LinearMap.lean

@@ -1338,3 +1338,115 @@ theorem End.intCast_def (z : ℤ) [AddCommGroup N₁] [Module R N₁] :
 #align module.End.int_cast_def Module.End.intCast_def
 
 end Module
+
+namespace LinearMap
+
+section AddCommMonoid
+
+section SMulRight
+
+variable [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁]
+variable [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M]
+
+/-- When `f` is an `R`-linear map taking values in `S`, then `fun ↦ b, f b • x` is an `R`-linear
+map. -/
+def smulRight (f : M₁ →ₗ[R] S) (x : M) : M₁ →ₗ[R] M where
+  toFun b := f b • x
+  map_add' x y := by dsimp only; rw [f.map_add, add_smul]
+  map_smul' b y := by dsimp; rw [map_smul, smul_assoc]
+#align linear_map.smul_right LinearMap.smulRight
+
+@[simp]
+theorem coe_smulRight (f : M₁ →ₗ[R] S) (x : M) : (smulRight f x : M₁ → M) = fun c => f c • x :=
+  rfl
+#align linear_map.coe_smul_right LinearMap.coe_smulRight
+
+theorem smulRight_apply (f : M₁ →ₗ[R] S) (x : M) (c : M₁) : smulRight f x c = f c • x :=
+  rfl
+#align linear_map.smul_right_apply LinearMap.smulRight_apply
+
+end SMulRight
+
+end AddCommMonoid
+
+section Module
+
+variable [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂]
+variable [Module R M] [Module R M₂] [Module S M₂] [SMulCommClass R S M₂]
+
+variable (S)
+
+/-- Applying a linear map at `v : M`, seen as `S`-linear map from `M →ₗ[R] M₂` to `M₂`.
+
+ See `LinearMap.applyₗ` for a version where `S = R`. -/
+@[simps]
+def applyₗ' : M →+ (M →ₗ[R] M₂) →ₗ[S] M₂ where
+  toFun v :=
+    { toFun := fun f => f v
+      map_add' := fun f g => f.add_apply g v
+      map_smul' := fun x f => f.smul_apply x v }
+  map_zero' := LinearMap.ext fun f => f.map_zero
+  map_add' _ _ := LinearMap.ext fun f => f.map_add _ _
+#align linear_map.applyₗ' LinearMap.applyₗ'
+
+end Module
+
+section CommSemiring
+
+variable [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃]
+variable [Module R M] [Module R M₂] [Module R M₃]
+variable (f g : M →ₗ[R] M₂)
+
+/-- Composition by `f : M₂ → M₃` is a linear map from the space of linear maps `M → M₂`
+to the space of linear maps `M₂ → M₃`. -/
+def compRight (f : M₂ →ₗ[R] M₃) : (M →ₗ[R] M₂) →ₗ[R] M →ₗ[R] M₃ where
+  toFun := f.comp
+  map_add' _ _ := LinearMap.ext fun _ => map_add f _ _
+  map_smul' _ _ := LinearMap.ext fun _ => map_smul f _ _
+#align linear_map.comp_right LinearMap.compRight
+
+@[simp]
+theorem compRight_apply (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) : compRight f g = f.comp g :=
+  rfl
+#align linear_map.comp_right_apply LinearMap.compRight_apply
+
+/-- Applying a linear map at `v : M`, seen as a linear map from `M →ₗ[R] M₂` to `M₂`.
+See also `LinearMap.applyₗ'` for a version that works with two different semirings.
+
+This is the `LinearMap` version of `toAddMonoidHom.eval`. -/
+@[simps]
+def applyₗ : M →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] M₂ :=
+  { applyₗ' R with
+    toFun := fun v => { applyₗ' R v with toFun := fun f => f v }
+    map_smul' := fun _ _ => LinearMap.ext fun f => map_smul f _ _ }
+#align linear_map.applyₗ LinearMap.applyₗ
+
+/--
+The family of linear maps `M₂ → M` parameterised by `f ∈ M₂ → R`, `x ∈ M`, is linear in `f`, `x`.
+-/
+def smulRightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M where
+  toFun f :=
+    { toFun := LinearMap.smulRight f
+      map_add' := fun m m' => by
+        ext
+        apply smul_add
+      map_smul' := fun c m => by
+        ext
+        apply smul_comm }
+  map_add' f f' := by
+    ext
+    apply add_smul
+  map_smul' c f := by
+    ext
+    apply mul_smul
+#align linear_map.smul_rightₗ LinearMap.smulRightₗ
+
+@[simp]
+theorem smulRightₗ_apply (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
+    (smulRightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M) f x c = f c • x :=
+  rfl
+#align linear_map.smul_rightₗ_apply LinearMap.smulRightₗ_apply
+
+end CommSemiring
+
+end LinearMap

Mathlib/Algebra/Module/Submodule/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2015 Nathaniel Thomas. 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
 -/
-import Mathlib.Algebra.Module.LinearMap
-import Mathlib.Algebra.Module.Equiv
 import Mathlib.GroupTheory.GroupAction.SubMulAction
 import Mathlib.GroupTheory.Submonoid.Membership
 
@@ -196,18 +194,6 @@ def toModule' (S R' R A : Type*) [Semiring R] [NonUnitalNonAssocSemiring A]
   haveI : SMulMemClass S R' A := SMulMemClass.ofIsScalarTower S R' R A
   SMulMemClass.toModule s
 
-/-- The natural `R`-linear map from a submodule of an `R`-module `M` to `M`. -/
-protected def subtype : S' →ₗ[R] M where
-  toFun := Subtype.val
-  map_add' _ _ := rfl
-  map_smul' _ _ := rfl
-#align submodule_class.subtype SMulMemClass.subtype
-
-@[simp]
-protected theorem coeSubtype : (SMulMemClass.subtype S' : S' → M) = Subtype.val :=
-  rfl
-#align submodule_class.coe_subtype SMulMemClass.coeSubtype
-
 end SMulMemClass
 
 namespace Submodule
@@ -365,29 +351,6 @@ instance noZeroSMulDivisors [NoZeroSMulDivisors R M] : NoZeroSMulDivisors R p :=
     this.imp_right (@Subtype.ext_iff _ _ x 0).mpr⟩
 #align submodule.no_zero_smul_divisors Submodule.noZeroSMulDivisors
 
-/-- Embedding of a submodule `p` to the ambient space `M`. -/
-protected def subtype : p →ₗ[R] M := by refine' { toFun := Subtype.val.. } <;> simp [coe_smul]
-#align submodule.subtype Submodule.subtype
-
-theorem subtype_apply (x : p) : p.subtype x = x :=
-  rfl
-#align submodule.subtype_apply Submodule.subtype_apply
-
-@[simp]
-theorem coeSubtype : (Submodule.subtype p : p → M) = Subtype.val :=
-  rfl
-#align submodule.coe_subtype Submodule.coeSubtype
-
-theorem injective_subtype : Injective p.subtype :=
-  Subtype.coe_injective
-#align submodule.injective_subtype Submodule.injective_subtype
-
-/-- Note the `AddSubmonoid` version of this lemma is called `AddSubmonoid.coe_finset_sum`. -/
--- porting note: removing the `@[simp]` attribute since it's literally `AddSubmonoid.coe_finset_sum`
-theorem coe_sum (x : ι → p) (s : Finset ι) : ↑(∑ i in s, x i) = ∑ i in s, (x i : M) :=
-  map_sum p.subtype _ _
-#align submodule.coe_sum Submodule.coe_sum
-
 section AddAction
 
 /-! ### Additive actions by `Submodule`s
@@ -411,10 +374,6 @@ instance vaddCommClass [VAdd M β] [VAdd α β] [VAddCommClass M α β] : VAddCo
 instance [VAdd M α] [FaithfulVAdd M α] : FaithfulVAdd p α :=
   ⟨fun h => Subtype.ext <| eq_of_vadd_eq_vadd h⟩
 
-/-- The action by a submodule is the action by the underlying module. -/
-instance [AddAction M α] : AddAction p α :=
-  AddAction.compHom _ p.subtype.toAddMonoidHom
-
 variable {p}
 
 theorem vadd_def [VAdd M α] (g : p) (m : α) : g +ᵥ m = (g : M) +ᵥ m :=
@@ -485,15 +444,6 @@ def restrictScalarsEmbedding : Submodule R M ↪o Submodule S M where
 #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
-
 end RestrictScalars
 
 end AddCommMonoid
@@ -590,6 +540,11 @@ instance addCommGroup : AddCommGroup p :=
   { p.toAddSubgroup.toAddCommGroup with }
 #align submodule.add_comm_group Submodule.addCommGroup
 
+-- See `neg_coe_set`
+theorem neg_coe : -(p : Set M) = p :=
+  Set.ext fun _ => p.neg_mem_iff
+#align submodule.neg_coe Submodule.neg_coe
+
 end AddCommGroup
 
 section IsDomain

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 -/
-import Mathlib.Algebra.Module.Submodule.Basic
+import Mathlib.Algebra.Module.Submodule.LinearMap
 import Mathlib.Algebra.PUnitInstances
 
 #align_import algebra.module.submodule.lattice from "leanprover-community/mathlib"@"f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c"