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

@[inline, reducible]

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

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

Equations

• ⋯ = ⋯

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

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

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

Equations

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

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

• CategoryTheory.IsKernelPair.lift k p q w = CategoryTheory.Limits.PullbackCone.IsLimit.lift (CategoryTheory.IsPullback.isLimit k) p q w

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

• CategoryTheory.IsKernelPair.lift' k p q w = { val := CategoryTheory.IsKernelPair.lift k p q w, property := ⋯ }

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

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

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