Theorems · Theorem · category theory

CategoryTheory.Abelian.Preradical.isPullback_colon

∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C),
  CategoryTheory.IsPullback (Φ.colon Ψ).ι (Φ.colonπ Ψ) Φ.π
    (CategoryTheory.CategoryStruct.comp (Φ.quotient.whiskerLeft Ψ.ι) Φ.quotient.rightUnitor.hom)

Defined in

Mathlib.CategoryTheory.Abelian.Preradical.Colon

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian