Theorems · Definition · category theory

CategoryTheory.Limits.IsImage.lift

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        {F : CategoryTheory.Limits.MonoFactorisation f} →
          CategoryTheory.Limits.IsImage F → (F' : CategoryTheory.Limits.MonoFactorisation f) → F.I ⟶ F'.I

Data exhibiting that a given factorisation through a mono is initial.

Defined in: Mathlib.CategoryTheory.Limits.Shapes.Images
Cited by: 15 results in Mathlib
Foundations: Depth 4 from the axioms · uses no axioms
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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 and proof · cited by 32,603
CategoryTheory.Limits.MonoFactorisation.Istatement · cited by 83
CategoryTheory.Limits.MonoFactorisationstatement and proof · cited by 69
CategoryTheory.Limits.IsImagestatement and proof · cited by 26

Cited by21

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.image.liftproof · cited by 16
CategoryTheory.Limits.IsImage.isoExtproof · cited by 8
CategoryTheory.Limits.IsImage.lift_facstatement · cited by 8
CategoryTheory.Limits.IsImage.isoExt_invstatement · cited by 5
CategoryTheory.Limits.IsImage.fac_liftstatement and proof · cited by 4
CategoryTheory.Limits.IsImage.isoExt_homstatement · cited by 4
CategoryTheory.Limits.IsImage.lift_ιstatement · cited by 4
CategoryTheory.Limits.IsImage.ofArrowIsoproof · cited by 2
CategoryTheory.Limits.IsImage.ofIsoIproof · cited by 2
CategoryTheory.Limits.IsImage.copyproof · cited by 2
CategoryTheory.Limits.image.isImage_liftstatement · cited by 1
CategoryTheory.Limits.IsImage.self_liftstatement and proof · cited by 1