[Merged by Bors] - doc(CategoryTheory): fix typos

Mathlib/CategoryTheory/Abelian/Basic.lean

@@ -482,7 +482,7 @@ noncomputable def isLimitMapConeOfKernelForkOfι
   change 𝟙 _ ≫ F.map i ≫ 𝟙 _ = F.map i
   rw [Category.comp_id, Category.id_comp]
 
-/-- If `F : D ⥤ C` is a functor to an abelian category, `p : X ⟶ Y` is a morphisms
+/-- If `F : D ⥤ C` is a functor to an abelian category, `p : X ⟶ Y` is a morphism
 admitting a kernel such that `F` preserves this kernel and `F.map p` is an epi,
 then `F.map Y` identifies to the cokernel of `F.map (kernel.ι p)`. -/
 noncomputable def isColimitMapCoconeOfCokernelCoforkOfπ

Mathlib/CategoryTheory/Abelian/FreydMitchell.lean

@@ -44,7 +44,7 @@ To prove (2), there are multiple options.
 
 * Some sources (for example Freyd's "Abelian Categories") choose `D := LeftExactFunctor C Ab`. The
   main difficulty with this approach is that it is not obvious that `D` is abelian. This approach
-  has a very algebraic flavor and requires a relatively large armount of ad-hoc reasoning.
+  has a very algebraic flavor and requires a relatively large amount of ad-hoc reasoning.
 * In the Stacks project, it is suggested to choose `D := Sheaf J Ab` for a suitable Grothendieck
   topology on `Cᵒᵖ` and there are reasons to believe that this `D` is in fact equivalent to
   `LeftExactFunctor C Ab`. This approach translates many of the interesting properties along the

Mathlib/CategoryTheory/Action.lean

@@ -13,7 +13,7 @@ import Mathlib.GroupTheory.SemidirectProduct
 # Actions as functors and as categories
 
 From a multiplicative action M ↻ X, we can construct a functor from M to the category of
-types, mapping the single object of M to X and an element `m : M` to map `X → X` given by
+types, mapping the single object of M to X and an element `m : M` to the map `X → X` given by
 multiplication by `m`.
   This functor induces a category structure on X -- a special case of the category of elements.
 A morphism `x ⟶ y` in this category is simply a scalar `m : M` such that `m • x = y`. In the case

Mathlib/CategoryTheory/Adjunction/Basic.lean

@@ -482,15 +482,15 @@ def ofNatIsoRight {F : C ⥤ D} {G H : D ⥤ C} (adj : F ⊣ G) (iso : G ≅ H)
   Adjunction.mkOfHomEquiv
     { homEquiv := fun X Y => (adj.homEquiv X Y).trans (equivHomsetRightOfNatIso iso) }
 
-/-- The isomorpism which an adjunction `F ⊣ G` induces on `G ⋙ yoneda`. This states that
+/-- The isomorphism which an adjunction `F ⊣ G` induces on `G ⋙ yoneda`. This states that
 `Adjunction.homEquiv` is natural in both arguments. -/
 @[simps!]
 def compYonedaIso {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₁} D]
     {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
     G ⋙ yoneda ≅ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op :=
   NatIso.ofComponents fun X => NatIso.ofComponents fun Y => (adj.homEquiv Y.unop X).toIso.symm
 
-/-- The isomorpism which an adjunction `F ⊣ G` induces on `F.op ⋙ coyoneda`. This states that
+/-- The isomorphism which an adjunction `F ⊣ G` induces on `F.op ⋙ coyoneda`. This states that
 `Adjunction.homEquiv` is natural in both arguments. -/
 @[simps!]
 def compCoyonedaIso {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₁} D]

Mathlib/CategoryTheory/Bicategory/EqToHom.lean

@@ -14,7 +14,7 @@ This file records some of the behavior of `eqToHom` 1-morphisms and
 
 Given an equality of objects `h : x = y` in a bicategory, there is a 1-morphism
 `eqToHom h : x ⟶ y` just like in an ordinary category. The definitional property
