chore(Algebra/Category/ModuleCat): rename ModuleCat.asHom to ModuleCat.ofHom (#19705)

Vierkantor · Vierkantor · commit ac7c96fc6d06 · 2024-12-03T14:22:21.000Z
As discussed in the comments for #19511. It seems the choice between `ofHom` and `asHom` is somewhat inconsistent in concrete categories, but `ofHom` wins. In particular, we want to be consistent with the newly refactored `AlgebraCat.ofHom` and the constructor for objects `ModuleCat.of`. The choice between `asHom` and `ofHom` was only made a few months ago: #17476. It's a bit unfortunate to go back on something that was deprecated so recently, but I think the result is worth the pain. I have not touched `asHomLeft` and `asHomRight` since #19511 will replace these with `ofHom` everywhere anyway.
diff --git a/Mathlib/Algebra/Category/AlgebraCat/Basic.lean b/Mathlib/Algebra/Category/AlgebraCat/Basic.lean
@@ -153,7 +153,7 @@ instance hasForgetToRing : HasForget₂ (AlgebraCat.{v} R) RingCat.{v} where
 instance hasForgetToModule : HasForget₂ (AlgebraCat.{v} R) (ModuleCat.{v} R) where
   forget₂ :=
     { obj := fun M => ModuleCat.of R M
-      map := fun f => ModuleCat.asHom f.hom.toLinearMap }
+      map := fun f => ModuleCat.ofHom f.hom.toLinearMap }
 
 @[simp]
 lemma forget₂_module_obj (X : AlgebraCat.{v} R) :
@@ -162,7 +162,7 @@ lemma forget₂_module_obj (X : AlgebraCat.{v} R) :
 
 @[simp]
 lemma forget₂_module_map {X Y : AlgebraCat.{v} R} (f : X ⟶ Y) :
-    (forget₂ (AlgebraCat.{v} R) (ModuleCat.{v} R)).map f = ModuleCat.asHom f.hom.toLinearMap :=
+    (forget₂ (AlgebraCat.{v} R) (ModuleCat.{v} R)).map f = ModuleCat.ofHom f.hom.toLinearMap :=
   rfl
 
 variable {R} in
diff --git a/Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean b/Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean
@@ -38,8 +38,8 @@ variable {R : Type u} [CommRing R]
 /-- An `R`-coalgebra is a comonoid object in the category of `R`-modules. -/
 @[simps] def toComonObj (X : CoalgebraCat R) : Comon_ (ModuleCat R) where
   X := ModuleCat.of R X
-  counit := ModuleCat.asHom Coalgebra.counit
-  comul := ModuleCat.asHom Coalgebra.comul
+  counit := ModuleCat.ofHom Coalgebra.counit
+  comul := ModuleCat.ofHom Coalgebra.comul
   counit_comul := by simpa only [ModuleCat.of_coe] using Coalgebra.rTensor_counit_comp_comul
   comul_counit := by simpa only [ModuleCat.of_coe] using Coalgebra.lTensor_counit_comp_comul
   comul_assoc := by simp_rw [ModuleCat.of_coe]; exact Coalgebra.coassoc.symm
@@ -50,7 +50,7 @@ variable (R) in
 def toComon : CoalgebraCat R ⥤ Comon_ (ModuleCat R) where
   obj X := toComonObj X
   map f :=
