Kernel pairs #

This file defines what it means for a parallel pair of morphisms a b : R ⟶ X to be the kernel pair for a morphism f. Some properties of kernel pairs are given, namely allowing one to transfer between the kernel pair of f₁ ≫ f₂ to the kernel pair of f₁. It is also proved that if f is a coequalizer of some pair, and a,b is a kernel pair for f then it is a coequalizer of a,b.

Implementation #

The definition is essentially just a wrapper for IsLimit (PullbackCone.mk _ _ _), but the constructions given here are useful, yet awkward to present in that language, so a basic API is developed here.

TODO #

• Internal equivalence relations (or congruences) and the fact that every kernel pair induces one, and the converse in an effective regular category (WIP by b-mehta).
@[reducible, inline]
abbrev CategoryTheory.IsKernelPair {C : Type u} {R : C} {X : C} {Y : C} (f : X Y) (a : R X) (b : R X) :

IsKernelPair f a b expresses that (a, b) is a kernel pair for f, i.e. a ≫ f = b ≫ f and the square R → X ↓ ↓ X → Y is a pullback square. This is just an abbreviation for IsPullback a b f f.

Equations
Instances For
instance CategoryTheory.IsKernelPair.instSubsingleton {C : Type u} {R : C} {X : C} {Y : C} (f : X Y) (a : R X) (b : R X) :

The data expressing that (a, b) is a kernel pair is subsingleton.

Equations
• =
theorem CategoryTheory.IsKernelPair.id_of_mono {C : Type u} {X : C} {Y : C} (f : X Y) :

If f is a monomorphism, then (𝟙 _, 𝟙 _) is a kernel pair for f.

instance CategoryTheory.IsKernelPair.instInhabitedIdOfMono {C : Type u} {X : C} {Y : C} (f : X Y) :
Equations
• = { default := }
noncomputable def CategoryTheory.IsKernelPair.lift {C : Type u} {R : C} {X : C} {Y : C} {f : X Y} {a : R X} {b : R X} {S : C} (k : ) (p : S X) (q : S X) :
S R

Given a pair of morphisms p, q to X which factor through f, they factor through any kernel pair of f.

Equations
• k.lift p q w =
Instances For
@[simp]
theorem CategoryTheory.IsKernelPair.lift_fst_assoc {C : Type u} {R : C} {X : C} {Y : C} {f : X Y} {a : R X} {b : R X} {S : C} (k : ) (p : S X) (q : S X) {Z : C} (h : X Z) :
@[simp]
theorem CategoryTheory.IsKernelPair.lift_fst {C : Type u} {R : C} {X : C} {Y : C} {f : X Y} {a : R X} {b : R X} {S : C} (k : ) (p : S X) (q : S X) :
@[simp]
theorem CategoryTheory.IsKernelPair.lift_snd_assoc {C : Type u} {R : C} {X : C} {Y : C} {f : X Y} {a : R X} {b : R X} {S : C} (k : ) (p : S X) (q : S X) {Z : C} (h : X Z) :
@[simp]
theorem CategoryTheory.IsKernelPair.lift_snd {C : Type u} {R : C} {X : C} {Y : C} {f : X Y} {a : R X} {b : R X} {S : C} (k : ) (p : S X) (q : S X) :
noncomputable def CategoryTheory.IsKernelPair.lift' {C : Type u} {R : C} {X : C} {Y : C} {f : X Y} {a : R X} {b : R X} {S : C} (k : ) (p : S X) (q : S X) :
{ t : S R // }

Given a pair of morphisms p, q to X which factor through f, they factor through any kernel pair of f.

Equations
• k.lift' p q w = k.lift p q w,
Instances For
theorem CategoryTheory.IsKernelPair.cancel_right {C : Type u} {R : C} {X : C} {Y : C} {Z : C} {a : R X} {b : R X} {f₁ : X Y} {f₂ : Y Z} (comm : ) (big_k : ) :

If (a,b) is a kernel pair for f₁ ≫ f₂ and a ≫ f₁ = b ≫ f₁, then (a,b) is a kernel pair for just f₁. That is, to show that (a,b) is a kernel pair for f₁ it suffices to only show the square commutes, rather than to additionally show it's a pullback.

theorem CategoryTheory.IsKernelPair.cancel_right_of_mono {C : Type u} {R : C} {X : C} {Y : C} {Z : C} {a : R X} {b : R X} {f₁ : X Y} {f₂ : Y Z} [] (big_k : ) :

If (a,b) is a kernel pair for f₁ ≫ f₂ and f₂ is mono, then (a,b) is a kernel pair for just f₁. The converse of comp_of_mono.

theorem CategoryTheory.IsKernelPair.comp_of_mono {C : Type u} {R : C} {X : C} {Y : C} {Z : C} {a : R X} {b : R X} {f₁ : X Y} {f₂ : Y Z} [] (small_k : ) :

If (a,b) is a kernel pair for f₁ and f₂ is mono, then (a,b) is a kernel pair for f₁ ≫ f₂. The converse of cancel_right_of_mono.

def CategoryTheory.IsKernelPair.toCoequalizer {C : Type u} {R : C} {X : C} {Y : C} {f : X Y} {a : R X} {b : R X} (k : ) [r : ] :

If (a,b) is the kernel pair of f, and f is a coequalizer morphism for some parallel pair, then f is a coequalizer morphism of a and b.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.IsKernelPair.pullback {C : Type u} {X : C} {Y : C} {Z : C} {A : C} {g : Y Z} {a₁ : A Y} {a₂ : A Y} (h : ) (f : X Z) :

If a₁ a₂ : A ⟶ Y is a kernel pair for g : Y ⟶ Z, then a₁ ×[Z] X and a₂ ×[Z] X (A ×[Z] X ⟶ Y ×[Z] X) is a kernel pair for Y ×[Z] X ⟶ X.

theorem CategoryTheory.IsKernelPair.mono_of_isIso_fst {C : Type u} {R : C} {X : C} {Y : C} {f : X Y} {a : R X} {b : R X} (h : ) :
theorem CategoryTheory.IsKernelPair.isIso_of_mono {C : Type u} {R : C} {X : C} {Y : C} {f : X Y} {a : R X} {b : R X} (h : ) :
theorem CategoryTheory.IsKernelPair.of_isIso_of_mono {C : Type u} {R : C} {X : C} {Y : C} {f : X Y} {a : R X} :