Documentation

Mathlib.CategoryTheory.Limits.Shapes.KernelPair

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 #

@[reducible, inline]
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) :

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} [CategoryTheory.Category.{v, u} C] {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
    • =

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

    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
    Instances For
      @[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) :
      @[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) :
      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) :

      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} [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) :

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

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

        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.

        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

          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.