diff --git a/Mathlib/Algebra/Module/Equiv/Defs.lean b/Mathlib/Algebra/Module/Equiv/Defs.lean index 14a412f258926e..ca3a9393feb7db 100644 --- a/Mathlib/Algebra/Module/Equiv/Defs.lean +++ b/Mathlib/Algebra/Module/Equiv/Defs.lean @@ -171,9 +171,11 @@ instance : SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M M₂ where map_add := (·.map_add') map_smulₛₗ := (·.map_smul') -theorem toLinearMap_eq_coe {e : M ≃ₛₗ[σ] M₂} : e.toLinearMap = SemilinearMapClass.semilinearMap e := +theorem toLinearMap_eq_ofClass {e : M ≃ₛₗ[σ] M₂} : e.toLinearMap = .ofClass e := rfl +@[deprecated (since := "2026-09-03")] alias toLinearMap_eq_coe := toLinearMap_eq_ofClass + @[simp] theorem coe_mk {f invFun left_inv right_inv} : ((⟨f, invFun, left_inv, right_inv⟩ : M ≃ₛₗ[σ] M₂) : M → M₂) = f := rfl diff --git a/Mathlib/Algebra/Module/LinearMap/Defs.lean b/Mathlib/Algebra/Module/LinearMap/Defs.lean index f17b667368926c..ad07dce7570820 100644 --- a/Mathlib/Algebra/Module/LinearMap/Defs.lean +++ b/Mathlib/Algebra/Module/LinearMap/Defs.lean @@ -158,31 +158,20 @@ theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : /-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/ @[coe] -def semilinearMap : M →ₛₗ[σ] M₃ where +def _root_.LinearMap.ofClass : M →ₛₗ[σ] M₃ where toFun := f map_add' := map_add f map_smul' := map_smulₛₗ f /-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/ instance instCoeToSemilinearMap : CoeHead F (M →ₛₗ[σ] M₃) where - coe f := semilinearMap f + coe f := LinearMap.ofClass f end SemilinearMapClass -namespace LinearMapClass -variable {F : Type*} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] - (f : F) [FunLike F M₁ M₂] [LinearMapClass F R M₁ M₂] - -/-- Reinterpret an element of a type of linear maps as a linear map. -/ -abbrev _root_.LinearMap.ofClass : M₁ →ₗ[R] M₂ := SemilinearMapClass.semilinearMap f - -@[deprecated (since := "2026-09-03")] alias linearMap := LinearMap.ofClass - -/-- Reinterpret an element of a type of linear maps as a linear map. -/ -instance instCoeToLinearMap : CoeHead F (M₁ →ₗ[R] M₂) where - coe f := SemilinearMapClass.semilinearMap f - -end LinearMapClass +@[deprecated (since := "2026-09-03")] alias SemilinearMapClass.semilinearMap := + LinearMap.ofClass +@[deprecated (since := "2026-09-03")] alias LinearMapClass.linearMap := LinearMap.ofClass namespace LinearMap @@ -210,10 +199,12 @@ instance semilinearMapClass : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M map_smulₛₗ := LinearMap.map_smul' @[simp, norm_cast] -lemma coe_coe {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f : F} : - ⇑(f : M →ₛₗ[σ] M₃) = f := +lemma coe_ofClass {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f : F} : + ⇑(ofClass f) = f := rfl +@[deprecated (since := "2026-09-07")] alias coe_coe := coe_ofClass + /-- The `DistribMulActionHom` underlying a `LinearMap`. -/ def toDistribMulActionHom (f : M →ₛₗ[σ] M₃) : DistribMulActionHom σ.toMonoidHom M M₃ := { f with map_zero' := show f 0 = 0 from map_zero f } @@ -254,17 +245,16 @@ theorem coe_addHom_mk {σ : R →+* S} (f : AddHom M M₃) (h) : ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : AddHom M M₃) = f := rfl -theorem coe_semilinearMap {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) : - ((f : M →ₛₗ[σ] M₃) : M → M₃) = f := - rfl +@[deprecated (since := "2026-09-07")] alias coe_semilinearMap := coe_ofClass -theorem toLinearMap_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] - {f g : F} (h : (f : M →ₛₗ[σ] M₃) = (g : M →ₛₗ[σ] M₃)) : - f = g := by +theorem ofClass_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] + {f g : F} (h : ofClass f = ofClass g) : f = g := by apply DFunLike.ext intro m exact DFunLike.congr_fun h m +@[deprecated (since := "2026-09-07")] alias toLinearMap_injective := ofClass_injective + /-- Identity map as a `LinearMap` -/ @[instance_reducible] def id : M →ₗ[R] M := diff --git a/Mathlib/Algebra/Module/Submodule/EqLocus.lean b/Mathlib/Algebra/Module/Submodule/EqLocus.lean index 0691c6e537e6bb..7da0b38b13d99f 100644 --- a/Mathlib/Algebra/Module/Submodule/EqLocus.lean +++ b/Mathlib/Algebra/Module/Submodule/EqLocus.lean @@ -78,7 +78,7 @@ include τ₁₂ in theorem eqOn_sup {f g : F} {S T : Submodule R M} (hS : Set.EqOn f g S) (hT : Set.EqOn f g T) : Set.EqOn f g ↑(S ⊔ T) := by - rw [← LinearMap.coe_coe (f := f), ← LinearMap.coe_coe (f := g), ← le_eqLocus] at hS hT ⊢ + rw [← LinearMap.coe_ofClass (f := f), ← LinearMap.coe_ofClass (f := g), ← le_eqLocus] at hS hT ⊢ exact sup_le hS hT include τ₁₂ in diff --git a/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean b/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean index 4045d9bded5440..1b93218a6b4e0f 100644 --- a/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean +++ b/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean @@ -453,7 +453,7 @@ def mapₙₐ [Fintype n] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A map_mul' M N := by ext -- Un-squeezing this `simp` seems to add about half a second elaboration time. - simp only [mapₗ_apply, map, LinearMap.coe_coe, ofMatrix_apply, mul_apply, map_sum, map_mul, + simp only [mapₗ_apply, map, LinearMap.coe_ofClass, ofMatrix_apply, mul_apply, map_sum, map_mul, ofMatrix_apply] map_star' M := by ext; simp [map, star_apply, map_star] diff --git a/Mathlib/Analysis/CStarAlgebra/CompletelyPositiveMap.lean b/Mathlib/Analysis/CStarAlgebra/CompletelyPositiveMap.lean index 6af76d4c993005..f8ae5cf2a52238 100644 --- a/Mathlib/Analysis/CStarAlgebra/CompletelyPositiveMap.lean +++ b/Mathlib/Analysis/CStarAlgebra/CompletelyPositiveMap.lean @@ -133,7 +133,7 @@ lemma map_cstarMatrix_nonneg {n : Type*} [Fintype n] (φ : A₁ →CP A₂) (M : let k := Fintype.card n let e := Fintype.equivFinOfCardEq (rfl : Fintype.card n = k) have hmain : 0 ≤ (reindexₐ ℂ A₁ e M).mapₗ (φ : A₁ →ₗ[ℂ] A₂) := by - simp only [mapₗ, LinearMap.coe_coe, LinearMap.coe_mk, AddHom.coe_mk] + simp only [mapₗ, LinearMap.coe_ofClass, LinearMap.coe_mk, AddHom.coe_mk] exact CompletelyPositiveMapClass.map_cstarMatrix_nonneg' _ k _ (map_nonneg _ hM) rw [← mapₗ_reindexₐ] at hmain simpa [reindexₐ_symm] using map_nonneg (reindexₐ ℂ A₂ e).symm hmain diff --git a/Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean b/Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean index 4db359d9b8c1ec..268eb6b84c1e19 100644 --- a/Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean +++ b/Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean @@ -76,7 +76,7 @@ lemma isClosedEmbedding_cfcAux : IsClosedEmbedding hA.cfcAux := by have h2 : diagonal (RCLike.ofReal ∘ f ∘ fun i ↦ ⟨hA.eigenvalues i, hA.eigenvalues_mem_spectrum_real i⟩) = (0 : Matrix n n 𝕜) := by - simp only [LinearMap.coe_coe, cfcAux_apply, conjStarAlgAut_apply] at hf + simp only [LinearMap.coe_ofClass, cfcAux_apply, conjStarAlgAut_apply] at hf replace hf := congr($hf * (hA.eigenvectorUnitary : Matrix n n 𝕜)) simp only [mul_assoc, SetLike.coe_mem, Unitary.star_mul_self_of_mem, mul_one, zero_mul] at hf simpa [← mul_assoc] using congr((star hA.eigenvectorUnitary : Matrix n n 𝕜) * $hf) diff --git a/Mathlib/Analysis/Normed/Operator/Basic.lean b/Mathlib/Analysis/Normed/Operator/Basic.lean index 2ed7ced28524d5..0e6112200b6435 100644 --- a/Mathlib/Analysis/Normed/Operator/Basic.lean +++ b/Mathlib/Analysis/Normed/Operator/Basic.lean @@ -66,7 +66,7 @@ theorem ball_zero_subset_range_iff_surjective [RingHomSurjective σ₁₂] {f : theorem ball_subset_range_iff_surjective [RingHomSurjective σ₁₂] {f : 𝓕} {x : F} {r : ℝ} (hr : 0 < r) : ball x r ⊆ Set.range f ↔ (⇑f).Surjective := by refine ⟨fun h ↦ ?_, by simp_all⟩ - rw [← ball_zero_subset_range_iff_surjective hr, ← LinearMap.coe_coe] + rw [← ball_zero_subset_range_iff_surjective hr, ← LinearMap.coe_ofClass] simp_rw [← LinearMap.coe_range, Set.subset_def, SetLike.mem_coe] at h ⊢ intro _ _ rw [← Submodule.add_mem_iff_left (f : E →ₛₗ[σ₁₂] F).range (h _ <| mem_ball_self hr)] diff --git a/Mathlib/LinearAlgebra/AffineSpace/Homogenization.lean b/Mathlib/LinearAlgebra/AffineSpace/Homogenization.lean index cf6b528913df4e..3042118c5b3242 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Homogenization.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Homogenization.lean @@ -171,7 +171,7 @@ section variable {F : Type*} [FunLike F (Homogenization R P) W] [LinearMapClass F R _ _] theorem hom_ext {f g : F} (h : ∀ x, f (ofPoint x) = g (ofPoint x)) : f = g := by - apply LinearMap.toLinearMap_injective + apply LinearMap.ofClass_injective rwa [← LinearMap.eqLocus_eq_top, eq_top_iff, ← span_range_ofPoint, Submodule.span_le, Set.range_subset_iff] diff --git a/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean b/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean index 2a3973c205e24d..30fc59aae96691 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean @@ -73,7 +73,7 @@ theorem mulMap_map_comp_eq {T : Type w} [Semiring T] [Algebra R T] (f : S →ₐ ext simp only [TensorProduct.AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars, - Function.comp_apply, TensorProduct.map_tmul, mulMap_tmul, LinearMap.coe_coe, map_mul] + Function.comp_apply, TensorProduct.map_tmul, mulMap_tmul, LinearMap.coe_ofClass, map_mul] rfl theorem coe_mulMap_comp_eq {T : Type w} [Semiring T] [Algebra R T] (f : S →ₐ[R] T) : diff --git a/Mathlib/RepresentationTheory/Intertwining.lean b/Mathlib/RepresentationTheory/Intertwining.lean index ea713727328263..cf9c11c0d26b6e 100644 --- a/Mathlib/RepresentationTheory/Intertwining.lean +++ b/Mathlib/RepresentationTheory/Intertwining.lean @@ -74,8 +74,9 @@ instance : LinearMapClass (IntertwiningMap ρ σ) A V W where -- we are actively moving away from these design decisions. -- See e.g. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20homomorphism.20type.20vs.20abstract.20class/with/492579416 @[simp] -lemma coe_eq_toLinearMap {f : IntertwiningMap ρ σ} : - SemilinearMapClass.semilinearMap f = f.toLinearMap := rfl +lemma ofClass_eq_toLinearMap {f : IntertwiningMap ρ σ} : .ofClass f = f.toLinearMap := rfl + +@[deprecated (since := "2026-09-03")] alias coe_eq_toLinearMap := ofClass_eq_toLinearMap @[simp] theorem coe_mk (f : V →ₗ[A] W) (h) : ⇑(⟨f, h⟩ : IntertwiningMap ρ σ) = f := rfl diff --git a/Mathlib/RepresentationTheory/Rep/Res.lean b/Mathlib/RepresentationTheory/Rep/Res.lean index f8f45bfb7ecdff..e71ba081da7827 100644 --- a/Mathlib/RepresentationTheory/Rep/Res.lean +++ b/Mathlib/RepresentationTheory/Rep/Res.lean @@ -31,7 +31,7 @@ namespace Rep @[expose, implicit_reducible] def resMap {X Y : Rep k G} (f : H →* G) (p : X ⟶ Y) : of (X := X.V) (X.ρ.comp f) ⟶ of (X := Y.V) (Y.ρ.comp f) := - ofHom ⟨p.hom, fun h ↦ by simpa using p.hom.2 (f h)⟩ + ofHom ⟨p.hom, fun h ↦ by simpa using! p.hom.2 (f h)⟩ /-- The restriction functor `Rep R G ⥤ Rep R H` for a subgroup `H` of `G`. -/ abbrev resFunctor (f : H →* G) : Rep.{t} k G ⥤ Rep k H where diff --git a/Mathlib/RingTheory/Bialgebra/Convolution.lean b/Mathlib/RingTheory/Bialgebra/Convolution.lean index 008da3aa3cef4d..48b7c00557b77e 100644 --- a/Mathlib/RingTheory/Bialgebra/Convolution.lean +++ b/Mathlib/RingTheory/Bialgebra/Convolution.lean @@ -113,7 +113,7 @@ lemma convOne_apply (c : C) : (1 : WithConv <| C →ₐc[R] A) c = algebraMap R @[simp] lemma toLinearMap_convOne : - toConv (SemilinearMapClass.semilinearMap (1 : WithConv <| C →ₐc[R] A).ofConv) = 1 := rfl + toConv (LinearMap.ofClass (1 : WithConv <| C →ₐc[R] A).ofConv) = 1 := rfl @[simp] lemma toAlgHom_convOne : toConv (1 : WithConv <| C →ₐc[R] A).ofConv.toAlgHom = 1 := rfl @@ -131,7 +131,7 @@ lemma convMul_def (f g : WithConv <| C →ₐc[R] A) : private lemma convPow_succ (f : WithConv <| C →ₐc[R] A) (n : ℕ) : f ^ (n + 1) = (f ^ n) * f := rfl --- TODO: Make simp once `SemilinearMapClass.semilinearMap` is not simp nf anymore. +-- TODO: Make simp once `LinearMap.ofClass` is not simp nf anymore. -- @[simp] lemma toLinearMap_convMul (f g : WithConv <| C →ₐc[R] A) : toConv (f * g).ofConv.toLinearMap = toConv f.ofConv.toLinearMap * toConv g.ofConv.toLinearMap := @@ -142,7 +142,7 @@ lemma toAlgHom_convMul (f g : WithConv <| C →ₐc[R] A) : toConv (f * g).ofConv.toAlgHom = toConv f.ofConv.toAlgHom * toConv g.ofConv.toAlgHom := rfl --- TODO: Make simp once `SemilinearMapClass.semilinearMap` is not simp nf anymore. +-- TODO: Make simp once `LinearMap.ofClass` is not simp nf anymore. -- @[simp] lemma toLinearMap_convPow (f : WithConv <| C →ₐc[R] A) : ∀ n, toConv (f ^ n).ofConv.toLinearMap = toConv f.ofConv.toLinearMap ^ n diff --git a/Mathlib/RingTheory/Coalgebra/Basic.lean b/Mathlib/RingTheory/Coalgebra/Basic.lean index 375dbb969e5b6d..7abb2ed7b2accf 100644 --- a/Mathlib/RingTheory/Coalgebra/Basic.lean +++ b/Mathlib/RingTheory/Coalgebra/Basic.lean @@ -143,7 +143,7 @@ theorem sum_counit_tmul_map_eq {B : Type*} [AddCommMonoid B] [Module R B] ∑ i ∈ repr.index, counit (R := R) (repr.left i) ⊗ₜ f (repr.right i) = 1 ⊗ₜ[R] f a := by have := sum_counit_tmul_eq repr apply_fun LinearMap.lTensor R (f : A →ₗ[R] B) at this - simp_all only [map_sum, LinearMap.lTensor_tmul, LinearMap.coe_coe] + simp_all only [map_sum, LinearMap.lTensor_tmul, LinearMap.coe_ofClass] @[simp] theorem sum_map_tmul_counit_eq {B : Type*} [AddCommMonoid B] [Module R B] @@ -151,7 +151,7 @@ theorem sum_map_tmul_counit_eq {B : Type*} [AddCommMonoid B] [Module R B] ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ counit (R := R) (repr.right i) = f a ⊗ₜ[R] 1 := by have := sum_tmul_counit_eq repr apply_fun LinearMap.rTensor R (f : A →ₗ[R] B) at this - simp_all only [map_sum, LinearMap.rTensor_tmul, LinearMap.coe_coe] + simp_all only [map_sum, LinearMap.rTensor_tmul, LinearMap.coe_ofClass] -- Cannot be @[simp] because `a₁` cannot be inferred by `simp`. theorem sum_map_tmul_tmul_eq {B : Type*} [AddCommMonoid B] [Module R B] @@ -164,7 +164,7 @@ theorem sum_map_tmul_tmul_eq {B : Type*} [AddCommMonoid B] [Module R B] have := sum_tmul_tmul_eq repr a₁ a₂ apply_fun TensorProduct.map (f : A →ₗ[R] B) (TensorProduct.map (g : A →ₗ[R] B) (h : A →ₗ[R] B)) at this - simp_all only [map_sum, TensorProduct.map_tmul, LinearMap.coe_coe] + simp_all only [map_sum, TensorProduct.map_tmul, LinearMap.coe_ofClass] lemma sum_counit_smul (𝓡 : Repr R a ι) : ∑ x ∈ 𝓡.index, counit (R := R) (𝓡.left x) • 𝓡.right x = a := by diff --git a/Mathlib/RingTheory/Coalgebra/Equiv.lean b/Mathlib/RingTheory/Coalgebra/Equiv.lean index c8e5ddacfb2f56..06571220e8f84a 100644 --- a/Mathlib/RingTheory/Coalgebra/Equiv.lean +++ b/Mathlib/RingTheory/Coalgebra/Equiv.lean @@ -313,7 +313,7 @@ structure on `B`. -/ ext x simpa only [toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, ← (ℛ R _).eq, map_sum, TensorProduct.map_tmul, - LinearMap.coe_coe, CoalgHom.coe_coe, LinearMap.rTensor_tmul, coe_symm_toLinearEquiv, + LinearMap.coe_ofClass, CoalgHom.coe_coe, LinearMap.rTensor_tmul, coe_symm_toLinearEquiv, symm_apply_apply, LinearMap.lTensor_comp_map, TensorProduct.sum_tmul, TensorProduct.assoc_tmul, TensorProduct.tmul_sum] using (sum_map_tmul_tmul_eq f f f x).symm rTensor_counit_comp_comul := by diff --git a/Mathlib/RingTheory/Finiteness/Basic.lean b/Mathlib/RingTheory/Finiteness/Basic.lean index ba59ec65b1eeeb..2b55e4242f03c0 100644 --- a/Mathlib/RingTheory/Finiteness/Basic.lean +++ b/Mathlib/RingTheory/Finiteness/Basic.lean @@ -265,7 +265,7 @@ instance quotient (R) {A M} [Semiring R] [AddCommGroup M] [Ring A] [Module A M] /-- The range of a linear map from a finite module is finite. -/ instance range [Module.Finite R M] (f : M →ₗ[R] N) : Module.Finite R f.range := - of_surjective (SemilinearMapClass.semilinearMap f).rangeRestrict + of_surjective f.rangeRestrict fun ⟨_, y, hy⟩ => ⟨y, Subtype.ext hy⟩ /-- Pushforwards of finite submodules are finite. -/ diff --git a/Mathlib/RingTheory/LocalRing/Quotient.lean b/Mathlib/RingTheory/LocalRing/Quotient.lean index 194d553b27abcf..23b8ee29422f72 100644 --- a/Mathlib/RingTheory/LocalRing/Quotient.lean +++ b/Mathlib/RingTheory/LocalRing/Quotient.lean @@ -38,7 +38,7 @@ theorem quotient_span_eq_top_iff_span_eq_top (s : Set S) : have H : (span (R ⧸ p) ((Ideal.Quotient.mk (I := pS)) '' s)).restrictScalars R = (span R s).map (IsScalarTower.toAlgHom R S (S ⧸ pS) : S →ₗ[R] S ⧸ pS) := by rw [map_span, ← restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective, - LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq] + LinearMap.coe_ofClass, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq] constructor · intro hs rw [← top_le_iff] @@ -55,7 +55,7 @@ theorem quotient_span_eq_top_iff_span_eq_top (s : Set S) : · intro hs rwa [hs, Submodule.map_top, LinearMap.range_eq_top.mpr, restrictScalars_eq_top_iff] at H - rw [LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq] + rw [LinearMap.coe_ofClass, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq] exact Ideal.Quotient.mk_surjective attribute [local instance] Ideal.Quotient.field