Theorems · Definition · category theory

CategoryTheory.Limits.Trident.IsLimit.homIso

{J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            {t : CategoryTheory.Limits.Trident f} →
              CategoryTheory.Limits.IsLimit t →
                (Z : C) →
                  (Z ⟶ t.pt) ≃
                    { h //
                      ∀ (j₁ j₂ : J),
                        CategoryTheory.CategoryStruct.comp h (f j₁) = CategoryTheory.CategoryStruct.comp h (f j₂) }

Given a limit cone for the family f : J → (X ⟶ Y), for any Z, morphisms from Z to its point are in bijection with morphisms h : Z ⟶ X such that ∀ j₁ j₂, h ≫ f j₁ = h ≫ f j₂. Further, this bijection is natural in Z: see Trident.Limits.homIso_natural.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryNonempty