# mathlib3documentation

category_theory.limits.shapes.kernel_pair

# Kernel pairs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 is_limit (pullback_cone.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]
def category_theory.is_kernel_pair {C : Type u} {R X Y : C} (f : X Y) (a b : R X) :
Prop

is_kernel_pair 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 is_pullback a b f f.

@[protected, instance]
def category_theory.is_kernel_pair.subsingleton {C : Type u} {R X Y : C} (f : X Y) (a b : R X) :

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

theorem category_theory.is_kernel_pair.id_of_mono {C : Type u} {X Y : C} (f : X Y)  :
(𝟙 X)

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

@[protected, instance]
def category_theory.is_kernel_pair.inhabited {C : Type u} {X Y : C} (f : X Y)  :
Equations
noncomputable def category_theory.is_kernel_pair.lift' {C : Type u} {R X Y : C} {f : X Y} {a b : R X} {S : C} (k : b) (p q : S X) (w : p f = q f) :
{t // t a = p t b = q}

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

Equations
theorem category_theory.is_kernel_pair.cancel_right {C : Type u} {R X Y Z : C} {a b : R X} {f₁ : X Y} {f₂ : Y Z} (comm : a f₁ = b f₁) (big_k : category_theory.is_kernel_pair (f₁ f₂) a b) :

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 category_theory.is_kernel_pair.cancel_right_of_mono {C : Type u} {R X Y Z : C} {a b : R X} {f₁ : X Y} {f₂ : Y Z} (big_k : category_theory.is_kernel_pair (f₁ f₂) a b) :

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 category_theory.is_kernel_pair.comp_of_mono {C : Type u} {R X Y Z : C} {a b : R X} {f₁ : X Y} {f₂ : Y Z} (small_k : b) :

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 category_theory.is_kernel_pair.to_coequalizer {C : Type u} {R X Y : C} {f : X Y} {a b : R X} (k : b)  :

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
@[protected]
theorem category_theory.is_kernel_pair.pullback {C : Type u} {X Y Z A : C} {g : Y Z} {a₁ a₂ : A Y} (h : a₂) (f : X Z) [ (a₁ g)] :
(a₁ g) f g (𝟙 X) a₁ (𝟙 Z) _ _) (a₁ g) f g (𝟙 X) a₂ (𝟙 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 category_theory.is_kernel_pair.mono_of_is_iso_fst {C : Type u} {R X Y : C} {f : X Y} {a b : R X} (h : b)  :
theorem category_theory.is_kernel_pair.is_iso_of_mono {C : Type u} {R X Y : C} {f : X Y} {a b : R X} (h : b)  :
theorem category_theory.is_kernel_pair.of_is_iso_of_mono {C : Type u} {R X Y : C} {f : X Y} {a : R X}  :