Objects that are (co)kernels of morphisms

Given a morphism property W on a category, we introduce two object properties kernels W and cokernels W, consisting of all (co)kernels of morphisms satisfying W.

Given an object property P, we also introduce two predicates P.IsClosedUnderKernels and P.IsClosedUnderCokernels, stating that all (co)kernels of morphisms between objects in P remain in P.

inductive CategoryTheory.MorphismProperty.kernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (W : MorphismProperty C) : ObjectProperty C

The property of objects that are kernels of morphisms satisfying W.

• of_isLimit {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {W : MorphismProperty C} {X₁ X₂ : C} (f : X₁ ⟶ X₂) (k : Limits.KernelFork f) (hk : Limits.IsLimit k) (hf : W f) : W.kernels k.pt

instance CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsKernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (W : MorphismProperty C) : W.kernels.IsClosedUnderIsomorphisms

inductive CategoryTheory.MorphismProperty.cokernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (W : MorphismProperty C) : ObjectProperty C

The property of objects that are cokernels of morphisms satisfying W.

• of_isColimit {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {W : MorphismProperty C} {X₁ X₂ : C} (f : X₁ ⟶ X₂) (k : Limits.CokernelCofork f) (hk : Limits.IsColimit k) (hf : W f) : W.cokernels k.pt

instance CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsCokernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (W : MorphismProperty C) : W.cokernels.IsClosedUnderIsomorphisms

class CategoryTheory.ObjectProperty.IsClosedUnderKernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : Prop

A property of objects satisfies P.IsClosedUnderKernels if whenever X and Y satisfy P, all kernels of morphisms from X to Y satisfy P.

• kernels_le : (MorphismProperty.ofObjectProperty P P).kernels ≤ P

theorem CategoryTheory.ObjectProperty.isClosedUnderKernels_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : P.IsClosedUnderKernels ↔ (MorphismProperty.ofObjectProperty P P).kernels ≤ P

theorem CategoryTheory.ObjectProperty.prop_of_isLimit_kernelFork {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.IsClosedUnderKernels] {X Y : C} {f : X ⟶ Y} {k : Limits.KernelFork f} (hk : Limits.IsLimit k) (hX : P X) (hY : P Y) : P k.pt

theorem CategoryTheory.ObjectProperty.prop_kernel {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.IsClosedUnderKernels] {X Y : C} (f : X ⟶ Y) [Limits.HasKernel f] (hX : P X) (hY : P Y) : P (Limits.kernel f)

instance CategoryTheory.ObjectProperty.instIsClosedUnderKernelsOfIsClosedUnderSubobjects {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.IsClosedUnderSubobjects] : P.IsClosedUnderKernels

theorem CategoryTheory.ObjectProperty.hasLimit_parallelPair_comp_ι {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) {X Y : P.FullSubcategory} (f : X ⟶ Y) [Limits.HasKernel f.hom] : Limits.HasLimit ((Limits.parallelPair f 0).comp P.ι)

@[reducible]

noncomputable def CategoryTheory.ObjectProperty.createsKernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.IsClosedUnderKernels] {X Y : P.FullSubcategory} (f : X ⟶ Y) [Limits.HasKernel f.hom] : CreatesLimit (Limits.parallelPair f 0) P.ι

If an object property P is closed under kernels, then P.ι creates kernels. In particular, this implies P.ι preserves kernels.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.ObjectProperty.instHasKernelsFullSubcategoryOfIsClosedUnderKernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.IsClosedUnderKernels] [Limits.HasKernels C] : Limits.HasKernels P.FullSubcategory

class CategoryTheory.ObjectProperty.IsClosedUnderCokernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : Prop

A property of objects satisfies P.IsClosedUnderCokernels if whenever X and Y satisfy P, all kernels of morphisms from X to Y satisfy P.

• cokernels_le : (MorphismProperty.ofObjectProperty P P).cokernels ≤ P

theorem CategoryTheory.ObjectProperty.isClosedUnderCokernels_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) : P.IsClosedUnderCokernels ↔ (MorphismProperty.ofObjectProperty P P).cokernels ≤ P

theorem CategoryTheory.ObjectProperty.prop_of_isColimit_cokernelCofork {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.IsClosedUnderCokernels] {X Y : C} {f : X ⟶ Y} {k : Limits.CokernelCofork f} (hk : Limits.IsColimit k) (hX : P X) (hY : P Y) : P k.pt

theorem CategoryTheory.ObjectProperty.prop_cokernel {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.IsClosedUnderCokernels] {X Y : C} (f : X ⟶ Y) [Limits.HasCokernel f] (hX : P X) (hY : P Y) : P (Limits.cokernel f)

instance CategoryTheory.ObjectProperty.instIsClosedUnderCokernelsOfIsClosedUnderQuotients {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.IsClosedUnderQuotients] : P.IsClosedUnderCokernels

theorem CategoryTheory.ObjectProperty.hasColimit_parallelPair_comp_ι {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) {X Y : P.FullSubcategory} (f : X ⟶ Y) [Limits.HasCokernel f.hom] : Limits.HasColimit ((Limits.parallelPair f 0).comp P.ι)

@[reducible]

noncomputable def CategoryTheory.ObjectProperty.createsCokernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.IsClosedUnderCokernels] {X Y : P.FullSubcategory} (f : X ⟶ Y) [Limits.HasCokernel f.hom] : CreatesColimit (Limits.parallelPair f 0) P.ι

If an object property P is closed under cokernels, then P.ι creates cokernels. In particular, this implies P.ι preserves cokernels.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.ObjectProperty.instHasCokernelsFullSubcategoryOfIsClosedUnderCokernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.IsClosedUnderCokernels] [Limits.HasCokernels C] : Limits.HasCokernels P.FullSubcategory