From 12c8e4f9ee7d8cbf672970c75a81ed2eed1c6b6d Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 20 Apr 2023 08:29:09 +0000 Subject: [PATCH] chore: fix simps projections in CategoryTheory.Monad.Basic (#3269) This fixes a regression of `@[simps]` to `@[simp]` from #2969, per [zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/!4.232969.20simps.20bug.3F.20.28Monad.2EBasic.29). There are a few incidental changes to `@[simps]` arguments in this PR, just removing arguments that had no effect on behaviour. Co-authored-by: Scott Morrison --- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean | 2 +- Mathlib/CategoryTheory/Bicategory/Functor.lean | 5 ++--- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean | 2 +- Mathlib/CategoryTheory/Monad/Basic.lean | 11 +++++++---- Mathlib/CategoryTheory/Monoidal/Functor.lean | 3 +++ .../Monoidal/NaturalTransformation.lean | 2 ++ 6 files changed, 16 insertions(+), 9 deletions(-) diff --git a/Mathlib/CategoryTheory/Abelian/NonPreadditive.lean b/Mathlib/CategoryTheory/Abelian/NonPreadditive.lean index a98310f5e312a..d12445cce5196 100644 --- a/Mathlib/CategoryTheory/Abelian/NonPreadditive.lean +++ b/Mathlib/CategoryTheory/Abelian/NonPreadditive.lean @@ -71,7 +71,7 @@ variable (C : Type u) [Category.{v} C] /-- We call a category `NonPreadditiveAbelian` if it has a zero object, kernels, cokernels, binary products and coproducts, and every monomorphism and every epimorphism is normal. -/ class NonPreadditiveAbelian extends HasZeroMorphisms C, NormalMonoCategory C, - NormalEpiCategory C where + NormalEpiCategory C where [has_zero_object : HasZeroObject C] [has_kernels : HasKernels C] [has_cokernels : HasCokernels C] diff --git a/Mathlib/CategoryTheory/Bicategory/Functor.lean b/Mathlib/CategoryTheory/Bicategory/Functor.lean index 708924de4edb4..81d33bda545ff 100644 --- a/Mathlib/CategoryTheory/Bicategory/Functor.lean +++ b/Mathlib/CategoryTheory/Bicategory/Functor.lean @@ -85,13 +85,12 @@ variable {D : Type u₃} [Quiver.{v₃ + 1} D] [∀ a b : D, Quiver.{w₃ + 1} ( structure PrelaxFunctor (B : Type u₁) [Quiver.{v₁ + 1} B] [∀ a b : B, Quiver.{w₁ + 1} (a ⟶ b)] (C : Type u₂) [Quiver.{v₂ + 1} C] [∀ a b : C, Quiver.{w₂ + 1} (a ⟶ b)] extends Prefunctor B C where + /-- The action of a prelax functor on 2-morphisms. -/ map₂ {a b : B} {f g : a ⟶ b} : (f ⟶ g) → (map f ⟶ map g) #align category_theory.prelax_functor CategoryTheory.PrelaxFunctor initialize_simps_projections PrelaxFunctor (+toPrefunctor, -obj, -map) -attribute [nolint docBlame] CategoryTheory.PrelaxFunctor.map₂ - /-- The prefunctor between the underlying quivers. -/ add_decl_doc PrelaxFunctor.toPrefunctor @@ -371,7 +370,7 @@ associator, the left unitor, and the right unitor modulo some adjustments of dom of 2-morphisms. -/ structure Pseudofunctor (B : Type u₁) [Bicategory.{w₁, v₁} B] (C : Type u₂) - [Bicategory.{w₂, v₂} C] extends PrelaxFunctor B C where + [Bicategory.{w₂, v₂} C] extends PrelaxFunctor B C where mapId (a : B) : map (𝟙 a) ≅ 𝟙 (obj a) mapComp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : map (f ≫ g) ≅ map f ≫ map g map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f) := by aesop_cat diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean index e667905368dda..be59c10e44b47 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean @@ -489,7 +489,7 @@ theorem Cofork.IsColimit.existsUnique {s : Cofork f g} (hs : IsColimit s) {W : C /-- This is a slightly more convenient method to verify that a fork is a limit cone. It only asks for a proof of facts that carry any mathematical content -/ -@[simps lift] +@[simps] def Fork.IsLimit.mk (t : Fork f g) (lift : ∀ s : Fork f g, s.pt ⟶ t.pt) (fac : ∀ s : Fork f g, lift s ≫ Fork.ι t = Fork.ι s) (uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt) (_ : m ≫ t.ι = s.ι), m = lift s) : IsLimit t := diff --git a/Mathlib/CategoryTheory/Monad/Basic.lean b/Mathlib/CategoryTheory/Monad/Basic.lean index 889483745d3d4..2bfbd963d2b27 100644 --- a/Mathlib/CategoryTheory/Monad/Basic.lean +++ b/Mathlib/CategoryTheory/Monad/Basic.lean @@ -183,6 +183,8 @@ structure MonadHom (T₁ T₂ : Monad C) extends NatTrans (T₁ : C ⥤ C) T₂ aesop_cat #align category_theory.monad_hom CategoryTheory.MonadHom +initialize_simps_projections MonadHom (+toNatTrans, -app) + /-- A morphism of comonads is a natural transformation compatible with ε and δ. -/ @[ext] structure ComonadHom (M N : Comonad C) extends NatTrans (M : C ⥤ C) N where @@ -190,9 +192,12 @@ structure ComonadHom (M N : Comonad C) extends NatTrans (M : C ⥤ C) N where app_δ : ∀ X, app X ≫ N.δ.app X = M.δ.app X ≫ app _ ≫ (N : C ⥤ C).map (app X) := by aesop_cat #align category_theory.comonad_hom CategoryTheory.ComonadHom +initialize_simps_projections ComonadHom (+toNatTrans, -app) + attribute [reassoc (attr := simp)] MonadHom.app_η MonadHom.app_μ attribute [reassoc (attr := simp)] ComonadHom.app_ε ComonadHom.app_δ + instance : Category (Monad C) where Hom := MonadHom id M := { toNatTrans := 𝟙 (M : C ⥤ C) } @@ -253,10 +258,9 @@ theorem comp_toNatTrans {T₁ T₂ T₃ : Comonad C} (f : T₁ ⟶ T₂) (g : T rfl #align category_theory.comp_to_nat_trans CategoryTheory.comp_toNatTrans --- porting note: was @[simps] /-- Construct a monad isomorphism from a natural isomorphism of functors where the forward direction is a monad morphism. -/ -@[simp] +@[simps] def MonadIso.mk {M N : Monad C} (f : (M : C ⥤ C) ≅ N) (f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X) (f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = @@ -275,10 +279,9 @@ def MonadIso.mk {M N : Monad C} (f : (M : C ⥤ C) ≅ N) simp } #align category_theory.monad_iso.mk CategoryTheory.MonadIso.mk --- porting note: was @[simps] /-- Construct a comonad isomorphism from a natural isomorphism of functors where the forward direction is a comonad morphism. -/ -@[simp] +@[simps] def ComonadIso.mk {M N : Comonad C} (f : (M : C ⥤ C) ≅ N) (f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X) (f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = diff --git a/Mathlib/CategoryTheory/Monoidal/Functor.lean b/Mathlib/CategoryTheory/Monoidal/Functor.lean index 0c6befc9174ad..fcad8e2139ceb 100644 --- a/Mathlib/CategoryTheory/Monoidal/Functor.lean +++ b/Mathlib/CategoryTheory/Monoidal/Functor.lean @@ -95,6 +95,8 @@ structure LaxMonoidalFunctor extends C ⥤ D where -- Porting note: todo: remove this configuration and use the default configuration. -- We keep this to be consistent with Lean 3. +-- See also `initialize_simps_projections MonoidalFunctor` below. +-- This may require waiting on https://github.com/leanprover-community/mathlib4/pull/2936 initialize_simps_projections LaxMonoidalFunctor (+toFunctor, -obj, -map) --Porting note: was `[simp, reassoc.1]` @@ -151,6 +153,7 @@ structure MonoidalFunctor extends LaxMonoidalFunctor.{v₁, v₂} C D where μ_isIso : ∀ X Y : C, IsIso (μ X Y) := by infer_instance #align category_theory.monoidal_functor CategoryTheory.MonoidalFunctor +-- See porting note on `initialize_simps_projections LaxMonoidalFunctor` initialize_simps_projections MonoidalFunctor (+toLaxMonoidalFunctor, -obj, -map, -ε, -μ) attribute [instance] MonoidalFunctor.ε_isIso MonoidalFunctor.μ_isIso diff --git a/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean b/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean index 67425a1d8ef10..3913b139b7694 100644 --- a/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean +++ b/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean @@ -57,6 +57,8 @@ structure MonoidalNatTrans (F G : LaxMonoidalFunctor C D) extends attribute [reassoc (attr := simp)] MonoidalNatTrans.tensor attribute [reassoc (attr := simp)] MonoidalNatTrans.unit +initialize_simps_projections MonoidalNatTrans (+toNatTrans, -app) + #align category_theory.monoidal_nat_trans.unit CategoryTheory.MonoidalNatTrans.unit #align category_theory.monoidal_nat_trans.unit_assoc CategoryTheory.MonoidalNatTrans.unit_assoc #align category_theory.monoidal_nat_trans.tensor CategoryTheory.MonoidalNatTrans.tensor