Theorems · Theorem · category theory

CategoryTheory.IsKernelPair.lift_snd

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

Defined in

Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Cited by

4 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category