chore(*): restrict operations to LinearMaps (leanprover-community#33241)

Make `LinearMap.ker`, `LinearMap.range`, `Submodule.map`, and `Submodule.comap`
work for `LinearMap`s only.

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

Author: urkud

Mathlib/Algebra/Algebra/Subalgebra/Tower.lean

@@ -123,7 +123,7 @@ section CommSemiring
 @[simp]
 lemma range_isScalarTower_toAlgHom [CommSemiring R] [CommSemiring A]
     [Algebra R A] (S : Subalgebra R A) :
-    LinearMap.range (IsScalarTower.toAlgHom R S A) = Subalgebra.toSubmodule S := by
+    LinearMap.range (IsScalarTower.toAlgHom R S A : S →ₗ[R] A) = Subalgebra.toSubmodule S := by
   ext
   simp [algebraMap_eq]
 

Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean

@@ -163,7 +163,7 @@ def _root_.continuousCohomology (n : ℕ) : Action (TopModuleCat R) G ⥤ TopMod
 /-- The `0`-homogeneous cochains are isomorphic to `Xᴳ`. -/
 def kerHomogeneousCochainsZeroEquiv
     (X : Action (TopModuleCat R) G) (n : ℕ) (hn : n = 1) :
-    LinearMap.ker (((homogeneousCochains R G).obj X).d 0 n).hom ≃L[R] (invariants R G).obj X where
+    (((homogeneousCochains R G).obj X).d 0 n).hom.ker ≃L[R] (invariants R G).obj X where
   toFun x :=
   { val := DFunLike.coe (F := C(G, _)) x.1.1 1
     property g := by

Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean

@@ -35,7 +35,7 @@ variable {M N : TopModuleCat.{v} R} (φ : M ⟶ N)
 section kernel
 
 /-- Kernel in `TopModuleCat R` is the kernel of the linear map with the subspace topology. -/
-abbrev ker : TopModuleCat R := .of R (LinearMap.ker φ.hom)
+abbrev ker : TopModuleCat R := .of R φ.hom.ker
 
 /-- The inclusion map from the kernel in `TopModuleCat R`. -/
 def kerι : ker φ ⟶ M := ofHom ⟨Submodule.subtype _, continuous_subtype_val⟩
@@ -49,9 +49,9 @@ instance : Mono (kerι φ) := ConcreteCategory.mono_of_injective (kerι φ) <| S
 /-- `TopModuleCat.ker` is indeed the kernel in `TopModuleCat R`. -/
 def isLimitKer : IsLimit (KernelFork.ofι (kerι φ) (kerι_comp φ)) :=
   isLimitAux (KernelFork.ofι (kerι φ) (kerι_comp φ))
-    (fun s ↦ ofHom <| (Fork.ι s).hom.codRestrict (LinearMap.ker φ.hom) fun m ↦ by
-      rw [LinearMap.mem_ker, ← ConcreteCategory.comp_apply (Fork.ι s) φ,
-        KernelFork.condition, hom_zero_apply])
+    (fun s ↦ ofHom <| (Fork.ι s).hom.codRestrict φ.hom.ker fun m ↦ by
+      rw [LinearMap.mem_ker, ContinuousLinearMap.coe_coe,
+        ← ConcreteCategory.comp_apply (Fork.ι s) φ, KernelFork.condition, hom_zero_apply])
     (fun s ↦ rfl)
     (fun s m h ↦ by dsimp at h ⊢; rw [← cancel_mono (kerι φ), h]; rfl)
 
@@ -60,7 +60,7 @@ end kernel
 section cokernel
 
 /-- Cokernel in `TopModuleCat R` is the cokernel of the linear map with the quotient topology. -/
-abbrev coker : TopModuleCat R := .of R (N ⧸ LinearMap.range φ.hom)
+abbrev coker : TopModuleCat R := .of R (N ⧸ φ.hom.range)
 
 /-- The projection map to the cokernel in `TopModuleCat R`. -/
 def cokerπ : N ⟶ coker φ := ofHom <| ⟨Submodule.mkQ _, by tauto⟩
@@ -81,7 +81,7 @@ instance : Epi (cokerπ φ) := ConcreteCategory.epi_of_surjective (cokerπ φ) (
 def isColimitCoker : IsColimit (CokernelCofork.ofπ (cokerπ φ) (comp_cokerπ φ)) :=
   isColimitAux (.ofπ (cokerπ φ) (comp_cokerπ φ))
   (fun s ↦ ofHom <|
-    { toLinearMap := (LinearMap.range φ.hom).liftQ s.π.hom.toLinearMap
+    { toLinearMap := φ.hom.range.liftQ s.π.hom.toLinearMap
         (LinearMap.range_le_ker_iff.mpr <| show (φ ≫ s.π).hom.toLinearMap = 0 by
           rw [s.condition, hom_zero, ContinuousLinearMap.coe_zero])
       cont := Continuous.quotient_lift s.π.hom.2 _ })

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -315,7 +315,7 @@ theorem zero_genWeightSpace_eq_top_of_nilpotent [IsNilpotent L M] :
 
 theorem exists_genWeightSpace_le_ker_of_isNoetherian [IsNoetherian R M] (χ : L → R) (x : L) :
     ∃ k : ℕ,
-      genWeightSpace M χ ≤ LinearMap.ker ((toEnd R L M x - algebraMap R _ (χ x)) ^ k) := by
+      genWeightSpace M χ ≤ ((toEnd R L M x - algebraMap R _ (χ x)) ^ k).ker := by
   use (toEnd R L M x).maxGenEigenspaceIndex (χ x)
   intro m hm
   replace hm : m ∈ (toEnd R L M x).maxGenEigenspace (χ x) :=

Mathlib/Algebra/Module/Submodule/Equiv.lean

@@ -61,12 +61,14 @@ def ofSubmodules (p : Submodule R M) (q : Submodule R₂ M₂) (h : p.map (e : M
   (e.submoduleMap p).trans (LinearEquiv.ofEq _ _ h)
 
 @[simp]
-theorem ofSubmodules_apply {p : Submodule R M} {q : Submodule R₂ M₂} (h : p.map ↑e = q) (x : p) :
+theorem ofSubmodules_apply {p : Submodule R M} {q : Submodule R₂ M₂}
+    (h : p.map (e : M →ₛₗ[σ₁₂] M₂) = q) (x : p) :
     ↑(e.ofSubmodules p q h x) = e x :=
   rfl
 
 @[simp]
-theorem ofSubmodules_symm_apply {p : Submodule R M} {q : Submodule R₂ M₂} (h : p.map ↑e = q)
+theorem ofSubmodules_symm_apply {p : Submodule R M} {q : Submodule R₂ M₂}
+    (h : p.map (e : M →ₛₗ[σ₁₂] M₂) = q)
     (x : q) : ↑((e.ofSubmodules p q h).symm x) = e.symm x :=
   rfl
 
@@ -116,11 +118,6 @@ theorem ofTop_symm_apply {h} (x : M) : (ofTop p h).symm x = ⟨x, h.symm ▸ tri
 protected theorem range : LinearMap.range (e : M →ₛₗ[σ₁₂] M₂) = ⊤ :=
   LinearMap.range_eq_top.2 e.toEquiv.surjective
 
-@[simp]
-protected theorem _root_.LinearEquivClass.range [Module R M] [Module R₂ M₂] {F : Type*}
-    [EquivLike F M M₂] [SemilinearEquivClass F σ₁₂ M M₂] (e : F) : LinearMap.range e = ⊤ :=
-  LinearMap.range_eq_top.2 (EquivLike.surjective e)
-
 theorem eq_bot_of_equiv [Module R₂ M₂] (e : p ≃ₛₗ[σ₁₂] (⊥ : Submodule R₂ M₂)) : p = ⊥ := by
   refine bot_unique (SetLike.le_def.2 fun b hb => (Submodule.mem_bot R).2 ?_)
   rw [← p.mk_eq_zero hb, ← e.map_eq_zero_iff]

Mathlib/Algebra/Module/Submodule/Invariant.lean

@@ -60,7 +60,7 @@ theorem mem_invtSubmodule_iff_forall_mem_of_mem {p : Submodule R M} :
 
 /-- `p` is `f.symm` invariant if and only if `p ≤ p.map f`. -/
 lemma mem_invtSubmodule_symm_iff_le_map {f : M ≃ₗ[R] M} {p : Submodule R M} :
-    p ∈ invtSubmodule f.symm ↔ p ≤ p.map f :=
+    p ∈ invtSubmodule f.symm ↔ p ≤ p.map (f : M →ₗ[R] M) :=
   (mem_invtSubmodule_iff_map_le _).trans (f.toEquiv.symm.subset_symm_image _ _).symm
 
 namespace invtSubmodule
@@ -166,16 +166,15 @@ protected lemma comp {p : Submodule R M} {g : End R M}
 @[simp] lemma _root_.LinearEquiv.map_mem_invtSubmodule_conj_iff {R M N : Type*} [CommSemiring R]
     [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : End R M}
     {e : M ≃ₗ[R] N} {p : Submodule R M} :
-    p.map e ∈ (e.conj f).invtSubmodule ↔ p ∈ f.invtSubmodule := by
-  change p.map e.toLinearMap ∈ _ ↔ _
+    p.map (e : M →ₗ[R] N) ∈ (e.conj f).invtSubmodule ↔ p ∈ f.invtSubmodule := by
   have : e.symm.toLinearMap ∘ₗ ((e ∘ₗ f) ∘ₗ e.symm.toLinearMap) ∘ₗ e = f := by ext; simp
   rw [LinearEquiv.conj_apply, mem_invtSubmodule, mem_invtSubmodule, Submodule.map_le_iff_le_comap,
     Submodule.map_equiv_eq_comap_symm, ← Submodule.comap_comp, ← Submodule.comap_comp, this]
 
 lemma _root_.LinearEquiv.map_mem_invtSubmodule_iff {R M N : Type*} [CommSemiring R]
     [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : End R N}
     {e : M ≃ₗ[R] N} {p : Submodule R M} :
-    p.map e ∈ f.invtSubmodule ↔ p ∈ (e.symm.conj f).invtSubmodule := by
+    p.map (e : M →ₗ[R] N) ∈ f.invtSubmodule ↔ p ∈ (e.symm.conj f).invtSubmodule := by
   simp [← e.map_mem_invtSubmodule_conj_iff]
 
 end invtSubmodule

Mathlib/Algebra/Module/Submodule/Ker.lean

@@ -54,23 +54,22 @@ open Submodule
 
 variable {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃}
 variable [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃]
-variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂]
 
 /-- The kernel of a linear map `f : M → M₂` is defined to be `comap f ⊥`. This is equivalent to the
 set of `x : M` such that `f x = 0`. The kernel is a submodule of `M`. -/
-def ker (f : F) : Submodule R M :=
+def ker (f : M →ₛₗ[τ₁₂] M₂) : Submodule R M :=
   comap f ⊥
 
 @[simp]
-theorem mem_ker {f : F} {y} : y ∈ ker f ↔ f y = 0 :=
+theorem mem_ker {f : M →ₛₗ[τ₁₂] M₂} {y} : y ∈ ker f ↔ f y = 0 :=
   mem_bot R₂
 
 @[simp]
 theorem ker_id : ker (LinearMap.id : M →ₗ[R] M) = ⊥ :=
   rfl
 
 @[simp]
-theorem map_coe_ker (f : F) (x : ker f) : f x = 0 :=
+theorem map_coe_ker (f : M →ₛₗ[τ₁₂] M₂) (x : ker f) : f x = 0 :=
   mem_ker.1 x.2
 
 theorem ker_toAddSubmonoid (f : M →ₛₗ[τ₁₂] M₂) : (ker f).toAddSubmonoid = (AddMonoidHom.mker f) :=
@@ -101,18 +100,18 @@ theorem ker_le_comap {p : Submodule R₂ M₂} (f : M →ₛₗ[τ₁₂] M₂)
     ker f ≤ p.comap f :=
   fun x hx ↦ by simp [mem_ker.mp hx]
 
-theorem disjoint_ker {f : F} {p : Submodule R M} :
+theorem disjoint_ker {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} :
     Disjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0 := by
   simp [disjoint_def]
 
-theorem ker_eq_bot' {f : F} : ker f = ⊥ ↔ ∀ m, f m = 0 → m = 0 := by
+theorem ker_eq_bot' {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊥ ↔ ∀ m, f m = 0 → m = 0 := by
   simpa [disjoint_iff_inf_le] using disjoint_ker (f := f) (p := ⊤)
 
 theorem ker_eq_bot_of_inverse {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂}
     {g : M₂ →ₛₗ[τ₂₁] M} (h : (g.comp f : M →ₗ[R] M) = id) : ker f = ⊥ :=
   ker_eq_bot'.2 fun m hm => by rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero]
 
-theorem le_ker_iff_map [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} :
+theorem le_ker_iff_map [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} :
     p ≤ ker f ↔ map f p = ⊥ := by rw [ker, eq_bot_iff, map_le_iff_le_comap]
 
 theorem ker_codRestrict {τ₂₁ : R₂ →+* R} (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf) :
@@ -144,7 +143,7 @@ theorem exists_ne_zero_of_sSup_eq_top {f : M →ₛₗ[τ₁₂] M₂} (h : f 
 theorem _root_.AddMonoidHom.coe_toIntLinearMap_ker {M M₂ : Type*} [AddCommGroup M] [AddCommGroup M₂]
     (f : M →+ M₂) : LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker := rfl
 
-theorem ker_eq_bot_of_injective {f : F} (hf : Injective f) : ker f = ⊥ := by
+theorem ker_eq_bot_of_injective {f : M →ₛₗ[τ₁₂] M₂} (hf : Injective f) : ker f = ⊥ := by
   rw [eq_bot_iff]
   intro x hx
   simpa only [mem_ker, mem_bot, ← map_zero f, hf.eq_iff] using hx
@@ -167,8 +166,7 @@ variable [Ring R] [Ring R₂]
 variable [AddCommGroup M] [AddCommGroup M₂]
 variable [Module R M] [Module R₂ M₂]
 variable {τ₁₂ : R →+* R₂}
-variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂]
-variable {f : F}
+variable {f : M →ₛₗ[τ₁₂] M₂}
 
 open Submodule
 
@@ -190,12 +188,11 @@ theorem injOn_of_disjoint_ker {p : Submodule R M} {s : Set M} (h : s ⊆ p)
     (hd : Disjoint p (ker f)) : Set.InjOn f s :=
   disjoint_ker_iff_injOn.mp hd |>.mono h
 
-variable (F) in
-theorem _root_.LinearMapClass.ker_eq_bot : ker f = ⊥ ↔ Injective f := by
+theorem ker_eq_bot {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊥ ↔ Injective f := by
   simpa [disjoint_iff_inf_le] using disjoint_ker_iff_injOn (f := f) (p := ⊤)
 
-theorem ker_eq_bot {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊥ ↔ Injective f :=
-  LinearMapClass.ker_eq_bot _
+@[deprecated (since := "2025-12-23")]
+alias _root_.LinearMapClass.ker_eq_bot := ker_eq_bot
 
 @[simp] lemma injective_domRestrict_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
     Injective (f.domRestrict S) ↔ S ⊓ LinearMap.ker f = ⊥ := by
@@ -242,12 +239,11 @@ variable [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂]
 variable [Module R M] [Module R₂ M₂]
 variable (p : Submodule R M)
 variable {τ₁₂ : R →+* R₂}
-variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂]
 
 open LinearMap
 
 @[simp]
-theorem comap_bot (f : F) : comap f ⊥ = ker f :=
+theorem comap_bot (f : M →ₛₗ[τ₁₂] M₂) : comap f ⊥ = ker f :=
   rfl
 
 @[simp]