# mathlibdocumentation

category_theory.limits.shapes.constructions.preserve_binary_products

Show that a functor F : C ⥤ D preserves binary products if and only if ⟨Fπ₁, Fπ₂⟩ : F (A ⨯ B) ⟶ F A ⨯ F B (that is, prod_comparison) is an isomorphism for all A, B.

@[simp]
theorem category_theory.limits.alternative_cone_π {C : Type u₁} {D : Type u₂} (F : C D) (A B : C) [category_theory.limits.has_limit (F.obj B))] :

def category_theory.limits.alternative_cone {C : Type u₁} {D : Type u₂} (F : C D) (A B : C) [category_theory.limits.has_limit (F.obj B))] :

(Implementation). Construct a cone for pair A B ⋙ F which we will show is limiting.

Equations
@[simp]
theorem category_theory.limits.alternative_cone_X {C : Type u₁} {D : Type u₂} (F : C D) (A B : C) [category_theory.limits.has_limit (F.obj B))] :
= (F.obj A F.obj B)

def category_theory.limits.alternative_cone_is_limit {C : Type u₁} {D : Type u₂} (F : C D) (A B : C) [category_theory.limits.has_limit (F.obj B))] :

(Implementation). Show that we have a limit for the shape pair A B ⋙ F.

Equations
def category_theory.limits.preserves_binary_prod_of_prod_comparison_iso {C : Type u₁} {D : Type u₂} (F : C D) (A B : C)  :

If prod_comparison F A B is an iso, then F preserves the limit A ⨯ B.

Equations
@[instance]

If prod_comparison F A B is an iso for all A, B , then F preserves binary products.

Equations
@[instance]

The product comparison isomorphism. Technically a special case of preserves_limit_iso, but this version is convenient to have.

Equations