mathlib documentation

category_theory.limits.shapes.types

Special shapes for limits in Type. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The general shape (co)limits defined in category_theory.limits.types are intended for use through the limits API, and the actual implementation should mostly be considered "sealed".

In this file, we provide definitions of the "standard" special shapes of limits in Type, giving the expected definitional implementation:

We first construct terms of is_limit and limit_cone, and then provide isomorphisms with the types generated by the has_limit API.

As an example, when setting up the monoidal category structure on Type we use the types_has_terminal and types_has_binary_products instances.

source
@[simp]
theorem category_theory.limits.types.pi_lift_π_apply {β : Type v} (f : β → Type (max v u)) {P : Type (max v u)} (s : Π (b : β), P ⟶ f b) (b : β) (x : P) :
category_theory.limits.pi.π f b (category_theory.limits.pi.lift s x) = s b x

A restatement of types.lift_π_apply that uses pi.π and pi.lift.

source
@[simp]
theorem category_theory.limits.types.pi_lift_π_apply' {β : Type v} (f : β → Type v) {P : Type v} (s : Π (b : β), P ⟶ f b) (b : β) (x : P) :
category_theory.limits.pi.π f b (category_theory.limits.pi.lift s x) = s b x

A restatement of types.lift_π_apply that uses pi.π and pi.lift, with specialized universes.

source
@[simp]
theorem category_theory.limits.types.pi_map_π_apply {β : Type v} {f g : β → Type (max v u)} (α : Π (j : β), f j ⟶ g j) (b : β) (x : ∏ λ (j : β), f j) :
category_theory.limits.pi.π g b (category_theory.limits.pi.map α x) = α b (category_theory.limits.pi.π f b x)

A restatement of types.map_π_apply that uses pi.π and pi.map.

source
@[simp]
theorem category_theory.limits.types.pi_map_π_apply' {β : Type v} {f g : β → Type v} (α : Π (j : β), f j ⟶ g j) (b : β) (x : ∏ λ (j : β), f j) :
category_theory.limits.pi.π g b (category_theory.limits.pi.map α x) = α b (category_theory.limits.pi.π f b x)

A restatement of types.map_π_apply that uses pi.π and pi.map, with specialized universes.

source
def category_theory.limits.types.terminal_limit_cone  :
category_theory.limits.limit_cone (category_theory.functor.empty (Type u))

The category of types has punit as a terminal object.

Equations
source
noncomputable def category_theory.limits.types.terminal_iso  :
⊤_ Type u ≅ punit

The terminal object in Type u is punit.

Equations
source
noncomputable def category_theory.limits.types.is_terminal_punit  :
category_theory.limits.is_terminal punit

The terminal object in Type u is punit.

Equations
source
def category_theory.limits.types.initial_colimit_cocone  :
category_theory.limits.colimit_cocone (category_theory.functor.empty (Type u))

The category of types has pempty as an initial object.

Equations
source
noncomputable def category_theory.limits.types.initial_iso  :
⊥_ Type u ≅ pempty

The initial object in Type u is pempty.

Equations
source
noncomputable def category_theory.limits.types.is_initial_punit  :
category_theory.limits.is_initial pempty

The initial object in Type u is pempty.

Equations
source
def category_theory.limits.types.binary_product_cone (X Y : Type u) :
category_theory.limits.binary_fan X Y

The product type X × Y forms a cone for the binary product of X and Y.

Equations
source
@[simp]
theorem category_theory.limits.types.binary_product_cone_X (X Y : Type u) :
(category_theory.limits.types.binary_product_cone X Y).X = (X × Y)
source
@[simp]
theorem category_theory.limits.types.binary_product_cone_fst (X Y : Type u) :
(category_theory.limits.types.binary_product_cone X Y).fst = prod.fst
source
@[simp]
theorem category_theory.limits.types.binary_product_cone_snd (X Y : Type u) :
(category_theory.limits.types.binary_product_cone X Y).snd = prod.snd
source
@[simp]
theorem category_theory.limits.types.binary_product_limit_lift (X Y : Type u) (s : category_theory.limits.binary_fan X Y) (x : s.X) :
(category_theory.limits.types.binary_product_limit X Y).lift s x = (s.fst x, s.snd x)
source
def category_theory.limits.types.binary_product_limit (X Y : Type u) :
category_theory.limits.is_limit (category_theory.limits.types.binary_product_cone X Y)

The product type X × Y is a binary product for X and Y.

Equations
source
def category_theory.limits.types.binary_product_limit_cone (X Y : Type u) :
category_theory.limits.limit_cone (category_theory.limits.pair X Y)

The category of types has X × Y, the usual cartesian product, as the binary product of X and Y.

Equations
source
@[simp]
theorem category_theory.limits.types.binary_product_limit_cone_cone (X Y : Type u) :
(category_theory.limits.types.binary_product_limit_cone X Y).cone = category_theory.limits.types.binary_product_cone X Y
source
@[simp]
theorem category_theory.limits.types.binary_product_limit_cone_is_limit (X Y : Type u) :
(category_theory.limits.types.binary_product_limit_cone X Y).is_limit = category_theory.limits.types.binary_product_limit X Y
source
noncomputable def category_theory.limits.types.binary_product_iso (X Y : Type u) :
X ⨯ Y ≅ X × Y

The categorical binary product in Type u is cartesian product.

Equations
source
@[simp]
theorem category_theory.limits.types.binary_product_iso_hom_comp_fst_apply (X Y : Type u) (x : ↥(X ⨯ Y)) :
((category_theory.limits.types.binary_product_iso X Y).hom x).fst = category_theory.limits.prod.fst x
source
@[simp]
theorem category_theory.limits.types.binary_product_iso_hom_comp_fst (X Y : Type u) :
(category_theory.limits.types.binary_product_iso X Y).hom ≫ prod.fst = category_theory.limits.prod.fst
source
@[simp]
theorem category_theory.limits.types.binary_product_iso_hom_comp_snd (X Y : Type u) :
(category_theory.limits.types.binary_product_iso X Y).hom ≫ prod.snd = category_theory.limits.prod.snd
source
@[simp]
theorem category_theory.limits.types.binary_product_iso_hom_comp_snd_apply (X Y : Type u) (x : ↥(X ⨯ Y)) :
((category_theory.limits.types.binary_product_iso X Y).hom x).snd = category_theory.limits.prod.snd x
source
@[simp]
theorem category_theory.limits.types.binary_product_iso_inv_comp_fst_apply (X Y : Type u) (x : ↥(X × Y)) :
category_theory.limits.prod.fst ((category_theory.limits.types.binary_product_iso X Y).inv x) = x.fst
source
@[simp]
theorem category_theory.limits.types.binary_product_iso_inv_comp_fst (X Y : Type u) :
(category_theory.limits.types.binary_product_iso X Y).inv ≫ category_theory.limits.prod.fst = prod.fst
source
@[simp]
theorem category_theory.limits.types.binary_product_iso_inv_comp_snd (X Y : Type u) :
(category_theory.limits.types.binary_product_iso X Y).inv ≫ category_theory.limits.prod.snd = prod.snd
source
@[simp]
theorem category_theory.limits.types.binary_product_iso_inv_comp_snd_apply (X Y : Type u) (x : ↥(X × Y)) :
category_theory.limits.prod.snd ((category_theory.limits.types.binary_product_iso X Y).inv x) = x.snd
source
def category_theory.limits.types.binary_product_functor  :
Type u ⥤ Type u ⥤ Type u

The functor which sends X, Y to the product type X × Y.

Equations
source
@[simp]
theorem category_theory.limits.types.binary_product_functor_obj_obj (X Y : Type u) :
(category_theory.limits.types.binary_product_functor.obj X).obj Y = (X × Y)
source
@[simp]
theorem category_theory.limits.types.binary_product_functor_map_app (X₁ X₂ : Type u) (f : X₁ ⟶ X₂) (Y : Type u) :
(category_theory.limits.types.binary_product_functor.map f).app Y = (category_theory.limits.types.binary_product_limit X₂ Y).lift (category_theory.limits.binary_fan.mk (prod.fst ≫ f) prod.snd)
source
@[simp]
theorem category_theory.limits.types.binary_product_functor_obj_map (X Y₁ Y₂ : Type u) (f : Y₁ ⟶ Y₂) :
(category_theory.limits.types.binary_product_functor.obj X).map f = (category_theory.limits.types.binary_product_limit X Y₂).lift (category_theory.limits.binary_fan.mk prod.fst (prod.snd ≫ f))
source
noncomputable def category_theory.limits.types.binary_product_iso_prod  :
category_theory.limits.types.binary_product_functor ≅ category_theory.limits.prod.functor

The product functor given by the instance has_binary_products (Type u) is isomorphic to the explicit binary product functor given by the product type.

Equations
source
@[simp]
theorem category_theory.limits.types.binary_coproduct_cocone_X (X Y : Type u) :
(category_theory.limits.types.binary_coproduct_cocone X Y).X = (X ⊕ Y)
source
def category_theory.limits.types.binary_coproduct_cocone (X Y : Type u) :
category_theory.limits.cocone (category_theory.limits.pair X Y)

The sum type X ⊕ Y forms a cocone for the binary coproduct of X and Y.

Equations
source
@[simp]
theorem category_theory.limits.types.binary_coproduct_cocone_ι_app (X Y : Type u) (j : category_theory.discrete category_theory.limits.walking_pair) (ᾰ : (category_theory.limits.pair X Y).obj j) :
(category_theory.limits.types.binary_coproduct_cocone X Y).ι.app j ᾰ = category_theory.discrete.rec (category_theory.limits.walking_pair.rec sum.inl sum.inr) j ᾰ
source
def category_theory.limits.types.binary_coproduct_colimit (X Y : Type u) :
category_theory.limits.is_colimit (category_theory.limits.types.binary_coproduct_cocone X Y)

The sum type X ⊕ Y is a binary coproduct for X and Y.

Equations
source
@[simp]
theorem category_theory.limits.types.binary_coproduct_colimit_desc (X Y : Type u) (s : category_theory.limits.binary_cofan X Y) (ᾰ : X ⊕ Y) :
(category_theory.limits.types.binary_coproduct_colimit X Y).desc s ᾰ = sum.elim s.inl s.inr ᾰ
source
def category_theory.limits.types.binary_coproduct_colimit_cocone (X Y : Type u) :
category_theory.limits.colimit_cocone (category_theory.limits.pair X Y)

The category of types has X ⊕ Y, as the binary coproduct of X and Y.

Equations
source
noncomputable def category_theory.limits.types.binary_coproduct_iso (X Y : Type u) :
X ⨿ Y ≅ X ⊕ Y

The categorical binary coproduct in Type u is the sum X ⊕ Y.

Equations
source
@[simp]
theorem category_theory.limits.types.binary_coproduct_iso_inl_comp_hom_apply (X Y : Type u) (x : ↥X) :
(category_theory.limits.types.binary_coproduct_iso X Y).hom (category_theory.limits.coprod.inl x) = sum.inl x
source
@[simp]
theorem category_theory.limits.types.binary_coproduct_iso_inl_comp_hom (X Y : Type u) :
category_theory.limits.coprod.inl ≫ (category_theory.limits.types.binary_coproduct_iso X Y).hom = sum.inl
source
@[simp]
theorem category_theory.limits.types.binary_coproduct_iso_inr_comp_hom_apply (X Y : Type u) (x : ↥Y) :
(category_theory.limits.types.binary_coproduct_iso X Y).hom (category_theory.limits.coprod.inr x) = sum.inr x
source
@[simp]
theorem category_theory.limits.types.binary_coproduct_iso_inr_comp_hom (X Y : Type u) :
category_theory.limits.coprod.inr ≫ (category_theory.limits.types.binary_coproduct_iso X Y).hom = sum.inr
source
@[simp]
theorem category_theory.limits.types.binary_coproduct_iso_inl_comp_inv (X Y : Type u) :
category_theory.as_hom sum.inl ≫ (category_theory.limits.types.binary_coproduct_iso X Y).inv = category_theory.limits.coprod.inl
source
@[simp]
theorem category_theory.limits.types.binary_coproduct_iso_inl_comp_inv_apply (X Y : Type u) (x : ↥X) :
(category_theory.limits.types.binary_coproduct_iso X Y).inv (category_theory.as_hom sum.inl x) = category_theory.limits.coprod.inl x
source
@[simp]
theorem category_theory.limits.types.binary_coproduct_iso_inr_comp_inv_apply (X Y : Type u) (x : ↥Y) :
(category_theory.limits.types.binary_coproduct_iso X Y).inv (category_theory.as_hom sum.inr x) = category_theory.limits.coprod.inr x
source
@[simp]
theorem category_theory.limits.types.binary_coproduct_iso_inr_comp_inv (X Y : Type u) :
category_theory.as_hom sum.inr ≫ (category_theory.limits.types.binary_coproduct_iso X Y).inv = category_theory.limits.coprod.inr
source
theorem category_theory.limits.types.binary_cofan_is_colimit_iff {X Y : Type u} (c : category_theory.limits.binary_cofan X Y) :
nonempty (category_theory.limits.is_colimit c) ↔ function.injective c.inl ∧ function.injective c.inr ∧ is_compl (set.range c.inl) (set.range c.inr)
source
noncomputable def category_theory.limits.types.is_coprod_of_mono {X Y : Type u} (f : X ⟶ Y) [category_theory.mono f] :
category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk f subtype.val)

