diff --git a/Mathlib.lean b/Mathlib.lean index 337013add4caf..008fc0e9566ba 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1708,15 +1708,15 @@ import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject import Mathlib.CategoryTheory.Abelian.Images -import Mathlib.CategoryTheory.Abelian.Injective -import Mathlib.CategoryTheory.Abelian.InjectiveResolution +import Mathlib.CategoryTheory.Abelian.Injective.Basic +import Mathlib.CategoryTheory.Abelian.Injective.Resolution import Mathlib.CategoryTheory.Abelian.LeftDerived import Mathlib.CategoryTheory.Abelian.Monomorphisms import Mathlib.CategoryTheory.Abelian.NonPreadditive import Mathlib.CategoryTheory.Abelian.Opposite -import Mathlib.CategoryTheory.Abelian.Projective -import Mathlib.CategoryTheory.Abelian.ProjectiveDimension -import Mathlib.CategoryTheory.Abelian.ProjectiveResolution +import Mathlib.CategoryTheory.Abelian.Projective.Basic +import Mathlib.CategoryTheory.Abelian.Projective.Dimension +import Mathlib.CategoryTheory.Abelian.Projective.Resolution import Mathlib.CategoryTheory.Abelian.Pseudoelements import Mathlib.CategoryTheory.Abelian.Refinements import Mathlib.CategoryTheory.Abelian.RightDerived @@ -2217,14 +2217,16 @@ import Mathlib.CategoryTheory.Preadditive.EilenbergMoore import Mathlib.CategoryTheory.Preadditive.EndoFunctor import Mathlib.CategoryTheory.Preadditive.FunctorCategory import Mathlib.CategoryTheory.Preadditive.HomOrthogonal -import Mathlib.CategoryTheory.Preadditive.Injective -import Mathlib.CategoryTheory.Preadditive.InjectiveResolution +import Mathlib.CategoryTheory.Preadditive.Injective.Basic +import Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties +import Mathlib.CategoryTheory.Preadditive.Injective.Resolution import Mathlib.CategoryTheory.Preadditive.LeftExact import Mathlib.CategoryTheory.Preadditive.Mat import Mathlib.CategoryTheory.Preadditive.OfBiproducts import Mathlib.CategoryTheory.Preadditive.Opposite -import Mathlib.CategoryTheory.Preadditive.Projective -import Mathlib.CategoryTheory.Preadditive.ProjectiveResolution +import Mathlib.CategoryTheory.Preadditive.Projective.Basic +import Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties +import Mathlib.CategoryTheory.Preadditive.Projective.Resolution import Mathlib.CategoryTheory.Preadditive.Schur import Mathlib.CategoryTheory.Preadditive.SingleObj import Mathlib.CategoryTheory.Preadditive.Transfer diff --git a/Mathlib/Algebra/Category/Grp/Injective.lean b/Mathlib/Algebra/Category/Grp/Injective.lean index fe5d86dc6079f..84a8a2b1a1db0 100644 --- a/Mathlib/Algebra/Category/Grp/Injective.lean +++ b/Mathlib/Algebra/Category/Grp/Injective.lean @@ -7,7 +7,7 @@ import Mathlib.Algebra.Category.ModuleCat.EpiMono import Mathlib.Algebra.Category.Grp.ZModuleEquivalence import Mathlib.Algebra.EuclideanDomain.Int import Mathlib.Algebra.Category.ModuleCat.Injective -import Mathlib.CategoryTheory.Preadditive.Injective +import Mathlib.CategoryTheory.Preadditive.Injective.Basic import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.Topology.Instances.AddCircle diff --git a/Mathlib/Algebra/Category/ModuleCat/Injective.lean b/Mathlib/Algebra/Category/ModuleCat/Injective.lean index e11b9d7185a1f..a0e3547845f39 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Injective.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Injective.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jujian Zhang -/ import Mathlib.Algebra.Module.Injective -import Mathlib.CategoryTheory.Preadditive.Injective +import Mathlib.CategoryTheory.Preadditive.Injective.Basic import Mathlib.Algebra.Category.ModuleCat.EpiMono /-! diff --git a/Mathlib/Algebra/Category/ModuleCat/Projective.lean b/Mathlib/Algebra/Category/ModuleCat/Projective.lean index b8dabad8c1093..bea83a3f94f6b 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Projective.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Projective.lean @@ -5,7 +5,7 @@ Authors: Markus Himmel, Kim Morrison -/ import Mathlib.Algebra.Category.ModuleCat.EpiMono import Mathlib.Algebra.Module.Projective -import Mathlib.CategoryTheory.Preadditive.Projective +import Mathlib.CategoryTheory.Preadditive.Projective.Basic import Mathlib.Data.Finsupp.SMul import Mathlib.LinearAlgebra.Finsupp.VectorSpace diff --git a/Mathlib/Algebra/Homology/ShortComplex/Exact.lean b/Mathlib/Algebra/Homology/ShortComplex/Exact.lean index 7b7ba4b2c4b1b..102b74b572c93 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/Exact.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/Exact.lean @@ -8,7 +8,7 @@ import Mathlib.Algebra.Homology.ShortComplex.Abelian import Mathlib.Algebra.Homology.ShortComplex.QuasiIso import Mathlib.CategoryTheory.Abelian.Opposite import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor -import Mathlib.CategoryTheory.Preadditive.Injective +import Mathlib.CategoryTheory.Preadditive.Injective.Basic /-! # Exact short complexes diff --git a/Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean b/Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean index ede79c322f850..d1c5e0307a8a6 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ import Mathlib.Algebra.Homology.ShortComplex.Exact -import Mathlib.CategoryTheory.Preadditive.Injective +import Mathlib.CategoryTheory.Preadditive.Injective.Basic /-! # Short exact short complexes diff --git a/Mathlib/CategoryTheory/Abelian/Ext.lean b/Mathlib/CategoryTheory/Abelian/Ext.lean index 16fc11a38e93a..6233dac9ee55f 100644 --- a/Mathlib/CategoryTheory/Abelian/Ext.lean +++ b/Mathlib/CategoryTheory/Abelian/Ext.lean @@ -7,7 +7,7 @@ import Mathlib.Algebra.Category.ModuleCat.Abelian import Mathlib.Algebra.Homology.Opposite import Mathlib.CategoryTheory.Abelian.LeftDerived import Mathlib.CategoryTheory.Abelian.Opposite -import Mathlib.CategoryTheory.Abelian.ProjectiveResolution +import Mathlib.CategoryTheory.Abelian.Projective.Resolution import Mathlib.CategoryTheory.Linear.Yoneda /-! diff --git a/Mathlib/CategoryTheory/Abelian/Injective.lean b/Mathlib/CategoryTheory/Abelian/Injective/Basic.lean similarity index 96% rename from Mathlib/CategoryTheory/Abelian/Injective.lean rename to Mathlib/CategoryTheory/Abelian/Injective/Basic.lean index b03c8db8b549c..5df5121b4d04f 100644 --- a/Mathlib/CategoryTheory/Abelian/Injective.lean +++ b/Mathlib/CategoryTheory/Abelian/Injective/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jakob von Raumer -/ import Mathlib.CategoryTheory.Abelian.Exact -import Mathlib.CategoryTheory.Preadditive.Injective +import Mathlib.CategoryTheory.Preadditive.Injective.Basic import Mathlib.CategoryTheory.Preadditive.Yoneda.Limits import Mathlib.CategoryTheory.Preadditive.Yoneda.Injective import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor diff --git a/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean b/Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean similarity index 99% rename from Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean rename to Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean index dac1bafa0aea2..53d6753f1f508 100644 --- a/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean +++ b/Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Jujian Zhang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jujian Zhang, Kim Morrison -/ -import Mathlib.CategoryTheory.Preadditive.InjectiveResolution +import Mathlib.CategoryTheory.Preadditive.Injective.Resolution import Mathlib.Algebra.Homology.HomotopyCategory import Mathlib.Data.Set.Subsingleton import Mathlib.Tactic.AdaptationNote diff --git a/Mathlib/CategoryTheory/Abelian/LeftDerived.lean b/Mathlib/CategoryTheory/Abelian/LeftDerived.lean index f9333349b110b..4894457f5170d 100644 --- a/Mathlib/CategoryTheory/Abelian/LeftDerived.lean +++ b/Mathlib/CategoryTheory/Abelian/LeftDerived.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kim Morrison, Riccardo Brasca, Adam Topaz, Jujian Zhang, Joël Riou -/ import Mathlib.Algebra.Homology.Additive -import Mathlib.CategoryTheory.Abelian.ProjectiveResolution +import Mathlib.CategoryTheory.Abelian.Projective.Resolution /-! # Left-derived functors diff --git a/Mathlib/CategoryTheory/Abelian/Projective.lean b/Mathlib/CategoryTheory/Abelian/Projective/Basic.lean similarity index 100% rename from Mathlib/CategoryTheory/Abelian/Projective.lean rename to Mathlib/CategoryTheory/Abelian/Projective/Basic.lean diff --git a/Mathlib/CategoryTheory/Abelian/ProjectiveDimension.lean b/Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean similarity index 100% rename from Mathlib/CategoryTheory/Abelian/ProjectiveDimension.lean rename to Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean diff --git a/Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean b/Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean similarity index 99% rename from Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean rename to Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean index b46ed6087d1b3..7836ab35befa8 100644 --- a/Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean +++ b/Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Jujian Zhang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel, Kim Morrison, Jakob von Raumer, Joël Riou -/ -import Mathlib.CategoryTheory.Preadditive.ProjectiveResolution +import Mathlib.CategoryTheory.Preadditive.Projective.Resolution import Mathlib.Algebra.Homology.HomotopyCategory import Mathlib.Tactic.SuppressCompilation diff --git a/Mathlib/CategoryTheory/Abelian/RightDerived.lean b/Mathlib/CategoryTheory/Abelian/RightDerived.lean index 8cf24315d8930..838ef0c925eef 100644 --- a/Mathlib/CategoryTheory/Abelian/RightDerived.lean +++ b/Mathlib/CategoryTheory/Abelian/RightDerived.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jujian Zhang, Kim Morrison, Joël Riou -/ import Mathlib.Algebra.Homology.Additive -import Mathlib.CategoryTheory.Abelian.InjectiveResolution +import Mathlib.CategoryTheory.Abelian.Injective.Resolution /-! # Right-derived functors diff --git a/Mathlib/CategoryTheory/Abelian/Yoneda.lean b/Mathlib/CategoryTheory/Abelian/Yoneda.lean index 82251e1797304..834fbf9d08460 100644 --- a/Mathlib/CategoryTheory/Abelian/Yoneda.lean +++ b/Mathlib/CategoryTheory/Abelian/Yoneda.lean @@ -5,7 +5,7 @@ Authors: Markus Himmel -/ import Mathlib.Algebra.Category.Grp.Abelian import Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four -import Mathlib.CategoryTheory.Abelian.Projective +import Mathlib.CategoryTheory.Abelian.Projective.Basic import Mathlib.CategoryTheory.Generator.Preadditive import Mathlib.CategoryTheory.Limits.Preserves.Opposites diff --git a/Mathlib/CategoryTheory/Generator/Abelian.lean b/Mathlib/CategoryTheory/Generator/Abelian.lean index 30b9e3f6febbc..a4ebb9ef111a3 100644 --- a/Mathlib/CategoryTheory/Generator/Abelian.lean +++ b/Mathlib/CategoryTheory/Generator/Abelian.lean @@ -5,7 +5,7 @@ Authors: Markus Himmel -/ import Mathlib.CategoryTheory.Abelian.Subobject import Mathlib.CategoryTheory.Limits.EssentiallySmall -import Mathlib.CategoryTheory.Preadditive.Injective +import Mathlib.CategoryTheory.Preadditive.Injective.Basic import Mathlib.CategoryTheory.Generator.Preadditive import Mathlib.CategoryTheory.Abelian.Opposite diff --git a/Mathlib/CategoryTheory/Preadditive/Injective.lean b/Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean similarity index 99% rename from Mathlib/CategoryTheory/Preadditive/Injective.lean rename to Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean index d9ce92c4eef09..377e44904959e 100644 --- a/Mathlib/CategoryTheory/Preadditive/Injective.lean +++ b/Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2022 Jujian Zhang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jujian Zhang, Kevin Buzzard -/ -import Mathlib.CategoryTheory.Preadditive.Projective +import Mathlib.CategoryTheory.Preadditive.Projective.Basic /-! # Injective objects and categories with enough injectives @@ -14,11 +14,7 @@ An object `J` is injective iff every morphism into `J` can be obtained by extend noncomputable section -open CategoryTheory - -open CategoryTheory.Limits - -open Opposite +open CategoryTheory Limits Opposite universe v v₁ v₂ u₁ u₂ diff --git a/Mathlib/CategoryTheory/Preadditive/Injective/LiftingProperties.lean b/Mathlib/CategoryTheory/Preadditive/Injective/LiftingProperties.lean new file mode 100644 index 0000000000000..8a3df179f793f --- /dev/null +++ b/Mathlib/CategoryTheory/Preadditive/Injective/LiftingProperties.lean @@ -0,0 +1,60 @@ +/- +Copyright (c) 2025 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.Preadditive.Injective.Basic +import Mathlib.CategoryTheory.MorphismProperty.LiftingProperty + +/-! +# Characterization of injective objects in terms of lifting properties + +An object `I` is injective iff the morphism `I ⟶ 0` has the +right lifting property with respect to monomorphisms, +`injective_iff_rlp_monomorphisms_zero`. + +-/ + +universe v u + +namespace CategoryTheory + +open Limits ZeroObject + +variable {C : Type u} [Category.{v} C] + +namespace Injective + +lemma hasLiftingProperty_of_isZero + {A B I Z : C} (i : A ⟶ B) [Mono i] [Injective I] (p : I ⟶ Z) (hZ : IsZero Z) : + HasLiftingProperty i p where + sq_hasLift {f g} sq := ⟨⟨{ + l := Injective.factorThru f i + fac_right := hZ.eq_of_tgt _ _ }⟩⟩ + +instance {A B I : C} (i : A ⟶ B) [Mono i] [Injective I] [HasZeroObject C] (p : I ⟶ 0) : + HasLiftingProperty i (p : I ⟶ 0) := + Injective.hasLiftingProperty_of_isZero i p (isZero_zero C) + +end Injective + +lemma injective_iff_rlp_monomorphisms_of_isZero + [HasZeroMorphisms C] {I Z : C} (p : I ⟶ Z) (hZ : IsZero Z) : + Injective I ↔ (MorphismProperty.monomorphisms C).rlp p := by + obtain rfl := hZ.eq_of_tgt p 0 + constructor + · intro _ A B i (_ : Mono i) + exact Injective.hasLiftingProperty_of_isZero i 0 hZ + · intro h + constructor + intro A B f i hi + have := h _ hi + have sq : CommSq f i (0 : I ⟶ Z) 0 := ⟨by simp⟩ + exact ⟨sq.lift, by simp⟩ + +lemma injective_iff_rlp_monomorphisms_zero + [HasZeroMorphisms C] [HasZeroObject C] (I : C) : + Injective I ↔ (MorphismProperty.monomorphisms C).rlp (0 : I ⟶ 0) := + injective_iff_rlp_monomorphisms_of_isZero _ (isZero_zero C) + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/Preadditive/InjectiveResolution.lean b/Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean similarity index 98% rename from Mathlib/CategoryTheory/Preadditive/InjectiveResolution.lean rename to Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean index 0416818a8fec6..ad3484b6f8c2d 100644 --- a/Mathlib/CategoryTheory/Preadditive/InjectiveResolution.lean +++ b/Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean @@ -6,7 +6,7 @@ Authors: Jujian Zhang, Kim Morrison, Joël Riou import Mathlib.Algebra.Homology.QuasiIso import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex import Mathlib.Algebra.Homology.SingleHomology -import Mathlib.CategoryTheory.Preadditive.Injective +import Mathlib.CategoryTheory.Preadditive.Injective.Basic /-! # Injective resolutions diff --git a/Mathlib/CategoryTheory/Preadditive/Projective.lean b/Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean similarity index 100% rename from Mathlib/CategoryTheory/Preadditive/Projective.lean rename to Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean diff --git a/Mathlib/CategoryTheory/Preadditive/Projective/LiftingProperties.lean b/Mathlib/CategoryTheory/Preadditive/Projective/LiftingProperties.lean new file mode 100644 index 0000000000000..746d825685a9a --- /dev/null +++ b/Mathlib/CategoryTheory/Preadditive/Projective/LiftingProperties.lean @@ -0,0 +1,60 @@ +/- +Copyright (c) 2025 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.Preadditive.Projective.Basic +import Mathlib.CategoryTheory.MorphismProperty.LiftingProperty + +/-! +# Characterization of projective objects in terms of lifting properties + +An object `P` is projective iff the morphism `0 ⟶ P` has the +left lifting property with respect to epimorphisms, +`projective_iff_llp_epimorphisms_zero`. + +-/ + +universe v u + +namespace CategoryTheory + +open Limits ZeroObject + +variable {C : Type u} [Category.{v} C] + +namespace Projective + +lemma hasLiftingProperty_of_isZero + {Z P X Y : C} (i : Z ⟶ P) (p : X ⟶ Y) [Epi p] [Projective P] (hZ : IsZero Z) : + HasLiftingProperty i p where + sq_hasLift {f g} sq := ⟨⟨{ + l := Projective.factorThru g p + fac_left := hZ.eq_of_src _ _ }⟩⟩ + +instance {X Y P : C} (p : X ⟶ Y) [Epi p] [Projective P] [HasZeroObject C] (i : 0 ⟶ P) : + HasLiftingProperty (i : 0 ⟶ P) p := + Projective.hasLiftingProperty_of_isZero i p (isZero_zero C) + +end Projective + +lemma projective_iff_llp_epimorphisms_of_isZero + [HasZeroMorphisms C] {P Z : C} (i : Z ⟶ P) (hZ : IsZero Z) : + Projective P ↔ (MorphismProperty.epimorphisms C).llp i := by + obtain rfl := hZ.eq_of_src i 0 + constructor + · intro _ X Y p (_ : Epi p) + exact Projective.hasLiftingProperty_of_isZero 0 p hZ + · intro h + constructor + intro X Y f p hp + have := h _ hp + have sq : CommSq 0 (0 : Z ⟶ P) p f := ⟨by simp⟩ + exact ⟨sq.lift, by simp⟩ + +lemma projective_iff_llp_epimorphisms_zero + [HasZeroMorphisms C] [HasZeroObject C] (P : C) : + Projective P ↔ (MorphismProperty.epimorphisms C).llp (0 : 0 ⟶ P) := + projective_iff_llp_epimorphisms_of_isZero _ (isZero_zero C) + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/Preadditive/ProjectiveResolution.lean b/Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean similarity index 100% rename from Mathlib/CategoryTheory/Preadditive/ProjectiveResolution.lean rename to Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean diff --git a/Mathlib/CategoryTheory/Preadditive/Yoneda/Injective.lean b/Mathlib/CategoryTheory/Preadditive/Yoneda/Injective.lean index 778a344fe5bbd..cb798437b70be 100644 --- a/Mathlib/CategoryTheory/Preadditive/Yoneda/Injective.lean +++ b/Mathlib/CategoryTheory/Preadditive/Yoneda/Injective.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel, Kim Morrison -/ import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic -import Mathlib.CategoryTheory.Preadditive.Injective +import Mathlib.CategoryTheory.Preadditive.Injective.Basic import Mathlib.Algebra.Category.Grp.EpiMono import Mathlib.Algebra.Category.ModuleCat.EpiMono diff --git a/Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.lean b/Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.lean index 6aea2be588fcd..25dcf13585285 100644 --- a/Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.lean +++ b/Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel, Kim Morrison -/ import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic -import Mathlib.CategoryTheory.Preadditive.Projective +import Mathlib.CategoryTheory.Preadditive.Projective.Basic import Mathlib.Algebra.Category.Grp.EpiMono import Mathlib.Algebra.Category.ModuleCat.EpiMono diff --git a/Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean b/Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean index 6f256af4b50c6..c3328dccf5996 100644 --- a/Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean +++ b/Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean @@ -5,7 +5,7 @@ Authors: Dagur Asgeirsson, Filippo A. E. Nuccio, Riccardo Brasca -/ import Mathlib.CategoryTheory.EffectiveEpi.Preserves import Mathlib.CategoryTheory.Limits.Final.ParallelPair -import Mathlib.CategoryTheory.Preadditive.Projective +import Mathlib.CategoryTheory.Preadditive.Projective.Basic import Mathlib.CategoryTheory.Sites.Canonical import Mathlib.CategoryTheory.Sites.Coherent.Basic import Mathlib.CategoryTheory.Sites.EffectiveEpimorphic diff --git a/Mathlib/Topology/Category/CompHaus/Projective.lean b/Mathlib/Topology/Category/CompHaus/Projective.lean index e891c0742ab6c..41b58a161ee2e 100644 --- a/Mathlib/Topology/Category/CompHaus/Projective.lean +++ b/Mathlib/Topology/Category/CompHaus/Projective.lean @@ -5,7 +5,7 @@ Authors: Johan Commelin -/ import Mathlib.Topology.Category.CompHaus.Basic import Mathlib.Topology.StoneCech -import Mathlib.CategoryTheory.Preadditive.Projective +import Mathlib.CategoryTheory.Preadditive.Projective.Basic import Mathlib.CategoryTheory.ConcreteCategory.EpiMono /-! diff --git a/Mathlib/Topology/Category/Profinite/Projective.lean b/Mathlib/Topology/Category/Profinite/Projective.lean index c15935e8aa672..0b77652c50502 100644 --- a/Mathlib/Topology/Category/Profinite/Projective.lean +++ b/Mathlib/Topology/Category/Profinite/Projective.lean @@ -5,7 +5,7 @@ Authors: Johan Commelin -/ import Mathlib.Topology.Category.Profinite.Basic import Mathlib.Topology.StoneCech -import Mathlib.CategoryTheory.Preadditive.Projective +import Mathlib.CategoryTheory.Preadditive.Projective.Basic import Mathlib.CategoryTheory.ConcreteCategory.EpiMono /-!