Theorems · Definition · category theory

CategoryTheory.Abelian.Preradical.isLimitKernelForkObj

{C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (Φ : CategoryTheory.Abelian.Preradical C) →
        (X : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (Φ.ι.app X) ⋯)

For X : C, the kernel fork KernelFork.ofι (Φ.ι.app X) (Φ.ι_π_app X) exhibits Φ.ι.app X : Φ.r.obj X ⟶ X as the kernel of the projection Φ.π.app X : X ⟶ Φ.quotient.obj X.

Defined in: Mathlib.CategoryTheory.Abelian.Preradical.Colon
Cited by: 1 results in Mathlib
Foundations: Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Abelian

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites18

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement · cited by 32,603
CategoryTheory.Functor.objstatement · cited by 19,642
CategoryTheory.NatTrans.appstatement · cited by 7,406
CategoryTheory.Functor.idstatement · cited by 3,333
CategoryTheory.Abelianstatement and proof · cited by 1,753
CategoryTheory.Limits.WalkingParallelPairstatement · cited by 781
CategoryTheory.Limits.parallelPairstatement · cited by 766
CategoryTheory.Limits.IsLimitstatement · cited by 664
CategoryTheory.Limits.KernelFork.ofιstatement · cited by 70
CategoryTheory.Abelian.Preradicalstatement and proof · cited by 32
CategoryTheory.Abelian.Preradical.rstatement · cited by 23

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.Abelian.Preradical.isIso_toColon_hom_left_app_iffproof · cited by 1