doc(Algebra,AlgebraicGeometry): remove mathlib3 names in doc comments (…

…#11955)

Mostly automatic, with a few manual corrections.

Mathlib/Algebra/BigOperators/Basic.lean

@@ -1208,7 +1208,7 @@ The difference with `Finset.prod_ite_eq` is that the arguments to `Eq` are swapp
 @[to_additive (attr := simp) "A sum taken over a conditional whose condition is an equality
 test on the index and whose alternative is `0` has value either the term at that index or `0`.
 
-The difference with `Finset.sum_ite_eq` is that the arguments to `eq` are swapped."]
+The difference with `Finset.sum_ite_eq` is that the arguments to `Eq` are swapped."]
 theorem prod_ite_eq' [DecidableEq α] (s : Finset α) (a : α) (b : α → β) :
     (∏ x in s, ite (x = a) (b x) 1) = ite (a ∈ s) (b a) 1 :=
   prod_dite_eq' s a fun x _ => b x

Mathlib/Algebra/BigOperators/Finsupp.lean

@@ -35,7 +35,7 @@ variable {β M M' N P G H R S : Type*}
 namespace Finsupp
 
 /-!
-### Declarations about `sum` and `prod`
+### Declarations about `Finsupp.sum` and `Finsupp.prod`
 
 In most of this section, the domain `β` is assumed to be an `AddMonoid`.
 -/
@@ -406,7 +406,7 @@ if `h` is an additive-to-multiplicative homomorphism.
 This is a more specialized version of `Finsupp.prod_add_index` with simpler hypotheses. -/
 @[to_additive
       "Taking the sum under `h` is an additive homomorphism of finsupps,if `h` is an additive
-      homomorphism. This is a more specific version of `finsupp.sum_add_index` with simpler
+      homomorphism. This is a more specific version of `Finsupp.sum_add_index` with simpler
       hypotheses."]
 theorem prod_add_index' [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} {h : α → M → N}
     (h_zero : ∀ a, h a 0 = 1) (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :

Mathlib/Algebra/Category/GroupCat/Adjunctions.lean

@@ -17,19 +17,19 @@ category of abelian groups.
 
 ## Main definitions
 
-* `AddCommGroup.free`: constructs the functor associating to a type `X` the free abelian group with
-  generators `x : X`.
-* `Group.free`: constructs the functor associating to a type `X` the free group with
+* `AddCommGroupCat.free`: constructs the functor associating to a type `X` the free abelian group
+  with generators `x : X`.
+* `GroupCat.free`: constructs the functor associating to a type `X` the free group with
   generators `x : X`.
 * `abelianize`: constructs the functor which associates to a group `G` its abelianization `Gᵃᵇ`.
 
 ## Main statements
 
-* `AddCommGroup.adj`: proves that `AddCommGroup.free` is the left adjoint of the forgetful functor
-  from abelian groups to types.
-* `Group.adj`: proves that `Group.free` is the left adjoint of the forgetful functor from groups to
-  types.
-* `abelianize_adj`: proves that `abelianize` is left adjoint to the forgetful functor from
+* `AddCommGroupCat.adj`: proves that `AddCommGroupCat.free` is the left adjoint
+  of the forgetful functor from abelian groups to types.
+* `GroupCat.adj`: proves that `GroupCat.free` is the left adjoint of the forgetful functor
+  from groups to types.
+* `abelianizeAdj`: proves that `abelianize` is left adjoint to the forgetful functor from
   abelian groups to groups.
 -/
 
@@ -179,7 +179,7 @@ def MonCat.units : MonCat.{u} ⥤ GroupCat.{u} where
   map_comp _ _ := MonoidHom.ext fun _ => Units.ext rfl
 #align Mon.units MonCat.units
 
-/-- The forgetful-units adjunction between `Group` and `Mon`. -/
+/-- The forgetful-units adjunction between `GroupCat` and `MonCat`. -/
 def GroupCat.forget₂MonAdj : forget₂ GroupCat MonCat ⊣ MonCat.units.{u} where
   homEquiv X Y :=
     { toFun := fun f => MonoidHom.toHomUnits f
@@ -208,7 +208,7 @@ def CommMonCat.units : CommMonCat.{u} ⥤ CommGroupCat.{u} where
   map_comp _ _ := MonoidHom.ext fun _ => Units.ext rfl
 #align CommMon.units CommMonCat.units
 
-/-- The forgetful-units adjunction between `CommGroup` and `CommMon`. -/
+/-- The forgetful-units adjunction between `CommGroupCat` and `CommMonCat`. -/
 def CommGroupCat.forget₂CommMonAdj : forget₂ CommGroupCat CommMonCat ⊣ CommMonCat.units.{u} where
   homEquiv X Y :=
     { toFun := fun f => MonoidHom.toHomUnits f

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -440,12 +440,12 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align add_equiv_iso_AddGroup_iso addEquivIsoAddGroupIso
 
-/-- "additive equivalences between `add_group`s are the same
-as (isomorphic to) isomorphisms in `AddGroup` -/
+/-- Additive equivalences between `AddGroup`s are the same
+as (isomorphic to) isomorphisms in `AddGroupCat`. -/
 add_decl_doc addEquivIsoAddGroupIso
 
-/-- multiplicative equivalences between `comm_group`s are the same as (isomorphic to) isomorphisms
-in `CommGroup` -/
+/-- Multiplicative equivalences between `CommGroup`s are the same as (isomorphic to) isomorphisms
+in `CommGroupCat`. -/
 @[to_additive]
 def mulEquivIsoCommGroupIso {X Y : CommGroupCat.{u}} : X ≃* Y ≅ X ≅ Y where
   hom e := e.toCommGroupCatIso
@@ -455,8 +455,8 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align add_equiv_iso_AddCommGroup_iso addEquivIsoAddCommGroupIso
 
-/-- additive equivalences between `AddCommGroup`s are
-the same as (isomorphic to) isomorphisms in `AddCommGroup` -/
+/-- Additive equivalences between `AddCommGroup`s are
+the same as (isomorphic to) isomorphisms in `AddCommGroupCat`. -/
 add_decl_doc addEquivIsoAddCommGroupIso
 
 namespace CategoryTheory.Aut
@@ -475,7 +475,7 @@ def isoPerm {α : Type u} : GroupCat.of (Aut α) ≅ GroupCat.of (Equiv.Perm α)
 set_option linter.uppercaseLean3 false in
 #align category_theory.Aut.iso_perm CategoryTheory.Aut.isoPerm
 
-/-- The (unbundled) group of automorphisms of a type is `mul_equiv` to the (unbundled) group
+/-- The (unbundled) group of automorphisms of a type is `MulEquiv` to the (unbundled) group
 of permutations. -/
 def mulEquivPerm {α : Type u} : Aut α ≃* Equiv.Perm α :=
   isoPerm.groupIsoToMulEquiv

Mathlib/Algebra/Category/GroupCat/Limits.lean

@@ -503,7 +503,7 @@ set_option linter.uppercaseLean3 false in
 -- Porting note: explicitly add what to be synthesized under `simps!`, because other lemmas
 -- automatically generated is not in normal form
 /-- The categorical kernel inclusion for `f : G ⟶ H`, as an object over `G`,
-agrees with the `subtype` map.
+agrees with the `AddSubgroup.subtype` map.
 -/
 @[simps! hom_left_apply_coe inv_left_apply]
 def kernelIsoKerOver {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -279,29 +279,29 @@ abbrev LinearEquiv.toModuleIso' {M N : ModuleCat.{v} R} (i : M ≃ₗ[R] N) : M
   i.toModuleIso
 #align linear_equiv.to_Module_iso' LinearEquiv.toModuleIso'
 
-/-- Build an isomorphism in the category `Module R` from a `linear_equiv` between `module`s. -/
+/-- Build an isomorphism in the category `ModuleCat R` from a `LinearEquiv` between `Module`s. -/
 abbrev LinearEquiv.toModuleIso'Left {X₁ : ModuleCat.{v} R} [AddCommGroup X₂] [Module R X₂]
     (e : X₁ ≃ₗ[R] X₂) : X₁ ≅ ModuleCat.of R X₂ :=
   e.toModuleIso
 #align linear_equiv.to_Module_iso'_left LinearEquiv.toModuleIso'Left
 
-/-- Build an isomorphism in the category `Module R` from a `linear_equiv` between `module`s. -/
+/-- Build an isomorphism in the category `ModuleCat R` from a `LinearEquiv` between `Module`s. -/
 abbrev LinearEquiv.toModuleIso'Right [AddCommGroup X₁] [Module R X₁] {X₂ : ModuleCat.{v} R}
     (e : X₁ ≃ₗ[R] X₂) : ModuleCat.of R X₁ ≅ X₂ :=
   e.toModuleIso
 #align linear_equiv.to_Module_iso'_right LinearEquiv.toModuleIso'Right
 
 namespace CategoryTheory.Iso
 
-/-- Build a `linear_equiv` from an isomorphism in the category `Module R`. -/
+/-- Build a `LinearEquiv` from an isomorphism in the category `ModuleCat R`. -/
 def toLinearEquiv {X Y : ModuleCat R} (i : X ≅ Y) : X ≃ₗ[R] Y :=
   LinearEquiv.ofLinear i.hom i.inv i.inv_hom_id i.hom_inv_id
 #align category_theory.iso.to_linear_equiv CategoryTheory.Iso.toLinearEquiv
 
 end CategoryTheory.Iso
 
-/-- linear equivalences between `module`s are the same as (isomorphic to) isomorphisms
-in `Module` -/
+/-- linear equivalences between `Module`s are the same as (isomorphic to) isomorphisms
+in `ModuleCat` -/
 @[simps]
 def linearEquivIsoModuleIso {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] [Module R X]
     [Module R Y] : (X ≃ₗ[R] Y) ≅ ModuleCat.of R X ≅ ModuleCat.of R Y where

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -240,7 +240,7 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddCommMon.of AddCommMonCat.of
 
-/-- Construct a bundled `AddCommMon` from the underlying type and typeclass. -/
+/-- Construct a bundled `AddCommMonCat` from the underlying type and typeclass. -/
 add_decl_doc AddCommMonCat.of
 
 @[to_additive]

Mathlib/Algebra/Category/MonCat/Colimits.lean

@@ -119,7 +119,7 @@ set_option linter.uppercaseLean3 false in
 
 attribute [instance] colimitSetoid
 
-/-- The underlying type of the colimit of a diagram in `Mon`.
+/-- The underlying type of the colimit of a diagram in `MonCat`.
 -/
 def ColimitType : Type v :=
   Quotient (colimitSetoid F)

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -324,7 +324,7 @@ def colimitDesc (t : Cocone F) : colimit.{v, u} F ⟶ t.pt where
 #align AddMon.filtered_colimits.colimit_desc AddMonCat.FilteredColimits.colimitDesc
 
 /-- The proposed colimit cocone is a colimit in `MonCat`. -/
-@[to_additive "The proposed colimit cocone is a colimit in `AddMon`."]
+@[to_additive "The proposed colimit cocone is a colimit in `AddMonCat`."]
 def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
   desc := colimitDesc.{v, u} F
   fac t j := MonoidHom.ext fun x => congr_fun ((Types.TypeMax.colimitCoconeIsColimit.{v, u}
@@ -401,7 +401,7 @@ noncomputable def colimitCocone : Cocone F where
 #align AddCommMon.filtered_colimits.colimit_cocone AddCommMonCat.FilteredColimits.colimitCocone
 
 /-- The proposed colimit cocone is a colimit in `CommMonCat`. -/
-@[to_additive "The proposed colimit cocone is a colimit in `AddCommMon`."]
+@[to_additive "The proposed colimit cocone is a colimit in `AddCommMonCat`."]
 def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
   desc t :=
     MonCat.FilteredColimits.colimitDesc.{v, u} (F ⋙ forget₂ CommMonCat MonCat.{max v u})

Mathlib/Algebra/Category/MonCat/Limits.lean

@@ -20,7 +20,7 @@ the underlying types are just the limits in the category of types.
 
 -/
 
-set_option linter.uppercaseLean3 false -- `Mon`
+set_option linter.uppercaseLean3 false
 
 noncomputable section
 

Mathlib/Algebra/Category/Ring/FilteredColimits.lean

@@ -14,11 +14,12 @@ import Mathlib.Algebra.Category.GroupCat.FilteredColimits
 Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend
 to preserve _filtered_ colimits.
 
-In this file, we start with a small filtered category `J` and a functor `F : J ⥤ SemiRing`.
-We show that the colimit of `F ⋙ forget₂ SemiRing Mon` (in `Mon`) carries the structure of a
-semiring, thereby showing that the forgetful functor `forget₂ SemiRing Mon` preserves filtered
-colimits. In particular, this implies that `forget SemiRing` preserves filtered colimits.
-Similarly for `CommSemiRing`, `Ring` and `CommRing`.
+In this file, we start with a small filtered category `J` and a functor `F : J ⥤ SemiRingCatMax`.
+We show that the colimit of `F ⋙ forget₂ SemiRingCatMax MonCat` (in `MonCat`)
+carries the structure of a semiring, thereby showing that the forgetful functor
+`forget₂ SemiRingCatMax MonCat` preserves filtered colimits.
+In particular, this implies that `forget SemiRingCatMax` preserves filtered colimits.
+Similarly for `CommSemiRingCat`, `RingCat` and `CommRingCat`.
 
 -/
 
@@ -47,7 +48,7 @@ section
 -- passing around `F` all the time.
 variable {J : Type v} [SmallCategory J] (F : J ⥤ SemiRingCatMax.{v, u})
 
--- This instance is needed below in `colimit_semiring`, during the verification of the
+-- This instance is needed below in `colimitSemiring`, during the verification of the
 -- semiring axioms.
 instance semiringObj (j : J) :
     Semiring (((F ⋙ forget₂ SemiRingCatMax.{v, u} MonCat) ⋙ forget MonCat).obj j) :=
@@ -57,7 +58,7 @@ set_option linter.uppercaseLean3 false in
 
 variable [IsFiltered J]
 
-/-- The colimit of `F ⋙ forget₂ SemiRing Mon` in the category `Mon`.
+/-- The colimit of `F ⋙ forget₂ SemiRingCat MonCat` in the category `MonCat`.
 In the following, we will show that this has the structure of a semiring.
 -/
 abbrev R : MonCatMax.{v, u} :=
@@ -134,7 +135,7 @@ def colimitCocone : Cocone F where
 set_option linter.uppercaseLean3 false in
 #align SemiRing.filtered_colimits.colimit_cocone SemiRingCat.FilteredColimits.colimitCocone
 
-/-- The proposed colimit cocone is a colimit in `SemiRing`. -/
+/-- The proposed colimit cocone is a colimit in `SemiRingCat`. -/
 def colimitCoconeIsColimit : IsColimit <| colimitCocone.{v, u} F where
   desc t :=
     { (MonCat.FilteredColimits.colimitCoconeIsColimit.{v, u}
@@ -181,7 +182,7 @@ section
 -- passing around `F` all the time.
 variable {J : Type v} [SmallCategory J] [IsFiltered J] (F : J ⥤ CommSemiRingCat.{max v u})
 
-/-- The colimit of `F ⋙ forget₂ CommSemiRing SemiRing` in the category `SemiRing`.
+/-- The colimit of `F ⋙ forget₂ CommSemiRingCat SemiRingCat` in the category `SemiRingCat`.
 In the following, we will show that this has the structure of a _commutative_ semiring.
 -/
 abbrev R : SemiRingCatMax.{v, u} :=
@@ -211,7 +212,7 @@ def colimitCocone : Cocone F where
 set_option linter.uppercaseLean3 false in
 #align CommSemiRing.filtered_colimits.colimit_cocone CommSemiRingCat.FilteredColimits.colimitCocone
 
-/-- The proposed colimit cocone is a colimit in `CommSemiRing`. -/
+/-- The proposed colimit cocone is a colimit in `CommSemiRingCat`. -/
 def colimitCoconeIsColimit : IsColimit <| colimitCocone.{v, u} F where
   desc t :=
     (SemiRingCat.FilteredColimits.colimitCoconeIsColimit.{v, u}
@@ -257,7 +258,7 @@ section
 -- passing around `F` all the time.
 variable {J : Type v} [SmallCategory J] [IsFiltered J] (F : J ⥤ RingCat.{max v u})
 
-/-- The colimit of `F ⋙ forget₂ Ring SemiRing` in the category `SemiRing`.
+/-- The colimit of `F ⋙ forget₂ RingCat SemiRingCat` in the category `SemiRingCat`.
 In the following, we will show that this has the structure of a ring.
 -/
 abbrev R : SemiRingCat.{max v u} :=
@@ -332,7 +333,7 @@ section
 -- passing around `F` all the time.
 variable {J : Type v} [SmallCategory J] [IsFiltered J] (F : J ⥤ CommRingCat.{max v u})
 
-/-- The colimit of `F ⋙ forget₂ CommRing Ring` in the category `Ring`.
+/-- The colimit of `F ⋙ forget₂ CommRingCat RingCat` in the category `RingCat`.
 In the following, we will show that this has the structure of a _commutative_ ring.
 -/
 abbrev R : RingCat.{max v u} :=
@@ -361,7 +362,7 @@ def colimitCocone : Cocone F where
 set_option linter.uppercaseLean3 false in
 #align CommRing.filtered_colimits.colimit_cocone CommRingCat.FilteredColimits.colimitCocone
 
-/-- The proposed colimit cocone is a colimit in `CommRing`. -/
+/-- The proposed colimit cocone is a colimit in `CommRingCat`. -/
 def colimitCoconeIsColimit : IsColimit <| colimitCocone.{v, u} F where
   desc t :=
     (RingCat.FilteredColimits.colimitCoconeIsColimit.{v, u}

Mathlib/Algebra/Category/SemigroupCat/Basic.lean

@@ -262,9 +262,9 @@ end
 
 namespace CategoryTheory.Iso
 
-/-- Build a `MulEquiv` from an isomorphism in the category `Magma`. -/
+/-- Build a `MulEquiv` from an isomorphism in the category `MagmaCat`. -/
 @[to_additive
-      "Build an `AddEquiv` from an isomorphism in the category `AddMagma`."]
+      "Build an `AddEquiv` from an isomorphism in the category `AddMagmaCat`."]
 def magmaCatIsoToMulEquiv {X Y : MagmaCat} (i : X ≅ Y) : X ≃* Y :=
   MulHom.toMulEquiv i.hom i.inv i.hom_inv_id i.inv_hom_id
 #align category_theory.iso.Magma_iso_to_mul_equiv CategoryTheory.Iso.magmaCatIsoToMulEquiv
@@ -281,10 +281,10 @@ def semigroupCatIsoToMulEquiv {X Y : SemigroupCat} (i : X ≅ Y) : X ≃* Y :=
 end CategoryTheory.Iso
 
 /-- multiplicative equivalences between `Mul`s are the same as (isomorphic to) isomorphisms
-in `Magma` -/
+in `MagmaCat` -/
 @[to_additive
     "additive equivalences between `Add`s are the same
-    as (isomorphic to) isomorphisms in `AddMagma`"]
+    as (isomorphic to) isomorphisms in `AddMagmaCat`"]
 def mulEquivIsoMagmaIso {X Y : Type u} [Mul X] [Mul Y] :
     X ≃* Y ≅ MagmaCat.of X ≅ MagmaCat.of Y where
   hom e := e.toMagmaCatIso

Mathlib/Algebra/Group/Prod.lean

@@ -747,9 +747,9 @@ section
 
 variable (M N M' N')
 
-/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
+/-- Four-way commutativity of `Prod`. The name matches `mul_mul_mul_comm`. -/
 @[to_additive (attr := simps apply) prodProdProdComm
-    "Four-way commutativity of `prod`.\nThe name matches `mul_mul_mul_comm`"]
+    "Four-way commutativity of `Prod`.\nThe name matches `mul_mul_mul_comm`"]
 def prodProdProdComm : (M × N) × M' × N' ≃* (M × M') × N × N' :=
   { Equiv.prodProdProdComm M N M' N' with
     toFun := fun mnmn => ((mnmn.1.1, mnmn.2.1), (mnmn.1.2, mnmn.2.2))

Mathlib/Algebra/Homology/ModuleCat.lean

@@ -96,7 +96,7 @@ set_option linter.uppercaseLean3 false in
 
 -- Porting note: `erw` had to be used instead of `simp`
 -- see https://github.com/leanprover-community/mathlib4/issues/5026
-/-- We give an alternative proof of `homology_map_eq_of_homotopy`,
+/-- We give an alternative proof of `homology'_map_eq_of_homotopy`,
 specialized to the setting of `V = Module R`,
 to demonstrate the use of extensionality lemmas for homology in `Module R`. -/
 example (f g : C ⟶ D) (h : Homotopy f g) (i : ι) :

Mathlib/Algebra/MvPolynomial/Monad.lean

@@ -42,7 +42,7 @@ whereas `MvPolynomial.map` is the "map" operation for the other pair.
 
 We add a `LawfulMonad` instance for the (`bind₁`, `join₁`) pair.
 The second pair cannot be instantiated as a `Monad`,
-since it is not a monad in `Type` but in `CommRing` (or rather `CommSemiRing`).
+since it is not a monad in `Type` but in `CommRingCat` (or rather `CommSemiRingCat`).
 
 -/
 

Mathlib/Algebra/Order/Monoid/WithZero.lean

@@ -298,7 +298,7 @@ instance instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual
   { Multiplicative.orderedCommMonoid, Multiplicative.linearOrder with
     zero := Multiplicative.ofAdd (⊤ : α)
     zero_mul := @top_add _ (_)
-    -- Porting note:  Here and elsewhere in the file, just `zero_mul` worked in Lean 3.  See
+    -- Porting note:  Here and elsewhere in the file, just `zero_mul` worked in Lean 3. See
     -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Type.20synonyms
     mul_zero := @add_top _ (_)
     zero_le_one := (le_top : (0 : α) ≤ ⊤) }

Mathlib/Algebra/Ring/Prod.lean

@@ -312,7 +312,7 @@ section
 
 variable (R R' S S')
 
-/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
+/-- Four-way commutativity of `Prod`. The name matches `mul_mul_mul_comm`. -/
 @[simps apply]
 def prodProdProdComm : (R × R') × S × S' ≃+* (R × S) × R' × S' :=
   { AddEquiv.prodProdProdComm R R' S S', MulEquiv.prodProdProdComm R R' S S' with

Mathlib/AlgebraicGeometry/Pullbacks.lean

@@ -669,7 +669,7 @@ def openCoverOfBase' (𝒰 : OpenCover Z) (f : X ⟶ Z) (g : Y ⟶ Z) : OpenCove
     -- Porting note: `simpa` failed, but this is indeed `rfl`
     rfl
   · simp only [Category.comp_id, Category.id_comp]
-  -- Porting note: this `IsIso` instance was `inferInstance`
+  -- Porting note: this `IsIso` instance was `infer_instance`
   · apply IsIso.comp_isIso
 #align algebraic_geometry.Scheme.pullback.open_cover_of_base' AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'