diff --git a/Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean b/Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean index 90fc859b2e71dc..0bc98d1925ba10 100644 --- a/Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean +++ b/Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean @@ -9,7 +9,6 @@ public import Mathlib.Algebra.Homology.HomotopyCategory public import Mathlib.Algebra.Homology.ShortComplex.ShortExact public import Mathlib.CategoryTheory.Abelian.Exact public import Mathlib.CategoryTheory.Preadditive.Injective.Resolution -public import Mathlib.Data.Set.Subsingleton public import Mathlib.Tactic.AdaptationNote /-! diff --git a/Mathlib/CategoryTheory/Abelian/LeftDerived.lean b/Mathlib/CategoryTheory/Abelian/LeftDerived.lean index 9a2d018b40184c..e1a56182230d02 100644 --- a/Mathlib/CategoryTheory/Abelian/LeftDerived.lean +++ b/Mathlib/CategoryTheory/Abelian/LeftDerived.lean @@ -5,7 +5,6 @@ Authors: Kim Morrison, Riccardo Brasca, Adam Topaz, Jujian Zhang, Joël Riou -/ module -public import Mathlib.Algebra.Homology.Additive public import Mathlib.CategoryTheory.Abelian.Projective.Resolution /-! diff --git a/Mathlib/CategoryTheory/Adhesive/Subobject.lean b/Mathlib/CategoryTheory/Adhesive/Subobject.lean index f0ec0576e4d5ab..b1b154346e4a16 100644 --- a/Mathlib/CategoryTheory/Adhesive/Subobject.lean +++ b/Mathlib/CategoryTheory/Adhesive/Subobject.lean @@ -7,7 +7,6 @@ module public import Mathlib.CategoryTheory.Adhesive.Basic public import Mathlib.CategoryTheory.Subobject.Basic -public import Mathlib.CategoryTheory.Subobject.Lattice /-! diff --git a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean index d3a6ececd33723..72811180047770 100644 --- a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean +++ b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean @@ -5,11 +5,9 @@ Authors: Bhavik Mehta -/ module -public import Mathlib.CategoryTheory.Comma.StructuredArrow.Small public import Mathlib.CategoryTheory.Generator.Basic public import Mathlib.CategoryTheory.Limits.ConeCategory public import Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial -public import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic public import Mathlib.CategoryTheory.Subobject.Comma /-! diff --git a/Mathlib/CategoryTheory/Adjunction/Basic.lean b/Mathlib/CategoryTheory/Adjunction/Basic.lean index 832b9966e0a402..b20a13c8e6f0b5 100644 --- a/Mathlib/CategoryTheory/Adjunction/Basic.lean +++ b/Mathlib/CategoryTheory/Adjunction/Basic.lean @@ -5,7 +5,6 @@ Authors: Reid Barton, Johan Commelin, Bhavik Mehta -/ module -public import Mathlib.CategoryTheory.Equivalence public import Mathlib.CategoryTheory.Yoneda /-! diff --git a/Mathlib/CategoryTheory/Adjunction/Evaluation.lean b/Mathlib/CategoryTheory/Adjunction/Evaluation.lean index cf9a4cfe1c9c35..6f59775acf1a51 100644 --- a/Mathlib/CategoryTheory/Adjunction/Evaluation.lean +++ b/Mathlib/CategoryTheory/Adjunction/Evaluation.lean @@ -6,7 +6,6 @@ Authors: Adam Topaz module public import Mathlib.CategoryTheory.Limits.Shapes.Products -public import Mathlib.CategoryTheory.Functor.EpiMono /-! diff --git a/Mathlib/CategoryTheory/Adjunction/Limits.lean b/Mathlib/CategoryTheory/Adjunction/Limits.lean index 12b78fe3fb842b..3ba7dcecad814b 100644 --- a/Mathlib/CategoryTheory/Adjunction/Limits.lean +++ b/Mathlib/CategoryTheory/Adjunction/Limits.lean @@ -5,7 +5,6 @@ Authors: Reid Barton, Johan Commelin -/ module -public import Mathlib.CategoryTheory.Adjunction.Basic public import Mathlib.CategoryTheory.Limits.Creates /-! diff --git a/Mathlib/CategoryTheory/Bicategory/Extension.lean b/Mathlib/CategoryTheory/Bicategory/Extension.lean index 544da9e4986eb0..ca08ab82eefa94 100644 --- a/Mathlib/CategoryTheory/Bicategory/Extension.lean +++ b/Mathlib/CategoryTheory/Bicategory/Extension.lean @@ -7,7 +7,6 @@ module public import Mathlib.CategoryTheory.Bicategory.Basic public import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic -public import Mathlib.Tactic.CategoryTheory.CancelIso /-! # Extensions and lifts in bicategories diff --git a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean index 3b788ef71aad9e..c8e955c91fb5d0 100644 --- a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean +++ b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean @@ -6,7 +6,6 @@ Authors: Yuma Mizuno, Calle Sönne module public import Mathlib.CategoryTheory.CommSq -public import Mathlib.CategoryTheory.Discrete.Basic public import Mathlib.CategoryTheory.Bicategory.Strict.Basic /-! diff --git a/Mathlib/CategoryTheory/Category/Cat.lean b/Mathlib/CategoryTheory/Category/Cat.lean index f85d24d863d9f8..d4cfb465cdfef6 100644 --- a/Mathlib/CategoryTheory/Category/Cat.lean +++ b/Mathlib/CategoryTheory/Category/Cat.lean @@ -7,7 +7,6 @@ module public import Mathlib.CategoryTheory.Bicategory.Strict.Basic public import Mathlib.CategoryTheory.ConcreteCategory.Bundled -public import Mathlib.CategoryTheory.Discrete.Basic public import Mathlib.CategoryTheory.Types.Basic /-! diff --git a/Mathlib/CategoryTheory/Category/Preorder.lean b/Mathlib/CategoryTheory/Category/Preorder.lean index f13f0360d232f9..6a0802ed2d49da 100644 --- a/Mathlib/CategoryTheory/Category/Preorder.lean +++ b/Mathlib/CategoryTheory/Category/Preorder.lean @@ -5,7 +5,6 @@ Authors: Stephen Morgan, Kim Morrison, Johannes Hölzl, Reid Barton -/ module -public import Mathlib.CategoryTheory.Equivalence public import Mathlib.CategoryTheory.EqToHom public import Mathlib.Order.Hom.Basic public import Mathlib.Data.ULift diff --git a/Mathlib/CategoryTheory/Category/RelCat.lean b/Mathlib/CategoryTheory/Category/RelCat.lean index dcd7ffc61a4c7d..72c463e23550e3 100644 --- a/Mathlib/CategoryTheory/Category/RelCat.lean +++ b/Mathlib/CategoryTheory/Category/RelCat.lean @@ -5,9 +5,6 @@ Authors: Kim Morrison, Uni Marx -/ module -public import Mathlib.CategoryTheory.EssentialImage -public import Mathlib.CategoryTheory.Iso -public import Mathlib.CategoryTheory.Opposites public import Mathlib.CategoryTheory.Types.Basic public import Mathlib.Data.Rel diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean index 3e5de1291687bb..10cd17f4e31358 100644 --- a/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean +++ b/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean @@ -5,7 +5,6 @@ Authors: Adam Topaz, Kim Morrison -/ module -public import Mathlib.CategoryTheory.Comma.Basic public import Mathlib.CategoryTheory.PUnit public import Mathlib.CategoryTheory.Limits.Shapes.IsTerminal public import Mathlib.CategoryTheory.Functor.EpiMono diff --git a/Mathlib/CategoryTheory/ComposableArrows/Basic.lean b/Mathlib/CategoryTheory/ComposableArrows/Basic.lean index f01bc0dbddb289..659f7f4c874f1c 100644 --- a/Mathlib/CategoryTheory/ComposableArrows/Basic.lean +++ b/Mathlib/CategoryTheory/ComposableArrows/Basic.lean @@ -8,10 +8,10 @@ module public import Mathlib.Algebra.Group.Nat.Defs public import Mathlib.CategoryTheory.Category.Preorder public import Mathlib.CategoryTheory.Comma.Arrow -public import Mathlib.CategoryTheory.EpiMono public import Mathlib.Data.Fintype.Basic public import Mathlib.Tactic.FinCases public import Mathlib.Tactic.SuppressCompilation + /-! # Composable arrows diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Forget.lean b/Mathlib/CategoryTheory/ConcreteCategory/Forget.lean index 3ac2f9d2fd3716..106e3ee8090230 100644 --- a/Mathlib/CategoryTheory/ConcreteCategory/Forget.lean +++ b/Mathlib/CategoryTheory/ConcreteCategory/Forget.lean @@ -6,7 +6,6 @@ Authors: Kim Morrison, Johannes Hölzl, Reid Barton, Sean Leather, Yury Kudryash -/ module -public import Mathlib.CategoryTheory.ConcreteCategory.Basic public import Mathlib.CategoryTheory.Types.Basic /-! # Forgetful functors diff --git a/Mathlib/CategoryTheory/Countable.lean b/Mathlib/CategoryTheory/Countable.lean index 6f2fe5a00da2d0..0addaeb860ed21 100644 --- a/Mathlib/CategoryTheory/Countable.lean +++ b/Mathlib/CategoryTheory/Countable.lean @@ -7,8 +7,8 @@ module public import Mathlib.CategoryTheory.EssentiallySmall public import Mathlib.CategoryTheory.FinCategory.Basic -public import Mathlib.Data.Fintype.EquivFin public import Mathlib.Data.Countable.Small + /-! # Countable categories diff --git a/Mathlib/CategoryTheory/Dialectica/Basic.lean b/Mathlib/CategoryTheory/Dialectica/Basic.lean index 451030504f6069..c42e0291d75e5b 100644 --- a/Mathlib/CategoryTheory/Dialectica/Basic.lean +++ b/Mathlib/CategoryTheory/Dialectica/Basic.lean @@ -6,7 +6,6 @@ Authors: Mario Carneiro module public import Mathlib.CategoryTheory.Subobject.Basic -public import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts /-! # Dialectica category diff --git a/Mathlib/CategoryTheory/Discrete/Basic.lean b/Mathlib/CategoryTheory/Discrete/Basic.lean index cc88d163f0e23a..6c3b16b74c7b16 100644 --- a/Mathlib/CategoryTheory/Discrete/Basic.lean +++ b/Mathlib/CategoryTheory/Discrete/Basic.lean @@ -5,7 +5,6 @@ Authors: Stephen Morgan, Kim Morrison, Floris van Doorn -/ module -public import Mathlib.CategoryTheory.EqToHom public import Mathlib.CategoryTheory.Pi.Basic /-! diff --git a/Mathlib/CategoryTheory/Elements.lean b/Mathlib/CategoryTheory/Elements.lean index e1dab61c6e1f97..17b14c9a0ecf56 100644 --- a/Mathlib/CategoryTheory/Elements.lean +++ b/Mathlib/CategoryTheory/Elements.lean @@ -6,7 +6,6 @@ Authors: Kim Morrison module public import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic -public import Mathlib.CategoryTheory.Category.Cat public import Mathlib.CategoryTheory.EssentiallySmall /-! diff --git a/Mathlib/CategoryTheory/EpiMono.lean b/Mathlib/CategoryTheory/EpiMono.lean index e34c6a44f3491b..9fcd9c470107df 100644 --- a/Mathlib/CategoryTheory/EpiMono.lean +++ b/Mathlib/CategoryTheory/EpiMono.lean @@ -5,7 +5,6 @@ Authors: Reid Barton, Kim Morrison -/ module -public import Mathlib.CategoryTheory.Opposites public import Mathlib.CategoryTheory.Groupoid /-! diff --git a/Mathlib/CategoryTheory/EssentiallySmall.lean b/Mathlib/CategoryTheory/EssentiallySmall.lean index db93a9bcfc1ac9..d4982dddb9d3e2 100644 --- a/Mathlib/CategoryTheory/EssentiallySmall.lean +++ b/Mathlib/CategoryTheory/EssentiallySmall.lean @@ -6,9 +6,7 @@ Authors: Kim Morrison module public import Mathlib.CategoryTheory.Category.ULift -public import Mathlib.CategoryTheory.EqToHom public import Mathlib.CategoryTheory.Skeletal -public import Mathlib.CategoryTheory.Comma.Arrow public import Mathlib.Logic.UnivLE public import Mathlib.Logic.Small.Basic diff --git a/Mathlib/CategoryTheory/Extensive.lean b/Mathlib/CategoryTheory/Extensive.lean index 29506c729d698f..e3c7e717c6f9cd 100644 --- a/Mathlib/CategoryTheory/Extensive.lean +++ b/Mathlib/CategoryTheory/Extensive.lean @@ -5,13 +5,10 @@ Authors: Andrew Yang -/ module -public import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial public import Mathlib.CategoryTheory.Limits.Types.Coproducts public import Mathlib.CategoryTheory.Limits.Types.Products public import Mathlib.CategoryTheory.Limits.Types.Pullbacks public import Mathlib.Topology.Category.TopCat.Limits.Pullbacks -public import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic -public import Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts public import Mathlib.CategoryTheory.Limits.VanKampen public import Mathlib.CategoryTheory.Limits.MonoCoprod public import Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct diff --git a/Mathlib/CategoryTheory/Functor/EpiMono.lean b/Mathlib/CategoryTheory/Functor/EpiMono.lean index b4db65ded541cb..8d1d05f730cb25 100644 --- a/Mathlib/CategoryTheory/Functor/EpiMono.lean +++ b/Mathlib/CategoryTheory/Functor/EpiMono.lean @@ -5,7 +5,6 @@ Authors: Markus Himmel -/ module -public import Mathlib.CategoryTheory.EpiMono public import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi public import Mathlib.CategoryTheory.LiftingProperties.Adjunction diff --git a/Mathlib/CategoryTheory/Functor/Hom.lean b/Mathlib/CategoryTheory/Functor/Hom.lean index d28859235676c0..686da62ecc73c9 100644 --- a/Mathlib/CategoryTheory/Functor/Hom.lean +++ b/Mathlib/CategoryTheory/Functor/Hom.lean @@ -5,7 +5,6 @@ Authors: Reid Barton, Kim Morrison -/ module -public import Mathlib.CategoryTheory.Products.Basic public import Mathlib.CategoryTheory.Types.Basic /-! diff --git a/Mathlib/CategoryTheory/Groupoid.lean b/Mathlib/CategoryTheory/Groupoid.lean index 85a18908a806c0..32556026769586 100644 --- a/Mathlib/CategoryTheory/Groupoid.lean +++ b/Mathlib/CategoryTheory/Groupoid.lean @@ -5,9 +5,6 @@ Authors: Reid Barton, Kim Morrison, David Wärn -/ module -public import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory -public import Mathlib.CategoryTheory.Products.Basic -public import Mathlib.CategoryTheory.Pi.Basic public import Mathlib.Combinatorics.Quiver.Symmetric public import Mathlib.CategoryTheory.Functor.ReflectsIso.Basic public import Mathlib.CategoryTheory.MorphismProperty.Basic diff --git a/Mathlib/CategoryTheory/Limits/Cones.lean b/Mathlib/CategoryTheory/Limits/Cones.lean index d88fbed2f6a9dc..abd42fe52aa6af 100644 --- a/Mathlib/CategoryTheory/Limits/Cones.lean +++ b/Mathlib/CategoryTheory/Limits/Cones.lean @@ -5,10 +5,7 @@ Authors: Stephen Morgan, Kim Morrison, Floris van Doorn -/ module -public import Mathlib.CategoryTheory.Functor.Const -public import Mathlib.CategoryTheory.Discrete.Basic public import Mathlib.CategoryTheory.Yoneda -public import Mathlib.CategoryTheory.Functor.ReflectsIso.Basic /-! # Cones and cocones diff --git a/Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean b/Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean index 90684b076e6506..a6eac607f7df52 100644 --- a/Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean +++ b/Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean @@ -7,7 +7,6 @@ module public import Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers public import Mathlib.CategoryTheory.Limits.Shapes.Products -public import Mathlib.CategoryTheory.Limits.Shapes.Terminal /-! # Constructions related to weakly initial objects diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean index 0813e60c6f0b11..6f68babdd27583 100644 --- a/Mathlib/CategoryTheory/Limits/HasLimits.lean +++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean @@ -6,10 +6,8 @@ Authors: Reid Barton, Mario Carneiro, Kim Morrison, Floris van Doorn module public import Mathlib.CategoryTheory.Limits.IsLimit -public import Mathlib.CategoryTheory.Category.ULift public import Mathlib.CategoryTheory.EssentiallySmall public import Mathlib.CategoryTheory.Functor.EpiMono -public import Mathlib.Logic.Equiv.Basic /-! # Existence of limits and colimits diff --git a/Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean b/Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean index e95a725f1ca011..b43755fdc4f0d6 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean @@ -5,7 +5,6 @@ Authors: Bhavik Mehta, Christian Merten -/ module -public import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic public import Mathlib.CategoryTheory.Limits.Shapes.Products public import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean index 0438270f2630ce..0e10d59ccb98b5 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean @@ -6,7 +6,6 @@ Authors: Kim Morrison, Bhavik Mehta module public import Mathlib.CategoryTheory.Limits.HasLimits -public import Mathlib.CategoryTheory.Discrete.Basic /-! # Categorical (co)products diff --git a/Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean b/Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean index a08b8a2f05cb9f..b3e13dabb80963 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean @@ -5,7 +5,6 @@ Authors: Bhavik Mehta -/ module -public import Mathlib.CategoryTheory.Limits.Shapes.Terminal public import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts /-! diff --git a/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean b/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean index 1c29b538d68185..0ff34e5e0be0b0 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean @@ -6,7 +6,6 @@ Authors: Bhavik Mehta, Jakob von Raumer module public import Mathlib.CategoryTheory.Limits.HasLimits -public import Mathlib.CategoryTheory.Thin /-! # Wide pullbacks diff --git a/Mathlib/CategoryTheory/Limits/VanKampen.lean b/Mathlib/CategoryTheory/Limits/VanKampen.lean index 54d198bb9a25c7..3956148965ceba 100644 --- a/Mathlib/CategoryTheory/Limits/VanKampen.lean +++ b/Mathlib/CategoryTheory/Limits/VanKampen.lean @@ -9,9 +9,7 @@ public import Mathlib.CategoryTheory.Adjunction.FullyFaithful public import Mathlib.CategoryTheory.Adjunction.Limits public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered public import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial -public import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic public import Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts -public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic /-! diff --git a/Mathlib/CategoryTheory/Monad/Algebra.lean b/Mathlib/CategoryTheory/Monad/Algebra.lean index 1eebbf293cf46c..92f9669202ac65 100644 --- a/Mathlib/CategoryTheory/Monad/Algebra.lean +++ b/Mathlib/CategoryTheory/Monad/Algebra.lean @@ -6,7 +6,6 @@ Authors: Kim Morrison, Bhavik Mehta module public import Mathlib.CategoryTheory.Monad.Basic -public import Mathlib.CategoryTheory.Adjunction.Basic public import Mathlib.CategoryTheory.Functor.EpiMono /-! diff --git a/Mathlib/CategoryTheory/Monad/Basic.lean b/Mathlib/CategoryTheory/Monad/Basic.lean index a81dec24df1974..67fb2591103f09 100644 --- a/Mathlib/CategoryTheory/Monad/Basic.lean +++ b/Mathlib/CategoryTheory/Monad/Basic.lean @@ -5,10 +5,7 @@ Authors: Kim Morrison, Bhavik Mehta, Adam Topaz -/ module -public import Mathlib.CategoryTheory.Functor.Category -public import Mathlib.CategoryTheory.Functor.FullyFaithful -public import Mathlib.CategoryTheory.Functor.ReflectsIso.Basic -public import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi +public import Mathlib.CategoryTheory.EpiMono /-! # Monads diff --git a/Mathlib/CategoryTheory/Monoidal/Action/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Action/Basic.lean index f6c9ab7100e240..55869eb650d373 100644 --- a/Mathlib/CategoryTheory/Monoidal/Action/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/Action/Basic.lean @@ -6,7 +6,6 @@ Authors: Robin Carlier module public import Mathlib.CategoryTheory.Monoidal.Category -public import Mathlib.CategoryTheory.Functor.Trifunctor /-! diff --git a/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean index 3369060df72eac..a4a248c6f7b58e 100644 --- a/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean @@ -6,10 +6,9 @@ Authors: Kim Morrison module public import Mathlib.CategoryTheory.Monoidal.Discrete -public import Mathlib.CategoryTheory.Monoidal.NaturalTransformation public import Mathlib.CategoryTheory.Monoidal.Opposite -public import Mathlib.Tactic.CategoryTheory.Monoidal.Basic public import Mathlib.CategoryTheory.CommSq +public import Mathlib.Tactic.CategoryTheory.Monoidal.Basic /-! # Braided and symmetric monoidal categories diff --git a/Mathlib/CategoryTheory/Monoidal/Discrete.lean b/Mathlib/CategoryTheory/Monoidal/Discrete.lean index 7a3abe8486f3e7..49ae3e31735c91 100644 --- a/Mathlib/CategoryTheory/Monoidal/Discrete.lean +++ b/Mathlib/CategoryTheory/Monoidal/Discrete.lean @@ -6,7 +6,6 @@ Authors: Kim Morrison module public import Mathlib.Algebra.Group.Hom.Defs -public import Mathlib.CategoryTheory.Discrete.Basic public import Mathlib.CategoryTheory.Monoidal.NaturalTransformation /-! diff --git a/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean b/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean index 264d9b44912b90..60505a12b403b0 100644 --- a/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean +++ b/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean @@ -6,7 +6,6 @@ Authors: Markus Himmel module public import Mathlib.CategoryTheory.Monoidal.Free.Basic -public import Mathlib.CategoryTheory.Discrete.Basic /-! # The monoidal coherence theorem diff --git a/Mathlib/CategoryTheory/Monoidal/Functor.lean b/Mathlib/CategoryTheory/Monoidal/Functor.lean index bf0182a0e0379c..93bf9f11869314 100644 --- a/Mathlib/CategoryTheory/Monoidal/Functor.lean +++ b/Mathlib/CategoryTheory/Monoidal/Functor.lean @@ -7,7 +7,6 @@ module public import Mathlib.CategoryTheory.Monoidal.Category public import Mathlib.CategoryTheory.Adjunction.FullyFaithful -public import Mathlib.CategoryTheory.Products.Basic /-! # (Lax) monoidal functors diff --git a/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean b/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean index 7bb47d2fa0012c..5ae95b6cc00b5d 100644 --- a/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean +++ b/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean @@ -6,8 +6,6 @@ Authors: Kim Morrison module public import Mathlib.CategoryTheory.Monoidal.Braided.Basic -public import Mathlib.CategoryTheory.Functor.Category -public import Mathlib.CategoryTheory.Functor.Const /-! # Monoidal structure on `C ⥤ D` when `D` is monoidal. diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean index 9ae4dafe23b257..05145483c18607 100644 --- a/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean +++ b/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean @@ -5,10 +5,10 @@ Authors: Kim Morrison, Bhavik Mehta -/ module -public import Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory -public import Mathlib.CategoryTheory.Monoidal.Limits.Basic -public import Mathlib.CategoryTheory.Limits.Preserves.Basic public import Mathlib.CategoryTheory.Limits.Creates +public import Mathlib.CategoryTheory.Monoidal.CommMon_ +public import Mathlib.CategoryTheory.Monoidal.Comon_ +public import Mathlib.CategoryTheory.Monoidal.FunctorCategory /-! # Limits of monoid objects. diff --git a/Mathlib/CategoryTheory/Monoidal/Mon.lean b/Mathlib/CategoryTheory/Monoidal/Mon.lean index 39199771933d2e..3fa554cabd6730 100644 --- a/Mathlib/CategoryTheory/Monoidal/Mon.lean +++ b/Mathlib/CategoryTheory/Monoidal/Mon.lean @@ -8,7 +8,6 @@ module public import Mathlib.Algebra.Group.PUnit public import Mathlib.CategoryTheory.Monoidal.Braided.Basic public import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas -public import Mathlib.CategoryTheory.Monoidal.Discrete public import Mathlib.CategoryTheory.Limits.Shapes.Terminal import Mathlib.Tactic.Attr.Register diff --git a/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean b/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean index bbbc1b0d349010..7d29e8c03b7825 100644 --- a/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean +++ b/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean @@ -5,9 +5,7 @@ Authors: Kim Morrison -/ module -public import Mathlib.CategoryTheory.Adjunction.FullyFaithful public import Mathlib.CategoryTheory.Monoidal.Functor -public import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory /-! # Monoidal natural transformations diff --git a/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean b/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean index 90b23165a95186..99ff5f7eb8a2b3 100644 --- a/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean +++ b/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean @@ -5,9 +5,8 @@ Authors: Kim Morrison, Simon Hudon -/ module -public import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic -public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts -public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal +public import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts +public import Mathlib.CategoryTheory.Monoidal.Braided.Basic /-! # The natural monoidal structure on any category with finite (co)products. diff --git a/Mathlib/CategoryTheory/Monoidal/Opposite/Mon.lean b/Mathlib/CategoryTheory/Monoidal/Opposite/Mon.lean index 5f12a51e57f035..d200bc35141f0a 100644 --- a/Mathlib/CategoryTheory/Monoidal/Opposite/Mon.lean +++ b/Mathlib/CategoryTheory/Monoidal/Opposite/Mon.lean @@ -5,7 +5,6 @@ Authors: Robin Carlier -/ module -public import Mathlib.CategoryTheory.Monoidal.Opposite public import Mathlib.CategoryTheory.Monoidal.Mon /-! diff --git a/Mathlib/CategoryTheory/PUnit.lean b/Mathlib/CategoryTheory/PUnit.lean index 63cca9bb5186de..fdbd8e6e56b429 100644 --- a/Mathlib/CategoryTheory/PUnit.lean +++ b/Mathlib/CategoryTheory/PUnit.lean @@ -5,7 +5,6 @@ Authors: Kim Morrison, Bhavik Mehta -/ module -public import Mathlib.CategoryTheory.Functor.Const public import Mathlib.CategoryTheory.Discrete.Basic public import Mathlib.Data.ULift diff --git a/Mathlib/CategoryTheory/Pi/Monoidal.lean b/Mathlib/CategoryTheory/Pi/Monoidal.lean index c83f8cd949478f..5d194ce1b506ab 100644 --- a/Mathlib/CategoryTheory/Pi/Monoidal.lean +++ b/Mathlib/CategoryTheory/Pi/Monoidal.lean @@ -5,8 +5,6 @@ Authors: Sina Hazratpour -/ module -public import Mathlib.CategoryTheory.Pi.Basic -public import Mathlib.CategoryTheory.Monoidal.Category public import Mathlib.CategoryTheory.Monoidal.Braided.Basic public import Mathlib.CategoryTheory.Monoidal.Closed.Basic diff --git a/Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean b/Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean index 700a6e36cfb219..cbdf8419ffbdf4 100644 --- a/Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean +++ b/Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean @@ -6,9 +6,7 @@ Authors: Jujian Zhang, Kim Morrison, Joël Riou module public import Mathlib.Algebra.Homology.QuasiIso -public import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex public import Mathlib.Algebra.Homology.SingleHomology -public import Mathlib.CategoryTheory.Preadditive.Injective.Basic /-! # Injective resolutions diff --git a/Mathlib/CategoryTheory/Quotient.lean b/Mathlib/CategoryTheory/Quotient.lean index 41cbec0cf28aa9..4ce992e4714346 100644 --- a/Mathlib/CategoryTheory/Quotient.lean +++ b/Mathlib/CategoryTheory/Quotient.lean @@ -5,8 +5,6 @@ Authors: David Wärn -/ module -public import Mathlib.CategoryTheory.NatIso -public import Mathlib.CategoryTheory.EqToHom public import Mathlib.CategoryTheory.Groupoid /-! diff --git a/Mathlib/CategoryTheory/Subobject/Types.lean b/Mathlib/CategoryTheory/Subobject/Types.lean index 5e1b1287883a2b..b009a83e7f75c4 100644 --- a/Mathlib/CategoryTheory/Subobject/Types.lean +++ b/Mathlib/CategoryTheory/Subobject/Types.lean @@ -6,8 +6,6 @@ Authors: Kim Morrison module public import Mathlib.CategoryTheory.Subobject.WellPowered -public import Mathlib.CategoryTheory.Types.Basic -public import Mathlib.Data.Set.Subsingleton /-! # `Type u` is well-powered diff --git a/Mathlib/CategoryTheory/Thin.lean b/Mathlib/CategoryTheory/Thin.lean index c177c615528024..bcdb471330e201 100644 --- a/Mathlib/CategoryTheory/Thin.lean +++ b/Mathlib/CategoryTheory/Thin.lean @@ -6,7 +6,6 @@ Authors: Kim Morrison, Bhavik Mehta module public import Mathlib.CategoryTheory.Functor.Category -public import Mathlib.CategoryTheory.Iso /-! # Thin categories diff --git a/Mathlib/CategoryTheory/Triangulated/Opposite/OpOp.lean b/Mathlib/CategoryTheory/Triangulated/Opposite/OpOp.lean index cb233e1fdcb5e1..d4b3f1d9368160 100644 --- a/Mathlib/CategoryTheory/Triangulated/Opposite/OpOp.lean +++ b/Mathlib/CategoryTheory/Triangulated/Opposite/OpOp.lean @@ -6,7 +6,6 @@ Authors: Joël Riou module public import Mathlib.CategoryTheory.Triangulated.Adjunction -public import Mathlib.CategoryTheory.Triangulated.Opposite.Basic /-! # The triangulated equivalence `Cᵒᵖᵒᵖ ≌ C`. diff --git a/Mathlib/CategoryTheory/Types/Basic.lean b/Mathlib/CategoryTheory/Types/Basic.lean index 611b4cd5e49e83..2a86cd297e3aba 100644 --- a/Mathlib/CategoryTheory/Types/Basic.lean +++ b/Mathlib/CategoryTheory/Types/Basic.lean @@ -7,7 +7,6 @@ module public import Mathlib.CategoryTheory.Elementwise public import Mathlib.CategoryTheory.EpiMono -public import Mathlib.Data.Set.CoeSort public import Mathlib.Tactic.PPWithUniv public import Mathlib.Tactic.ToAdditive diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean index d42555d101e4f9..b9654179bd2eec 100644 --- a/Mathlib/CategoryTheory/Yoneda.lean +++ b/Mathlib/CategoryTheory/Yoneda.lean @@ -6,9 +6,6 @@ Authors: Kim Morrison module public import Mathlib.CategoryTheory.Functor.Hom -public import Mathlib.CategoryTheory.Products.Basic -public import Mathlib.Data.ULift -public import Mathlib.Logic.Function.ULift /-! # The Yoneda embedding