-    { hom := ModuleCat.asHom f.1
+    { hom := ModuleCat.ofHom f.1
       hom_counit := f.1.counit_comp
       hom_comul := f.1.map_comp_comul.symm }
 
diff --git a/Mathlib/Algebra/Category/FGModuleCat/Basic.lean b/Mathlib/Algebra/Category/FGModuleCat/Basic.lean
@@ -267,8 +267,8 @@ end FGModuleCat
 @[simp] theorem LinearMap.comp_id_fgModuleCat
     {R} [Ring R] {G : FGModuleCat.{u} R} {H : Type u} [AddCommGroup H] [Module R H]
     (f : G →ₗ[R] H) : f.comp (𝟙 G) = f :=
-  Category.id_comp (ModuleCat.asHom f)
+  Category.id_comp (ModuleCat.ofHom f)
 @[simp] theorem LinearMap.id_fgModuleCat_comp
     {R} [Ring R] {G : Type u} [AddCommGroup G] [Module R G] {H : FGModuleCat.{u} R}
     (f : G →ₗ[R] H) : LinearMap.comp (𝟙 H) f = f :=
-  Category.comp_id (ModuleCat.asHom f)
+  Category.comp_id (ModuleCat.ofHom f)
diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -209,21 +209,21 @@ variable {X₁ X₂ : Type v}
 open ModuleCat
 
 /-- Reinterpreting a linear map in the category of `R`-modules. -/
-def ModuleCat.asHom [AddCommGroup X₁] [Module R X₁] [AddCommGroup X₂] [Module R X₂] :
+def ModuleCat.ofHom [AddCommGroup X₁] [Module R X₁] [AddCommGroup X₂] [Module R X₂] :
     (X₁ →ₗ[R] X₂) → (ModuleCat.of R X₁ ⟶ ModuleCat.of R X₂) :=
   id
 
-@[deprecated (since := "2024-10-06")] alias ModuleCat.ofHom := ModuleCat.asHom
+@[deprecated (since := "2024-12-03")] alias ModuleCat.asHom := ModuleCat.ofHom
 
 /-- Reinterpreting a linear map in the category of `R`-modules -/
-scoped[ModuleCat] notation "↟" f:1024 => ModuleCat.asHom f
+scoped[ModuleCat] notation "↟" f:1024 => ModuleCat.ofHom f
 
 @[simp 1100]
-theorem ModuleCat.asHom_apply {R : Type u} [Ring R] {X Y : Type v} [AddCommGroup X] [Module R X]
+theorem ModuleCat.ofHom_apply {R : Type u} [Ring R] {X Y : Type v} [AddCommGroup X] [Module R X]
     [AddCommGroup Y] [Module R Y] (f : X →ₗ[R] Y) (x : X) : (↟ f) x = f x :=
   rfl
 
-@[deprecated (since := "2024-10-06")] alias ModuleCat.ofHom_apply := ModuleCat.asHom_apply
+@[deprecated (since := "2024-10-06")] alias ModuleCat.asHom_apply := ModuleCat.ofHom_apply
 
 /-- Reinterpreting a linear map in the category of `R`-modules. -/
 def ModuleCat.asHomRight [AddCommGroup X₁] [Module R X₁] {X₂ : ModuleCat.{v} R} :
@@ -440,8 +440,8 @@ end ModuleCat
 @[simp] theorem LinearMap.comp_id_moduleCat
     {R} [Ring R] {G : ModuleCat.{u} R} {H : Type u} [AddCommGroup H] [Module R H] (f : G →ₗ[R] H) :
     f.comp (𝟙 G) = f :=
-  Category.id_comp (ModuleCat.asHom f)
+  Category.id_comp (ModuleCat.ofHom f)
 @[simp] theorem LinearMap.id_moduleCat_comp
     {R} [Ring R] {G : Type u} [AddCommGroup G] [Module R G] {H : ModuleCat.{u} R} (f : G →ₗ[R] H) :
     LinearMap.comp (𝟙 H) f = f :=
-  Category.comp_id (ModuleCat.asHom f)
+  Category.comp_id (ModuleCat.ofHom f)
diff --git a/Mathlib/Algebra/Category/ModuleCat/Biproducts.lean b/Mathlib/Algebra/Category/ModuleCat/Biproducts.lean
@@ -144,8 +144,8 @@ of modules. -/
 noncomputable def lequivProdOfRightSplitExact {f : B →ₗ[R] M} (hj : Function.Injective j)
     (exac : LinearMap.range j = LinearMap.ker g) (h : g.comp f = LinearMap.id) : (A × B) ≃ₗ[R] M :=
   ((ShortComplex.Splitting.ofExactOfSection _
-    (ShortComplex.Exact.moduleCat_of_range_eq_ker (ModuleCat.asHom j)
-    (ModuleCat.asHom g) exac) (asHom f) h
+    (ShortComplex.Exact.moduleCat_of_range_eq_ker (ModuleCat.ofHom j)
+    (ModuleCat.ofHom g) exac) (ofHom f) h
     (by simpa only [ModuleCat.mono_iff_injective])).isoBinaryBiproduct ≪≫
     biprodIsoProd _ _ ).symm.toLinearEquiv
 
@@ -154,8 +154,8 @@ of modules. -/
 noncomputable def lequivProdOfLeftSplitExact {f : M →ₗ[R] A} (hg : Function.Surjective g)
     (exac : LinearMap.range j = LinearMap.ker g) (h : f.comp j = LinearMap.id) : (A × B) ≃ₗ[R] M :=
   ((ShortComplex.Splitting.ofExactOfRetraction _
-    (ShortComplex.Exact.moduleCat_of_range_eq_ker (ModuleCat.asHom j)
-    (ModuleCat.asHom g) exac) (ModuleCat.asHom f) h
+    (ShortComplex.Exact.moduleCat_of_range_eq_ker (ModuleCat.ofHom j)
+    (ModuleCat.ofHom g) exac) (ModuleCat.ofHom f) h
     (by simpa only [ModuleCat.epi_iff_surjective] using hg)).isoBinaryBiproduct ≪≫
     biprodIsoProd _ _).symm.toLinearEquiv
 
diff --git a/Mathlib/Algebra/Category/ModuleCat/Images.lean b/Mathlib/Algebra/Category/ModuleCat/Images.lean
@@ -97,12 +97,12 @@ noncomputable def imageIsoRange {G H : ModuleCat.{v} R} (f : G ⟶ H) :
 
 @[simp, reassoc, elementwise]
 theorem imageIsoRange_inv_image_ι {G H : ModuleCat.{v} R} (f : G ⟶ H) :
-    (imageIsoRange f).inv ≫ Limits.image.ι f = ModuleCat.asHom f.range.subtype :=
+    (imageIsoRange f).inv ≫ Limits.image.ι f = ModuleCat.ofHom f.range.subtype :=
   IsImage.isoExt_inv_m _ _
 
 @[simp, reassoc, elementwise]
 theorem imageIsoRange_hom_subtype {G H : ModuleCat.{v} R} (f : G ⟶ H) :
-    (imageIsoRange f).hom ≫ ModuleCat.asHom f.range.subtype = Limits.image.ι f := by
+    (imageIsoRange f).hom ≫ ModuleCat.ofHom f.range.subtype = Limits.image.ι f := by
   rw [← imageIsoRange_inv_image_ι f, Iso.hom_inv_id_assoc]
 
 end ModuleCat
diff --git a/Mathlib/Algebra/Category/ModuleCat/Injective.lean b/Mathlib/Algebra/Category/ModuleCat/Injective.lean
@@ -27,8 +27,8 @@ theorem injective_module_of_injective_object
     [inj : CategoryTheory.Injective <| ModuleCat.of R M] :
     Module.Injective R M where
   out X Y _ _ _ _ f hf g := by
-    have : CategoryTheory.Mono (ModuleCat.asHom f) := (ModuleCat.mono_iff_injective _).mpr hf
-    obtain ⟨l, rfl⟩ := inj.factors (ModuleCat.asHom g) (ModuleCat.asHom f)
+    have : CategoryTheory.Mono (ModuleCat.ofHom f) := (ModuleCat.mono_iff_injective _).mpr hf
+    obtain ⟨l, rfl⟩ := inj.factors (ModuleCat.ofHom g) (ModuleCat.ofHom f)
     exact ⟨l, fun _ ↦ rfl⟩
 
 theorem injective_iff_injective_object :
diff --git a/Mathlib/Algebra/Category/ModuleCat/Kernels.lean b/Mathlib/Algebra/Category/ModuleCat/Kernels.lean
@@ -26,7 +26,7 @@ variable {M N : ModuleCat.{v} R} (f : M ⟶ N)
 /-- The kernel cone induced by the concrete kernel. -/
 def kernelCone : KernelFork f :=
   -- Porting note: previously proven by tidy
-  KernelFork.ofι (asHom f.ker.subtype) <| by ext x; cases x; assumption
+  KernelFork.ofι (ofHom f.ker.subtype) <| by ext x; cases x; assumption
 
 /-- The kernel of a linear map is a kernel in the categorical sense. -/
 def kernelIsLimit : IsLimit (kernelCone f) :=
@@ -44,7 +44,7 @@ def kernelIsLimit : IsLimit (kernelCone f) :=
 
 /-- The cokernel cocone induced by the projection onto the quotient. -/
 def cokernelCocone : CokernelCofork f :=
-  CokernelCofork.ofπ (asHom f.range.mkQ) <| LinearMap.range_mkQ_comp _
+  CokernelCofork.ofπ (ofHom f.range.mkQ) <| LinearMap.range_mkQ_comp _
 
 /-- The projection onto the quotient is a cokernel in the categorical sense. -/
 def cokernelIsColimit : IsColimit (cokernelCocone f) :=
@@ -53,10 +53,10 @@ def cokernelIsColimit : IsColimit (cokernelCocone f) :=
       f.range.liftQ (Cofork.π s) <| LinearMap.range_le_ker_iff.2 <| CokernelCofork.condition s)
     (fun s => f.range.liftQ_mkQ (Cofork.π s) _) fun s m h => by
     -- Porting note (https://github.com/leanprover-community/mathlib4/pull/11036): broken dot notation
-    haveI : Epi (asHom (LinearMap.range f).mkQ) :=
+    haveI : Epi (ofHom (LinearMap.range f).mkQ) :=
       (epi_iff_range_eq_top _).mpr (Submodule.range_mkQ _)
     -- Porting note (https://github.com/leanprover-community/mathlib4/pull/11036): broken dot notation
-    apply (cancel_epi (asHom (LinearMap.range f).mkQ)).1
+    apply (cancel_epi (ofHom (LinearMap.range f).mkQ)).1
     convert h
     -- Porting note: no longer necessary
     -- exact Submodule.liftQ_mkQ _ _ _
diff --git a/Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean b/Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean
@@ -33,7 +33,7 @@ linear maps `f` and `g` and the vanishing of their composition. -/
 def moduleCatMk {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃]
     [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃)
     (hfg : g.comp f = 0) : ShortComplex (ModuleCat.{v} R) :=
-  ShortComplex.mk (ModuleCat.asHom f) (ModuleCat.asHom g) hfg
+  ShortComplex.mk (ModuleCat.ofHom f) (ModuleCat.ofHom g) hfg
 
 variable (S : ShortComplex (ModuleCat.{v} R))
 
@@ -138,7 +138,7 @@ def moduleCatLeftHomologyData : S.LeftHomologyData where
     erw [Submodule.Quotient.mk_eq_zero]
     rw [LinearMap.mem_range]
     apply exists_apply_eq_apply
-  hπ := ModuleCat.cokernelIsColimit (ModuleCat.asHom S.moduleCatToCycles)
+  hπ := ModuleCat.cokernelIsColimit (ModuleCat.ofHom S.moduleCatToCycles)
 
 @[simp]
 lemma moduleCatLeftHomologyData_f' :
diff --git a/Mathlib/CategoryTheory/Linear/Yoneda.lean b/Mathlib/CategoryTheory/Linear/Yoneda.lean
@@ -28,7 +28,7 @@ namespace CategoryTheory
 variable (R : Type w) [Ring R] {C : Type u} [Category.{v} C] [Preadditive C] [Linear R C]
 variable (C)
 
--- Porting note: inserted specific `ModuleCat.asHom` in the definition of `linearYoneda`
+-- Porting note: inserted specific `ModuleCat.ofHom` in the definition of `linearYoneda`
 -- and similarly in `linearCoyoneda`, otherwise many simp lemmas are not triggered automatically.
 -- Eventually, doing so allows more proofs to be automatic!
 /-- The Yoneda embedding for `R`-linear categories `C`,
@@ -38,9 +38,9 @@ with value on `Y : Cᵒᵖ` given by `ModuleCat.of R (unop Y ⟶ X)`. -/
 def linearYoneda : C ⥤ Cᵒᵖ ⥤ ModuleCat R where
   obj X :=
     { obj := fun Y => ModuleCat.of R (unop Y ⟶ X)
-      map := fun f => ModuleCat.asHom (Linear.leftComp R _ f.unop) }
+      map := fun f => ModuleCat.ofHom (Linear.leftComp R _ f.unop) }
   map {X₁ X₂} f :=
-    { app := fun Y => @ModuleCat.asHom R _ (Y.unop ⟶ X₁) (Y.unop ⟶ X₂) _ _ _ _
+    { app := fun Y => @ModuleCat.ofHom R _ (Y.unop ⟶ X₁) (Y.unop ⟶ X₂) _ _ _ _
         (Linear.rightComp R _ f) }
 
 /-- The Yoneda embedding for `R`-linear categories `C`,
@@ -50,9 +50,9 @@ with value on `X : C` given by `ModuleCat.of R (unop Y ⟶ X)`. -/
 def linearCoyoneda : Cᵒᵖ ⥤ C ⥤ ModuleCat R where
   obj Y :=
     { obj := fun X => ModuleCat.of R (unop Y ⟶ X)
-      map := fun f => ModuleCat.asHom (Linear.rightComp R _ f) }
+      map := fun f => ModuleCat.ofHom (Linear.rightComp R _ f) }
   map {Y₁ Y₂} f :=
-    { app := fun X => @ModuleCat.asHom R _ (unop Y₁ ⟶ X) (unop Y₂ ⟶ X) _ _ _ _
+    { app := fun X => @ModuleCat.ofHom R _ (unop Y₁ ⟶ X) (unop Y₂ ⟶ X) _ _ _ _
         (Linear.leftComp _ _ f.unop) }
 
 instance linearYoneda_obj_additive (X : C) : ((linearYoneda R C).obj X).Additive where
diff --git a/Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean b/Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean
@@ -39,7 +39,7 @@ object `X` to the `End Y`-module of morphisms `X ⟶ Y`.
 @[simps]
 def preadditiveYonedaObj (Y : C) : Cᵒᵖ ⥤ ModuleCat.{v} (End Y) where
   obj X := ModuleCat.of _ (X.unop ⟶ Y)
-  map f := ModuleCat.asHom
+  map f := ModuleCat.ofHom
     { toFun := fun g => f.unop ≫ g
       map_add' := fun _ _ => comp_add _ _ _ _ _ _
       map_smul' := fun _ _ => Eq.symm <| Category.assoc _ _ _ }
@@ -66,7 +66,7 @@ object `Y` to the `End X`-module of morphisms `X ⟶ Y`.
 @[simps]
 def preadditiveCoyonedaObj (X : Cᵒᵖ) : C ⥤ ModuleCat.{v} (End X) where
   obj Y := ModuleCat.of _ (unop X ⟶ Y)
-  map f := ModuleCat.asHom
+  map f := ModuleCat.ofHom
     { toFun := fun g => g ≫ f
       map_add' := fun _ _ => add_comp _ _ _ _ _ _
       map_smul' := fun _ _ => Category.assoc _ _ _ }
diff --git a/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean b/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
@@ -201,9 +201,9 @@ theorem dOne_comp_dZero : dOne A ∘ₗ dZero A = 0 := by
   rfl
 
 theorem dTwo_comp_dOne : dTwo A ∘ₗ dOne A = 0 := by
-  show ModuleCat.asHom (dOne A) ≫ ModuleCat.asHom (dTwo A) = _
-  have h1 : _ ≫ ModuleCat.asHom (dOne A) = _ ≫ _ := congr_arg ModuleCat.asHom (dOne_comp_eq A)
-  have h2 : _ ≫ ModuleCat.asHom (dTwo A) = _ ≫ _ := congr_arg ModuleCat.asHom (dTwo_comp_eq A)
+  show ModuleCat.ofHom (dOne A) ≫ ModuleCat.ofHom (dTwo A) = _
+  have h1 : _ ≫ ModuleCat.ofHom (dOne A) = _ ≫ _ := congr_arg ModuleCat.ofHom (dOne_comp_eq A)
+  have h2 : _ ≫ ModuleCat.ofHom (dTwo A) = _ ≫ _ := congr_arg ModuleCat.ofHom (dTwo_comp_eq A)
   simp only [← LinearEquiv.toModuleIso_hom] at h1 h2
   simp only [(Iso.eq_inv_comp _).2 h2, (Iso.eq_inv_comp _).2 h1,
     Category.assoc, Iso.hom_inv_id_assoc, HomologicalComplex.d_comp_d_assoc, zero_comp, comp_zero]
@@ -749,7 +749,7 @@ lemma shortComplexH0_exact : (shortComplexH0 A).Exact := by
 `(inhomogeneousCochains A).d 0 1` of the complex of inhomogeneous cochains of `A`. -/
 @[simps! hom_left hom_right inv_left inv_right]
 def dZeroArrowIso : Arrow.mk ((inhomogeneousCochains A).d 0 1) ≅
-    Arrow.mk (ModuleCat.asHom (dZero A)) :=
+    Arrow.mk (ModuleCat.ofHom (dZero A)) :=
   Arrow.isoMk (zeroCochainsLequiv A).toModuleIso
     (oneCochainsLequiv A).toModuleIso (dZero_comp_eq A)
 
@@ -797,7 +797,7 @@ def isoOneCocycles : cocycles A 1 ≅ ModuleCat.of k (oneCocycles A) :=
     cyclesMapIso (shortComplexH1Iso A) ≪≫ (shortComplexH1 A).moduleCatCyclesIso
 
 lemma isoOneCocycles_hom_comp_subtype :
-    (isoOneCocycles A).hom ≫ ModuleCat.asHom (oneCocycles A).subtype =
+    (isoOneCocycles A).hom ≫ ModuleCat.ofHom (oneCocycles A).subtype =
       iCocycles A 1 ≫ (oneCochainsLequiv A).toModuleIso.hom := by
   dsimp [isoOneCocycles]
   rw [Category.assoc, Category.assoc]
@@ -807,7 +807,7 @@ lemma isoOneCocycles_hom_comp_subtype :
 lemma toCocycles_comp_isoOneCocycles_hom :
     toCocycles A 0 1 ≫ (isoOneCocycles A).hom =
       (zeroCochainsLequiv A).toModuleIso.hom ≫
-        ModuleCat.asHom (shortComplexH1 A).moduleCatToCycles := by
+        ModuleCat.ofHom (shortComplexH1 A).moduleCatToCycles := by
   simp [isoOneCocycles]
   rfl
 
@@ -845,7 +845,7 @@ def isoTwoCocycles : cocycles A 2 ≅ ModuleCat.of k (twoCocycles A) :=
     cyclesMapIso (shortComplexH2Iso A) ≪≫ (shortComplexH2 A).moduleCatCyclesIso
 
 lemma isoTwoCocycles_hom_comp_subtype :
-    (isoTwoCocycles A).hom ≫ ModuleCat.asHom (twoCocycles A).subtype =
+    (isoTwoCocycles A).hom ≫ ModuleCat.ofHom (twoCocycles A).subtype =
       iCocycles A 2 ≫ (twoCochainsLequiv A).toModuleIso.hom := by
   dsimp [isoTwoCocycles]
   rw [Category.assoc, Category.assoc]
@@ -855,7 +855,7 @@ lemma isoTwoCocycles_hom_comp_subtype :
 lemma toCocycles_comp_isoTwoCocycles_hom :
     toCocycles A 1 2 ≫ (isoTwoCocycles A).hom =
       (oneCochainsLequiv A).toModuleIso.hom ≫
-        ModuleCat.asHom (shortComplexH2 A).moduleCatToCycles := by
+        ModuleCat.ofHom (shortComplexH2 A).moduleCatToCycles := by
   simp [isoTwoCocycles]
   rfl
 
diff --git a/Mathlib/RepresentationTheory/Rep.lean b/Mathlib/RepresentationTheory/Rep.lean
@@ -332,7 +332,7 @@ variable [Group G] (A B C : Rep k G)
 protected def ihom (A : Rep k G) : Rep k G ⥤ Rep k G where
   obj B := Rep.of (Representation.linHom A.ρ B.ρ)
   map := fun {X} {Y} f =>
-    { hom := ModuleCat.asHom (LinearMap.llcomp k _ _ _ f.hom)
+    { hom := ModuleCat.ofHom (LinearMap.llcomp k _ _ _ f.hom)
       comm := fun g => LinearMap.ext fun x => LinearMap.ext fun y => by
         show f.hom (X.ρ g _) = _
         simp only [hom_comm_apply]; rfl }
diff --git a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
@@ -241,17 +241,17 @@ private instance : AddCommGroup (AdicCompletion I R ⊗[R] (LinearMap.ker f)) :=
 
 private def firstRow : ComposableArrows (ModuleCat (AdicCompletion I R)) 4 :=
   ComposableArrows.mk₄
-    (ModuleCat.asHom <| lTensorKerIncl I M f)
-    (ModuleCat.asHom <| lTensorf I M f)
-    (ModuleCat.asHom (0 : AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] PUnit))
-    (ModuleCat.asHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
+    (ModuleCat.ofHom <| lTensorKerIncl I M f)
+    (ModuleCat.ofHom <| lTensorf I M f)
+    (ModuleCat.ofHom (0 : AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] PUnit))
+    (ModuleCat.ofHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
 
 private def secondRow : ComposableArrows (ModuleCat (AdicCompletion I R)) 4 :=
   ComposableArrows.mk₄
-    (ModuleCat.asHom (map I <| (LinearMap.ker f).subtype))
-    (ModuleCat.asHom (map I f))
-    (ModuleCat.asHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
-    (ModuleCat.asHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
+    (ModuleCat.ofHom (map I <| (LinearMap.ker f).subtype))
+    (ModuleCat.ofHom (map I f))
+    (ModuleCat.ofHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
+    (ModuleCat.ofHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
 
 include hf
 
@@ -282,25 +282,25 @@ private lemma secondRow_exact [Fintype ι] [IsNoetherianRing R] : (secondRow I M
 /- The compatible vertical maps between the first and the second row. -/
 private def firstRowToSecondRow : firstRow I M f ⟶ secondRow I M f :=
   ComposableArrows.homMk₄
-    (ModuleCat.asHom (ofTensorProduct I (LinearMap.ker f)))
-    (ModuleCat.asHom (ofTensorProduct I (ι → R)))
-    (ModuleCat.asHom (ofTensorProduct I M))
-    (ModuleCat.asHom 0)
-    (ModuleCat.asHom 0)
+    (ModuleCat.ofHom (ofTensorProduct I (LinearMap.ker f)))
+    (ModuleCat.ofHom (ofTensorProduct I (ι → R)))
+    (ModuleCat.ofHom (ofTensorProduct I M))
+    (ModuleCat.ofHom 0)
+    (ModuleCat.ofHom 0)
     (ofTensorProduct_naturality I <| (LinearMap.ker f).subtype).symm
     (ofTensorProduct_naturality I f).symm
     rfl
     rfl
 
 private lemma ofTensorProduct_iso [Fintype ι] [IsNoetherianRing R] :
-    IsIso (ModuleCat.asHom (ofTensorProduct I M)) := by
+    IsIso (ModuleCat.ofHom (ofTensorProduct I M)) := by
   refine Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
     (firstRow_exact I M f hf) (secondRow_exact I M f hf) (firstRowToSecondRow I M f) ?_ ?_ ?_ ?_
   · apply ConcreteCategory.epi_of_surjective
     exact ofTensorProduct_surjective_of_finite I (LinearMap.ker f)
   · apply (ConcreteCategory.isIso_iff_bijective _).mpr
     exact ofTensorProduct_bijective_of_pi_of_fintype I ι
-  · show IsIso (ModuleCat.asHom 0)
+  · show IsIso (ModuleCat.ofHom 0)
     apply Limits.isIso_of_isTerminal
       <;> exact Limits.IsZero.isTerminal (ModuleCat.isZero_of_subsingleton _)
   · apply ConcreteCategory.mono_of_injective
@@ -310,9 +310,9 @@ private lemma ofTensorProduct_iso [Fintype ι] [IsNoetherianRing R] :
 private
 lemma ofTensorProduct_bijective_of_map_from_fin [Fintype ι] [IsNoetherianRing R] :
     Function.Bijective (ofTensorProduct I M) := by
-  have : IsIso (ModuleCat.asHom (ofTensorProduct I M)) :=
+  have : IsIso (ModuleCat.ofHom (ofTensorProduct I M)) :=
     ofTensorProduct_iso I M f hf
-  exact ConcreteCategory.bijective_of_isIso (ModuleCat.asHom (ofTensorProduct I M))
+  exact ConcreteCategory.bijective_of_isIso (ModuleCat.ofHom (ofTensorProduct I M))
 
 end
 
diff --git a/Mathlib/RingTheory/Coalgebra/TensorProduct.lean b/Mathlib/RingTheory/Coalgebra/TensorProduct.lean
@@ -58,7 +58,7 @@ noncomputable instance TensorProduct.instCoalgebra : Coalgebra R (M ⊗[R] N) :=
         rw [CoalgebraCat.ofComonObjCoalgebraStruct_comul]
         simp [-Mon_.monMonoidalStruct_tensorObj_X,
           ModuleCat.MonoidalCategory.instMonoidalCategoryStruct_tensorHom,
-          ModuleCat.comp_def, ModuleCat.of, ModuleCat.asHom,
+          ModuleCat.comp_def, ModuleCat.of, ModuleCat.ofHom,
           ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm] }
 
 end
diff --git a/Mathlib/RingTheory/Flat/CategoryTheory.lean b/Mathlib/RingTheory/Flat/CategoryTheory.lean
diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean
