Theorems · Definition · category theory

CategoryTheory.Limits.Concrete.pullbackEquiv

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type v} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {X₁ X₂ S : C} →
              (f₁ : X₁ ⟶ S) →
                (f₂ : X₂ ⟶ S) →
                  [inst_3 : CategoryTheory.Limits.HasPullback f₁ f₂] →
                    [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂)
                          (CategoryTheory.forget C)] →
                      CategoryTheory.ToType (CategoryTheory.Limits.pullback f₁ f₂) ≃
                        { p //
                          (CategoryTheory.ConcreteCategory.hom f₁) p.1 = (CategoryTheory.ConcreteCategory.hom f₂) p.2 }

In a concrete category C, given two morphisms f₁ : X₁ ⟶ S and f₂ : X₂ ⟶ S, the elements in pullback f₁ f₂ can be identified to compatible tuples of elements in X₁ and X₂.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.PreservesLimit