refactor(category_theory/functor): a folder for concepts directly related to functors (#12346)

TwoFX · TwoFX · commit 73dd4b5411ec · 2022-03-01T01:31:29.000Z
diff --git a/docs/tutorial/category_theory/intro.lean b/docs/tutorial/category_theory/intro.lean
@@ -1,4 +1,4 @@
-import category_theory.functor_category -- this transitively imports
+import category_theory.functor.category -- this transitively imports
 -- category_theory.category
 -- category_theory.functor
 -- category_theory.natural_transformation
diff --git a/src/algebra/category/Mon/basic.lean b/src/algebra/category/Mon/basic.lean
@@ -6,7 +6,7 @@ Authors: Scott Morrison
 import tactic.elementwise
 import category_theory.concrete_category.bundled_hom
 import algebra.punit_instances
-import category_theory.reflects_isomorphisms
+import category_theory.functor.reflects_isomorphisms
 
 /-!
 # Category instances for monoid, add_monoid, comm_monoid, and add_comm_monoid.
diff --git a/src/algebra/category/Semigroup/basic.lean b/src/algebra/category/Semigroup/basic.lean
@@ -5,7 +5,7 @@ Authors: Julian Kuelshammer
 -/
 import algebra.pempty_instances
 import category_theory.concrete_category.bundled_hom
-import category_theory.reflects_isomorphisms
+import category_theory.functor.reflects_isomorphisms
 
 /-!
 # Category instances for has_mul, has_add, semigroup and add_semigroup
diff --git a/src/category_theory/abelian/ext.lean b/src/category_theory/abelian/ext.lean
@@ -5,7 +5,7 @@ Authors: Scott Morrison, Adam Topaz
 -/
 import algebra.category.Group.basic
 import algebra.category.Module.abelian
-import category_theory.derived
+import category_theory.functor.derived
 import category_theory.linear.yoneda
 import category_theory.abelian.opposite
 import category_theory.abelian.projective
diff --git a/src/category_theory/adjunction/reflective.lean b/src/category_theory/adjunction/reflective.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import category_theory.adjunction.fully_faithful
-import category_theory.reflects_isomorphisms
+import category_theory.functor.reflects_isomorphisms
 import category_theory.epi_mono
 
 /-!
diff --git a/src/category_theory/comma.lean b/src/category_theory/comma.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johan Commelin, Bhavik Mehta
 -/
 import category_theory.isomorphism
-import category_theory.functor_category
+import category_theory.functor.category
 import category_theory.eq_to_hom
 
 /-!
diff --git a/src/category_theory/concrete_category/reflects_isomorphisms.lean b/src/category_theory/concrete_category/reflects_isomorphisms.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.concrete_category.basic
-import category_theory.reflects_isomorphisms
+import category_theory.functor.reflects_isomorphisms
 
 /-!
 A `forget₂ C D` forgetful functor between concrete categories `C` and `D`
diff --git a/src/category_theory/equivalence.lean b/src/category_theory/equivalence.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
 -/
-import category_theory.fully_faithful
+import category_theory.functor.fully_faithful
 import category_theory.full_subcategory
 import category_theory.whiskering
 import category_theory.essential_image
diff --git a/src/category_theory/full_subcategory.lean b/src/category_theory/full_subcategory.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Reid Barton
 -/
-import category_theory.fully_faithful
+import category_theory.functor.fully_faithful
 
 /-!
 # Induced categories and full subcategories
diff --git a/src/category_theory/functor/basic.lean b/src/category_theory/functor/basic.lean
diff --git a/src/category_theory/functor/category.lean b/src/category_theory/functor/category.lean
diff --git a/src/category_theory/functor/const.lean b/src/category_theory/functor/const.lean
diff --git a/src/category_theory/functor/currying.lean b/src/category_theory/functor/currying.lean
diff --git a/src/category_theory/functor/default.lean b/src/category_theory/functor/default.lean
@@ -0,0 +1 @@
+import category_theory.functor.basic
diff --git a/src/category_theory/functor/derived.lean b/src/category_theory/functor/derived.lean
diff --git a/src/category_theory/functor/flat.lean b/src/category_theory/functor/flat.lean
diff --git a/src/category_theory/functor/fully_faithful.lean b/src/category_theory/functor/fully_faithful.lean
diff --git a/src/category_theory/functor/functorial.lean b/src/category_theory/functor/functorial.lean
diff --git a/src/category_theory/functor/hom.lean b/src/category_theory/functor/hom.lean
diff --git a/src/category_theory/functor/reflects_isomorphisms.lean b/src/category_theory/functor/reflects_isomorphisms.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
-import category_theory.fully_faithful
+import category_theory.functor.fully_faithful
 
 /-!
 # Functors which reflect isomorphisms
diff --git a/src/category_theory/limits/colimit_limit.lean b/src/category_theory/limits/colimit_limit.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.limits.types
-import category_theory.currying
+import category_theory.functor.currying
 import category_theory.limits.functor_category
 
 /-!
diff --git a/src/category_theory/limits/cones.lean b/src/category_theory/limits/cones.lean
@@ -3,10 +3,10 @@ Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stephen Morgan, Scott Morrison, Floris van Doorn
 -/
-import category_theory.const
+import category_theory.functor.const
 import category_theory.discrete_category
 import category_theory.yoneda
-import category_theory.reflects_isomorphisms
+import category_theory.functor.reflects_isomorphisms
 
 -- morphism levels before object levels. See note [category_theory universes].
 universes v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
diff --git a/src/category_theory/limits/fubini.lean b/src/category_theory/limits/fubini.lean
@@ -5,7 +5,7 @@ Authors: Scott Morrison
 -/
 import category_theory.limits.has_limits
 import category_theory.products.basic
-import category_theory.currying
+import category_theory.functor.currying
 
 /-!
 # A Fubini theorem for categorical limits
diff --git a/src/category_theory/limits/is_limit.lean b/src/category_theory/limits/is_limit.lean
@@ -5,7 +5,6 @@ Authors: Reid Barton, Mario Carneiro, Scott Morrison, Floris van Doorn
 -/
 import category_theory.adjunction.basic
 import category_theory.limits.cones
-import category_theory.reflects_isomorphisms
 
 /-!
 # Limits and colimits
diff --git a/src/category_theory/monad/algebra.lean b/src/category_theory/monad/algebra.lean
@@ -5,7 +5,6 @@ Authors: Scott Morrison, Bhavik Mehta
 -/
 import category_theory.monad.basic
 import category_theory.adjunction.basic
-import category_theory.reflects_isomorphisms
 
 /-!
 # Eilenberg-Moore (co)algebras for a (co)monad
diff --git a/src/category_theory/monad/basic.lean b/src/category_theory/monad/basic.lean
@@ -3,9 +3,9 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Bhavik Mehta, Adam Topaz
 -/
-import category_theory.functor_category
-import category_theory.fully_faithful
-import category_theory.reflects_isomorphisms
+import category_theory.functor.category
+import category_theory.functor.fully_faithful
+import category_theory.functor.reflects_isomorphisms
 
 namespace category_theory
 open category
diff --git a/src/category_theory/monoidal/center.lean b/src/category_theory/monoidal/center.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.monoidal.braided
-import category_theory.reflects_isomorphisms
+import category_theory.functor.reflects_isomorphisms
 
 /-!
 # Half braidings and the Drinfeld center of a monoidal category
diff --git a/src/category_theory/monoidal/functor_category.lean b/src/category_theory/monoidal/functor_category.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.monoidal.braided
-import category_theory.functor_category
-import category_theory.const
+import category_theory.functor.category
+import category_theory.functor.const
 
 /-!
 # Monoidal structure on `C ⥤ D` when `D` is monoidal.
diff --git a/src/category_theory/monoidal/functorial.lean b/src/category_theory/monoidal/functorial.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.monoidal.functor
-import category_theory.functorial
+import category_theory.functor.functorial
 
 /-!
 # Unbundled lax monoidal functors
diff --git a/src/category_theory/monoidal/tor.lean b/src/category_theory/monoidal/tor.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.derived
+import category_theory.functor.derived
 import category_theory.monoidal.preadditive
 
 /-!
diff --git a/src/category_theory/natural_isomorphism.lean b/src/category_theory/natural_isomorphism.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
 -/
-import category_theory.functor_category
+import category_theory.functor.category
 import category_theory.isomorphism
 
 /-!
diff --git a/src/category_theory/over.lean b/src/category_theory/over.lean
@@ -5,7 +5,7 @@ Authors: Johan Commelin, Bhavik Mehta
 -/
 import category_theory.structured_arrow
 import category_theory.punit
-import category_theory.reflects_isomorphisms
+import category_theory.functor.reflects_isomorphisms
 import category_theory.epi_mono
 
 /-!
diff --git a/src/category_theory/punit.lean b/src/category_theory/punit.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Bhavik Mehta
 -/
-import category_theory.const
+import category_theory.functor.const
 import category_theory.discrete_category
 
 /-!
diff --git a/src/category_theory/sigma/basic.lean b/src/category_theory/sigma/basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import category_theory.whiskering
-import category_theory.fully_faithful
+import category_theory.functor.fully_faithful
 import category_theory.natural_isomorphism
 import data.sigma.basic
 
diff --git a/src/category_theory/sites/cover_preserving.lean b/src/category_theory/sites/cover_preserving.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import category_theory.sites.limits
-import category_theory.flat_functors
+import category_theory.functor.flat
 import category_theory.limits.preserves.filtered
 import category_theory.sites.left_exact
 
diff --git a/src/category_theory/subobject/mono_over.lean b/src/category_theory/subobject/mono_over.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Scott Morrison
 -/
-import category_theory.currying
+import category_theory.functor.currying
 import category_theory.limits.over
 import category_theory.limits.shapes.images
 import category_theory.adjunction.reflective
diff --git a/src/category_theory/thin.lean b/src/category_theory/thin.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison, Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Bhavik Mehta
 -/
-import category_theory.functor_category
+import category_theory.functor.category
 import category_theory.isomorphism
 
 /-!
diff --git a/src/category_theory/types.lean b/src/category_theory/types.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl
 -/
 import category_theory.epi_mono
-import category_theory.fully_faithful
+import category_theory.functor.fully_faithful
 import data.equiv.basic
 
 /-!
diff --git a/src/category_theory/whiskering.lean b/src/category_theory/whiskering.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.isomorphism
-import category_theory.functor_category
-import category_theory.fully_faithful
+import category_theory.functor.category
+import category_theory.functor.fully_faithful
 
 /-!
 # Whiskering
diff --git a/src/category_theory/yoneda.lean b/src/category_theory/yoneda.lean
@@ -3,8 +3,8 @@ Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.hom_functor
-import category_theory.currying
+import category_theory.functor.hom
+import category_theory.functor.currying
 import category_theory.products.basic
 
 /-!

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-import category_theory.functor_category -- this transitively imports`
	`1`	`+import category_theory.functor.category -- this transitively imports`
`2`	`2`	`-- category_theory.category`
`3`	`3`	`-- category_theory.functor`
`4`	`4`	`-- category_theory.natural_transformation`