-of this morhism is that if `h : x = x`, `eqToHom h = 𝟙 x`. This is
+of this morphism is that if `h : x = x`, `eqToHom h = 𝟙 x`. This is
 implemented as the `eqToHom` morphism in the `CategoryStruct` underlying the
 bicategory.
 

Mathlib/CategoryTheory/Bicategory/Functor/StrictlyUnitary.lean

@@ -62,7 +62,7 @@ field `mapId`. -/
 structure StrictlyUnitaryLaxFunctorCore where
   /-- action on objects -/
   obj : B → C
-  /-- action on 1-morhisms -/
+  /-- action on 1-morphisms -/
   map : ∀ {X Y : B}, (X ⟶ Y) → (obj X ⟶ obj Y)
   map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
   /-- action on 2-morphisms -/

Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean

@@ -39,7 +39,7 @@ section LeftExtension
 
 open LeftExtension
 
-/-- For an adjuntion `f ⊣ u`, `u` is an absolute left Kan extension of the identity along `f`.
+/-- For an adjunction `f ⊣ u`, `u` is an absolute left Kan extension of the identity along `f`.
 The unit of this Kan extension is given by the unit of the adjunction. -/
 def Adjunction.isAbsoluteLeftKan {f : a ⟶ b} {u : b ⟶ a} (adj : f ⊣ u) :
     IsAbsKan (.mk u adj.unit) := fun {x} h ↦
@@ -94,7 +94,7 @@ def LeftExtension.IsKan.adjunction {f : a ⟶ b} {t : LeftExtension f (𝟙 a)}
         _ = _ := by
           rw [← leftZigzag, Hε]; bicategory }
 
-/-- For an adjuntion `f ⊣ u`, `u` is a left Kan extension of the identity along `f`.
+/-- For an adjunction `f ⊣ u`, `u` is a left Kan extension of the identity along `f`.
 The unit of this Kan extension is given by the unit of the adjunction. -/
 def LeftExtension.IsAbsKan.adjunction {f : a ⟶ b} (t : LeftExtension f (𝟙 a)) (H : IsAbsKan t) :
     f ⊣ t.extension :=
@@ -119,7 +119,7 @@ section LeftLift
 
 open LeftLift
 
-/-- For an adjuntion `f ⊣ u`, `f` is an absolute left Kan lift of the identity along `u`.
+/-- For an adjunction `f ⊣ u`, `f` is an absolute left Kan lift of the identity along `u`.
 The unit of this Kan lift is given by the unit of the adjunction. -/
 def Adjunction.isAbsoluteLeftKanLift {f : a ⟶ b} {u : b ⟶ a} (adj : f ⊣ u) :
     IsAbsKan (.mk f adj.unit) := fun {x} h ↦
@@ -173,7 +173,7 @@ def LeftLift.IsKan.adjunction {u : b ⟶ a} {t : LeftLift u (𝟙 a)}
           rw [← rightZigzag, Hε]; bicategory
     right_triangle := Hε }
 
-/-- For an adjuntion `f ⊣ u`, `f` is a left Kan lift of the identity along `u`.
+/-- For an adjunction `f ⊣ u`, `f` is a left Kan lift of the identity along `u`.
 The unit of this Kan lift is given by the unit of the adjunction. -/
 def LeftLift.IsAbsKan.adjunction {u : b ⟶ a} (t : LeftLift u (𝟙 a)) (H : IsAbsKan t) :
     t.lift ⊣ u :=

Mathlib/CategoryTheory/CodiscreteCategory.lean

@@ -20,7 +20,7 @@ whose Hom type are Unit types.
 `f : C ⥤ Codiscrete A`.
 
 Similarly, `Codiscrete.natTrans` and `Codiscrete.natIso` promote `I`-indexed families of morphisms,
-or `I`-indexed families of isomorphisms to natural transformations or natural isomorphism.
+or `I`-indexed families of isomorphisms to natural transformations or natural isomorphisms.
 
 We define `functorToCat : Type u ⥤ Cat.{0,u}` which sends a type to the codiscrete category and show
 it is right adjoint to `Cat.objects.`
