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₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
(A B : C) :
(category_theory.limits.alternative_cone F A B).π = category_theory.discrete.nat_trans (λ (j : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on j category_theory.limits.prod.fst category_theory.limits.prod.snd)
def
category_theory.limits.alternative_cone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
(A B : C) :
(Implementation). Construct a cone for pair A B ⋙ F which we will show is limiting.
Equations
- category_theory.limits.alternative_cone F A B = {X := F.obj A ⨯ F.obj B, π := category_theory.discrete.nat_trans (λ (j : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on j category_theory.limits.prod.fst category_theory.limits.prod.snd)}
@[simp]
theorem
category_theory.limits.alternative_cone_X
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
(A B : C) :
def
category_theory.limits.alternative_cone_is_limit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
(A B : C) :
(Implementation). Show that we have a limit for the shape pair A B ⋙ F.
Equations
- category_theory.limits.alternative_cone_is_limit F A B = {lift := λ (s : category_theory.limits.cone (category_theory.limits.pair A B ⋙ F)), category_theory.limits.prod.lift (s.π.app category_theory.limits.walking_pair.left) (s.π.app category_theory.limits.walking_pair.right), fac' := _, uniq' := _}
def
category_theory.limits.preserves_binary_prod_of_prod_comparison_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
[category_theory.limits.has_binary_products C]
(A B : C)
[category_theory.is_iso (category_theory.limits.prod_comparison F A B)] :
If prod_comparison F A B is an iso, then F preserves the limit A ⨯ B.
Equations
- category_theory.limits.preserves_binary_prod_of_prod_comparison_iso F A B = category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.limit.is_limit (category_theory.limits.pair A B)) ((category_theory.limits.alternative_cone_is_limit F A B).of_iso_limit (category_theory.limits.cones.ext (category_theory.as_iso (category_theory.limits.prod_comparison F A B)).symm _))
@[instance]
def
category_theory.limits.preserves_binary_prods_of_prod_comparison_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
[category_theory.limits.has_binary_products C]
[Π (A B : C), category_theory.is_iso (category_theory.limits.prod_comparison F A B)] :
If prod_comparison F A B is an iso for all A, B , then F preserves binary products.
@[instance]
def
category_theory.limits.prod_comparison_iso_of_preserves_binary_prods
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
[category_theory.limits.has_binary_products C]
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F]
(A B : C) :
The product comparison isomorphism. Technically a special case of preserves_limit_iso, but
this version is convenient to have.
Equations
- category_theory.limits.prod_comparison_iso_of_preserves_binary_prods F A B = let t : category_theory.limits.is_limit (F.map_cone (category_theory.limits.limit.cone (category_theory.limits.pair A B))) := category_theory.limits.preserves_limit.preserves (category_theory.limits.limit.is_limit (category_theory.limits.pair A B)) in {inv := t.lift (category_theory.limits.alternative_cone F A B), hom_inv_id' := _, inv_hom_id' := _}