Weak kernels

These are weak equalizers for functors of the form parallelPair f 0.

If the category is preadditive, then weak equalizers exist if and only if weak kernels exist. (See hasWeakEqualizer_of_hasWeakKernel and hasWeakKernel_of_hasWeakEqualizer.)

@[reducible, inline]

abbrev CategoryTheory.Limits.HasWeakKernel {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) : Prop

A morphism f has a weak kernel if the functor ParallelPair f 0 has a weak limit.

Equations

• CategoryTheory.Limits.HasWeakKernel f = CategoryTheory.Limits.HasWeakLimit (CategoryTheory.Limits.parallelPair f 0)

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

HasWeakKernels represents the existence of weak kernels for every morphism.

• hasWeakLimit {X Y : C} (f : X ⟶ Y) : HasWeakKernel f

@[instance 100]

instance CategoryTheory.Limits.HasWeakKernelsOfHasKernels {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] [HasKernels C] : HasWeakKernels C

If a category has kernels, then it has weak kernels.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakKernel {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasWeakKernel f] : C

The weak kernel of a morphism.

Equations

• CategoryTheory.Limits.weakKernel f = CategoryTheory.Limits.weakEqualizer f 0

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakKernel.ι {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasWeakKernel f] : weakKernel f ⟶ X

The map from weakKernel f into the source of f.

Equations

• CategoryTheory.Limits.weakKernel.ι f = CategoryTheory.Limits.weakEqualizer.ι f 0

@[simp]

theorem CategoryTheory.Limits.weakEqualizer_as_weakKernel {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasWeakKernel f] : weakEqualizer.ι f 0 = weakKernel.ι f

@[simp]

theorem CategoryTheory.Limits.weakKernel.condition {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasWeakKernel f] : CategoryStruct.comp (ι f) f = 0

@[simp]

theorem CategoryTheory.Limits.weakKernel.condition_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasWeakKernel f] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (ι f) (CategoryStruct.comp f h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Limits.weakKernelIsWeakKernel {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasWeakKernel f] : IsWeakLimit (Fork.ofι (weakKernel.ι f) ⋯)

The weak kernel built from weakKernel.ι f is weakly limiting.

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakKernel.lift {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasWeakKernel f] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = 0) : W ⟶ weakKernel f

Given any morphism k : W ⟶ X satisfying k ≫ f = 0, k factors through weakKernel.ι f via weakKernel.lift : W ⟶ weakKernel f.

Equations

• CategoryTheory.Limits.weakKernel.lift f k h = (CategoryTheory.Limits.weakKernelIsWeakKernel f).lift (CategoryTheory.Limits.KernelFork.ofι k h)

@[simp]

theorem CategoryTheory.Limits.weakKernel.lift_ι {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasWeakKernel f] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = 0) : CategoryStruct.comp (lift f k h) (ι f) = k

@[simp]

theorem CategoryTheory.Limits.weakKernel.lift_ι_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasWeakKernel f] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = 0) {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp (lift f k h) (CategoryStruct.comp (ι f) h✝) = CategoryStruct.comp k h✝

noncomputable def CategoryTheory.Limits.weakKernel.lift' {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasWeakKernel f] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = 0) : { l : W ⟶ weakKernel f // CategoryStruct.comp l (ι f) = k }

Any morphism k : W ⟶ X satisfying k ≫ f = 0 induces a morphism l : W ⟶ weakKernel f such that l ≫ weakKernel.ι f = k.

Equations

• CategoryTheory.Limits.weakKernel.lift' f k h = ⟨CategoryTheory.Limits.weakKernel.lift f k h, ⋯⟩

def CategoryTheory.Preadditive.isWeakLimitForkOfKernelFork {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : Limits.KernelFork (f - g)} (i : Limits.IsWeakLimit c) : Limits.IsWeakLimit (forkOfKernelFork c)

A weak kernel of f - g is a weak equalizer of f and g.

Equations

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

@[simp]

theorem CategoryTheory.Preadditive.isWeakLimitForkOfKernelFork_lift {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : Limits.KernelFork (f - g)} (i : Limits.IsWeakLimit c) (s : Limits.Fork f g) : (isWeakLimitForkOfKernelFork i).lift s = i.lift (kernelForkOfFork s)

def CategoryTheory.Preadditive.isWeakLimitKernelForkOfFork {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} {f g : X ⟶ Y} {c : Limits.Fork f g} (i : Limits.IsWeakLimit c) : Limits.IsWeakLimit (kernelForkOfFork c)

A weak equalizer of f and g is a weak kernel of f - g.

Equations

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

theorem CategoryTheory.Preadditive.hasWeakEqualizer_of_hasWeakKernel {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} (f g : X ⟶ Y) [Limits.HasWeakKernel (f - g)] : Limits.HasWeakEqualizer f g

A preadditive category has a weak equalizer for f and g if it has a weak kernel for f - g.

theorem CategoryTheory.Preadditive.hasWeakKernel_of_hasWeakEqualizer {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} (f g : X ⟶ Y) [Limits.HasWeakEqualizer f g] : Limits.HasWeakKernel (f - g)

A preadditive category has a weak kernel for f - g if it has a weak equalizer for f and g.

theorem CategoryTheory.Preadditive.hasWeakEqualizers_of_hasWeakKernels {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [Limits.HasWeakKernels C] : Limits.HasWeakEqualizers C

If a preadditive category has all weak kernels, then it also has all weak equalizers.