Pure subobjects

In this file, we define the notion of κ-pure morphisms (IsCardinalPure) in a category C, where κ is a regular cardinal. This class contains split monomorphisms and is stable under κ-filtered colimits. When C is a κ-accessible category, we show that κ-pure morphisms are monomorphisms.

References

• Adámek, J. and Rosický, J., Locally presentable and accessible categories

class CategoryTheory.IsCardinalPure {C : Type u_1} [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] {X Y : C} (f : X ⟶ Y) : Prop

Given a regular cardinal κ, we say that a morphism f : X ⟶ Y is κ-pure if for any commutative square:

      t
 X' -----> Y'
 |         |
l|         |r
 v         v
 X  -----> Y
      f

where X' and Y' are κ-presentable, there exists a morphism ρ : Y' ⟶ X such that t ≫ ρ = l.

• exists_of_commSq {X' Y' : C} {t : X' ⟶ Y'} {l : X' ⟶ X} {r : Y' ⟶ Y} [IsCardinalPresentable X' κ] [IsCardinalPresentable Y' κ] (sq : CommSq t l r f) : ∃ (ρ : Y' ⟶ X), CategoryStruct.comp t ρ = l

@[reducible, inline]

abbrev CategoryTheory.isCardinalPure (C : Type u_1) [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : MorphismProperty C

κ-pure morphisms, as a property of morphisms in a category C.

Equations

• CategoryTheory.isCardinalPure C κ f = CategoryTheory.IsCardinalPure κ f

instance CategoryTheory.instIsCardinalPureOfIsSplitMono {C : Type u_1} [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : IsCardinalPure κ f

instance CategoryTheory.instIsCardinalPureComp {C : Type u_1} [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsCardinalPure κ f] [IsCardinalPure κ g] : IsCardinalPure κ (CategoryStruct.comp f g)

instance CategoryTheory.instIsMultiplicativeIsCardinalPure {C : Type u_1} [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : (isCardinalPure C κ).IsMultiplicative

instance CategoryTheory.instRespectsIsoIsCardinalPure {C : Type u_1} [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : (isCardinalPure C κ).RespectsIso

theorem CategoryTheory.IsCardinalPure.of_postcomp {C : Type u_1} [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsCardinalPure κ (CategoryStruct.comp f g)] : IsCardinalPure κ f

instance CategoryTheory.instHasOfPostcompPropertyIsCardinalPureTopMorphismProperty {C : Type u_1} [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] : (isCardinalPure C κ).HasOfPostcompProperty ⊤

theorem CategoryTheory.IsCardinalAccessibleCategory.mono_iff {C : Type u_1} [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalAccessibleCategory C κ] {X Y : C} (f : X ⟶ Y) : Mono f ↔ ∀ (T : C) [IsCardinalPresentable T κ] (g₁ g₂ : T ⟶ X), CategoryStruct.comp g₁ f = CategoryStruct.comp g₂ f → g₁ = g₂

theorem CategoryTheory.IsCardinalPure.mono {C : Type u_1} [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalAccessibleCategory C κ] {X Y : C} (f : X ⟶ Y) [IsCardinalPure κ f] : Mono f

In a κ-accessible category, κ-pure morphisms are monomorphisms. (This is proposition 2.29 in [AR94].)

theorem CategoryTheory.isCardinalPure_le_monomorphisms (C : Type u_1) [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalAccessibleCategory C κ] : isCardinalPure C κ ≤ MorphismProperty.monomorphisms C

instance CategoryTheory.instIsStableUnderColimitsOfShapeIsCardinalPureOfEssentiallySmallOfIsCardinalFiltered {C : Type u_1} [Category.{v_1, u_1} C] (κ : Cardinal.{w}) [Fact κ.IsRegular] (J : Type u_2) [Category.{v_2, u_2} J] [EssentiallySmall.{w, v_2, u_2} J] [IsCardinalFiltered J κ] : (isCardinalPure C κ).IsStableUnderColimitsOfShape J

κ-pure morphisms are stable under κ-filtered colimits. (This is proposition 2.30 (i) in [AR94].)