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} [Category.{v, u} C] {R X Y : C} (f : X ⟶ Y) (a b : R ⟶ X) : Prop

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

• CategoryTheory.IsKernelPair f a b = CategoryTheory.IsPullback a b f f

instance CategoryTheory.IsKernelPair.instSubsingleton {C : Type u} [Category.{v, u} C] {R X Y : C} (f : X ⟶ Y) (a b : R ⟶ X) : Subsingleton (IsKernelPair f a b)

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

theorem CategoryTheory.IsKernelPair.id_of_mono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : IsKernelPair f (CategoryStruct.id X) (CategoryStruct.id X)

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

instance CategoryTheory.IsKernelPair.instInhabitedIdOfMono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] : Inhabited (IsKernelPair f (CategoryStruct.id X) (CategoryStruct.id X))

Equations

• CategoryTheory.IsKernelPair.instInhabitedIdOfMono f = { default := ⋯ }

noncomputable def CategoryTheory.IsKernelPair.lift {C : Type u} [Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C} (k : IsKernelPair f a b) (p q : S ⟶ X) (w : CategoryStruct.comp p f = CategoryStruct.comp q f) : 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 = CategoryTheory.Limits.PullbackCone.IsLimit.lift (CategoryTheory.IsPullback.isLimit k) p q w

@[simp]

theorem CategoryTheory.IsKernelPair.lift_fst {C : Type u} [Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C} (k : IsKernelPair f a b) (p q : S ⟶ X) (w : CategoryStruct.comp p f = CategoryStruct.comp q f) : CategoryStruct.comp (k.lift p q w) a = p

@[simp]

theorem CategoryTheory.IsKernelPair.lift_fst_assoc {C : Type u} [Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C} (k : IsKernelPair f a b) (p q : S ⟶ X) (w : CategoryStruct.comp p f = CategoryStruct.comp q f) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (k.lift p q w) (CategoryStruct.comp a h) = CategoryStruct.comp p h

@[simp]

theorem CategoryTheory.IsKernelPair.lift_snd {C : Type u} [Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C} (k : IsKernelPair f a b) (p q : S ⟶ X) (w : CategoryStruct.comp p f = CategoryStruct.comp q f) : CategoryStruct.comp (k.lift p q w) b = q

@[simp]

theorem CategoryTheory.IsKernelPair.lift_snd_assoc {C : Type u} [Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C} (k : IsKernelPair f a b) (p q : S ⟶ X) (w : CategoryStruct.comp p f = CategoryStruct.comp q f) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (k.lift p q w) (CategoryStruct.comp b h) = CategoryStruct.comp q h

noncomputable def CategoryTheory.IsKernelPair.lift' {C : Type u} [Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C} (k : IsKernelPair f a b) (p q : S ⟶ X) (w : CategoryStruct.comp p f = CategoryStruct.comp q f) : { t : S ⟶ R // CategoryStruct.comp t a = p ∧ CategoryStruct.comp 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 = ⟨k.lift p q w, ⋯⟩

theorem CategoryTheory.IsKernelPair.cancel_right {C : Type u} [Category.{v, u} C] {R X Y Z : C} {a b : R ⟶ X} {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z} (comm : CategoryStruct.comp a f₁ = CategoryStruct.comp b f₁) (big_k : IsKernelPair (CategoryStruct.comp f₁ f₂) a b) : IsKernelPair 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 CategoryTheory.IsKernelPair.cancel_right_of_mono {C : Type u} [Category.{v, u} C] {R X Y Z : C} {a b : R ⟶ X} {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z} [Mono f₂] (big_k : IsKernelPair (CategoryStruct.comp f₁ f₂) a b) : IsKernelPair 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 CategoryTheory.IsKernelPair.comp_of_mono {C : Type u} [Category.{v, u} C] {R X Y Z : C} {a b : R ⟶ X} {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z} [Mono f₂] (small_k : IsKernelPair f₁ a b) : IsKernelPair (CategoryStruct.comp 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.

def CategoryTheory.IsKernelPair.toCoequalizer {C : Type u} [Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} (k : IsKernelPair f a b) [r : RegularEpi f] : Limits.IsColimit (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

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

theorem CategoryTheory.IsKernelPair.pullback {C : Type u} [Category.{v, u} C] {X Y Z A : C} {g : Y ⟶ Z} {a₁ a₂ : A ⟶ Y} (h : IsKernelPair g a₁ a₂) (f : X ⟶ Z) [Limits.HasPullback f g] [Limits.HasPullback f (CategoryStruct.comp a₁ g)] : IsKernelPair (Limits.pullback.fst f g) (Limits.pullback.map f (CategoryStruct.comp a₁ g) f g (CategoryStruct.id X) a₁ (CategoryStruct.id Z) ⋯ ⋯) (Limits.pullback.map f (CategoryStruct.comp a₁ g) f g (CategoryStruct.id X) a₂ (CategoryStruct.id 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} [Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} (h : IsKernelPair f a b) [IsIso a] : Mono f

theorem CategoryTheory.IsKernelPair.isIso_of_mono {C : Type u} [Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} (h : IsKernelPair f a b) [Mono f] : IsIso a

theorem CategoryTheory.IsKernelPair.of_isIso_of_mono {C : Type u} [Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a : R ⟶ X} [IsIso a] [Mono f] : IsKernelPair f a a