Any monomorphism in Type is an coproduct injection.

Equations
source
def category_theory.limits.types.product_limit_cone {J : Type u} (F : J → Type (max u v)) :
category_theory.limits.limit_cone (category_theory.discrete.functor F)

The category of types has Π j, f j as the product of a type family f : J → Type.

Equations
source
noncomputable def category_theory.limits.types.product_iso {J : Type u} (F : J → Type (max u v)) :
∏ F ≅ Π (j : J), F j

The categorical product in Type u is the type theoretic product Π j, F j.

Equations
source
@[simp]
theorem category_theory.limits.types.product_iso_hom_comp_eval {J : Type u} (F : J → Type (max u v)) (j : J) :
((category_theory.limits.types.product_iso F).hom ≫ λ (f : Π (j : J), F j), f j) = category_theory.limits.pi.π F j
source
@[simp]
theorem category_theory.limits.types.product_iso_hom_comp_eval_apply {J : Type u} (F : J → Type (max u v)) (j : J) (x : ↥∏ F) :
(category_theory.limits.types.product_iso F).hom x j = category_theory.limits.pi.π F j x
source
@[simp]
theorem category_theory.limits.types.product_iso_inv_comp_π {J : Type u} (F : J → Type (max u v)) (j : J) :
(category_theory.limits.types.product_iso F).inv ≫ category_theory.limits.pi.π F j = λ (f : Π (j : J), F j), f j
source
@[simp]
theorem category_theory.limits.types.product_iso_inv_comp_π_apply {J : Type u} (F : J → Type (max u v)) (j : J) (x : ↥(Π (j : J), F j)) :
category_theory.limits.pi.π F j ((category_theory.limits.types.product_iso F).inv x) = x j
source
def category_theory.limits.types.coproduct_colimit_cocone {J : Type u} (F : J → Type u) :
category_theory.limits.colimit_cocone (category_theory.discrete.functor F)

The category of types has Σ j, f j as the coproduct of a type family f : J → Type.

Equations
source
noncomputable def category_theory.limits.types.coproduct_iso {J : Type u} (F : J → Type u) :
∐ F ≅ Σ (j : J), F j

The categorical coproduct in Type u is the type theoretic coproduct Σ j, F j.

Equations
source
@[simp]
theorem category_theory.limits.types.coproduct_iso_ι_comp_hom_apply {J : Type u} (F : J → Type u) (j : J) (x : ↥(F j)) :
(category_theory.limits.types.coproduct_iso F).hom (category_theory.limits.sigma.ι F j x) = ⟨j, x⟩
source
@[simp]
theorem category_theory.limits.types.coproduct_iso_ι_comp_hom {J : Type u} (F : J → Type u) (j : J) :
category_theory.limits.sigma.ι F j ≫ (category_theory.limits.types.coproduct_iso F).hom = λ (x : F j), ⟨j, x⟩
source
@[simp]
theorem category_theory.limits.types.coproduct_iso_mk_comp_inv_apply {J : Type u} (F : J → Type u) (j : J) (x : ↥(F j)) :
(category_theory.limits.types.coproduct_iso F).inv (category_theory.as_hom (sigma.mk j) x) = category_theory.limits.sigma.ι F j x
source
@[simp]
theorem category_theory.limits.types.coproduct_iso_mk_comp_inv {J : Type u} (F : J → Type u) (j : J) :
category_theory.as_hom (λ (x : F j), ⟨j, x⟩) ≫ (category_theory.limits.types.coproduct_iso F).inv = category_theory.limits.sigma.ι F j
source
noncomputable def category_theory.limits.types.type_equalizer_of_unique {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : f ≫ g = f ≫ h) (t : ∀ (y : Y), g y = h y → (∃! (x : X), f x = y)) :
category_theory.limits.is_limit (category_theory.limits.fork.of_ι f w)