@@ -33,12 +33,12 @@ universe u v w
 -- to enforce using `CodiscreteEquiv` (or `Codiscrete.mk` and `Codiscrete.as`) to move between
 -- `Codiscrete α` and `α`. Otherwise there is too much API leakage.
 /-- A wrapper for promoting any type to a category,
-with a unique morphisms between any two objects of the category.
+with a unique morphism between any two objects of the category.
 -/
 @[ext, aesop safe cases (rule_sets := [CategoryTheory])]
 structure Codiscrete (α : Type u) where
   /-- A wrapper for promoting any type to a category,
-  with a unique morphisms between any two objects of the category. -/
+  with a unique morphism between any two objects of the category. -/
   as : α
 
 @[simp]
@@ -77,7 +77,7 @@ def invFunctor (F : C ⥤ Codiscrete A) : C → A := Codiscrete.as ∘ F.obj
 def natTrans {F G : C ⥤ Codiscrete A} : F ⟶ G where
   app _ := ⟨⟩
 
-/-- Given two functors into a codiscrete category, the trivial natural transformation is an
+/-- Given two functors into a codiscrete category, the trivial natural transformation is a
 natural isomorphism. -/
 def natIso {F G : C ⥤ Codiscrete A} : F ≅ G where
   hom := natTrans

Mathlib/CategoryTheory/CofilteredSystem.lean

@@ -14,7 +14,7 @@ This file deals with properties of cofiltered (and inverse) systems.
 
 Given a functor `F : J ⥤ Type v`:
 
-* For `j : J`, `F.eventualRange j` is the intersections of all ranges of morphisms `F.map f`
+* For `j : J`, `F.eventualRange j` is the intersection of all ranges of morphisms `F.map f`
   where `f` has codomain `j`.
 * `F.IsMittagLeffler` states that the functor `F` satisfies the Mittag-Leffler
   condition: the ranges of morphisms `F.map f` (with `f` having codomain `j`) stabilize.

Mathlib/CategoryTheory/CommSq.lean

@@ -8,7 +8,7 @@ import Mathlib.CategoryTheory.Comma.Arrow
 /-!
 # Commutative squares
 
-This file provide an API for commutative squares in categories.
+This file provides an API for commutative squares in categories.
 If `top`, `left`, `right` and `bottom` are four morphisms which are the edges
 of a square, `CommSq top left right bottom` is the predicate that this
 square is commutative.

Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean

@@ -136,7 +136,7 @@ def isPointwiseLeftKanExtensionAtOfIsoOfIsLocalization
     simp only [← this, map_id, comp_id, Iso.inv_hom_id_app_assoc]
 
 /-- If `L` is a localization functor for `W` and `e : F ≅ L ⋙ G` is an isomorphism,
-then `e.hom` makes `G` a poinwise left Kan extension of `F` along `L`. -/
+then `e.hom` makes `G` a pointwise left Kan extension of `F` along `L`. -/
 noncomputable def isPointwiseLeftKanExtensionOfIsoOfIsLocalization
     {G : D ⥤ H} (e : F ≅ L ⋙ G) [L.IsLocalization W] :
     (LeftExtension.mk _ e.hom).IsPointwiseLeftKanExtension := fun Y ↦

Mathlib/CategoryTheory/Join/Basic.lean

@@ -11,16 +11,16 @@ import Mathlib.CategoryTheory.Products.Basic
 
 Given categories `C, D`, this file constructs a category `C ⋆ D`. Its objects are either
 objects of `C` or objects of `D`, morphisms between objects of `C` are morphisms in `C`,
-morphisms between object of `D` are morphisms in `D`, and finally, given `c : C` and `d : D`,
+morphisms between objects of `D` are morphisms in `D`, and finally, given `c : C` and `d : D`,
 there is a unique morphism `c ⟶ d` in `C ⋆ D`.
 
 ## Main constructions
 
 * `Join.edge c d`: the unique map from `c` to `d`.
-* `Join.inclLeft : C ⥤ C ⋆ D`, the left inclusion. Its action on morphism is the main entry point
+* `Join.inclLeft : C ⥤ C ⋆ D`, the left inclusion. Its action on morphisms is the main entry point
   to construct maps in `C ⋆ D` between objects coming from `C`.
