Merge pull request #2249 from patrick-nicodemus/aspell

Spelling and style changes

Author: Alizter

theories/Algebra/AbGroups/AbPullback.v

@@ -25,6 +25,6 @@ Section AbPullback.
 
   Definition ab_pullback : AbGroup := Build_AbGroup (grp_pullback f g) _.
 
-  (** The corecursion principle is inherited from Groups; use grp_pullback_corec and friends from Groups/GrpPullback.v. *)
+  (** The corecursion principle is inherited from [Group]; use [grp_pullback_corec] and friends from Groups/GrpPullback.v. *)
 
 End AbPullback.

theories/Algebra/AbGroups/AbelianGroup.v

@@ -154,7 +154,7 @@ Instance is0gpd_grouphomomorphism {A B : AbGroup} : Is0Gpd (A $-> B)
 Instance is2graph_abgroup : Is2Graph AbGroup
   := is2graph_induced abgroup_group.
 
-(** AbGroup forms a 1Cat *)
+(** [AbGroup] forms a 1Cat *)
 Instance is1cat_abgroup : Is1Cat AbGroup
   := is1cat_induced _.
 
@@ -164,15 +164,15 @@ Instance hasmorext_abgroup `{Funext} : HasMorExt AbGroup
 Instance hasequivs_abgroup : HasEquivs AbGroup
   := hasequivs_induced _.
 
-(** Zero object of AbGroup *)
+(** Zero object of [AbGroup] *)
 
 Definition abgroup_trivial : AbGroup.
 Proof.
   rapply (Build_AbGroup grp_trivial).
   by intros [].
 Defined.
 
-(** AbGroup is a pointed category *)
+(** [AbGroup] is a pointed category *)
 Instance ispointedcat_abgroup : IsPointedCat AbGroup.
 Proof.
   apply Build_IsPointedCat with abgroup_trivial.

theories/Algebra/AbGroups/Abelianization.v

@@ -123,7 +123,7 @@ Section Abel.
     rapply Coeq_ind_beta_cglue.
   Defined.
 
-  (** We also have a recursion princple. *)
+  (** We also have a recursion principle. *)
   Definition Abel_rec (P : Type) `{IsHSet P} (a : G -> P)
     (c : forall x y z, a (x * (y * z)) = a (x * (z * y)))
     : Abel -> P.

theories/Algebra/AbGroups/Centralizer.v

@@ -65,22 +65,22 @@ Proof.
   destruct h as [h H]; cbn in H.
   destruct k as [k K]; cbn in K.
   strip_truncations.