Show the given fork in Type u is an equalizer given that any element in the "difference kernel" comes from X. The converse of unique_of_type_equalizer.

Equations
source
theorem category_theory.limits.types.unique_of_type_equalizer {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : f ≫ g = f ≫ h) (t : category_theory.limits.is_limit (category_theory.limits.fork.of_ι f w)) (y : Y) (hy : g y = h y) :
∃! (x : X), f x = y

The converse of type_equalizer_of_unique.

source
theorem category_theory.limits.types.type_equalizer_iff_unique {X Y Z : Type u} (f : X ⟶ Y) {g h : Y ⟶ Z} (w : f ≫ g = f ≫ h) :
nonempty (category_theory.limits.is_limit (category_theory.limits.fork.of_ι f w)) ↔ ∀ (y : Y), g y = h y → (∃! (x : X), f x = y)
source
def category_theory.limits.types.equalizer_limit {Y Z : Type u} {g h : Y ⟶ Z} :
category_theory.limits.limit_cone (category_theory.limits.parallel_pair g h)

Show that the subtype {x : Y // g x = h x} is an equalizer for the pair (g,h).

Equations
source
noncomputable def category_theory.limits.types.equalizer_iso {Y Z : Type u} (g h : Y ⟶ Z) :
category_theory.limits.equalizer g h ≅ {x // g x = h x}

The categorical equalizer in Type u is {x : Y // g x = h x}.

Equations
source
@[simp]
theorem category_theory.limits.types.equalizer_iso_hom_comp_subtype {Y Z : Type u} (g h : Y ⟶ Z) :
(category_theory.limits.types.equalizer_iso g h).hom ≫ subtype.val = category_theory.limits.equalizer.ι g h
source
@[simp]
theorem category_theory.limits.types.equalizer_iso_hom_comp_subtype_apply {Y Z : Type u} (g h : Y ⟶ Z) (x : ↥(category_theory.limits.equalizer g h)) :
((category_theory.limits.types.equalizer_iso g h).hom x).val = category_theory.limits.equalizer.ι g h x
source
@[simp]
theorem category_theory.limits.types.equalizer_iso_inv_comp_ι {Y Z : Type u} (g h : Y ⟶ Z) :
(category_theory.limits.types.equalizer_iso g h).inv ≫ category_theory.limits.equalizer.ι g h = subtype.val
source
@[simp]
theorem category_theory.limits.types.equalizer_iso_inv_comp_ι_apply {Y Z : Type u} (g h : Y ⟶ Z) (x : ↥{x // g x = h x}) :
category_theory.limits.equalizer.ι g h ((category_theory.limits.types.equalizer_iso g h).inv x) = x.val
source
inductive category_theory.limits.types.coequalizer_rel {X Y : Type u} (f g : X ⟶ Y) :
Y → Y → Prop

(Implementation) The relation to be quotiented to obtain the coequalizer.

source
def category_theory.limits.types.coequalizer_colimit {X Y : Type u} (f g : X ⟶ Y) :
category_theory.limits.colimit_cocone (category_theory.limits.parallel_pair f g)

Show that the quotient by the relation generated by f(x) ~ g(x) is a coequalizer for the pair (f, g).

Equations
source
theorem category_theory.limits.types.coequalizer_preimage_image_eq_of_preimage_eq {X Y Z : Type u} (f g : X ⟶ Y) (π : Y ⟶ Z) (e : f ≫ π = g ≫ π) (h : category_theory.limits.is_colimit (category_theory.limits.cofork.of_π π e)) (U : set Y) (H : f ⁻¹' U = g ⁻¹' U) :
π ⁻¹' (π '' U) = U

If π : Y ⟶ Z is an equalizer for (f, g), and U ⊆ Y such that f ⁻¹' U = g ⁻¹' U, then π ⁻¹' (π '' U) = U.

source
noncomputable def category_theory.limits.types.coequalizer_iso {X Y : Type u} (f g : X ⟶ Y) :
category_theory.limits.coequalizer f g ≅ quot (category_theory.limits.types.coequalizer_rel f g)

The categorical coequalizer in Type u is the quotient by f g ~ g x.

Equations
source
@[simp]
theorem category_theory.limits.types.coequalizer_iso_π_comp_hom_apply {X Y : Type u} (f g : X ⟶ Y) (x : ↥Y) :
(category_theory.limits.types.coequalizer_iso f g).hom (category_theory.limits.coequalizer.π f g x) = quot.mk (category_theory.limits.types.coequalizer_rel f g) x
source
@[simp]
theorem category_theory.limits.types.coequalizer_iso_π_comp_hom {X Y : Type u} (f g : X ⟶ Y) :
category_theory.limits.coequalizer.π f g ≫ (category_theory.limits.types.coequalizer_iso f g).hom = quot.mk (category_theory.limits.types.coequalizer_rel f g)
source
@[simp]
theorem category_theory.limits.types.coequalizer_iso_quot_comp_inv_apply {X Y : Type u} (f g : X ⟶ Y) (x : ↥Y) :
(category_theory.limits.types.coequalizer_iso f g).inv (category_theory.as_hom (quot.mk (category_theory.limits.types.coequalizer_rel f g)) x) = category_theory.limits.coequalizer.π f g x
source
@[simp]
theorem category_theory.limits.types.coequalizer_iso_quot_comp_inv {X Y : Type u} (f g : X ⟶ Y) :
category_theory.as_hom (quot.mk (category_theory.limits.types.coequalizer_rel f g)) ≫ (category_theory.limits.types.coequalizer_iso f g).inv = category_theory.limits.coequalizer.π f g
source
@[nolint, reducible]
def category_theory.limits.types.pullback_obj {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) :
Type u

The usual explicit pullback in the category of types, as a subtype of the product. The full limit_cone data is bundled as pullback_limit_cone f g.

source
@[reducible]
def category_theory.limits.types.pullback_cone {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) :
category_theory.limits.pullback_cone f g

The explicit pullback cone on pullback_obj f g. This is bundled with the is_limit data as pullback_limit_cone f g.

source
def category_theory.limits.types.pullback_limit_cone {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) :
category_theory.limits.limit_cone (category_theory.limits.cospan f g)

The explicit pullback in the category of types, bundled up as a limit_cone for given f and g.

Equations
source
@[simp]
theorem category_theory.limits.types.pullback_limit_cone_is_limit {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.types.pullback_limit_cone f g).is_limit = (category_theory.limits.types.pullback_cone f g).is_limit_aux (λ (s : category_theory.limits.pullback_cone f g) (x : s.X), ⟨(s.fst x, s.snd x), _⟩) _ _ _
source
@[simp]
theorem category_theory.limits.types.pullback_limit_cone_cone {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.types.pullback_limit_cone f g).cone = category_theory.limits.types.pullback_cone f g
source
noncomputable def category_theory.limits.types.pullback_cone_iso_pullback {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) :
category_theory.limits.limit.cone (category_theory.limits.cospan f g) ≅ category_theory.limits.types.pullback_cone f g

The pullback cone given by the instance has_pullbacks (Type u) is isomorphic to the explicit pullback cone given by pullback_limit_cone.

Equations
source
noncomputable def category_theory.limits.types.pullback_iso_pullback {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) :
category_theory.limits.pullback f g ≅ category_theory.limits.types.pullback_obj f g

The pullback given by the instance has_pullbacks (Type u) is isomorphic to the explicit pullback object given by pullback_limit_obj.

Equations
source
@[simp]
theorem category_theory.limits.types.pullback_iso_pullback_hom_fst {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : category_theory.limits.pullback f g) :
↑((category_theory.limits.types.pullback_iso_pullback f g).hom p).fst = category_theory.limits.pullback.fst p
source
@[simp]
theorem category_theory.limits.types.pullback_iso_pullback_hom_snd {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : category_theory.limits.pullback f g) :
↑((category_theory.limits.types.pullback_iso_pullback f g).hom p).snd = category_theory.limits.pullback.snd p
source
@[simp]
theorem category_theory.limits.types.pullback_iso_pullback_inv_fst {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.types.pullback_iso_pullback f g).inv ≫ category_theory.limits.pullback.fst = λ (p : category_theory.limits.types.pullback_obj f g), ↑p.fst
source
@[simp]
theorem category_theory.limits.types.pullback_iso_pullback_inv_snd {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.types.pullback_iso_pullback f g).inv ≫ category_theory.limits.pullback.snd = λ (p : category_theory.limits.types.pullback_obj f g), ↑p.snd