doc(CategoryTheory): fix stale names (#33035)

harahu · harahu · commit 8c38971b569e · 2025-12-18T17:46:29.000Z
These stale names were found and fixed by Codex.
diff --git a/Mathlib/CategoryTheory/Bicategory/CatEnriched.lean b/Mathlib/CategoryTheory/Bicategory/CatEnriched.lean
@@ -20,11 +20,11 @@ We define a type alias `CatEnriched C` for a type `C` with an `EnrichedCategory
 provide this with an instance of a strict bicategory structure constructing
 `Bicategory.Strict (CatEnriched C)`.
 
-If `C` is a type with an `EnrichedOrdinaryCategory Cat C` structure, then it has an `Enriched Cat C`
-structure, so the previous construction would again produce a strict bicategory. However, in this
-setting `C` is also given a `Category C` structure, together with an equivalence between this
-category and the underlying category of the `Enriched Cat C`, and in examples the given category
-structure is the preferred one.
+If `C` is a type with an `EnrichedOrdinaryCategory Cat C` structure, then it has an
+`EnrichedCategory Cat C` structure, so the previous construction would again produce a strict
+bicategory. However, in this setting `C` is also given a `Category C` structure, together with an
+equivalence between this category and the underlying category of the `EnrichedCategory Cat C`, and
+in examples the given category structure is the preferred one.
 
 Thus, we define a type alias `CatEnrichedOrdinary C` for a type `C` with an
 `EnrichedOrdinaryCategory Cat C` structure. We provide this with an instance of a strict bicategory
diff --git a/Mathlib/CategoryTheory/Functor/EpiMono.lean b/Mathlib/CategoryTheory/Functor/EpiMono.lean
@@ -269,7 +269,7 @@ theorem mono_map_iff_mono [hF₁ : PreservesMonomorphisms F] [hF₂ : ReflectsMo
   · intro h
     exact F.map_mono f
 
-/-- If `F : C ⥤ D` is an equivalence of categories and `C` is a `split_epi_category`,
+/-- If `F : C ⥤ D` is an equivalence of categories and `C` is a `SplitEpiCategory`,
 then `D` also is. -/
 theorem splitEpiCategoryImpOfIsEquivalence [IsEquivalence F] [SplitEpiCategory C] :
     SplitEpiCategory D :=
diff --git a/Mathlib/CategoryTheory/Iso.lean b/Mathlib/CategoryTheory/Iso.lean
@@ -16,7 +16,7 @@ This file defines isomorphisms between objects of a category.
 ## Main definitions
 
 - `structure Iso` : a bundled isomorphism between two objects of a category;
-- `class IsIso` : an unbundled version of `iso`;
+- `class IsIso` : an unbundled version of `Iso`;
   note that `IsIso f` is a `Prop`, and only asserts the existence of an inverse.
   Of course, this inverse is unique, so it doesn't cost us much to use choice to retrieve it.
 - `inv f`, for the inverse of a morphism with `[IsIso f]`
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
@@ -38,7 +38,7 @@ Each of these has a dual.
 
 ## Implementation notes
 As with the other special shapes in the limits library, all the definitions here are given as
-`abbreviation`s of the general statements for limits, so all the `simp` lemmas and theorems about
+`abbrev`s of the general statements for limits, so all the `simp` lemmas and theorems about
 general limits can be used.
 
 ## References
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean b/Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean
@@ -31,7 +31,7 @@ namespace CategoryTheory.Limits
 
 variable (C : Type u) [Category.{v} C]
 
--- We can't just made this an `abbreviation`
+-- We can't just made this an `abbrev`
 -- because of https://github.com/leanprover-community/lean/issues/429
 /-- A category has all finite limits if every functor `J ⥤ C` with a `FinCategory J`
 instance and `J : Type` has a limit.
@@ -213,7 +213,7 @@ instance finCategoryWidePullback [Fintype J] : FinCategory (WidePullbackShape J)
 instance finCategoryWidePushout [Fintype J] : FinCategory (WidePushoutShape J) where
   fintypeHom := WidePushoutShape.fintypeHom
 
--- We can't just made this an `abbreviation`
+-- We can't just made this an `abbrev`
 -- because of https://github.com/leanprover-community/lean/issues/429
 /-- A category `HasFiniteWidePullbacks` if it has all limits of shape `WidePullbackShape J` for
 finite `J`, i.e. if it has a wide pullback for every finite collection of morphisms with the same
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean
@@ -825,7 +825,7 @@ section
 
 variable (C) [HasImages C]
 
-/-- If a category `has_image_maps`, then all commutative squares induce morphisms on images. -/
+/-- If a category `HasImageMaps`, then all commutative squares induce morphisms on images. -/
 class HasImageMaps : Prop where
   has_image_map : ∀ {f g : Arrow C} (st : f ⟶ g), HasImageMap st
 
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
@@ -136,7 +136,7 @@ def IsInitial.ofUniqueHom {X : C} (h : ∀ Y : C, X ⟶ Y) (uniq : ∀ (Y : C) (
 def isInitialBot {α : Type*} [Preorder α] [OrderBot α] : IsInitial (⊥ : α) :=
   IsInitial.ofUnique _
 
-/-- Transport a term of type `is_initial` across an isomorphism. -/
+/-- Transport a term of type `IsInitial` across an isomorphism. -/
 def IsInitial.ofIso {X Y : C} (hX : IsInitial X) (i : X ≅ Y) : IsInitial Y :=
   IsColimit.ofIsoColimit hX
     { hom := { hom := i.hom }
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean b/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
@@ -39,7 +39,7 @@ and the corresponding dual statements.
 
 ## Implementation notes
 As with the other special shapes in the limits library, all the definitions here are given as
-`abbreviation`s of the general statements for limits, so all the `simp` lemmas and theorems about
+`abbrev`s of the general statements for limits, so all the `simp` lemmas and theorems about
 general limits can be used.
 
 ## References
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
@@ -29,7 +29,7 @@ Each of these has a dual.
 
 ## Implementation notes
 As with the other special shapes in the limits library, all the definitions here are given as
-`abbreviation`s of the general statements for limits, so all the `simp` lemmas and theorems about
+`abbrev`s of the general statements for limits, so all the `simp` lemmas and theorems about
 general limits can be used.
 -/
 
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
@@ -35,7 +35,7 @@ Each of these has a dual.
 
 ## Implementation notes
 As with the other special shapes in the limits library, all the definitions here are given as
-`abbreviation`s of the general statements for limits, so all the `simp` lemmas and theorems about
+`abbrev`s of the general statements for limits, so all the `simp` lemmas and theorems about
 general limits can be used.
 
 ## References
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean b/Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
@@ -223,7 +223,7 @@ morphisms for some other reason, for example from additivity. Library code that
 `zeroMorphismsOfZeroObject` will then be incompatible with these categories because
 the `HasZeroMorphisms` instances will not be definitionally equal. For this reason library
 code should generally ask for an instance of `HasZeroMorphisms` separately, even if it already
-asks for an instance of `HasZeroObjects`. -/
+asks for an instance of `HasZeroObject`. -/
 def IsZero.hasZeroMorphisms {O : C} (hO : IsZero O) : HasZeroMorphisms C where
   zero X Y := { zero := hO.from_ X ≫ hO.to_ Y }
   zero_comp X {Y Z} f := by
@@ -248,9 +248,9 @@ open ZeroObject
 It is rarely a good idea to use this. Many categories that have a zero object have zero
 morphisms for some other reason, for example from additivity. Library code that uses
 `zeroMorphismsOfZeroObject` will then be incompatible with these categories because
-the `has_zero_morphisms` instances will not be definitionally equal. For this reason library
+the `HasZeroMorphisms` instances will not be definitionally equal. For this reason library
 code should generally ask for an instance of `HasZeroMorphisms` separately, even if it already
-asks for an instance of `HasZeroObjects`. -/
+asks for an instance of `HasZeroObject`. -/
 def zeroMorphismsOfZeroObject : HasZeroMorphisms C where
   zero X _ := { zero := (default : X ⟶ 0) ≫ default }
   zero_comp X {Y Z} f := by
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean b/Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean
@@ -40,7 +40,7 @@ namespace Limits
 /-- An object `X` in a category is a *zero object* if for every object `Y`
 there is a unique morphism `to : X → Y` and a unique morphism `from : Y → X`.
 
-This is a characteristic predicate for `has_zero_object`. -/
+This is a characteristic predicate for `HasZeroObject`. -/
 structure IsZero (X : C) : Prop where
   /-- there are unique morphisms to the object -/
   unique_to : ∀ Y, Nonempty (Unique (X ⟶ Y))
diff --git a/Mathlib/CategoryTheory/Localization/Construction.lean b/Mathlib/CategoryTheory/Localization/Construction.lean
@@ -182,7 +182,7 @@ theorem uniq (G₁ G₂ : W.Localization ⥤ D) (h : W.Q ⋙ G₁ = W.Q ⋙ G₂
 
 variable (W) in
 /-- The canonical bijection between objects in a category and its
-localization with respect to a morphism_property `W` -/
+localization with respect to a `MorphismProperty` `W` -/
 @[simps]
 def objEquiv : C ≃ W.Localization where
   toFun := W.Q.obj
diff --git a/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
@@ -363,7 +363,7 @@ This has to be a definition rather than an instance to avoid diamonds, for examp
 `category_theory.monoidal_closed.functor_closed` and
 `CategoryTheory.Monoidal.functorHasLeftDual`. Moreover, in concrete applications there is often
 a more useful definition of the internal hom object than `ᘁY ⊗ X`, in which case the closed
-structure shouldn't come from `has_left_dual` (e.g. in the category `FinVect k`, it is more
+structure shouldn't come from `HasLeftDual` (e.g. in the category `FinVect k`, it is more
 convenient to define the internal hom as `Y →ₗ[k] X` rather than `ᘁY ⊗ X` even though these are
 naturally isomorphic).
 -/
diff --git a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean
@@ -132,8 +132,8 @@ instance IsStableUnderComposition.inverseImage {P : MorphismProperty D} [P.IsSta
   comp_mem f g hf hg := by simpa only [← F.map_comp] using P.comp_mem _ _ hf hg
 
 /-- Given `app : Π X, F₁.obj X ⟶ F₂.obj X` where `F₁` and `F₂` are two functors,
-this is the `morphism_property C` satisfied by the morphisms in `C` with respect
-to whom `app` is natural. -/
+this is the `MorphismProperty C` satisfied by the morphisms in `C` with respect
+to which `app` is natural. -/
 @[simp]
 def naturalityProperty {F₁ F₂ : C ⥤ D} (app : ∀ X, F₁.obj X ⟶ F₂.obj X) : MorphismProperty C :=
   fun X Y f => F₁.map f ≫ app Y = app X ≫ F₂.map f
diff --git a/Mathlib/CategoryTheory/Thin.lean b/Mathlib/CategoryTheory/Thin.lean
@@ -14,7 +14,7 @@ A thin category (also known as a sparse category) is a category with at most one
 each pair of objects.
 Examples include posets, but also some indexing categories (diagrams) for special shapes of
 (co)limits.
-To construct a category instance one only needs to specify the `category_struct` part,
+To construct a category instance one only needs to specify the `CategoryStruct` part,
 as the axioms hold for free.
 If `C` is thin, then the category of functors to `C` is also thin.
 Further, to show two objects are isomorphic in a thin category, it suffices only to give a morphism
@@ -34,7 +34,7 @@ section
 
 variable [CategoryStruct.{v₁} C] [Quiver.IsThin C]
 
-/-- Construct a category instance from a category_struct, using the fact that
+/-- Construct a category instance from a `CategoryStruct`, using the fact that
     hom spaces are subsingletons to prove the axioms. -/
 def thin_category : Category C where
 
