Constructing equalizers from pullbacks and binary products.
If a category has pullbacks and binary products, then it has equalizers.
TODO: provide the dual result.
def
category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.construct_equalizer
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_pullbacks C] :
Define the equalizing object
Equations
- category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.construct_equalizer F = category_theory.limits.pullback (category_theory.limits.prod.lift (𝟙 (F.obj category_theory.limits.walking_parallel_pair.zero)) (F.map category_theory.limits.walking_parallel_pair_hom.left)) (category_theory.limits.prod.lift (𝟙 (F.obj category_theory.limits.walking_parallel_pair.zero)) (F.map category_theory.limits.walking_parallel_pair_hom.right))
def
category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.pullback_fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_pullbacks C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
Define the equalizing morphism
def
category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.equalizer_cone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_pullbacks C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
Define the equalizing cone
def
category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.equalizer_cone_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_pullbacks C]
(F : category_theory.limits.walking_parallel_pair ⥤ C) :
Show the equalizing cone is a limit
Equations
- category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.equalizer_cone_is_limit F = {lift := λ (c : category_theory.limits.cone F), category_theory.limits.pullback.lift (c.π.app category_theory.limits.walking_parallel_pair.zero) (c.π.app category_theory.limits.walking_parallel_pair.zero) _, fac' := _, uniq' := _}
def
category_theory.limits.has_equalizers_of_pullbacks_and_binary_products
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_pullbacks C] :
Any category with pullbacks and binary products, has equalizers.
Equations
- category_theory.limits.has_equalizers_of_pullbacks_and_binary_products = {has_limit := λ (F : category_theory.limits.walking_parallel_pair ⥤ C), {cone := category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.equalizer_cone F, is_limit := category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.equalizer_cone_is_limit F}}