mathlib documentation

category_theory.limits.shapes.constructions.equalizers

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] (F : category_theory.limits.walking_parallel_pair ⥤ C) :

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) :

category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.construct_equalizer F ⟶ F.obj category_theory.limits.walking_parallel_pair.zero

Define the equalizing morphism

theorem category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.pullback_fst_eq_pullback_snd {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) :

category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.pullback_fst F = category_theory.limits.pullback.snd

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) :

category_theory.limits.cone F

Define the equalizing cone

Equations

category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.equalizer_cone F = category_theory.limits.cone.of_fork (category_theory.limits.fork.of_ι (category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.pullback_fst F) _)

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) :

category_theory.limits.is_limit (category_theory.limits.has_equalizers_of_pullbacks_and_binary_products.equalizer_cone F)

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' := _}

theorem 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] :

category_theory.limits.has_equalizers C

Any category with pullbacks and binary products, has equalizers.