From 4996b16443a7ec4a774dad3497f9e6538e526213 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 7 Sep 2026 09:03:23 +0200 Subject: [PATCH 1/3] wip --- Mathlib/Algebra/Module/Equiv/Defs.lean | 4 +++- Mathlib/Algebra/Module/LinearMap/Defs.lean | 13 +++++++------ Mathlib/RepresentationTheory/Intertwining.lean | 6 ++++-- Mathlib/RingTheory/Bialgebra/Convolution.lean | 6 +++--- Mathlib/RingTheory/Finiteness/Basic.lean | 2 +- 5 files changed, 18 insertions(+), 13 deletions(-) diff --git a/Mathlib/Algebra/Module/Equiv/Defs.lean b/Mathlib/Algebra/Module/Equiv/Defs.lean index 14a412f258926e..e50897e4c0b59e 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 = SemilinearMap.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..60a07c38247d20 100644 --- a/Mathlib/Algebra/Module/LinearMap/Defs.lean +++ b/Mathlib/Algebra/Module/LinearMap/Defs.lean @@ -158,29 +158,30 @@ 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_.SemilinearMap.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 := SemilinearMap.ofClass f end SemilinearMapClass +@[deprecated (since := "2026-09-03")] alias SemilinearMapClass.semilinearMap := + SemilinearMap.ofClass + 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 +abbrev linearMap : M₁ →ₗ[R] M₂ := SemilinearMap.ofClass f /-- 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 + coe f := SemilinearMap.ofClass f end LinearMapClass diff --git a/Mathlib/RepresentationTheory/Intertwining.lean b/Mathlib/RepresentationTheory/Intertwining.lean index ea5f350d885493..04996b0341d7e8 100644 --- a/Mathlib/RepresentationTheory/Intertwining.lean +++ b/Mathlib/RepresentationTheory/Intertwining.lean @@ -74,8 +74,10 @@ 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 ρ σ} : + SemilinearMap.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/RingTheory/Bialgebra/Convolution.lean b/Mathlib/RingTheory/Bialgebra/Convolution.lean index 008da3aa3cef4d..3d7f0ac9b47c78 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 (SemilinearMap.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 `SemilinearMap.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 `SemilinearMap.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/Finiteness/Basic.lean b/Mathlib/RingTheory/Finiteness/Basic.lean index 789c0beb4703fd..fa5ce50f4487c7 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. -/ From 351e453c3011e08bf8582a42e5c64a856a9ed886 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 7 Sep 2026 09:28:43 +0200 Subject: [PATCH 2/3] Docs; fix bad merge --- Mathlib/Algebra/Module/LinearMap/Defs.lean | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Module/LinearMap/Defs.lean b/Mathlib/Algebra/Module/LinearMap/Defs.lean index 60a07c38247d20..7b72dd6fb96d84 100644 --- a/Mathlib/Algebra/Module/LinearMap/Defs.lean +++ b/Mathlib/Algebra/Module/LinearMap/Defs.lean @@ -156,7 +156,10 @@ variable {F} (f : F) [FunLike F M M₃] [SemilinearMapClass F σ M M₃] theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : c • f x = f (σ' c • x) := by simp [map_smulₛₗ _] -/-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/ +/-- Reinterpret an element of a type of semilinear maps as a semilinear map. + +See `LinearMap.ofClass` for the analogous definition on *linear* maps. +(In the linear case, both coincide.) -/ @[coe] def _root_.SemilinearMap.ofClass : M →ₛₗ[σ] M₃ where toFun := f @@ -176,8 +179,13 @@ 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 linearMap : M₁ →ₗ[R] M₂ := SemilinearMap.ofClass f +/-- Reinterpret an element of a type of linear maps as a linear map. +See `SemilinearMap.ofClass` for the analogous definition on *semilinear* maps. +(In the linear case, both coincide.) +-/ +abbrev _root_.LinearMap.ofClass : M₁ →ₗ[R] M₂ := SemilinearMap.ofClass 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 From b08917227c9390541f02dc707ac100d7ede24efa Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 7 Sep 2026 09:54:54 +0200 Subject: [PATCH 3/3] Clean-ups - rename now-misnamed lemmas - rename coe_coe lemma which was already a bad name - use ofClass instead of manual type ascription, a few times --- Mathlib/Algebra/Module/LinearMap/Defs.lean | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/Module/LinearMap/Defs.lean b/Mathlib/Algebra/Module/LinearMap/Defs.lean index 7b72dd6fb96d84..363770d5a3c92e 100644 --- a/Mathlib/Algebra/Module/LinearMap/Defs.lean +++ b/Mathlib/Algebra/Module/LinearMap/Defs.lean @@ -218,10 +218,12 @@ instance semilinearMapClass : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M map_add f := f.map_add' map_smulₛₗ := LinearMap.map_smul' +-- TODO: should this be renamed to `SemilinearMap.coe_ofClass`? @[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} : + ⇑(SemilinearMap.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₃ := @@ -264,15 +266,18 @@ theorem coe_addHom_mk {σ : R →+* S} (f : AddHom M M₃) (h) : rfl theorem coe_semilinearMap {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) : - ((f : M →ₛₗ[σ] M₃) : M → M₃) = f := + ⇑(SemilinearMap.ofClass f) = f := rfl +-- TODO: is duplicate to coe_ofClass! +--@[deprecated (since := "2026-09-07")] alias coe_semilinearMap := coe_semilinearMap -theorem toLinearMap_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] - {f g : F} (h : (f : M →ₛₗ[σ] M₃) = (g : M →ₛₗ[σ] M₃)) : +theorem ofClass_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] + {f g : F} (h : SemilinearMap.ofClass f = SemilinearMap.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] @@ -283,7 +288,7 @@ theorem id_apply (x : M) : @id R M _ _ _ x = x := rfl @[simp, norm_cast] -theorem id_coe : ((LinearMap.id : M →ₗ[R] M) : M → M) = _root_.id := +theorem id_coe : ⇑((LinearMap.id : M →ₗ[R] M)) = _root_.id := rfl /-- A generalisation of `LinearMap.id` that constructs the identity function @@ -298,7 +303,7 @@ def id' {σ : R →+* R} [RingHomId σ] : M →ₛₗ[σ] M where rfl @[simp, norm_cast] -theorem id'_coe {σ : R →+* R} [RingHomId σ] : ((id' : M →ₛₗ[σ] M) : M → M) = _root_.id := +theorem id'_coe {σ : R →+* R} [RingHomId σ] : ⇑(id' : M →ₛₗ[σ] M) = _root_.id := rfl end