-* `Join.inclRight : D ⥤ C ⋆ D`, the left inclusion. Its action on morphism is the main entry point
-  to construct maps in `C ⋆ D` between object coming from `D`.
+* `Join.inclRight : D ⥤ C ⋆ D`, the right inclusion. Its action on morphisms is the main entry point
+  to construct maps in `C ⋆ D` between objects coming from `D`.
 * `Join.mkFunctor`, A constructor for functors out of a join of categories.
 * `Join.mkNatTrans`, A constructor for natural transformations between functors out of a join
   of categories.
@@ -58,7 +58,7 @@ section CategoryStructure
 
 variable {C D}
 
-/-- Morphisms in `C ⋆ D` are those of `C` and `D`, plus an unique
+/-- Morphisms in `C ⋆ D` are those of `C` and `D`, plus a unique
 morphism `(left c ⟶ right d)` for every `c : C` and `d : D`. -/
 def Hom : C ⋆ D → C ⋆ D → Type (max v₁ v₂)
   | .left x, .left y => ULift (x ⟶ y)
@@ -107,7 +107,7 @@ end CategoryStructure
 section Inclusions
 
 /-- The canonical inclusion from C to `C ⋆ D`.
-Terms of the form `(inclLeft C D).map f`should be treated as primitive when working with joins
+Terms of the form `(inclLeft C D).map f` should be treated as primitive when working with joins
 and one should avoid trying to reduce them. For this reason, there is no `inclLeft_map` simp
 lemma. -/
 @[simps! obj]
@@ -116,7 +116,7 @@ def inclLeft : C ⥤ C ⋆ D where
   map := ULift.up
 
 /-- The canonical inclusion from D to `C ⋆ D`.
-Terms of the form `(inclRight C D).map f`should be treated as primitive when working with joins
+Terms of the form `(inclRight C D).map f` should be treated as primitive when working with joins
 and one should avoid trying to reduce them. For this reason, there is no `inclRight_map` simp
 lemma. -/
 @[simps! obj]
@@ -205,7 +205,7 @@ section Functoriality
 
 variable {C D} {E : Type u₃} [Category.{v₃} E] {E' : Type u₄} [Category.{v₄} E']
 
-/-- A pair of functor `F : C ⥤ E, G : D ⥤ E` as well as a natural transformation
+/-- A pair of functors `F : C ⥤ E, G : D ⥤ E` as well as a natural transformation
 `α : (Prod.fst C D) ⋙ F ⟶ (Prod.snd C D) ⋙ G`. defines a functor out of `C ⋆ D`.
 This is the main entry point to define functors out of a join of categories. -/
 def mkFunctor (F : C ⥤ E) (G : D ⥤ E) (α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G) :

Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean

@@ -23,7 +23,7 @@ namespace CategoryTheory.Types
 
 open Limits
 
-/-! The forgetful fuctor on `Type u` is the identity; copy the instances on `𝟭 (Type u)`
+/-! The forgetful functor on `Type u` is the identity; copy the instances on `𝟭 (Type u)`
 over to `forget (Type u)`.
 
 We currently have two instances for `HasForget (Type u)`:

Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

@@ -184,7 +184,7 @@ lemma isPullback_of_binaryFan_isLimit (c : BinaryFan Y Z) (hc : IsLimit c) :
 
 variable (Y Z) [HasPullback Y.hom Z.hom] [HasBinaryProduct Y Z]
 
-/-- The product of `Y` and `Z` in `Over X` is isomorpic to `Y ×ₓ Z`. -/
+/-- The product of `Y` and `Z` in `Over X` is isomorphic to `Y ×ₓ Z`. -/
 noncomputable
 def prodLeftIsoPullback :
     (Y ⨯ Z).left ≅ pullback Y.hom Z.hom :=

Mathlib/CategoryTheory/Limits/Final.lean

@@ -354,7 +354,7 @@ theorem ι_colimitIso_inv [HasColimit G] (X : C) :
   simp [colimitIso]
 
 /-- A pointfree version of `colimitIso`, stating that whiskering by `F` followed by taking the
