feat(RingTheory): lemmas on finiteness of LinearMap and Module.End

Mathlib/Algebra/Module/LinearMap/End.lean

@@ -340,8 +340,9 @@ 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 [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂]
+variable [Module R M] [Module R M₁] [Module R M₂] [Module S M₁] [Module S M₂]
+variable [SMulCommClass R 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₂`.
@@ -356,25 +357,27 @@ def applyₗ' : M →+ (M →ₗ[R] M₂) →ₗ[S] M₂ where
   map_zero' := LinearMap.ext fun f => f.map_zero
   map_add' _ _ := LinearMap.ext fun f => f.map_add _ _
 
-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 : M →ₗ[R] M₂)
+variable [CompatibleSMul M₁ M₂ S R]
 
 /-- 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
+def compRight (f : M₁ →ₗ[R] M₂) : (M →ₗ[R] M₁) →ₗ[S] M →ₗ[R] M₂ where
   toFun g := f.comp g
-  map_add' _ _ := LinearMap.ext fun _ => map_add f _ _
-  map_smul' _ _ := LinearMap.ext fun _ => map_smul f _ _
+  map_add' _ _ := LinearMap.ext fun _ ↦ map_add f _ _
+  map_smul' _ _ := LinearMap.ext fun _ ↦ map_smul_of_tower ..
 
 @[simp]
-theorem compRight_apply (f : M₂ →ₗ[R] M₃) (g : M →ₗ[R] M₂) : compRight f g = f.comp g :=
+theorem compRight_apply (f : M₁ →ₗ[R] M₂) (g : M →ₗ[R] M₁) : compRight S f g = f.comp g :=
   rfl
 
+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 : M →ₗ[R] M₂)
+
 /-- 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.
 

Mathlib/GroupTheory/GroupAction/SubMulAction.lean

@@ -87,6 +87,10 @@ variable [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] (s : S)
 instance (priority := 50) smul : SMul R s :=
   ⟨fun r x => ⟨r • x.1, smul_mem r x.2⟩⟩
 
+@[to_additive] instance (priority := 50) [SMul T M] [SMulMemClass S T M] [SMulCommClass T R M] :
+    SMulCommClass T R s where
+  smul_comm _ _ _ := Subtype.ext (smul_comm ..)
+
 /-- This can't be an instance because Lean wouldn't know how to find `N`, but we can still use
 this to manually derive `SMulMemClass` on specific types. -/
 @[to_additive] theorem _root_.SMulMemClass.ofIsScalarTower (S M N α : Type*) [SetLike S α]
@@ -153,6 +157,12 @@ theorem smul_of_tower_def (r : M) (x : s) :
     r • x = ⟨r • x, smul_one_smul N r x.1 ▸ smul_mem _ x.2⟩ :=
   rfl
 
+@[to_additive] instance (priority := 50) [SMulCommClass M N α] : SMulCommClass M N s where
+  smul_comm _ _ _ := Subtype.ext (smul_comm ..)
+
+@[to_additive] instance (priority := 50) [SMulCommClass N M α] : SMulCommClass N M s where
+  smul_comm _ _ _ := Subtype.ext (smul_comm ..)
+
 end OfTower
 
 end SetLike

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -119,6 +119,24 @@
     -- It looks like we now run out of assignable metavariables.
     (fun c n  m  => by simp only [map_smulₛₗ _, smul_apply])
 
+section lcomp
+
+variable (S N) [Module R N] [SMulCommClass R S N]
+
+/-- Composing a given linear map `M → N` with a linear map `N → P` as a linear map from
+`Nₗ →ₗ[R] Pₗ` to `M →ₗ[R] Pₗ`. -/
+def lcomp (f : M →ₗ[R] M₂) : (M₂ →ₗ[R] N) →ₗ[S] M →ₗ[R] N :=
+  flip <| LinearMap.comp (flip id) f
+
+variable {S N}
+
+@[simp]
+theorem lcomp_apply (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] N) (x : M) : lcomp S N f g x = g (f x) := rfl
+
+theorem lcomp_apply' (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] N) : lcomp S N f g = g ∘ₗ f := rfl
+
+end lcomp
+
 end
 
 @[simp]
@@ -254,21 +272,24 @@
 
 variable (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
 
+@[simp]
+theorem lflip_apply (m : M) (n : N) : lflip f n m = f m n := rfl
+
 variable (A Pₗ)
 variable [Module A Pₗ] [SMulCommClass R A Pₗ]
 
 /-- Composing a given linear map `M → N` with a linear map `N → P` as a linear map from
 `Nₗ →ₗ[R] Pₗ` to `M →ₗ[R] Pₗ`. -/
 def lcomp (f : M →ₗ[R] Nₗ) : (Nₗ →ₗ[R] Pₗ) →ₗ[A] M →ₗ[R] Pₗ :=
   letI := SMulCommClass.symm
   flip <| LinearMap.comp (flip id) f
 
 variable {A Pₗ}
 
 @[simp]
 theorem lcomp_apply (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) (x : M) : lcomp A _ f g x = g (f x) := rfl
 
 theorem lcomp_apply' (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) : lcomp A Pₗ f g = g ∘ₗ f := rfl
 
 variable (P σ₂₃)
 

Mathlib/LinearAlgebra/Dual/Lemmas.lean

@@ -1025,7 +1025,7 @@ sending `f ⊗ g` to the composition of `TensorProduct.map f g` with
 the natural isomorphism `R ⊗ R ≃ R`.
 -/
 def dualDistrib : Dual R M ⊗[R] Dual R N →ₗ[R] Dual R (M ⊗[R] N) :=
-  compRight ↑(TensorProduct.lid R R) ∘ₗ homTensorHomMap R M N R R
+  compRight _ (TensorProduct.lid R R) ∘ₗ homTensorHomMap R M N R R
 
 variable {R M N}
 
@@ -1042,7 +1042,7 @@ variable [Module R M] [Module A M] [Module R N] [IsScalarTower R A M]
 
 /-- Heterobasic version of `TensorProduct.dualDistrib` -/
 def dualDistrib : Dual A M ⊗[R] Dual R N →ₗ[A] Dual A (M ⊗[R] N) :=
-  compRight (Algebra.TensorProduct.rid R A A).toLinearMap ∘ₗ homTensorHomMap R A A M N A R
+  compRight _ (Algebra.TensorProduct.rid R A A).toLinearMap ∘ₗ homTensorHomMap R A A M N A R
 
 variable {R M N}
 

Mathlib/LinearAlgebra/Projection.lean

@@ -258,6 +258,14 @@ theorem ofIsCompl_smul {R : Type*} [CommRing R] {E : Type*} [AddCommGroup E] [Mo
     {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (c : R) : ofIsCompl h (c • φ) (c • ψ) = c • ofIsCompl h φ ψ :=
   ofIsCompl_eq _ (by simp) (by simp)
 
+theorem surjective_comp_linearProjOfIsCompl (h : IsCompl p q) [Module R M] :
+    Function.Surjective (comp (p.linearProjOfIsCompl q h) : (M →ₗ[R] E) → _) :=
+  fun f ↦ ⟨p.subtype ∘ₗ f, by ext; simp⟩
+
+theorem surjective_comp_subtype_of_isComplemented (h : IsComplemented p) [Module R M] :
+    Function.Surjective fun f : E →ₗ[R] M ↦ f ∘ₗ p.subtype :=
+  have ⟨q, h⟩ := h; fun f ↦ ⟨f ∘ₗ p.linearProjOfIsCompl q h, by ext; simp⟩
+
 section
 
 variable {R₁ : Type*} [CommRing R₁] [Module R₁ E] [Module R₁ F]

Mathlib/RingTheory/Finiteness/Basic.lean

@@ -256,8 +256,7 @@ theorem of_restrictScalars_finite (R A M : Type*) [Semiring R] [Semiring A] [Add
   obtain ⟨S, hSfin, hSgen⟩ := hM
   refine ⟨S, hSfin, eq_top_iff.2 ?_⟩
   have := Submodule.span_le_restrictScalars R A S
-  rw [hSgen] at this
-  exact this
+  rwa [hSgen] at this
 
 variable {R M}
 
@@ -267,6 +266,8 @@ theorem equiv [Module.Finite R M] (e : M ≃ₗ[R] N) : Module.Finite R N :=
 theorem equiv_iff (e : M ≃ₗ[R] N) : Module.Finite R M ↔ Module.Finite R N :=
   ⟨fun _ ↦ equiv e, fun _ ↦ equiv e.symm⟩
 
+instance [Module.Finite R M] : Module.Finite R Mᵐᵒᵖ := equiv (MulOpposite.opLinearEquiv R)
+
 instance ulift [Module.Finite R M] : Module.Finite R (ULift M) := equiv ULift.moduleEquiv.symm
 
 theorem iff_fg {N : Submodule R M} : Module.Finite R N ↔ N.FG := Module.finite_def.trans N.fg_top

Mathlib/RingTheory/SimpleModule/Basic.lean

@@ -182,6 +182,37 @@ theorem IsSemisimpleModule.of_sSup_simples_eq_top
     (h : sSup { m : Submodule R M | IsSimpleModule R m } = ⊤) : IsSemisimpleModule R M :=
   complementedLattice_of_sSup_atoms_eq_top (by simp_rw [← h, isSimpleModule_iff_isAtom])
 
+namespace Module.Finite
+
+variable (R₀ P : Type*) [Semiring R₀] [AddCommMonoid P] [Module R P]
+
+section
+
+variable [Module R₀ P] [SMulCommClass R R₀ P] [Module.Finite R₀ (M →ₗ[R] P)]
+
+theorem of_isComplemented_domain (h : IsComplemented m) : Module.Finite R₀ (m →ₗ[R] P) :=
+  .of_surjective (.lcomp ..) (LinearMap.surjective_comp_subtype_of_isComplemented h)
+
+instance [IsSemisimpleModule R M] : Module.Finite R₀ (m →ₗ[R] P) :=
+  .of_isComplemented_domain _ _ (exists_isCompl m)
+
+end
+
+section
+
+variable [Module R₀ M] [SMulCommClass R R₀ M] [SMul R₀ R]
+  [IsScalarTower R₀ R M] [Module.Finite R₀ (P →ₗ[R] M)]
+
+theorem of_isComplemented_codomain (h : IsComplemented m) : Module.Finite R₀ (P →ₗ[R] m) :=
+  .of_surjective (.compRight ..) (LinearMap.surjective_comp_linearProjOfIsCompl h.choose_spec)
+
+instance [IsSemisimpleModule R M] : Module.Finite R₀ (P →ₗ[R] m) :=
+  .of_isComplemented_codomain _ _ (exists_isCompl m)
+
+end
+
+end Module.Finite
+
 namespace IsSemisimpleModule
 
 variable [IsSemisimpleModule R M]