-  (* It's enough to check equality after including into G: *)
+  (* It's enough to check equality after including into [G]: *)
   apply (equiv_ap_isembedding (subgroup_incl _) _ _)^-1.  cbn.
   induction H as [h [[] p]| |h1 h2 H1 H2 IHH1 IHH2].
-  - (* The case when h = g: *)
+  - (* The case when [h = g]: *)
     induction p.
     induction K as [k [[] q]| |k1 k2 K1 K2 IHK1 IHK2].
     + (* The case when k = g: *)
       induction q.
       reflexivity.
-    + (* The case when k = mon_unit: *)
+    + (* The case when [k = mon_unit]: *)
       apply centralizer_unit.
-    + (* The case when k = k1 (-k2): *)
+    + (* The case when [k = k1 (-k2)]: *)
       srapply (issubgroup_in_op_inv (H:=centralizer (gen tt))); assumption.
-  - (* The case when h = mon_unit: *)
+  - (* The case when [h = mon_unit]: *)
     symmetry; apply centralizer_unit.
-  - (* The case when h = h1 (-h2): *)
+  - (* The case when [h = h1 (-h2)]: *)
     symmetry.
     srapply (issubgroup_in_op_inv (H:=centralizer k)); unfold centralizer; symmetry; assumption.
 Defined.

theories/Algebra/AbGroups/TensorProduct.v

@@ -222,7 +222,7 @@ Proof.
       apply Hin.
 Defined.
 
-(** As a commonly occuring special case of the above induction principle, we have the case when the predicate in question is showing that two group homomorphisms out of the tensor product are homotopic. In order to do this, it suffices to show it only for simple tensors. The homotopy is closed under addition, so we don't need to hypothesise anything else. *)
+(** As a commonly occurring special case of the above induction principle, we have the case when the predicate in question is showing that two group homomorphisms out of the tensor product are homotopic. In order to do this, it suffices to show it only for simple tensors. The homotopy is closed under addition, so we don't need to hypothesise anything else. *)
 Definition ab_tensor_prod_ind_homotopy {A B G : AbGroup}
   {f f' : ab_tensor_prod A B $-> G}
   (H : forall a b, f (tensor a b) = f' (tensor a b))
@@ -361,7 +361,7 @@ Proof.
     napply grp_homo_op.
 Defined.
 
-(** The universal property of the tensor product is that biadditive maps between abelian groups are in one-to-one corresondance with maps out of the tensor product. In this sense, the tensor product is the most perfect object describing biadditive maps between two abelian groups. *)
+(** The universal property of the tensor product is that biadditive maps between abelian groups are in one-to-one correspondence with maps out of the tensor product. In this sense, the tensor product is the most perfect object describing biadditive maps between two abelian groups. *)
 Definition equiv_ab_tensor_prod_rec `{Funext} (A B C : AbGroup)
   : Biadditive A B C <~> (ab_tensor_prod A B $-> C).
 Proof.
@@ -451,7 +451,7 @@ Defined.
 
 (** ** Symmetry of the Tensor Product *)
 
-(** The tensor product is symmetric in that the order in which we take the tensor shouldn't matter upto isomorphism. *)
+(** The tensor product is symmetric in that the order in which we take the tensor shouldn't matter up to isomorphism. *)
 
 (** We can define a swap map which swaps the order of simple tensors. *)
 Definition ab_tensor_swap {A B} : ab_tensor_prod A B $-> ab_tensor_prod B A.
@@ -649,7 +649,7 @@ Proof.
   exact (tensor_ab_mul z a b).
 Defined.
 
-(** The hexagon identity is also straighforward to prove. We simply have to reduce all the involved functions on the simple tensors using our custom triple tensor induction principle. *)
+(** The hexagon identity is also straightforward to prove. We simply have to reduce all the involved functions on the simple tensors using our custom triple tensor induction principle. *)
 Instance hexagon_ab_tensor_prod : HexagonIdentity ab_tensor_prod.
 Proof.
   snapply hexagon_twist.

theories/Algebra/AbSES/Ext.v

@@ -166,7 +166,7 @@ Proof.
   symmetry; by apply abext_trivial_projective.
 Defined.
 
-(* Converely, if all extensions ending in [P] are trivial, then [P] is projective. *)
+(* Conversely, if all extensions ending in [P] are trivial, then [P] is projective. *)
 Proposition abext_projective_trivial `{Univalence} (P : AbGroup)
   (ext_triv : forall A, forall E : AbSES P A, tr E = point (Ext P A))
   : IsAbProjective P.

theories/Algebra/AbSES/Pullback.v

@@ -221,7 +221,7 @@ Definition abses_pullback_pmap `{Univalence} {A B B' : AbGroup} (f : B' $-> B)
 
 (** ** Functoriality of [abses_pullback] *)
 
-(** [abses_pullback] is psuedo-functorial, and we can state this in terms of actual homotopies or "path data homotopies." We decorate the latter with the suffix ('). *)
+(** [abses_pullback] is pseudo-functorial, and we can state this in terms of actual homotopies or "path data homotopies." We decorate the latter with the suffix ('). *)
 
 (** For every [E : AbSES B A], the pullback of [E] along [id_B] is [E]. *)
 Definition abses_pullback_id `{Univalence} {A B : AbGroup}

theories/Algebra/AbSES/Pushout.v

@@ -143,7 +143,7 @@ Definition abses_directsum_distributive_pushouts `{Univalence}
     = abses_direct_sum (abses_pushout f E) (abses_pushout g F)
   := abses_pushout_component3_id (abses_directsum_pushout_morphism f g) (fun _ => idpath).
 
-(** Given an AbSESMorphism whose third component is the identity, we know that it induces a path from the pushout of the domain along the first map to the codomain. Conversely, given a path from a pushout, we can deduce that the following square commutes: *)
+(** Given an [AbSESMorphism] whose third component is the identity, we know that it induces a path from the pushout of the domain along the first map to the codomain. Conversely, given a path from a pushout, we can deduce that the following square commutes: *)
 Definition abses_path_pushout_inclusion_commsq `{Univalence} {A A' B : AbGroup}
   (alpha : A $-> A') (E : AbSES B A) (F : AbSES B A')
   (p : abses_pushout alpha E = F)

theories/Algebra/Categorical/MonoidObject.v

@@ -20,7 +20,7 @@ Section MonoidObject.
   Class IsMonoidObject (x : A) := {
     (** A multiplication map from the tensor product of [x] with itself to [x]. *)
     mo_mult : tensor x x $-> x;
-    (** A unit of the multplication. *)
+    (** A unit of the multiplication. *)
     mo_unit : unit $-> x;
     (** The multiplication map is associative. *)
     mo_assoc : mo_mult $o fmap10 tensor mo_mult x $o associator x x x
@@ -57,7 +57,7 @@ Section ComonoidObject.
 
   (** We can build comonoid objects from the following data: *)
   Definition Build_IsComonoidObject (x : A)
-    (** A comultplication map. *)
+    (** A comultiplication map. *)
     (co_comult : x $-> tensor x x)
     (** A counit. *)
     (co_counit : x $-> unit)
@@ -184,7 +184,7 @@ Proof.
     exact (co_right_counit (A:=A^op) tensor unit (x:=x)).
 Defined.
 
-(** A cocommutative cocomonoid object in [A^op] is a commutative monoid object in [A]. *)
+(** A cocommutative comonoid object in [A^op] is a commutative monoid object in [A]. *)
 Definition cmo_coco_op {A : Type} {tensor : A -> A -> A} {unit : A}
   `{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor}
   `{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit,

theories/Algebra/Groups/FreeGroup.v

@@ -371,7 +371,7 @@ Section Reduction.
       exact (ap _ p).
   Defined.
 
-  (** Now we need to prove that the free group satisifes the unviersal property of the free group. *)
+  (** Now we need to prove that the free group satisfies the universal property of the free group. *)
   (** TODO: remove funext from here and universal property of free group *)
   #[export] Instance isfreegroupon_freegroup `{Funext}
     : IsFreeGroupOn A FreeGroup freegroup_in.

theories/Algebra/Groups/FreeProduct.v

@@ -27,9 +27,9 @@ Local Open Scope mc_mult_scope.
    | omega_K : forall (x y : list (H + K)),
       amal_eta (x ++ [inr mon_unit] ++ y) = amal_eta (x ++ y).
 
-  We will build this HIT up sucessively out of coequalizers. *)
+  We will build this HIT up successively out of coequalizers. *)
 
-(** We will call M [amal_type] and prefix all the constructors with [amal_] (for amalgmated free product). *)
+(** We will call M [amal_type] and prefix all the constructors with [amal_] (for amalgamated free product). *)
 
 Section FreeProduct.
 
@@ -756,7 +756,7 @@ Proof.
   exact (grp_homo_unit _ @ (grp_homo_unit _)^).
 Defined.
 
-(** The freeproduct is the coproduct in the category of groups. *)
+(** The free product is the coproduct in the category of groups. *)
 Instance hasbinarycoproducts : HasBinaryCoproducts Group.
 Proof.
   intros G H.

theories/Algebra/Groups/Group.v

@@ -79,7 +79,7 @@ Defined.
 (** We create a database of hints for the group theory library *)
 Create HintDb group_db.
 
-(** Our group laws can be proven easily with tactics such as [rapply associativity]. However this requires a typeclass search on more general algebraic structures. Therefore we explicitly list many groups laws here so that coq can use them. We also create hints for each law in our groups database. *)
+(** Our group laws can be proven easily with tactics such as [rapply associativity]. However this requires a typeclass search on more general algebraic structures. Therefore we explicitly list many groups laws here so that Coq can use them. We also create hints for each law in our groups database. *)
 Section GroupLaws.
   Context {G : Group} (x y z : G).
 
@@ -306,7 +306,7 @@ Defined.
 
 (** ** Group Isomorphisms *)
 
-(** Group isomorphsims are group homomorphisms whose underlying map happens to be an equivalence. They allow us to consider two groups to be the "same". They can be inverted and composed just like equivalences. *)
+(** Group isomorphisms are group homomorphisms whose underlying map happens to be an equivalence. They allow us to consider two groups to be the "same". They can be inverted and composed just like equivalences. *)
 
 (** An isomorphism of groups is defined as group homomorphism that is an equivalence. *)
 Record GroupIsomorphism (G H : Group) := Build_GroupIsomorphism {
@@ -508,7 +508,7 @@ Section GroupEquations.
 
 End GroupEquations.
 
-(** ** Cancelation lemmas *)
+(** ** Cancellation lemmas *)
 
 (** Group elements can be cancelled both on the left and the right. *)
 Definition grp_cancelL {G : Group} {x y : G} z : x = y <~> z * x = z * y

theories/Algebra/Groups/GrpPullback.v

@@ -2,7 +2,7 @@ Require Import Basics Types Limits.Pullback Cubical.PathSquare.
 Require Import Algebra.Groups.Group.
 Require Import WildCat.Core.
 
-(** Pullbacks of groups are formalized by equipping the set-pullback with the desired group structure. The universal property in the category of groups is proved by saying that the corecursion principle (grp_pullback_corec) is an equivalence. *) 
+(** Pullbacks of groups are formalized by equipping the set-pullback with the desired group structure. The universal property in the category of groups is proved by saying that the corecursion principle [grp_pullback_corec] is an equivalence. *) 
 
 Local Open Scope mc_scope.
 Local Open Scope mc_mult_scope.

theories/Algebra/Groups/QuotientGroup.v

@@ -111,7 +111,7 @@ End GroupCongruenceQuotient.
 Section Cosets.
 
   Context (G : Group) (H : Subgroup G).
-  
+
   Definition LeftCoset := G / in_cosetL H.
 
   (** TODO: Way too many universes, needs fixing *)
@@ -130,7 +130,7 @@ Section Cosets.
     := fcard LeftCoset.
 
   Definition RightCoset := G / in_cosetR H.
-  
+
   (** The set of left cosets is equivalent to the set of right coset. *)
   Definition equiv_leftcoset_rightcoset
     : LeftCoset <~> RightCoset.
@@ -226,7 +226,7 @@ Definition QuotientGroup' (G : Group) (N : Subgroup G) (H : IsNormalSubgroup N)
 
 Local Open Scope group_scope.
 
-(** Computation rule for grp_quotient_rec. *)
+(** Computation rule for [grp_quotient_rec]. *)
 Corollary grp_quotient_rec_beta `{F : Funext} {G : Group}
           (N : NormalSubgroup G) (H : Group)
           {A : Group} (f : G $-> A)
@@ -236,15 +236,15 @@ Proof.
   apply equiv_path_grouphomomorphism; reflexivity.
 Defined.
 
-(** Computation rule for grp_quotient_rec. *)
+(** Computation rule for [grp_quotient_rec]. *)
 Definition grp_quotient_rec_beta' {G : Group}
           (N : NormalSubgroup G) (H : Group)
           {A : Group} (f : G $-> A)
           (h : forall n:G, N n -> f n = mon_unit)
   : (grp_quotient_rec G N f h) $o grp_quotient_map == f
     := fun _ => idpath.
 
-(** The proof of normality is irrelevent up to equivalence. This is unfortunate that it doesn't hold definitionally. *)
+(** The proof of normality is irrelevant up to equivalence. It is unfortunate that it doesn't hold definitionally. *)
 Definition grp_iso_quotient_normal (G : Group) (H : Subgroup G)
   {k k' : IsNormalSubgroup H}
   : QuotientGroup' G H k ≅ QuotientGroup' G H k'.

theories/Algebra/Groups/Subgroup.v

@@ -459,7 +459,7 @@ Proof.
   all: exact isnormal.
 Defined.
 
-(** Our definiiton of normal subgroup implies the usual definition of invariance under conjugation. *)
+(** Our definition of normal subgroup implies the usual definition of invariance under conjugation. *)
 Definition isnormal_conj {G : Group} (N : Subgroup G)
   `{!IsNormalSubgroup N} {x y : G}
   : N x <~> N (y * x * y^).
@@ -1062,7 +1062,7 @@ Proof.
   apply grp_image_in.
 Defined.
 
-(** ** Image of a subgroup under a group homomoprhism *)
+(** ** Image of a subgroup under a group homomorphism *)
 
 (** The image of a subgroup under group homomorphism. *) 
 Definition subgroup_image {G H : Group} (f : G $-> H)

theories/Algebra/Rings/CRing.v

@@ -96,7 +96,7 @@ Defined.
 Section IdealCRing.
   Context {R : CRing}.
 
-  (** The section is meant to complement the IdealLemmas section in Algebra.Rings.Ideal. Since the results here only hold in commutative rings, they have to be kept here. *)
+  (** The section is meant to complement the [IdealLemmas] section in Algebra.Rings.Ideal. Since the results here only hold in commutative rings, they have to be kept here. *)
 
   (** We import ideal notations as used in Algebra.Rings.Ideal but only for this section. Important to note is that [↔] corresponds to equality of ideals. *)
   Import Ideal.Notation.

theories/Algebra/Rings/ChineseRemainder.v

@@ -140,7 +140,7 @@ Section ChineseRemainderTheorem.
 
 End ChineseRemainderTheorem.
 
-(** We also have the same for products of ideals when in a commuatative ring. *)
+(** We also have the same for products of ideals when in a commutative ring. *)
 Theorem chinese_remainder_prod `{Univalence}
   {R : CRing} (I J : Ideal R) (c : Coprime I J)
   : R / (I ⋅ J)%ideal ≅ (R / I) × (R / J).

theories/Algebra/Rings/Ideal.v

@@ -14,7 +14,7 @@ Local Open Scope ideal_scope.
 
 (** ** Definition of Ideals *)
 
-(** An additive subgroup [I] of a ring [R] is a left ideal when it is closed under multiplciation on the left. *)
+(** An additive subgroup [I] of a ring [R] is a left ideal when it is closed under multiplication on the left. *)
 Class IsLeftIdeal {R : Ring} (I : Subgroup R) :=
   isleftideal (r x : R) : I x -> I (r * x).
 
@@ -368,7 +368,7 @@ Definition ideal_kernel {R S : Ring} (f : RingHomomorphism R S) : Ideal R
 
 (** *** Ideal generated by a subset *)
 
-(** It seems tempting to define ideals generated by a subset in terms of subgroups generated by a subset but this does not work. Left ideals also have to be closed under left multiplciation by ring elements, and similarly for right and two sided ideals. Therefore we will do an analagous construction to the one done in Subgroup.v. *)
+(** It seems tempting to define ideals generated by a subset in terms of subgroups generated by a subset but this does not work. Left ideals also have to be closed under left multiplication by ring elements, and similarly for right and two sided ideals. Therefore we will do an analagous construction to the one done in Subgroup.v. *)
 
 (** Underlying type family of a left ideal generated by subset. *)
 Inductive leftideal_generated_type (R : Ring) (X : R -> Type) : R -> Type :=
@@ -482,7 +482,7 @@ Proof.
   rapply equiv_path_subgroup'.
 Defined.
 
-(** Under funext, ideal equiality is a proposition. *)
+(** Under funext, ideal equality is a proposition. *)
 Instance ishprop_ideal_eq `{Funext} {R : Ring} (I J : Ideal R)
   : IsHProp (ideal_eq I J) := _.
 
@@ -651,7 +651,7 @@ Proof.
   apply rng_mult_zero_r.
 Defined.
 
-(** The left annihilator of a left ideal also happens to be a right ideal. In fact, left ideal could be weakened to subset closed under multplication, however we don't need this generality currently. *)
+(** The left annihilator of a left ideal also happens to be a right ideal. In fact, left ideal could be weakened to subset closed under multiplication, however we don't need this generality currently. *)
 Instance isrightideal_ideal_left_annihilator {R : Ring} (I : Subgroup R)
   `{IsLeftIdeal R I}
   : IsRightIdeal (subgroup_ideal_left_annihilator I).
@@ -778,7 +778,7 @@ Defined.
 
 (** *** Ideal notations *)
 
-(** We declare and import a module for various (unicode) ideal notations. These exist in their own special case, and can be imported and used in other files when needing to reason about ideals. *)
+(** We declare and import a module for various (Unicode) ideal notations. These exist in their own special case, and can be imported and used in other files when needing to reason about ideals. *)
 
 Module Import Notation.
   Infix "⊆" := ideal_subset       : ideal_scope.