-colimit is isomorpic to taking the colimit on the codomain of `F`. -/
+colimit is isomorphic to taking the colimit on the codomain of `F`. -/
 def colimIso [HasColimitsOfShape D E] [HasColimitsOfShape C E] :
     (whiskeringLeft _ _ _).obj F ⋙ colim ≅ colim (J := D) (C := E) :=
   NatIso.ofComponents (fun G => colimitIso F G) fun f => by
@@ -691,7 +691,7 @@ def limitIso [HasLimit G] : limit (F ⋙ G) ≅ limit G :=
   (asIso (limit.pre G F)).symm
 
 /-- A pointfree version of `limitIso`, stating that whiskering by `F` followed by taking the
-limit is isomorpic to taking the limit on the codomain of `F`. -/
+limit is isomorphic to taking the limit on the codomain of `F`. -/
 def limIso [HasLimitsOfShape D E] [HasLimitsOfShape C E] :
     (whiskeringLeft _ _ _).obj F ⋙ lim ≅ lim (J := D) (C := E) :=
   Iso.symm <| NatIso.ofComponents (fun G => (limitIso F G).symm) fun f => by

Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

@@ -92,7 +92,7 @@ inductive WalkingMulticospan (J : MulticospanShape.{w, w'}) : Type max w w'
   | left : J.L → WalkingMulticospan J
   | right : J.R → WalkingMulticospan J
 
-/-- The type underlying the multiecoqualizer diagram. -/
+/-- The type underlying the multicoequalizer diagram. -/
 inductive WalkingMultispan (J : MultispanShape.{w, w'}) : Type max w w'
   | left : J.L → WalkingMultispan J
   | right : J.R → WalkingMultispan J
@@ -754,7 +754,7 @@ abbrev multiequalizer {J : MulticospanShape.{w, w'}} (I : MulticospanIndex J C)
 abbrev HasMulticoequalizer {J : MultispanShape.{w, w'}} (I : MultispanIndex J C) :=
   HasColimit I.multispan
 
-/-- The multiecoqualizer of `I : MultispanIndex J C`. -/
+/-- The multicoequalizer of `I : MultispanIndex J C`. -/
 abbrev multicoequalizer {J : MultispanShape.{w, w'}} (I : MultispanIndex J C)
     [HasMulticoequalizer I] : C :=
   colimit I.multispan

Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean

@@ -8,7 +8,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
 /-!
 # HasPullback
 `HasPullback f g` and `pullback f g` provides API for `HasLimit` and `limit` in the case of
-pullacks.
+pullbacks.
 
 # Main definitions
 

Mathlib/CategoryTheory/Limits/Sifted.lean

@@ -23,7 +23,7 @@ preserves finite products. We achieve this characterization in this file.
 - `IsSifted.colimPreservesFiniteProductsOfIsSifted`: The `Type`-valued colimit functor for sifted
   diagrams preserves finite products.
 - `IsSifted.of_colimit_preservesFiniteProducts`: The converse: if the `Type`-valued colimit functor
-  preserves finite producs, the category is sifted.
+  preserves finite products, the category is sifted.
 - `IsSifted.of_final_functor_from_sifted`: A category admitting a final functor from a sifted
   category is itself sifted.
 

Mathlib/CategoryTheory/Localization/Resolution.lean

@@ -93,7 +93,7 @@ structure Hom (R R' : Φ.RightResolution X₂) where
 
 attribute [reassoc (attr := simp)] Hom.comm
 
-/-- The identity of a object in `Φ.RightResolution X₂`. -/
+/-- The identity of an object in `Φ.RightResolution X₂`. -/
 @[simps]
 def Hom.id (R : Φ.RightResolution X₂) : Hom R R where
   f := 𝟙 _
@@ -137,7 +137,7 @@ structure Hom (L L' : Φ.LeftResolution X₂) where
 
 attribute [reassoc (attr := simp)] Hom.comm
 
-/-- The identity of a object in `Φ.LeftResolution X₂`. -/
+/-- The identity of an object in `Φ.LeftResolution X₂`. -/
 @[simps]
 def Hom.id (L : Φ.LeftResolution X₂) : Hom L L where
   f := 𝟙 _

Mathlib/CategoryTheory/Monoidal/Bimon_.lean

@@ -34,7 +34,7 @@ variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] [Braide
 open scoped MonObj ComonObj
 
 /--
-A bimonoid object in a braided category `C` is a object that is simultaneously monoid and comonoid
+A bimonoid object in a braided category `C` is an object that is simultaneously monoid and comonoid
 objects, and structure morphisms of them satisfy appropriate consistency conditions.
 -/
 class BimonObj (M : C) extends MonObj M, ComonObj M where

Mathlib/CategoryTheory/Monoidal/Braided/Multifunctor.lean

@@ -101,11 +101,11 @@ we phrase the forward hexagon identity as an equality of natural transformations
 same on the object level on three objects `X₁ X₂ X₃`).
 
 ```
-            funtor₁₂₃                         (X₁ ⊗ X₂) ⊗ X₃
-associtator/          \ secondMap₁             /           \
+            functor₁₂₃                        (X₁ ⊗ X₂) ⊗ X₃
+associator /          \ secondMap₁             /           \
           v            v                      v             v
      functor₁₂₃'    functor₂₁₃          X₁ ⊗ (X₂ ⊗ X₃)    (X₂ ⊗ X₁) ⊗ X₃
- firsMap₂ |            |secondMap₂            |             |
+firstMap₂ |            |secondMap₂            |             |
           v            v                      v             v
      functor₂₃₁     functor₂₁₃'         (X₂ ⊗ X₃) ⊗ X₁    X₂ ⊗ (X₁ ⊗ X₃)
   firstMap₃\           / secondMap₃            \            /
@@ -157,11 +157,11 @@ we phrase the reverse hexagon identity as an equality of natural transformations
 same on the object level on three objects `X₁ X₂ X₃`).
 
 ```
-            funtor₁₂₃'                        X₁ ⊗ (X₂ ⊗ X₃)
-associtator/          \ secondMap₁             /           \
+            functor₁₂₃'                       X₁ ⊗ (X₂ ⊗ X₃)
+associator /          \ secondMap₁             /           \
           v            v                      v             v
      functor₁₂₃    functor₁₃₂'          (X₁ ⊗ X₂) ⊗ X₃    X₁ ⊗ (X₃ ⊗ X₂)
- firsMap₂ |            |secondMap₂            |             |
+firstMap₂ |            |secondMap₂            |             |
           v            v                      v             v
      functor₃₁₂'    functor₁₃₂          X₃ ⊗ (X₁ ⊗ X₂)    (X₁ ⊗ X₃) ⊗ X₂
   firstMap₃\           / secondMap₃            \            /

Mathlib/CategoryTheory/Monoidal/Category.lean

@@ -51,11 +51,11 @@ performed by the `coherence` tactic.
 The simp-normal form of morphisms is defined to be an expression that has the minimal number of
 parentheses. More precisely,
 1. it is a composition of morphisms like `f₁ ≫ f₂ ≫ f₃ ≫ f₄ ≫ f₅` such that each `fᵢ` is
-  either a structural morphisms (morphisms made up only of identities, associators, unitors)
-  or non-structural morphisms, and
+  either a structural morphism (morphisms made up only of identities, associators, unitors)
+  or a non-structural morphism, and
 2. each non-structural morphism in the composition is of the form `X₁ ◁ X₂ ◁ X₃ ◁ f ▷ X₄ ▷ X₅`,
-  where each `Xᵢ` is a object that is not the identity or a tensor and `f` is a non-structural
-  morphisms that is not the identity or a composite.
+  where each `Xᵢ` is an object that is not the identity or a tensor and `f` is a non-structural
+  morphism that is not the identity or a composite.
 
 Note that `X₁ ◁ X₂ ◁ X₃ ◁ f ▷ X₄ ▷ X₅` is actually `X₁ ◁ (X₂ ◁ (X₃ ◁ ((f ▷ X₄) ▷ X₅)))`.