From 78cdacd3e16b2dcbb607f9f541dfd7ea49eb9c73 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 6 Apr 2024 22:07:02 +0200 Subject: [PATCH 1/7] doc(Algebra,AlgebraicGeometry): remove mathlib3 names in doc comments Mostly automatic, with a few manual corrections. --- Mathlib/Algebra/BigOperators/Basic.lean | 2 +- Mathlib/Algebra/BigOperators/Finsupp.lean | 4 ++-- Mathlib/Algebra/Category/GroupCat/Adjunctions.lean | 14 +++++++------- Mathlib/Algebra/Category/GroupCat/Basic.lean | 6 +++--- Mathlib/Algebra/Category/GroupCat/Limits.lean | 2 +- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 8 ++++---- Mathlib/Algebra/Category/MonCat/Basic.lean | 2 +- Mathlib/Algebra/Category/MonCat/Colimits.lean | 2 +- .../Algebra/Category/MonCat/FilteredColimits.lean | 4 ++-- Mathlib/Algebra/Category/MonCat/Limits.lean | 2 +- .../Algebra/Category/Ring/FilteredColimits.lean | 14 +++++++------- Mathlib/Algebra/Category/SemigroupCat/Basic.lean | 8 ++++---- Mathlib/Algebra/GCDMonoid/Basic.lean | 2 +- Mathlib/Algebra/Group/Prod.lean | 4 ++-- Mathlib/Algebra/Homology/Homology.lean | 2 +- Mathlib/Algebra/Homology/ImageToKernel.lean | 4 ++-- Mathlib/Algebra/Homology/ModuleCat.lean | 2 +- Mathlib/Algebra/MvPolynomial/Monad.lean | 2 +- Mathlib/Algebra/Order/Monoid/WithZero.lean | 2 +- Mathlib/Algebra/Polynomial/Laurent.lean | 4 ++-- Mathlib/Algebra/Ring/Prod.lean | 2 +- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean | 4 ++-- Mathlib/AlgebraicGeometry/Pullbacks.lean | 2 +- 23 files changed, 49 insertions(+), 49 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean index e6c81b4d5ed1f..8719e5b022c26 100644 --- a/Mathlib/Algebra/BigOperators/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/BigOperators/Finsupp.lean b/Mathlib/Algebra/BigOperators/Finsupp.lean index 40ec823eddb03..0077058678886 100644 --- a/Mathlib/Algebra/BigOperators/Finsupp.lean +++ b/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 `Sum` and `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₂) : diff --git a/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean b/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean index 8859515e7524a..291b68588ea0a 100644 --- a/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean +++ 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 +* `AddCommGroupCat.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 +* `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 +* `AddCommGroupCat.adj`: proves that `AddCommGroupCat.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 +* `GroupCat.adj`: proves that `GroupCat.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 +* `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 `Group` 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 `CommGroup` and `CommMonCat`. -/ def CommGroupCat.forget₂CommMonAdj : forget₂ CommGroupCat CommMonCat ⊣ CommMonCat.units.{u} where homEquiv X Y := { toFun := fun f => MonoidHom.toHomUnits f diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean index 96c5070fa933f..62a144ab27d54 100644 --- a/Mathlib/Algebra/Category/GroupCat/Basic.lean +++ b/Mathlib/Algebra/Category/GroupCat/Basic.lean @@ -440,11 +440,11 @@ 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 +/-- "additive equivalences between `AddGroup`s are the same as (isomorphic to) isomorphisms in `AddGroup` -/ add_decl_doc addEquivIsoAddGroupIso -/-- multiplicative equivalences between `comm_group`s are the same as (isomorphic to) isomorphisms +/-- multiplicative equivalences between `CommGroup`s are the same as (isomorphic to) isomorphisms in `CommGroup` -/ @[to_additive] def mulEquivIsoCommGroupIso {X Y : CommGroupCat.{u}} : X ≃* Y ≅ X ≅ Y where @@ -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 diff --git a/Mathlib/Algebra/Category/GroupCat/Limits.lean b/Mathlib/Algebra/Category/GroupCat/Limits.lean index 2c102694a1bd2..87d049a5d074c 100644 --- a/Mathlib/Algebra/Category/GroupCat/Limits.lean +++ b/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 `Subtype` map. -/ @[simps! hom_left_apply_coe inv_left_apply] def kernelIsoKerOver {G H : AddCommGroupCat.{u}} (f : G ⟶ H) : diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index a442bd76e77fd..60f26be1f296f 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -279,13 +279,13 @@ 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 `Module 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 `Module 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 @@ -293,14 +293,14 @@ abbrev LinearEquiv.toModuleIso'Right [AddCommGroup X₁] [Module R X₁] {X₂ : namespace CategoryTheory.Iso -/-- Build a `linear_equiv` from an isomorphism in the category `Module R`. -/ +/-- Build a `LinearEquiv` from an isomorphism in the category `Module 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 +/-- linear equivalences between `Module`s are the same as (isomorphic to) isomorphisms in `Module` -/ @[simps] def linearEquivIsoModuleIso {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] [Module R X] diff --git a/Mathlib/Algebra/Category/MonCat/Basic.lean b/Mathlib/Algebra/Category/MonCat/Basic.lean index c2dbca73f1374..4a4048070b388 100644 --- a/Mathlib/Algebra/Category/MonCat/Basic.lean +++ b/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] diff --git a/Mathlib/Algebra/Category/MonCat/Colimits.lean b/Mathlib/Algebra/Category/MonCat/Colimits.lean index 644d7ac40d977..3deed36a476cd 100644 --- a/Mathlib/Algebra/Category/MonCat/Colimits.lean +++ b/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) diff --git a/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean b/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean index 8581f44035b5b..18f4ec99e959e 100644 --- a/Mathlib/Algebra/Category/MonCat/FilteredColimits.lean +++ b/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}) diff --git a/Mathlib/Algebra/Category/MonCat/Limits.lean b/Mathlib/Algebra/Category/MonCat/Limits.lean index dc89a8f3e54ed..fc8ce7da79960 100644 --- a/Mathlib/Algebra/Category/MonCat/Limits.lean +++ b/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 -- `MonCat` noncomputable section diff --git a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean index 6784ffde5ca30..fb5d0e69b0f15 100644 --- a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean +++ b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean @@ -15,10 +15,10 @@ Forgetful functors from algebraic categories usually don't preserve colimits. Ho 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 +We show that the colimit of `F ⋙ forget₂ SemiRing Mon` (in `MonCat`) 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`. +Similarly for `CommSemiRingCat`, `Ring` and `CommRing`. -/ @@ -57,7 +57,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₂ SemiRing Mon` 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 +134,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 +181,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₂ CommSemiRing SemiRing` 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 +211,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 +257,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₂ Ring SemiRing` in the category `SemiRingCat`. In the following, we will show that this has the structure of a ring. -/ abbrev R : SemiRingCat.{max v u} := diff --git a/Mathlib/Algebra/Category/SemigroupCat/Basic.lean b/Mathlib/Algebra/Category/SemigroupCat/Basic.lean index e6b02036baa57..e1bcf1e40568f 100644 --- a/Mathlib/Algebra/Category/SemigroupCat/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean index 33ee935b116c2..ea10b8b749030 100644 --- a/Mathlib/Algebra/GCDMonoid/Basic.lean +++ b/Mathlib/Algebra/GCDMonoid/Basic.lean @@ -1091,7 +1091,7 @@ noncomputable def normalizedGCDMonoidOfGCD [NormalizationMonoid α] [DecidableEq set l := Classical.choose (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (Dvd.intro b rfl))) obtain rfl | hb := eq_or_ne b 0 -- Porting note: using `simp only` causes the propositions inside `Classical.choose` to - -- differ, so `set` is unable to produce `l = 0` inside `this`. See + -- differ, so `Set` is unable to produce `l = 0` inside `this`. See -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ -- Classical.2Echoose/near/317491179 · rw [mul_zero a, normalize_zero, mul_eq_zero] at this diff --git a/Mathlib/Algebra/Group/Prod.lean b/Mathlib/Algebra/Group/Prod.lean index 1ded29fe49955..cfcf959f0f7e1 100644 --- a/Mathlib/Algebra/Group/Prod.lean +++ b/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)) diff --git a/Mathlib/Algebra/Homology/Homology.lean b/Mathlib/Algebra/Homology/Homology.lean index bf5a22710dac1..5ba59f652a40f 100644 --- a/Mathlib/Algebra/Homology/Homology.lean +++ b/Mathlib/Algebra/Homology/Homology.lean @@ -21,7 +21,7 @@ as `cyclesMap' f i` and `boundariesMap f i`. As a consequence we construct `homologyFunctor' i : HomologicalComplex V c ⥤ V`, computing the `i`-th homology. -Note: Some definitions (specifically, names containing components `homology`, `cycles`) +Note: Some definitions (specifically, names containing components `homology'`, `cycles`) in this file have the suffix `'` so as to allow the development of the new homology API of homological complex (starting from `Algebra.Homology.ShortComplex.HomologicalComplex`). It is planned that these definitions diff --git a/Mathlib/Algebra/Homology/ImageToKernel.lean b/Mathlib/Algebra/Homology/ImageToKernel.lean index c3008f8e56470..0e596e219d93b 100644 --- a/Mathlib/Algebra/Homology/ImageToKernel.lean +++ b/Mathlib/Algebra/Homology/ImageToKernel.lean @@ -18,7 +18,7 @@ we have `image_le_kernel f g w : imageSubobject f ≤ kernelSubobject g` We define `homology' f g w` of such a pair as the cokernel of `imageToKernel f g w`. -Note: As part of the transition to the new homology API, `homology` is temporarily +Note: As part of the transition to the new homology API, `homology'` is temporarily renamed `homology'`. It is planned that this definition shall be removed and replaced by `ShortComplex.homology`. @@ -371,7 +371,7 @@ variable {A B C : V} {f : A ⟶ B} {g : B ⟶ C} (w : f ≫ g = 0) {f' : A ⟶ B (w' : f' ≫ g' = 0) [HasKernels V] [HasCokernels V] [HasImages V] [HasImageMaps V] -- Porting note: removed the private auxiliary tactic which becomes unnecessary ---/-- Custom tactic to golf and speedup boring proofs in `homology.congr`. -/ +--/-- Custom tactic to golf and speedup boring proofs in `homology'.congr`. -/ --private unsafe def aux_tac : tactic Unit := -- sorry diff --git a/Mathlib/Algebra/Homology/ModuleCat.lean b/Mathlib/Algebra/Homology/ModuleCat.lean index 2fb6e6239277a..3290219d85351 100644 --- a/Mathlib/Algebra/Homology/ModuleCat.lean +++ b/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 : ι) : diff --git a/Mathlib/Algebra/MvPolynomial/Monad.lean b/Mathlib/Algebra/MvPolynomial/Monad.lean index 6cef26b2cfb9e..28e26172e57fe 100644 --- a/Mathlib/Algebra/MvPolynomial/Monad.lean +++ b/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 `CommRing` (or rather `CommSemiRingCat`). -/ diff --git a/Mathlib/Algebra/Order/Monoid/WithZero.lean b/Mathlib/Algebra/Order/Monoid/WithZero.lean index ac7bcf02579a7..676c038268cef 100644 --- a/Mathlib/Algebra/Order/Monoid/WithZero.lean +++ b/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 `MulZeroClass.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 : α) ≤ ⊤) } diff --git a/Mathlib/Algebra/Polynomial/Laurent.lean b/Mathlib/Algebra/Polynomial/Laurent.lean index fb6db87175b02..426f162bc1a60 100644 --- a/Mathlib/Algebra/Polynomial/Laurent.lean +++ b/Mathlib/Algebra/Polynomial/Laurent.lean @@ -53,7 +53,7 @@ Lots is missing! -- (Riccardo) add inclusion into Laurent series. -- (Riccardo) giving a morphism (as `R`-alg, so in the commutative case) from `R[T,T⁻¹]` to `S` is the same as choosing a unit of `S`. --- A "better" definition of `trunc` would be as an `R`-linear map. This works: +-- A "better" definition of `Trunc` would be as an `R`-linear map. This works: -- ``` -- def trunc : R[T;T⁻¹] →[R] R[X] := -- refine (?_ : R[ℕ] →[R] R[X]).comp ?_ @@ -344,7 +344,7 @@ set_option linter.uppercaseLean3 false in /-- `trunc : R[T;T⁻¹] →+ R[X]` maps a Laurent polynomial `f` to the polynomial whose terms of nonnegative degree coincide with the ones of `f`. The terms of negative degree of `f` "vanish". -`trunc` is a left-inverse to `Polynomial.toLaurent`. -/ +`Trunc` is a left-inverse to `Polynomial.toLaurent`. -/ def trunc : R[T;T⁻¹] →+ R[X] := (toFinsuppIso R).symm.toAddMonoidHom.comp <| comapDomain.addMonoidHom fun _ _ => Int.ofNat.inj #align laurent_polynomial.trunc LaurentPolynomial.trunc diff --git a/Mathlib/Algebra/Ring/Prod.lean b/Mathlib/Algebra/Ring/Prod.lean index 2df1e78fc47ba..dc07c249822db 100644 --- a/Mathlib/Algebra/Ring/Prod.lean +++ b/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 diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean index b048c71947138..42f144b7261c6 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean @@ -71,10 +71,10 @@ namespace WeierstrassCurve.Affine variable {R : Type u} [CommRing R] (W : Affine R) -- Porting note: in Lean 3, this is a `def` under a `derive comm_ring` tag. --- This generates a reducible instance of `comm_ring` for `coordinate_ring`. In certain +-- This generates a reducible instance of `CommRing` for `CoordinateRing`. In certain -- circumstances this might be extremely slow, because all instances in its definition are unified -- exponentially many times. In this case, one solution is to manually add the local attribute --- `local attribute [irreducible] coordinate_ring.comm_ring` to block this type-level unification. +-- `local attribute [irreducible] CoordinateRing.CommRing` to block this type-level unification. -- In Lean 4, this is no longer an issue and is now an `abbrev`. See Zulip thread: -- https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.E2.9C.94.20class_group.2Emk /-- The coordinate ring $R[W] := R[X, Y] / \langle W(X, Y) \rangle$ of `W`. -/ diff --git a/Mathlib/AlgebraicGeometry/Pullbacks.lean b/Mathlib/AlgebraicGeometry/Pullbacks.lean index da72611136248..f72d68a7a7b80 100644 --- a/Mathlib/AlgebraicGeometry/Pullbacks.lean +++ b/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' From 205d7757f2ed81c2bc9dcd79058b972a44cc85c6 Mon Sep 17 00:00:00 2001 From: grunweg Date: Sun, 7 Apr 2024 09:02:34 +0200 Subject: [PATCH 2/7] Manual fix-ups. --- Mathlib/Algebra/BigOperators/Finsupp.lean | 2 +- Mathlib/Algebra/Category/GroupCat/Adjunctions.lean | 4 ++-- Mathlib/Algebra/Homology/Homology.lean | 2 +- Mathlib/Algebra/Homology/ImageToKernel.lean | 4 ++-- Mathlib/Algebra/Polynomial/Laurent.lean | 4 ++-- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Finsupp.lean b/Mathlib/Algebra/BigOperators/Finsupp.lean index 0077058678886..261af50a82733 100644 --- a/Mathlib/Algebra/BigOperators/Finsupp.lean +++ b/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`. -/ diff --git a/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean b/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean index 291b68588ea0a..7f302d7cc79c8 100644 --- a/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean +++ b/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean @@ -17,8 +17,8 @@ category of abelian groups. ## Main definitions -* `AddCommGroupCat.free`: constructs the functor associating to a type `X` the free abelian group with - generators `x : X`. +* `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ᵃᵇ`. diff --git a/Mathlib/Algebra/Homology/Homology.lean b/Mathlib/Algebra/Homology/Homology.lean index 5ba59f652a40f..bf5a22710dac1 100644 --- a/Mathlib/Algebra/Homology/Homology.lean +++ b/Mathlib/Algebra/Homology/Homology.lean @@ -21,7 +21,7 @@ as `cyclesMap' f i` and `boundariesMap f i`. As a consequence we construct `homologyFunctor' i : HomologicalComplex V c ⥤ V`, computing the `i`-th homology. -Note: Some definitions (specifically, names containing components `homology'`, `cycles`) +Note: Some definitions (specifically, names containing components `homology`, `cycles`) in this file have the suffix `'` so as to allow the development of the new homology API of homological complex (starting from `Algebra.Homology.ShortComplex.HomologicalComplex`). It is planned that these definitions diff --git a/Mathlib/Algebra/Homology/ImageToKernel.lean b/Mathlib/Algebra/Homology/ImageToKernel.lean index 0e596e219d93b..c3008f8e56470 100644 --- a/Mathlib/Algebra/Homology/ImageToKernel.lean +++ b/Mathlib/Algebra/Homology/ImageToKernel.lean @@ -18,7 +18,7 @@ we have `image_le_kernel f g w : imageSubobject f ≤ kernelSubobject g` We define `homology' f g w` of such a pair as the cokernel of `imageToKernel f g w`. -Note: As part of the transition to the new homology API, `homology'` is temporarily +Note: As part of the transition to the new homology API, `homology` is temporarily renamed `homology'`. It is planned that this definition shall be removed and replaced by `ShortComplex.homology`. @@ -371,7 +371,7 @@ variable {A B C : V} {f : A ⟶ B} {g : B ⟶ C} (w : f ≫ g = 0) {f' : A ⟶ B (w' : f' ≫ g' = 0) [HasKernels V] [HasCokernels V] [HasImages V] [HasImageMaps V] -- Porting note: removed the private auxiliary tactic which becomes unnecessary ---/-- Custom tactic to golf and speedup boring proofs in `homology'.congr`. -/ +--/-- Custom tactic to golf and speedup boring proofs in `homology.congr`. -/ --private unsafe def aux_tac : tactic Unit := -- sorry diff --git a/Mathlib/Algebra/Polynomial/Laurent.lean b/Mathlib/Algebra/Polynomial/Laurent.lean index 426f162bc1a60..fb6db87175b02 100644 --- a/Mathlib/Algebra/Polynomial/Laurent.lean +++ b/Mathlib/Algebra/Polynomial/Laurent.lean @@ -53,7 +53,7 @@ Lots is missing! -- (Riccardo) add inclusion into Laurent series. -- (Riccardo) giving a morphism (as `R`-alg, so in the commutative case) from `R[T,T⁻¹]` to `S` is the same as choosing a unit of `S`. --- A "better" definition of `Trunc` would be as an `R`-linear map. This works: +-- A "better" definition of `trunc` would be as an `R`-linear map. This works: -- ``` -- def trunc : R[T;T⁻¹] →[R] R[X] := -- refine (?_ : R[ℕ] →[R] R[X]).comp ?_ @@ -344,7 +344,7 @@ set_option linter.uppercaseLean3 false in /-- `trunc : R[T;T⁻¹] →+ R[X]` maps a Laurent polynomial `f` to the polynomial whose terms of nonnegative degree coincide with the ones of `f`. The terms of negative degree of `f` "vanish". -`Trunc` is a left-inverse to `Polynomial.toLaurent`. -/ +`trunc` is a left-inverse to `Polynomial.toLaurent`. -/ def trunc : R[T;T⁻¹] →+ R[X] := (toFinsuppIso R).symm.toAddMonoidHom.comp <| comapDomain.addMonoidHom fun _ _ => Int.ofNat.inj #align laurent_polynomial.trunc LaurentPolynomial.trunc From 8c9fbbb65f29c8f1d0cf49fd69d3c4d42fdd0c80 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 7 Apr 2024 09:05:42 +0200 Subject: [PATCH 3/7] Fix line length. --- Mathlib/Algebra/Category/GroupCat/Adjunctions.lean | 8 ++++---- Mathlib/Algebra/Order/Monoid/WithZero.lean | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean b/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean index 7f302d7cc79c8..71cb76e1dee66 100644 --- a/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean +++ b/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean @@ -25,10 +25,10 @@ category of abelian groups. ## Main statements -* `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. +* `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. -/ diff --git a/Mathlib/Algebra/Order/Monoid/WithZero.lean b/Mathlib/Algebra/Order/Monoid/WithZero.lean index 676c038268cef..0a720a3666060 100644 --- a/Mathlib/Algebra/Order/Monoid/WithZero.lean +++ b/Mathlib/Algebra/Order/Monoid/WithZero.lean @@ -298,8 +298,8 @@ instance instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual { Multiplicative.orderedCommMonoid, Multiplicative.linearOrder with zero := Multiplicative.ofAdd (⊤ : α) zero_mul := @top_add _ (_) - -- Porting note: Here and elsewhere in the file, just `MulZeroClass.zero_mul` worked in Lean 3. See - -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Type.20synonyms + -- Porting note: Here and elsewhere in the file, just `MulZeroClass.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 : α) ≤ ⊤) } #align multiplicative.linear_ordered_comm_monoid_with_zero instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual From 3ef53927df1fa5281cf9dade80d07da961509915 Mon Sep 17 00:00:00 2001 From: grunweg Date: Sun, 7 Apr 2024 10:48:27 +0200 Subject: [PATCH 4/7] Apply suggestions from code review Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> --- Mathlib/Algebra/Category/GroupCat/Adjunctions.lean | 4 ++-- Mathlib/Algebra/Category/GroupCat/Basic.lean | 4 ++-- Mathlib/Algebra/Category/GroupCat/Limits.lean | 2 +- Mathlib/Algebra/Category/ModuleCat/Basic.lean | 8 ++++---- Mathlib/Algebra/Category/MonCat/Limits.lean | 2 +- Mathlib/Algebra/Category/Ring/FilteredColimits.lean | 2 +- Mathlib/Algebra/GCDMonoid/Basic.lean | 2 +- Mathlib/Algebra/MvPolynomial/Monad.lean | 2 +- Mathlib/Algebra/Order/Monoid/WithZero.lean | 4 ++-- 9 files changed, 15 insertions(+), 15 deletions(-) diff --git a/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean b/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean index 71cb76e1dee66..8f5723deaa1ed 100644 --- a/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean +++ b/Mathlib/Algebra/Category/GroupCat/Adjunctions.lean @@ -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 `MonCat`. -/ +/-- 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 `CommMonCat`. -/ +/-- 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 diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean index 62a144ab27d54..5289c3d2e4983 100644 --- a/Mathlib/Algebra/Category/GroupCat/Basic.lean +++ b/Mathlib/Algebra/Category/GroupCat/Basic.lean @@ -441,11 +441,11 @@ set_option linter.uppercaseLean3 false in #align add_equiv_iso_AddGroup_iso addEquivIsoAddGroupIso /-- "additive equivalences between `AddGroup`s are the same -as (isomorphic to) isomorphisms in `AddGroup` -/ +as (isomorphic to) isomorphisms in `AddGroupCat` -/ add_decl_doc addEquivIsoAddGroupIso /-- multiplicative equivalences between `CommGroup`s are the same as (isomorphic to) isomorphisms -in `CommGroup` -/ +in `CommGroupCat` -/ @[to_additive] def mulEquivIsoCommGroupIso {X Y : CommGroupCat.{u}} : X ≃* Y ≅ X ≅ Y where hom e := e.toCommGroupCatIso diff --git a/Mathlib/Algebra/Category/GroupCat/Limits.lean b/Mathlib/Algebra/Category/GroupCat/Limits.lean index 87d049a5d074c..aaff0a0051bb6 100644 --- a/Mathlib/Algebra/Category/GroupCat/Limits.lean +++ b/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) : diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean index 60f26be1f296f..778df52098971 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Basic.lean @@ -279,13 +279,13 @@ 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 `LinearEquiv` 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 `LinearEquiv` 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 @@ -293,7 +293,7 @@ abbrev LinearEquiv.toModuleIso'Right [AddCommGroup X₁] [Module R X₁] {X₂ : namespace CategoryTheory.Iso -/-- Build a `LinearEquiv` 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 @@ -301,7 +301,7 @@ def toLinearEquiv {X Y : ModuleCat R} (i : X ≅ Y) : X ≃ₗ[R] Y := end CategoryTheory.Iso /-- linear equivalences between `Module`s are the same as (isomorphic to) isomorphisms -in `Module` -/ +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 diff --git a/Mathlib/Algebra/Category/MonCat/Limits.lean b/Mathlib/Algebra/Category/MonCat/Limits.lean index fc8ce7da79960..bb8007bc6dfca 100644 --- a/Mathlib/Algebra/Category/MonCat/Limits.lean +++ b/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 -- `MonCat` +set_option linter.uppercaseLean3 false noncomputable section diff --git a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean index fb5d0e69b0f15..3449860723af4 100644 --- a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean +++ b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean @@ -57,7 +57,7 @@ set_option linter.uppercaseLean3 false in variable [IsFiltered J] -/-- The colimit of `F ⋙ forget₂ SemiRing Mon` in the category `MonCat`. +/-- 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} := diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean index ea10b8b749030..33ee935b116c2 100644 --- a/Mathlib/Algebra/GCDMonoid/Basic.lean +++ b/Mathlib/Algebra/GCDMonoid/Basic.lean @@ -1091,7 +1091,7 @@ noncomputable def normalizedGCDMonoidOfGCD [NormalizationMonoid α] [DecidableEq set l := Classical.choose (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (Dvd.intro b rfl))) obtain rfl | hb := eq_or_ne b 0 -- Porting note: using `simp only` causes the propositions inside `Classical.choose` to - -- differ, so `Set` is unable to produce `l = 0` inside `this`. See + -- differ, so `set` is unable to produce `l = 0` inside `this`. See -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ -- Classical.2Echoose/near/317491179 · rw [mul_zero a, normalize_zero, mul_eq_zero] at this diff --git a/Mathlib/Algebra/MvPolynomial/Monad.lean b/Mathlib/Algebra/MvPolynomial/Monad.lean index 28e26172e57fe..3875f44ad3f74 100644 --- a/Mathlib/Algebra/MvPolynomial/Monad.lean +++ b/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 `CommSemiRingCat`). +since it is not a monad in `Type` but in `CommRingCat` (or rather `CommSemiRingCat`). -/ diff --git a/Mathlib/Algebra/Order/Monoid/WithZero.lean b/Mathlib/Algebra/Order/Monoid/WithZero.lean index 0a720a3666060..7f78ad7f24b1b 100644 --- a/Mathlib/Algebra/Order/Monoid/WithZero.lean +++ b/Mathlib/Algebra/Order/Monoid/WithZero.lean @@ -298,8 +298,8 @@ instance instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual { Multiplicative.orderedCommMonoid, Multiplicative.linearOrder with zero := Multiplicative.ofAdd (⊤ : α) zero_mul := @top_add _ (_) - -- Porting note: Here and elsewhere in the file, just `MulZeroClass.zero_mul` worked in Lean 3. - -- See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Type.20synonyms + -- 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 : α) ≤ ⊤) } #align multiplicative.linear_ordered_comm_monoid_with_zero instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual From 0ef6ba34d56a0a0bb536f1a53d6190b48e98b7fe Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 7 Apr 2024 10:50:15 +0200 Subject: [PATCH 5/7] One more. --- Mathlib/Algebra/Category/GroupCat/Basic.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean index 5289c3d2e4983..86122255b1317 100644 --- a/Mathlib/Algebra/Category/GroupCat/Basic.lean +++ b/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 `AddGroup`s are the same -as (isomorphic to) isomorphisms in `AddGroupCat` -/ +/-- Additive equivalences between `AddGroup`s are the same +as (isomorphic to) isomorphisms in `AddGroupCat`. -/ add_decl_doc addEquivIsoAddGroupIso -/-- multiplicative equivalences between `CommGroup`s are the same as (isomorphic to) isomorphisms -in `CommGroupCat` -/ +/-- 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 From 1f4e733aad70e80b842377c13a07c9582daf6439 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 7 Apr 2024 10:51:34 +0200 Subject: [PATCH 6/7] Revert one more. --- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean index 42f144b7261c6..b048c71947138 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean @@ -71,10 +71,10 @@ namespace WeierstrassCurve.Affine variable {R : Type u} [CommRing R] (W : Affine R) -- Porting note: in Lean 3, this is a `def` under a `derive comm_ring` tag. --- This generates a reducible instance of `CommRing` for `CoordinateRing`. In certain +-- This generates a reducible instance of `comm_ring` for `coordinate_ring`. In certain -- circumstances this might be extremely slow, because all instances in its definition are unified -- exponentially many times. In this case, one solution is to manually add the local attribute --- `local attribute [irreducible] CoordinateRing.CommRing` to block this type-level unification. +-- `local attribute [irreducible] coordinate_ring.comm_ring` to block this type-level unification. -- In Lean 4, this is no longer an issue and is now an `abbrev`. See Zulip thread: -- https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.E2.9C.94.20class_group.2Emk /-- The coordinate ring $R[W] := R[X, Y] / \langle W(X, Y) \rangle$ of `W`. -/ From 891702c770fff05e61efaad8207ca6f26486640f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 7 Apr 2024 10:55:14 +0200 Subject: [PATCH 7/7] chore(Algebra/Category/Ring/FilteredColimits): remaining changes --- .../Category/Ring/FilteredColimits.lean | 21 ++++++++++--------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean index 3449860723af4..06647a9f71d27 100644 --- a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean +++ b/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 `MonCat`) 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 `CommSemiRingCat`, `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) := @@ -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 `SemiRingCat`. +/-- 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} := @@ -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 `SemiRingCat`. +/-- 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}