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 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).

source

structure category_theory.is_kernel_pair {C : Type u} [category_theory.category C] {R X Y : C} (f : X ⟶ Y) (a b : R ⟶ X) :

Type (max u v)

comm : a ≫ f = b ≫ f
is_limit : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk a b _)

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 essentially just a convenience wrapper over is_limit (pullback_cone.mk _ _ _).

Instances for category_theory.is_kernel_pair

category_theory.is_kernel_pair.has_sizeof_inst
category_theory.is_kernel_pair.subsingleton
category_theory.is_kernel_pair.inhabited

source

theorem category_theory.is_kernel_pair.comm_assoc {C : Type u} [category_theory.category C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} (self : category_theory.is_kernel_pair f a b) {X' : C} (f' : Y ⟶ X') :

a ≫ f ≫ f' = b ≫ f ≫ f'

source

@[protected, instance]

def category_theory.is_kernel_pair.subsingleton {C : Type u} [category_theory.category C] {R X Y : C} (f : X ⟶ Y) (a b : R ⟶ X) :

subsingleton (category_theory.is_kernel_pair f a b)

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

source

def category_theory.is_kernel_pair.id_of_mono {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

category_theory.is_kernel_pair f (𝟙 X) (𝟙 X)

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

Equations

category_theory.is_kernel_pair.id_of_mono f = {comm := _, is_limit := category_theory.limits.pullback_cone.is_limit_mk_id_id f _inst_2}

source

@[protected, instance]

def category_theory.is_kernel_pair.inhabited {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

inhabited (category_theory.is_kernel_pair f (𝟙 X) (𝟙 X))

Equations

category_theory.is_kernel_pair.inhabited f = {default := category_theory.is_kernel_pair.id_of_mono f _inst_2}

source

def category_theory.is_kernel_pair.lift' {C : Type u} [category_theory.category C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C} (k : category_theory.is_kernel_pair f a 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

k.lift' p q w = category_theory.limits.pullback_cone.is_limit.lift' k.is_limit p q w

source

def category_theory.is_kernel_pair.cancel_right {C : Type u} [category_theory.category C] {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) :

category_theory.is_kernel_pair 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.

Equations

category_theory.is_kernel_pair.cancel_right comm big_k = {comm := comm, is_limit := (category_theory.limits.pullback_cone.mk a b comm).is_limit_aux' (λ (s : category_theory.limits.pullback_cone f₁ f₁), let s' : category_theory.limits.pullback_cone (f₁ ≫ f₂) (f₁ ≫ f₂) := category_theory.limits.pullback_cone.mk s.fst s.snd _ in ⟨big_k.is_limit.lift s', _⟩)}

source

def category_theory.is_kernel_pair.cancel_right_of_mono {C : Type u} [category_theory.category C] {R X Y Z : C} {a b : R ⟶ X} {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z} [category_theory.mono f₂] (big_k : category_theory.is_kernel_pair (f₁ ≫ f₂) a b) :

category_theory.is_kernel_pair 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.

Equations

big_k.cancel_right_of_mono = category_theory.is_kernel_pair.cancel_right _ big_k

source

def category_theory.is_kernel_pair.comp_of_mono {C : Type u} [category_theory.category C] {R X Y Z : C} {a b : R ⟶ X} {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z} [category_theory.mono f₂] (small_k : category_theory.is_kernel_pair f₁ a b) :

category_theory.is_kernel_pair (f₁ ≫ f₂) a 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.

Equations

small_k.comp_of_mono = {comm := _, is_limit := (category_theory.limits.pullback_cone.mk a b _).is_limit_aux' (λ (s : category_theory.limits.pullback_cone (f₁ ≫ f₂) (f₁ ≫ f₂)), ⟨(category_theory.limits.pullback_cone.is_limit.lift' small_k.is_limit s.fst s.snd _).val, _⟩)}

source

def category_theory.is_kernel_pair.to_coequalizer {C : Type u} [category_theory.category C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} (k : category_theory.is_kernel_pair f a b) [r : category_theory.regular_epi f] :

category_theory.limits.is_colimit (category_theory.limits.cofork.of_π f _)

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

source

@[protected]

noncomputable def category_theory.is_kernel_pair.pullback {C : Type u} [category_theory.category C] {X Y Z A : C} {g : Y ⟶ Z} {a₁ a₂ : A ⟶ Y} (h : category_theory.is_kernel_pair g a₁ a₂) (f : X ⟶ Z) [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback f (a₁ ≫ g)] :

category_theory.is_kernel_pair category_theory.limits.pullback.fst (category_theory.limits.pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) _ category_theory.is_kernel_pair.pullback._proof_2) (category_theory.limits.pullback.map f (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.

Equations

h.pullback f = {comm := _, is_limit := (category_theory.limits.pullback_cone.mk (category_theory.limits.pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) _ category_theory.is_kernel_pair.pullback._proof_6) (category_theory.limits.pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) _ _) _).is_limit_aux' (λ (s : category_theory.limits.pullback_cone category_theory.limits.pullback.fst category_theory.limits.pullback.fst), ⟨category_theory.limits.pullback.lift (s.fst ≫ category_theory.limits.pullback.fst) (h.lift' (s.fst ≫ category_theory.limits.pullback.snd) (s.snd ≫ category_theory.limits.pullback.snd) _).val _, _⟩)}