chore: split CategoryTheory.MorphismProperty (#12393)

The file `CategoryTheory.MorphismProperty` is split into five files `Basic`, `Composition`, `Limits`, `Concrete`, `IsInvertedBy`.
leanprover-community · May 16, 2024 · d051bf3 · d051bf3
1 parent 963333a
commit d051bf3
Show file tree

Hide file tree

Showing 19 changed files with 1,168 additions and 1,045 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1436,7 +1436,11 @@ import Mathlib.CategoryTheory.Monoidal.Transport
 import Mathlib.CategoryTheory.Monoidal.Types.Basic
 import Mathlib.CategoryTheory.Monoidal.Types.Coyoneda
 import Mathlib.CategoryTheory.Monoidal.Types.Symmetric
-import Mathlib.CategoryTheory.MorphismProperty
+import Mathlib.CategoryTheory.MorphismProperty.Basic
+import Mathlib.CategoryTheory.MorphismProperty.Composition
+import Mathlib.CategoryTheory.MorphismProperty.Concrete
+import Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
+import Mathlib.CategoryTheory.MorphismProperty.Limits
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Noetherian

diff --git a/Mathlib/Algebra/Homology/HomotopyCategory.lean b/Mathlib/Algebra/Homology/HomotopyCategory.lean
@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import Mathlib.Algebra.Homology.Homotopy
 import Mathlib.Algebra.Homology.Linear
+import Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
 import Mathlib.CategoryTheory.Quotient.Linear
 import Mathlib.CategoryTheory.Quotient.Preadditive
 

diff --git a/Mathlib/Algebra/Homology/HomotopyCofiber.lean b/Mathlib/Algebra/Homology/HomotopyCofiber.lean
@@ -5,6 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.Algebra.Homology.HomologicalComplexBiprod
 import Mathlib.Algebra.Homology.Homotopy
+import Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
 
 /-! The homotopy cofiber of a morphism of homological complexes
 

diff --git a/Mathlib/Algebra/Homology/Localization.lean b/Mathlib/Algebra/Homology/Localization.lean
@@ -5,10 +5,10 @@ Authors: Joël Riou
 -/
 
 import Mathlib.Algebra.Homology.HomotopyCofiber
-import Mathlib.Algebra.Homology.QuasiIso
 import Mathlib.Algebra.Homology.HomotopyCategory
-import Mathlib.CategoryTheory.Localization.HasLocalization
+import Mathlib.Algebra.Homology.QuasiIso
 import Mathlib.CategoryTheory.Localization.Composition
+import Mathlib.CategoryTheory.Localization.HasLocalization
 
 /-! The category of homological complexes up to quasi-isomorphisms
 

diff --git a/Mathlib/Algebra/Homology/ShortComplex/Exact.lean b/Mathlib/Algebra/Homology/ShortComplex/Exact.lean
@@ -7,7 +7,6 @@ import Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
 import Mathlib.Algebra.Homology.ShortComplex.Abelian
 import Mathlib.Algebra.Homology.ShortComplex.QuasiIso
 import Mathlib.CategoryTheory.Abelian.Exact
-import Mathlib.CategoryTheory.MorphismProperty
 import Mathlib.CategoryTheory.Preadditive.Injective
 
 /-!

diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
@@ -5,7 +5,7 @@ Authors: Andrew Yang
 -/
 import Mathlib.AlgebraicGeometry.AffineScheme
 import Mathlib.AlgebraicGeometry.Pullbacks
-import Mathlib.CategoryTheory.MorphismProperty
+import Mathlib.CategoryTheory.MorphismProperty.Limits
 import Mathlib.Data.List.TFAE
 
 #align_import algebraic_geometry.morphisms.basic from "leanprover-community/mathlib"@"434e2fd21c1900747afc6d13d8be7f4eedba7218"

diff --git a/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean b/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
@@ -3,7 +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
 -/
-import Mathlib.CategoryTheory.MorphismProperty
+import Mathlib.CategoryTheory.Adjunction.Basic
+import Mathlib.CategoryTheory.MorphismProperty.Basic
+import Mathlib.CategoryTheory.Yoneda
 
 #align_import category_theory.adjunction.fully_faithful from "leanprover-community/mathlib"@"9e7c80f638149bfb3504ba8ff48dfdbfc949fb1a"
 

diff --git a/Mathlib/CategoryTheory/Adjunction/Reflective.lean b/Mathlib/CategoryTheory/Adjunction/Reflective.lean
@@ -5,6 +5,7 @@ Authors: Bhavik Mehta
 -/
 import Mathlib.CategoryTheory.Adjunction.FullyFaithful
 import Mathlib.CategoryTheory.Conj
+import Mathlib.CategoryTheory.Functor.ReflectsIso
 
 #align_import category_theory.adjunction.reflective from "leanprover-community/mathlib"@"239d882c4fb58361ee8b3b39fb2091320edef10a"
 

diff --git a/Mathlib/CategoryTheory/Localization/Construction.lean b/Mathlib/CategoryTheory/Localization/Construction.lean
@@ -3,7 +3,8 @@ Copyright (c) 2022 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
-import Mathlib.CategoryTheory.MorphismProperty
+import Mathlib.CategoryTheory.MorphismProperty.Composition
+import Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
 import Mathlib.CategoryTheory.Category.Quiv
 
 #align_import category_theory.localization.construction from "leanprover-community/mathlib"@"1a5e56f2166e4e9d0964c71f4273b1d39227678d"

diff --git a/Mathlib/CategoryTheory/Localization/FiniteProducts.lean b/Mathlib/CategoryTheory/Localization/FiniteProducts.lean
@@ -8,6 +8,7 @@ import Mathlib.CategoryTheory.Limits.Preserves.Finite
 import Mathlib.CategoryTheory.Localization.Adjunction
 import Mathlib.CategoryTheory.Localization.HasLocalization
 import Mathlib.CategoryTheory.Localization.Pi
+import Mathlib.CategoryTheory.MorphismProperty.Limits
 
 /-! The localized category has finite products
 

diff --git a/Mathlib/CategoryTheory/Localization/Pi.lean b/Mathlib/CategoryTheory/Localization/Pi.lean
@@ -5,6 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.Localization.Prod
 import Mathlib.CategoryTheory.Localization.Equivalence
+import Mathlib.Data.Fintype.Option
 
 /-!
 # Localization of product categories

diff --git a/Mathlib/CategoryTheory/Localization/Prod.lean b/Mathlib/CategoryTheory/Localization/Prod.lean
@@ -3,7 +3,9 @@ Copyright (c) 2023 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
+import Mathlib.CategoryTheory.Functor.Currying
 import Mathlib.CategoryTheory.Localization.Predicate
+import Mathlib.CategoryTheory.MorphismProperty.Composition
 
 /-!
 # Localization of product categories