Theorems · Definition · category theory

CategoryTheory.IsKernelPair

{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {R X Y : C} → (X ⟶ Y) → (R ⟶ X) → (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.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Cited by

24 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category